如何检查是否已分配z3::expr

How to check whether z3::expr is assigned

本文关键字：分配 z3 是否 expr 何检查 检查      更新时间：2023-10-16

我通过c++接口使用z3。z3:：expr可以是一个基本变量/常数（c.real_const，c.real_val）或一个表达式。我经常遇到由于使用z3:：expr而导致的错误。问题可以用以下代码描述：

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

如果根本不执行循环，我将得到一个错误。我知道原因是exp没有分配。如何检查是否分配了z3:：expr变量？

expr类派生自ast，后者具有可用于此目的的布尔（）运算符。这意味着我们可以简单地编写

if (exp)
  cout << exp;

（内部表达式和AST只是指针，只要指针为非零，它们就应该有效，所以bool（）运算符只检查非零指针：return m_ast != 0;）。

相关文章：