Z3 抱怨假设不是命题变量，即使它实际上是

Question

我正在使用 Java API。这是此警告的最小工作示例：

HashMap<String, String> cfg = new HashMap<String, String>();
cfg.put("model", "true");
Context ctx = new Context(cfg);
Solver solver = ctx.mkSolver();
BoolExpr a = ctx.mkBoolConst("a");
BoolExpr b = ctx.mkBoolConst("b");
BoolExpr and = ctx.mkAnd(a,b); 
solver.check(and);

对于这个小程序，Z3投诉说：

WARNING: an assumption must be a propositional variable or the negation of one

除非我理解错了什么，and是一个命题变量，所以我不明白为什么会有这个警告。而且check方法的参数是BoolExpr的数组，为什么要命题变量呢？

我的问题：我可以安全地忽略这个警告吗？

Answer 1

不，and 不是命题变量，而是命题项（或者换句话说是 BoolExpr）。 solver.check(...) 的假设文字需要是变量或变量的否定，即 a 或 not a，但不是 a and b。

忽略此警告是不安全的，因为这意味着 Z3 将忽略这些假设，即您可能会得到意想不到的结果。

只是为了避免混淆：solver.check(...) 的参数是 assumption 文字，它们不是 assertions，即，如果我们想检查 and 是否可满足我们需要先断言它，然后要求求解器在没有进一步假设的情况下进行检查，例如，

...
solver.assert(and);
solver.check();

Z3 抱怨假设不是命题变量，即使它实际上是

Z3 complains that assumption is not a propositional variable, even when it actually is

z3