Z3 : C API를 사용하여 가능한 모든 솔루션 찾기

Question

저는 Z3 솔버의 새 고객이며 Windows 10, VS2013 명령 프롬프트를 사용합니다.

C를 사용하려고하는데 Z3 해결사를 사용하여 아래 문제를 해결하려고했습니다.

문제 설정 :a + 2*b + 3*c = 7 만족 a, b의 가능한 조합 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를 실행 한 후) 아래의 결과를 얻었다 :

그래서 나는 Z3의 C 코드 예제를 기반으로, C 코드 아래에 만든

---

그러나 가능한 모든 조합을 얻기 위해 내 C 코드를 수정하는 방법을 묻고 싶습니다. a, b, c?

(예를 들어 : a = 1, b = 0, c = 2, a = 0, b = 2, c = 1 등) 위의 문제를 해결 예제 C 코드를 제공 할 수 있다면 매우 감사하겠습니다

.

감사합니다.

최고, Lee.

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 수 없어 첫 번째로 인해 0이됩니다. And.