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

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 的实例，它们封装了您的意思的语句（而不是它们的插值或引用）。