Z3_parse_smtlib_string使用问题

Z3_parse_smtlib_string usage issues

本文关键字：问题 smtlib parse Z3 string      更新时间：2023-10-16

在下面的代码中，我放置了一个明显不令人满意的Z3声明，然后尝试使用c++/C Z3 api来查看它的编程解决。

问题是这段代码总是触发输出:"SAT?!"的检查。即，在API调用的当前使用中，确定明显不能满足的表达式是可以满足的。

我怎样才能使这种操作按预期工作?

#include "z3++.h"
int main(){
  z3::context c;
  std::string testing = "(declare-const p0 Bool)(assert(= p0 true))(assert(= p0 false))(check-sat)";
  Z3_ast parsed = Z3_parse_smtlib2_string(c,testing.c_str(),0,0,0,0,0,0);
  z3::expr e(c, parsed);
  z3::solver s(c);
  if(s.check() == z3::sat)
    std::cout << "SAT?!n";
  return 0;
}

Z3在这种情况下是正确的，因为没有向求解器添加任何约束，因此这是平凡的可满足的。关键的部分是:

Z3_ast parsed = Z3_parse_...
z3::expr e(c, parsed);
z3::solver s(c);
s.add(e); // <--- Add constraints to solver here
if(s.check() ...
相关文章：