title: Z3: finding all possible solutions using C API
body: <p>I am a newcomer in Z3 solver, and using Windows 10, VS2013 command prompt.</p>
  
  <p>I am trying to use C and I have tried to solve the below problem using Z3 solver.</p>
  
  <p><em>Problem set:</em> What is the possible combination of <code>a</code>, <code>b</code>, <code>c</code> that satisfies <code>a + 2*b + 3*c = 7</code>?</p>
  
  <p>So I made below C code, based on the C code example of Z3:</p>
  
  <pre><code>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 &lt; 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, &amp;v);
              Z3_string val = Z3_get_numeral_string(ctx, v);
  
              int var_val;
              var_val = (int)*val - '0';
  
              if (strcmp(&amp;var_name, "a") == 0){
                  a_new = mk_int(ctx, var_val);
              }
              else if (strcmp(&amp;var_name, "b") == 0){
                  b_new = mk_int(ctx, var_val);
              }
              else if (strcmp(&amp;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;
  }
  </code></pre>
  
  <p>In result, I got the below result (after building and running <code>c_example.exe</code>)</p>
  
  <hr>
  
  <pre><code>D:\z3-master\z3-master\build&gt;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&gt;c_example.exe
  model for: a + 2*b + 3*c = 7 (loop: 0)
  b -&gt; 0
  c -&gt; 0
  a -&gt; 7
  
  model for: a + 2*b + 3*c = 7 (loop: 1)
  b -&gt; 2
  a -&gt; 0
  c -&gt; 1
  </code></pre>
  
  <hr>
  
  <p>But I want to ask how to revise my c code to get all possible combinations of <code>a</code>, <code>b</code>, <code>c</code>?</p>
  
  <p>(e.g.: <code>a = 1, b = 0, c = 2</code>, <code>a = 0, b = 2, c = 1</code> and so on)</p>
  
  <p>I would be very appreciated if you can provide an example C code which solves the above problem.</p>
  
  <p>Thank you very much for your time.</p>
  
  <p>Best,
  Lee.</p>