Question

I'm using z3 via c++ interface. z3::expr could be a basic variable/constant(c.real_const, c.real_val) or an expression. I often encountered an error caused of the using of z3::expr. The problem can be described by the following code:

z3::context c; 
z3::expr exp(c);
for(...){
   exp=...;
}
 cout<<exp;

If the loop is not executed at all, I will get an error. I know the reason is that exp is not assigned. How can I check whether an z3::expr variable is assigned or not?

Was it helpful?

Solution

The expr class derive from ast which has a bool() operator that can be used for this purpose. This means we can simply write

if (exp)
  cout << exp;

(Internally expressions and ASTs are simply pointers, and they should be valid whenever the pointer is non-zero, so the bool() operator simply checks for nonzero pointers: return m_ast != 0;).

Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow
scroll top