iZ3 - Interpolant violates interpolation constraints

[MarcusVoelker]

I had z3 compute an interpolant via the Java API (using a hacked ComputeInterpolant function to bypass the unusable function in the current API, see below).

This is the Java code I use

private void test()
{
    HashMap<String, String> options = new HashMap<>();
    options.put("proof", "true");
    options.put("model", "true");
    InterpolationContext ctx = new InterpolationContext(options);

    IntExpr pc0 = ctx.mkIntConst("#PC");
    IntExpr pc1 = ctx.mkIntConst("#PC'");
    IntExpr pc2 = ctx.mkIntConst("#PC''");
    IntExpr ctr0 = ctx.mkIntConst("Counter");
    IntExpr ctr1 = ctx.mkIntConst("Counter'");
    IntExpr ctr2 = ctx.mkIntConst("Counter''");

    IntExpr const0 = ctx.mkInt(0);
    IntExpr const1 = ctx.mkInt(1);
    IntExpr const2 = ctx.mkInt(2);
    IntExpr const4 = ctx.mkInt(4);
    IntExpr const5 = ctx.mkInt(5);

    BoolExpr p00 = ctx.mkBoolConst("#P0");
    BoolExpr p02 = ctx.mkBoolConst("#P0''");
    BoolExpr init0 = ctx.mkBoolConst("#Init");
    BoolExpr init2 = ctx.mkBoolConst("#Init''");
    BoolExpr ip20 = ctx.mkBoolConst("#IP_2");
    BoolExpr ip22 = ctx.mkBoolConst("#IP_2''");
    BoolExpr ip30 = ctx.mkBoolConst("#IP_3");
    BoolExpr ip32 = ctx.mkBoolConst("#IP_3''");
    BoolExpr ip40 = ctx.mkBoolConst("#IP_4");
    BoolExpr ip42 = ctx.mkBoolConst("#IP_4''");
    BoolExpr ip50 = ctx.mkBoolConst("#IP_5");
    BoolExpr ip52 = ctx.mkBoolConst("#IP_5''");
    BoolExpr ip60 = ctx.mkBoolConst("#IP_6");
    BoolExpr ip62 = ctx.mkBoolConst("#IP_6''");
    BoolExpr ip70 = ctx.mkBoolConst("#IP_7");
    BoolExpr ip72 = ctx.mkBoolConst("#IP_7''");

    BoolExpr t00 = ctx.mkImplies(ctx.mkEq(pc0, const0), ctx.mkAnd(
            ctx.mkEq(ctr1, ctx.mkAdd(ctr0, const1)),
            ctx.mkEq(pc1, ctx.mkAdd(pc0, const1)),
            ctx.mkAnd()
            ));
    BoolExpr t10 = ctx.mkImplies(ctx.mkEq(pc0, const1), ctx.mkAnd(
            ctx.mkEq(ctr1, ctx.mkMod(ctr0, const5)),
            ctx.mkEq(pc1, ctx.mkAdd(pc0, const1)),
            ctx.mkAnd()
            ));
    BoolExpr t20 = ctx.mkImplies(ctx.mkEq(pc0, const2), ctx.mkAnd(
            ctx.mkEq(pc1, const0),
            ctx.mkEq(ctr1, ctr0)
            ));
    BoolExpr t01 = ctx.mkImplies(ctx.mkEq(pc1, const0), ctx.mkAnd(
            ctx.mkEq(ctr2, ctx.mkAdd(ctr1, const1)),
            ctx.mkEq(pc2, ctx.mkAdd(pc1, const1)),
            ctx.mkAnd()
            ));
    BoolExpr t11 = ctx.mkImplies(ctx.mkEq(pc1, const1), ctx.mkAnd(
            ctx.mkEq(ctr2, ctx.mkMod(ctr1, const5)),
            ctx.mkEq(pc2, ctx.mkAdd(pc1, const1)),
            ctx.mkAnd()
            ));
    BoolExpr t21 = ctx.mkImplies(ctx.mkEq(pc1, const2), ctx.mkAnd(
            ctx.mkEq(pc2, const0),
            ctx.mkEq(ctr2, ctr1)
            ));

    BoolExpr a = ctx.mkAnd(
            ctx.mkNot(ip30),
            init0,
            ctx.mkNot(ip40),
            ctx.mkNot(ip20),
            ctx.mkNot(ip70),
            ip50,
            p00,
            ip60,
            ctx.mkEq(ip20, ctx.mkEq(const1, pc0)),
            ctx.mkEq(ip30, ctx.mkEq(const2, pc0)),
            ctx.mkEq(ip40, ctx.mkGe(pc0, const1)),
            ctx.mkEq(ip50, ctx.mkEq(const0, pc0)),
            ctx.mkEq(ip60, ctx.mkGe(pc0, const0)),
            ctx.mkEq(ip70, ctx.mkGe(ctr0, const4)),
            ctx.mkEq(init0, ctx.mkAnd(ctx.mkEq(ctr0, const0), ctx.mkEq(pc0, const0))),
            ctx.mkEq(p00, ctx.mkLt(ctr0, const5)),
            t00,
            t10,
            t20
            );

    BoolExpr b = ctx.mkAnd(
            t01,
            t11,
            t21,
            ctx.mkEq(ip22, ctx.mkEq(const1, pc2)),
            ctx.mkEq(ip32, ctx.mkEq(const2, pc2)),
            ctx.mkEq(ip42, ctx.mkGe(pc2, const1)),
            ctx.mkEq(ip52, ctx.mkEq(const0, pc2)),
            ctx.mkEq(ip62, ctx.mkGe(pc2, const0)),
            ctx.mkEq(ip72, ctx.mkGe(ctr2, const4)),
            ctx.mkEq(init2, ctx.mkAnd(ctx.mkEq(ctr2, const0), ctx.mkEq(pc2, const0))),
            ctx.mkEq(p02, ctx.mkLt(ctr2, const5)),
            ip32,
            ctx.mkNot(init2),
            ip42,
            ctx.mkNot(ip22),
            ip72,
            ctx.mkNot(ip52),
            p02,
            ip62
            );

    BoolExpr pat = ctx.mkAnd(ctx.MkInterpolant(a), b);
    System.out.println("Pattern:");
    System.out.println(pat);
    Expr[] exps = ctx.ComputeInterpolant(pat);

    System.out.println("Interpolant:");
    for (Expr e : exps)
    {
        System.out.println(e);
    }

    Solver solver = ctx.mkSolver();
    BoolExpr i = (BoolExpr) exps[0];
    for (int idx = 1; idx < exps.length; ++idx) {
        i = ctx.mkAnd(i, (BoolExpr) exps[idx]);
    }
    solver.add(ctx.mkNot(ctx.mkImplies(b, ctx.mkNot(i))));
    System.out.println(solver.check() == Status.UNSATISFIABLE ? "B -> not(I) is a tautology" : "B -> not(I) is not a tautology");
}

