由网友(温柔女Boss.)分享简介:我使用的是Java API。这是此警告的最小工作示例:HashMap cfg = new HashMap();cfg.put("model", "true");Context ctx = new Context(cfg);Solver solver...
我使用的是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();
相关推荐
最新文章