Z3_parse_smtlib_string使用问题 [英] Z3_parse_smtlib_string usage issues

问题描述

在下面的代码中，我提出了一个明显不能令人满意的Z3声明，然后尝试使用C ++ / C Z3 API来以编程方式解决。

In the following code, I put a clearly unsatisfiable Z3 declaration and then try to use the C++/C Z3 APIs to see it programmatically solved.

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

The problem is that this code always triggers the check that outputs: "SAT?!". i.e. the clearly unsatisfiable expression is determined to be satisfiable in the current usage of the API calls.

如何使这种操作按预期工作？

How can I get this kind of operation to work as expected?

#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 is correct in this case, because no constraints have been added to the solver, thus this is trivially satisfiable. The crucial part is this:

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

这篇关于Z3_parse_smtlib_string使用问题的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！