Z3: finding all possible solutions using C API

Question

I am a newcomer in Z3 solver, and using Windows 10, VS2013 command prompt.

I am trying to use C and I have tried to solve the below problem using Z3 solver.

Problem set: What is the possible combination of a, b, c that satisfies a + 2*b + 3*c = 7?

So I made below C code, based on the C code example of Z3:

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;
}

In result, I got the below result (after building and running c_example.exe)

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

But I want to ask how to revise my c code to get all possible combinations of a, b, c?

(e.g.: a = 1, b = 0, c = 2, a = 0, b = 2, c = 1 and so on)

I would be very appreciated if you can provide an example C code which solves the above problem.

Thank you very much for your time.

Best, Lee.

Please don't post pictures of text. Insteads do the obvious: post the text. — Jabberwocky, Dec 18 '17 at 17:02
I would suggest you use the C++ API and not the C API. Your code creates a context twice and creates a solver twice. You can walk a model for values of your variables and create formulas that block a previous model. — Nikolaj Bjorner, Dec 18 '17 at 19:57
I revised the main text. Any help would be very appreciated. Thank you very much. — Sang Hun Lee, Dec 18 '17 at 21:14

score 0 · Answer 1 · edited Feb 23 '18 at 10:10

Referring to this answer: Z3: finding all satisfying models

Replace your and with an or, then it should generate the other models.

new_constraint_and = Z3_mk_and(ctx, 3, new_constraint);

The reason it's stopping is you've asserted:

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

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

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

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

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

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

So, e.g., a=1,b=0,c=2 is unsat since b cannot be 0 due to the first And.

Z3: finding all possible solutions using C API

1 Answers1

Linked