I store numbers as z3::expr and want to compare them. I tried the following:
z3::context c;
z3::expr a = c.real_val("0");
z3::expr b = c.real_val("1");
z3::expr comp = (a < b);
std::cout << comp.is_bool() << std::endl;
std::cout << comp.bool_value() << std::endl;
I am a bit confused, why is comp.bool_value() false?
If I use a solver everything works as expected:
z3::solver s(c);
s.add(comp);
std::cout << s.check() << std::endl;
I have to compare z3::exprs relatively often, what would be the fasted method to do so? Using a solver seems to me like a lot of overhead.
The < operator (and pretty much all other operators) simply pushes the decision to the solver: That is, it is a symbolic-expression that does not "evaluate" while it runs, but rather creates the expression that will do the comparison when the solver is invoked, over arbitrary expressions.
Having said that, you can use the simplifier to achieve what you want in certain cases. If you try:
z3::expr simpComp = comp.simplify();
std::cout << simpComp.bool_value() << std::endl;
you'll see that it'll print 1 for you. However, you shouldn't count on the simplifier to be able to reduce arbitrary expressions like this. For the simplest cases it'll do the job, but it'll give up if you have more complicated expressions.
In general, once you construct an expression you have to wait till the solver is called, and inspect the resulting model, if there is any.
Side note You can build your own functions to do some constant-folding yourself, in certain cases. This will be possible for Bool values, for instance (since they can be represented fully in C++), and bit-vectors of various sizes (upto your machine word-size), floats etc. But not for reals (because z3 reals are infinite precision, and you cannot represent those in C++ directly), and integers (because they're unbounded.) But this is not a trivial thing to do, and unless you're intimately familiar with the internals of z3, I'd recommend not going down that route.
Bottom line: If you have a lot of these sorts of constants folding around: See if you can re-architect your program so you don't create real_val in the first place; and keep them as constants, and only convert them to z3-expressions when you no longer can keep them as such. You can rely on simplify in certain cases, though don't expect it to be very performant either.