Z3：C APIを使用してすべての解決策を見つける

Question

私はZ3ソルバーの新人で、Windows 10、VS2013コマンドプロンプトを使用しています。

私はCを使用しようとしていますが、私はZ3ソルバーを使用して以下の問題を解決しようとしました。設定

問題：a + 2*b + 3*c = 7を満たすa、b、cの可能な組み合わせは何ですか？

は、だから私はZ3のCのコード例に基づいて、Cコードの下に作られた：

void example(){ 
    Z3_context ctx = mk_context(); 
    Z3_solver s = mk_solver(ctx); 
    Z3_model m = 0; 
    Z3_ast a, b, c, b_mul_two, c_mul_three, zero, two, three, seven, sum; 
    Z3_ast args2[2], args3[3]; 
    Z3_ast c1, c2, new_constraint[3], new_constraint_and; 
    Z3_ast a_new, b_new, c_new, a_eq_new, b_eq_new, c_eq_new; 
    unsigned num_constants, i, iter; 

    a = mk_int_var(ctx, "a"); 
    b = mk_int_var(ctx, "b"); 
    c = mk_int_var(ctx, "c"); 

    zero = mk_int(ctx, 0); 
    two = mk_int(ctx, 2); 
    three = mk_int(ctx, 3); 
    seven = mk_int(ctx, 7); 

    args2[0] = b; 
    args2[1] = two; 
    b_mul_two = Z3_mk_mul(ctx, 2, args2); 

    args2[0] = c; 
    args2[1] = three; 
    c_mul_three = Z3_mk_mul(ctx, 2, args2); 

    args3[0] = a; 
    args3[1] = b_mul_two; 
    args3[2] = c_mul_three; 
    sum = Z3_mk_add(ctx, 3, args3); 

    c1 = Z3_mk_eq(ctx, sum, seven); 
    Z3_solver_assert(ctx, s, c1); 

    c2 = Z3_mk_ge(ctx, a, zero); 
    Z3_solver_assert(ctx, s, c2); 

    c2 = Z3_mk_ge(ctx, b, zero); 
    Z3_solver_assert(ctx, s, c2); 

    c2 = Z3_mk_ge(ctx, c, zero); 
    Z3_solver_assert(ctx, s, c2); 

    iter = 0; 
    while (Z3_solver_check(ctx, s) == Z3_L_TRUE){ 

     // find solution for the model 
     m = Z3_solver_get_model(ctx, s); 
     printf("model for: a + 2*b + 3*c = 7 (loop: %d)\n", iter); 
     printf("%s\n", Z3_model_to_string(ctx, m)); 

     // Create the finded solution as new constraints to the model 
     // (for each variable a, b, c) 
     num_constants = Z3_model_get_num_consts(ctx, m); 

     for (i = 0; i < num_constants; i++) { 
      Z3_symbol name; 
      Z3_func_decl cnst = Z3_model_get_const_decl(ctx, m, i); 
      Z3_ast k, v; 
      Z3_bool ok; 

      name = Z3_get_decl_name(ctx, cnst); 
      Z3_string str = Z3_get_symbol_string(ctx, name); 

      char* var_name = (char*)*str; 

      k = Z3_mk_app(ctx, cnst, 0, 0); 
      v = k; 
      ok = Z3_model_eval(ctx, m, k, 1, &v); 
      Z3_string val = Z3_get_numeral_string(ctx, v); 

      int var_val; 
      var_val = (int)*val - '0'; 

      if (strcmp(&var_name, "a") == 0){ 
       a_new = mk_int(ctx, var_val); 
      } 
      else if (strcmp(&var_name, "b") == 0){ 
       b_new = mk_int(ctx, var_val); 
      } 
      else if (strcmp(&var_name, "c") == 0){ 
       c_new = mk_int(ctx, var_val); 
      } 
      else{ 
      } 
     } 

     a_eq_new = Z3_mk_eq(ctx, a, a_new); 
     b_eq_new = Z3_mk_eq(ctx, b, b_new); 
     c_eq_new = Z3_mk_eq(ctx, c, c_new); 

     new_constraint[0] = Z3_mk_not(ctx, a_eq_new); 
     new_constraint[1] = Z3_mk_not(ctx, b_eq_new); 
     new_constraint[2] = Z3_mk_not(ctx, c_eq_new); 

     new_constraint_and = Z3_mk_and(ctx, 3, new_constraint); 

     // Add a new contraint to the existing model(?) 
     Z3_solver_assert(ctx, s, new_constraint_and); 

     iter++; 
    } 

    del_solver(ctx, s); 
    Z3_del_context(ctx); 
} 


int main() { 
#ifdef LOG_Z3_CALLS 
    Z3_open_log("z3.log"); 
#endif 
    example(); 
    return 0; 
} 

を結果では、私は

---

D:\z3-master\z3-master\build>make examples 
cl /nologo /c /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG 
/D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /GS /fp:precise 
/Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2 /openmp /MD /D _WINDOWS 
/Fotest_capi2.obj /nologo /MD -I..\src\api ..\examples\c\test_capi2.c 
test_capi2.c 
cl /Fec_example.exe /nologo /MD test_capi2.obj libz3.lib /link /DEBUG 
/MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF 
/OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT 
Z3 examples were successfully built. 

D:\z3-master\z3-master\build>c_example.exe 
model for: a + 2*b + 3*c = 7 (loop: 0) 
b -> 0 
c -> 0 
a -> 7 

model for: a + 2*b + 3*c = 7 (loop: 1) 
b -> 2 
a -> 0 
c -> 1 

（ c_example.exeを構築し、実行した後に）、以下の結果を得ました

---

しかし、私はのすべての可能な組み合わせを得るために私のCコードを修正する方法を尋ねたい10,b,c？

（例えば：a = 1, b = 0, c = 2、a = 0, b = 2, c = 1など）あなたは上記の問題を解決し、例えばCコードを提供することができる場合、私は非常に高く評価されるだろう

。

ありがとうございます。

最高、 リー。

Answer 1

この回答を参照：Z3: finding all satisfying models

があなたとかと交換し、それは他のモデルを生成する必要があります。

new_constraint_and = Z3_mk_and(ctx, 3, new_constraint); 

それは停止だ理由は、あなたがアサートきている：

model for: a + 2*b + 3*c = 7 (loop: 0) 

b -> 0 
c -> 0 
a -> 7 

And(a!=7,b!=0,c!=0) 

モデル用：a + 2*b + 3*c = 7（ループ：1）

b -> 2 
a -> 0 
c -> 1 

And(a!=0,b!=2,c!=1) 

ので、例えば、a=1,b=0,c=2がUNSATされているのでbはできません最初のAndのため0になります。