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

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

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

Answer 2

命令

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

要求为目标 g 启用 unsat 核心提取（第二个 true），但 propagate-ineqs 策略不支持该功能，因此它抛出异常.

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

Z3 Managed Exception : Java API while trying to use propagate-ineqs tactic

java

exception

smt

z3