Z3 Java:简化分配表达式

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包含简化表达式