java - Z3 Java : simplify a distributive expression

Question

我需要使用 z3 定理证明器简化 Java 中的分配表达式:

(simplify (or (and (<= b 0) (<= a 0)) (and (not (<= b 0)) (<= a 0))))

通常 z3 证明者应返回以下表达式:

(<= a 0)

但是我得到的又是相同的表达式:

(or (and (<= b 0) (<= a 0)) (and (not (<= b 0)) (<= a 0)))

这是java代码:

Context ctx = new Context(configuration);

ArithExpr a = (ArithExpr) ctx.mkConst(ctx.mkSymbol("a"), ctx.getIntSort());
ArithExpr b = (ArithExpr) ctx.mkConst(ctx.mkSymbol("b"), ctx.getIntSort());
IntNum zero = this.context.mkInt(0);

Expr expr = ctx.mkOr(
    ctx.mkAnd(ctx.mkLe(a, zero), ctx.mkLe(b, zero)),
    ctx.mkAnd(ctx.mkLe(a, zero), ctx.mkGt(b, zero)));

expr = expr.simplify();

我错过了什么吗？我能做什么？ 感谢您的帮助。

Answer 1

我找到了解决问题的方法。我所做的就是使用 ctx-solver-simplify 策略应用我的表达式。这将显示一组结果目标。在 Java 中，它看起来像这样:

Goal g = this.context.mkGoal(true, false, false);
g.add((BoolExpr) expr);

ApplyResult ar = this.context.mkTactic("ctx-solver-simplify").apply(g);
Goal[] subgoals = ar.getSubgoals();
BoolExpr[] formulas_0 = subgoals[0].getFormulas();

数组formulas_0包含简化的表达式。