Search code examples
c++z3smt

Z3 and let statement in C/C++

SMT-LIB support a let statement:

 (let ((x1 t1) · · · (xn tn)) t)

Which statements must be used if the C/C++ library of Z3 is being used?

Solution

  • There's no corresponding statement in C/C++, because it is not needed.

    Note that SMTLib's let statement allows you to give a name to a subexpression so you can use it multiple times. If you want to do the same thing in C/C++, you'd simply use a C/C++ variable (of the right type) that contains that expression, and use it later on in building bigger expressions. So, in this sense, the let expression of SMTLib corresponds to the regular variables and expressions in C/C++.

    PS. I suspect, however, you might actually have a different question about writing z3 programs in C/C++, and perhaps the way you formulated it is an instance of the so called XY problem. If you ask about exactly what you're trying to achieve, you'll no doubt receive a better answer.