質問

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?

役に立ちましたか?

解決

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;).

ライセンス: CC-BY-SA帰属
所属していません StackOverflow
scroll top