c++ - 用微不足道的方法得到未知的结果

Question

我正在使用 z3 C++ API。如果我创建这个简单的错误表达式：

z3::expr x = C->int_const("x");
z3::expr p = z3::forall(x, x==0);

并尝试解决，我得到一个未知的结果。我不是战略和战术方面的专家，但如果我使用正确的战术，我相信 z3 可以解决这个问题。

我也试过

z3::expr p = !z3::forall(x, x==0);

当然，同样的结果也是众所周知的。

Answer 1

我不熟悉 z3，但从一般 C++ 的角度来看，不会x==0先评估，即你的调用不等于implies(x, 1)? 从快速搜索看来，您可能必须将语句的每个部分构造为 z3 对象，例如：

Z3_ast consequent = Z3_mk_eq(ctx, x, 0);
Z3_ast theorem = Z3_mk_implies(ctx, x, consequent);

但上面的说法也不对。我相信参数x和0它们本身必须是Z3_ast封装您所指的语句的实例（而不是它们的插值或引用）。