c - 带有Craig插值的Z3(iz3)

我正在尝试使用C API生成Craig插值，但得到的结果不正确。
但是，当我通过Z3_write_interpolation_problem将相同的问题转储到文件中并调用iZ3时，我得到了预期的插值。

我附加了代码，以便能够重现相同的结果。
我正在使用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();
}

我使用以下命令生成可执行文件:



请注意，约束基本上是:



这显然是不满意的。此外，还很容易看到唯一的公共(public)变量是x2。因此，任何有效插值只能包含x2。

如果我运行可执行文件./interpolation，我将获得无用的插值:

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

但是，如果我运行“iz3 tmp.smt”(其中tmp.smt是使用Z3_write_interpolation_problem生成的文件)，则可以获得有效的插值:



这是一个错误吗？还是我在调用Z3_interpolate时缺少一些重要的前提条件？

P.S.我找不到将iZ3与C API一起使用的任何示例。

干杯，
乔治

最佳答案

iZ3并非针对版本4+以及版本中的枚举类型和其他功能而构建
不同版本的 header 已更改。您还不能针对最新的版本使用iZ3
Z3版本。我们希望尽快解决此问题，最可能的方法是将iZ3堆栈与
Z3的其余部分，但与此同时使用iZ3所针对的先前发行版。