我正在尝试使用 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();
}
我使用以下命令生成可执行文件:
g++ -fopenmp -o 插值插值.c -I/home/jorge/Systems/z3/include -I/home/jorge/Systems/z3/iz3/include -L/home/jorge/Systems/z3/lib -L/主页/jorge/Systems/z3/iz3/lib -L/home/jorge/Systems/libfoci-1.1 -lz3 -liz3 -lfoci
请注意,约束基本上是:
A = (x=0 and x1 = x0+2 and x2 = x1 + 2),
和 B = (x2 > 10)
这显然是不满意的。此外,很容易看出唯一的公共变量是 x2。因此,任何有效的插值只能包括 x2。
如果我运行可执行文件 ./interpolation 我会得到无意义的插值:
(and (>= (+ x0 (* -1 x1)) -2) (>= (+ x1 (* -1 x3)) -2) (<= x0 0))
但是,如果我运行“iz3 tmp.smt”(其中 tmp.smt 是使用 Z3_write_interpolation_problem 生成的文件),我将获得一个有效的插值:
未饱和插值:(<= x2 10)
这是一个错误吗?还是我在调用 Z3_interpolate 时遗漏了一些重要的先决条件?
PS 我找不到任何使用 iZ3 和 C API 的示例。
干杯,豪尔赫