Как проверить, назначен ли z3::expr

Question

Я использую z3 через интерфейс C++. z3::expr может быть базовой переменной / константой (c.real_const, c.real_val) или выражением. Я часто сталкивался с ошибкой, вызванной использованием z3::expr. Проблема может быть описана с помощью следующего кода:

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

Если цикл не выполняется вообще, я получу ошибку. Я знаю, что причина в том, что опыт не назначен. Как я могу проверить, назначена ли переменная z3:: expr или нет?

Answer 1

expr класс происходит от ast который имеет оператор bool(), который можно использовать для этой цели. Это означает, что мы можем просто написать

if (exp)
  cout << exp;

(Внутренние выражения и AST - это просто указатели, и они должны быть действительными, когда указатель ненулевой, поэтому оператор bool() просто проверяет ненулевые указатели: return m_ast != 0;).