在下面的代码中,我放置了一个显然无法令人满意的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() ...