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 被视为解释词汇的一部分，因此“true”（或 x 上的任何其他公式！）是插值.

2) 改用 ComputeInterpolant 方法。使用 GetInterpolant 的唯一原因是逐步使用求解器。

说了这么多，我试了（1），发现GetInterpolant调用坏了。现已修复在 github 的不稳定分支上。