java - Z3 的 Java 插值 API 似乎返回错误的插值

Question

我正在尝试创建一些使用 Z3 的 Java 插值 API 的简单示例。我的目的是复制以下 SMT-LIB:

(declare-const x Int)
(compute-interpolant (> x 5) (< x 5))

当我在标准输入上将上述 SMT-LIB 提供给 Z3 时，它返回:

unsat
(not (<= x 5))

这是一个有效的插值。

但是，当我尝试通过 Java API 解决同样的问题时:

    System.out.print("Z3 Major Version: ");
    System.out.println(Version.getMajor());
    System.out.print("Z3 Full Version: ");
    System.out.println(Version.getString());
    HashMap<String, String> cfg = new HashMap<String, String>();
    cfg.put("proof", "true");
    cfg.put("model", "true");
    InterpolationContext ictx = new InterpolationContext(cfg);
    Solver s = ictx.mkSolver();
    // A = x > 5
    // B = x < 5
    //Whats Interp(A,B)?
    IntExpr x = ictx.mkIntConst("x");
    IntExpr five = ictx.mkInt(5);
    BoolExpr A = ictx.mkGt(x, five);
    BoolExpr B = ictx.mkLt(x, five);
    BoolExpr iA = ictx.MkInterpolant(A);
    BoolExpr AB = ictx.mkAnd(A, B);
    BoolExpr pat = ictx.mkAnd(iA, B);
    System.out.println("A: " + A);
    System.out.println("B: " + B);
    System.out.println("Pattern: " +  pat);
    Params params = ictx.mkParams();
    s.add(AB);
    //s.add(B);
    s.check();
    Expr proof = s.getProof();         
    Expr[] interps = ictx.GetInterpolant(proof, pat, params);
    for(int i = 0; i < interps.length; i++){
        System.out.println("Interpolant: " + interps[i]);
    }

我得到:

Z3 Major Version: 4
Z3 Full Version: 4.4.0.0
A: (> x 5)
B: (< x 5)
Pattern: (and (interp (> x 5)) (< x 5))
Interpolant: true

我做错了什么吗？

Answer 1

两个可能的修复:

1) 分别断言 A 和 B，如下所示:

s.add(A)
s.add(B)

未逐字出现在模式中的断言公式被视为“背景理论”。在您的示例中，这意味着 (and (< x 5) (> x 5)) 被视为同义反复，而 x 作为解释词汇的一部分，因此“true”(或 x 上的任何其他公式!)是一个插值.

2) 使用ComputeInterpolant 方法代替。使用 GetInterpolant 的唯一原因是增量使用求解器。

话虽如此，我尝试了(1)，发现 GetInterpolant 调用已损坏。现在已修复在 github 的不稳定分支上。