5

C APIを使用してCraig補間関数を生成しようとしていますが、間違った結果が得られます。ただし、同じ問題をZ3_write_interpolation_problemを介してファイルにダンプし、iZ3を呼び出すと、期待される補間が得られます。

同じ結果を再現できるようにコードを添付します。z34.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 ​​/ home / jorge / Systems / z3 / iz3 / lib -L ​​/ home / jorge / Systems / libfoci-1.1 -lz3 -liz3 -lfoci

制約は基本的に次のとおりであることに注意してください。

A =（x=0およびx1=x0+2および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を使用して生成されたファイル）を実行すると、有効な補間が得られます。

unsat補間：（<= x2 10）

これはバグですか？または、Z3_interpolateを呼び出すときに、いくつかの重要な前提条件が欠落していますか？

PSCAPIでiZ3を使用した例は見つかりませんでした。

乾杯、ホルヘ

4

1 に答える 1

1

iZ3 はバージョン 4+ に対してビルドされておらず、さまざまなバージョンのヘッダーの列挙型やその他の機能が変更されています。Z3 の最新バージョンに対して iZ3 を使用することはまだできません。おそらく、残りの Z3 ソースと一緒に iZ3 スタックを配置することで、この問題にすぐに対処したいと考えていますが、その間は、iZ3 がビルドされた以前のリリースを使用してください。

于 2012-11-30T06:16:27.240 に答える