Z3抱怨说，假设不是命题变量，即使它实际上是命题变量 [英] Z3 complains that assumption is not a propositional variable, even when it actually is

问题描述

我使用的是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投诉：

警告：假设必须是命题变量或 否定一

除非我误解了什么，and是一个命题变量，所以我不明白为什么会有这个警告。此外，check方法接受BoolExpr数组作为参数，为什么它需要命题变量？

我的问题：我是否可以安全地忽略此警告？

推荐答案

不，and不是命题变量，但它是一个命题术语(或换句话说，BoolExpr)。solver.check(...)的假设文字需要是变量或变量的反，即a或not a，但不是a and b。

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

为了避免混淆：solver.check(...)的参数是假设，而不是断言，也就是说，如果我们想检查and是否可满足，我们需要首先断言它，然后要求求解器检查而不做进一步的假设，例如

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

这篇关于Z3抱怨说，假设不是命题变量，即使它实际上是命题变量的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！