Z3 托管异常：Java API 尝试使用传播-ineqs 策略

Question

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)

(assert (exists ((a0 Int) (b0 Int) (c0 Int))
 (and (<= a 3)
      (>= a 0)
      (<= b 3)
      (>= b 0)
      (<= c 3)
      (>= c 0)
      (= 3 (+ a b c))
      (> a 1)
      (= a0 a)
      (= b0 b)
      (= c0 c)
      (= a0 2)
      (= b0 0)
      (= c0 1))))
(apply  (then qe ctx-solver-simplify propagate-ineqs))

我正在尝试使用为 Z3 Solver 提供的 Java-API 生成此代码。但是，这最终会引发以下异常：

Z3 托管异常：propagate-ineqs 不支持 unsat 核心生产

 Goal g = ctx.mkGoal(true, true, false);
 g.add((BoolExpr) exp);
 Tactic qe = ctx.mkTactic("qe");
 Tactic simpify = ctx.mkTactic("simplify");
 Tactic ctxSimpify = ctx.mkTactic("ctx-simplify");
 Tactic ctxSolverSimplify = ctx.mkTactic("ctx-solver-simplify");
 Tactic propagateIneqs = ctx.mkTactic("propagate-ineqs");
 Tactic then = ctx.then(qe, simpify, ctxSimpify, ctxSolverSimplify,
            propagateIneqs);
 ApplyResult ar = then.apply(g);
 BoolExpr result = ctx.mkAnd(ar.getSubgoals()[0].getFormulas());

请让我知道我哪里出错了，以及如何在 Java-API 中使用 propagate-ineqs 策略。这样，我可以得到简化的不等式的答案。

Answer 1

命令

 Goal g = ctx.mkGoal(true, true, false);

要求为目标g 启用未饱和核心提取（第二个true），但propagate-ineqs 策略不支持该功能，因此会引发异常。

Answer 2

您可以尝试在构建 Context ctx 期间明确关闭 unsat 核心功能。您可以传递带有选项及其值的 Map。 unsat cores 的选项是“unsat_core”，可以设置为“true”或“false”。