with the following ComputeInterpolant function added to InterpolationContext.java:

public Expr[] ComputeInterpolant(Expr pat)
{
    checkContextMatch(pat);

    Params p = mkParams();

    Native.LongPtr n_i = new Native.LongPtr();
    Native.LongPtr n_m = new Native.LongPtr();
    int r = Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m);
    ASTVector seq = new ASTVector(this, n_i.value);
    int n = seq.size();
    Expr[] res = new Expr[n];
    for (int i = 0; i < n; i++)
        res[i] = Expr.create(this, seq.get(i).getNativeObject());
    return res;
}

When I run this function, the interpolant given is (= |#PC'| 1), but as the output at the end of the function proves, B -> not(I) is not a tautology, hence the interpolant is wrong.

[wintersteiger]

ComputeInterpolant has been fixed to return a return value class that contains all the required out parameters of the corresponding C function (see #82).

[kenmcmil]

Following is a patch for this issue, pushed to unstable:

diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp
index 5a7f719..78dd6f1 100755
--- a/src/interp/iz3mgr.cpp
+++ b/src/interp/iz3mgr.cpp
@@ -556,6 +556,20 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<rational>& rats){
     extract_lcd(rats);
 }

+void iz3mgr::get_broken_gcd_test_coeffs(const ast &proof, std::vector<rational>& rats){
+    symb s = sym(proof);
+    int numps = s->get_num_parameters();
+    rats.resize(numps-2);
+    for(int i = 2; i < numps; i++){
+        rational r;
+        bool ok = s->get_parameter(i).is_rational(r);
+        if(!ok)
+            throw "Bad Farkas coefficient";
+        rats[i-2] = r;
+    }
+    extract_lcd(rats);
+}
+
 void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector<ast>& coeffs){
     std::vector<rational> rats;
     get_assign_bounds_coeffs(proof,rats);
diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h
index 54fb35a..8d4479f 100755
--- a/src/interp/iz3mgr.h
+++ b/src/interp/iz3mgr.h
@@ -424,6 +424,8 @@ class iz3mgr  {

     void get_farkas_coeffs(const ast &proof, std::vector<rational>& rats);

+    void get_broken_gcd_test_coeffs(const ast &proof, std::vector<rational>& rats);
+
     void get_assign_bounds_coeffs(const ast &proof, std::vector<rational>& rats);

     void get_assign_bounds_coeffs(const ast &proof, std::vector<ast>& rats);
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index 36cf802..360748b 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -1021,6 +1021,12 @@ public:
                 my_coeffs.push_back(make_int(c));
                 my_prem_cons.push_back(conc(prem(proof,i)));
             }
+            else if(c.is_neg()){
+                int j = (i % 2 == 0) ? i + 1 : i - 1;
+                my_prems.push_back(prems[j]);
+                my_coeffs.push_back(make_int(-coeffs[j]));
+                my_prem_cons.push_back(conc(prem(proof,j)));
+            }
         }
         ast my_con = sum_inequalities(my_coeffs,my_prem_cons);

@@ -1882,7 +1891,7 @@ public:
                     }
                     case GCDTestKind: {
                         std::vector<rational> farkas_coeffs;
-                        get_farkas_coeffs(proof,farkas_coeffs);
+                        get_broken_gcd_test_coeffs(proof,farkas_coeffs);
                         if(farkas_coeffs.size() != nprems){
                             pfgoto(proof);
                             throw unsupported();

[kenmcmil]

Christophe, your new version of ComputeInterpolant does not seem to be in unstable.

[wintersteiger]

Ken: Yes it is, see here. Note that this was a fix exclusively for the Java API, because Java doesn't support output parameters.

[kenmcmil]

I think this issue is fixed. Closing.