Z3 with Craig interpolation (iz3)

Question

I'm trying to generate Craig interpolants using the C API but I get incorrect results. However, when I dump the same problem to a file via Z3_write_interpolation_problem and call iZ3 I get the expected interpolant.

I attach the code to be able to reproduce the same results. I'm using z3 4.1

---

#include<stdio.h>
#include<stdlib.h
#include<assert.h>
#include<stdarg.h>
#include<memory.h>
#include<setjmp.h>
#include<iz3.h>

Z3_ast mk_var(Z3_context ctx, const char * name, Z3_sort ty) 
{
   Z3_symbol   s  = Z3_mk_string_symbol(ctx, name);
   return Z3_mk_const(ctx, s, ty);
}

Z3_ast mk_int_var(Z3_context ctx, const char * name) 
{
   Z3_sort ty = Z3_mk_int_sort(ctx);
   return mk_var(ctx, name, ty); 
}

void interpolation_1(){
// Create context
Z3_config  cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_interpolation_context(cfg);        

// Build formulae
Z3_ast x0,x1,x2;
x0 = mk_int_var(ctx, "x0");
x1 = mk_int_var(ctx, "x1");
x2 = mk_int_var(ctx, "x2");
Z3_ast zero = Z3_mk_numeral(ctx, "0", Z3_mk_int_sort(ctx));
Z3_ast two  = Z3_mk_numeral(ctx, "2", Z3_mk_int_sort(ctx));
Z3_ast ten  = Z3_mk_numeral(ctx, "10", Z3_mk_int_sort(ctx));

Z3_ast c2_operands[2] = { x0, two };
Z3_ast c1 = Z3_mk_eq(ctx, x0, zero);
Z3_ast c2 = Z3_mk_eq(ctx, x1, Z3_mk_add(ctx, 2, c2_operands));
Z3_ast c3_operands[2] = { x1, two };
Z3_ast c3 = Z3_mk_eq(ctx, x2, Z3_mk_add(ctx, 2, c3_operands));
Z3_ast c4 = Z3_mk_gt(ctx, x2, ten);

Z3_ast A_operands[3] = { c1, c2, c3};
Z3_ast AB[2] = { Z3_mk_and(ctx,3, A_operands), c4 };

// Generate interpolant
Z3_push(ctx);
Z3_ast interps[1];
Z3_lbool status = Z3_interpolate(ctx, 2, AB, NULL, NULL, interps); 
assert(status ==  Z3_L_FALSE && "A and B should be unsat");
printf("Interpolant: %s\n",Z3_ast_to_string(ctx, interps[0]));

// To dump the interpolation into a SMT file
// execute "iz3 tmp.smt" to compare 
Z3_write_interpolation_problem(ctx, 2, AB, NULL, "tmp.smt");

Z3_pop(ctx,1);  
}

int main() {
  interpolation_1(); 
}

I generate an executable using the command:

g++ -fopenmp -o interpolation interpolation.c -I/home/jorge/Systems/z3/include -I/home/jorge/Systems/z3/iz3/include -L/home/jorge/Systems/z3/lib -L/home/jorge/Systems/z3/iz3/lib -L/home/jorge/Systems/libfoci-1.1 -lz3 -liz3 -lfoci

Note that the constraints are basically:

A = (x=0 and x1 = x0+2 and x2 = x1 + 2),

and B = (x2 > 10)

which are clearly unsat. Moreover, it's also easy to see that the only common variable is x2. Thus, any valid interpolant can only include x2.

If I run the executable ./interpolation I obtain the nonsense interpolant:

(and (>= (+ x0 (* -1 x1)) -2) (>= (+ x1 (* -1 x3)) -2) (<= x0 0))

However, If I run "iz3 tmp.smt" (where tmp.smt is the file generated using Z3_write_interpolation_problem) I obtain a valid interpolant:

unsat interpolant: (<= x2 10)

Is this a bug? or am I missing some important precondition when I call Z3_interpolate?

P.S. I could not find any example using iZ3 with the C API.

Cheers, Jorge

Answer 1

iZ3 was not built against version 4+ and the enumeration types and other features from the headers from the different versions have changed. You cannot yet use iZ3 against the latest versions of Z3. We hope to address this soon, most likely by placing the iZ3 stack along with the rest of Z3 sources, but in the meanwhile use the previous release where iZ3 was built for.