自4.8.11以来的断言软问题

Question

我从这个优化程序中得到了一个意外的结果。

我希望优化器抛出断言"；一个"；并保持"；两个"；通过将a设置为5或更小。4.11.2在命令行上设置a=5和b=5。但当我在4.11.2下运行Java程序时，它设置a=6和b=6，并抛出断言"；二">

我做错了什么？

第页。S.我相信它在4.8.11上运行良好，在那里它设置了a=b=0。

(set-option :produce-unsat-cores true)
(set-option :produce-models true)
(set-option :produce-assertions true)
(declare-const a Int)
(declare-const b Int)
(assert-soft (! (> a 10) :named one) :weight 10)
(assert-soft (! (< a 6) :named two) :weight 5)
; force "one" false
(assert (! (< b 8) :named three))
(assert (! (= a b) :named four))
(check-sat)
(get-model)

public class Main {
public static void main(String[] args) {
var example = new Main.Example();
example.run();
}
public static class Example {
Map<String, String> options = Map.of(
"auto_config", "false",
"proof", "false",
"model", "true",
"unsat_core", "true"
);
Context z3 = new Context(options);
public void run() {
var a = z3.mkIntConst("a");
var b = z3.mkIntConst("b");
var opt = z3.mkOptimize();
var trackers = new LinkedList<BoolExpr>();
trackers.add(assertSoft(opt, z3.mkGt(a, z3.mkInt(10)), "one", 10, "default"));
trackers.add(assertSoft(opt, z3.mkLt(a, z3.mkInt(6)), "two", 5, "default"));
trackers.add(assertHard(opt, z3.mkLt(b, z3.mkInt(8)), "three"));
trackers.add(assertHard(opt, z3.mkEq(a, b), "four"));
var status = opt.Check();
System.out.println("Z3 ver: " + Version.getFullVersion());
System.out.println("Status: " + status);
var model = opt.getModel();
System.out.println("a = " + model.getConstInterp(a));
System.out.println("b = " + model.getConstInterp(b));
System.out.println("assertion one   = " + getBool(model, trackers.get(0)));
System.out.println("assertion two   = " + getBool(model, trackers.get(1)));
System.out.println("assertion three = " + getBool(model, trackers.get(2)));
System.out.println("assertion four  = " + getBool(model, trackers.get(3)));
}
private String getBool(Model model, BoolExpr expr) {
var eval = model.eval(expr, true);
return eval.toString();
}
private BoolExpr assertHard(Optimize optimizer, BoolExpr assertion, String name) {
var tracker = createTracker(name);
optimizer.AssertAndTrack(assertion, tracker);
return tracker;
}
private BoolExpr assertSoft(Optimize optimizer, BoolExpr assertion, String name, int weight, String id) {
var tracker = createTracker(name);
var trackerExpr = z3.mkEq(assertion, tracker);
optimizer.AssertSoft(assertion, weight, id);
optimizer.Assert(trackerExpr);
return tracker;
}
protected BoolExpr createTracker(String name) {
return z3.mkBoolConst(name);
}
}
}

这是Java代码的输出

Z3 ver: Z3 4.11.2.0
Status: SATISFIABLE
a = 6
b = 6
assertion one   = false
assertion two   = false
assertion three = true
assertion four  = true

以下是CLI输出的

sat
(
(define-fun one () Bool
(> a 10))
(define-fun a () Int
5)
(define-fun two () Bool
(< a 6))
(define-fun four () Bool
(= a b))
(define-fun three () Bool
(< b 8))
(define-fun b () Int
5)
)

Answer 1

我相信你已经回答了自己的问题。CLI是隐式增量的。要在Java中获得相同的效果，必须明确地将其设置为增量。

如果这是行为的变化，您可以在中报告https://github.com/Z3Prover/z3/issues