c - Z3:使用C API找到所有可能的解决方案

Question

我是 Z3 求解器的新手，使用 Windows 10、VS2013 命令提示符。

我正在尝试使用 C，并且尝试使用 Z3 求解器解决以下问题。

问题集: a 的可能组合是什么, b , c满足a + 2*b + 3*c = 7 ？

所以我根据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;
}

结果，我得到了以下结果(构建并运行 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

<小时/>

但是我想问如何修改我的c代码以获得a的所有可能组合, b , c ？

(例如: a = 1, b = 0, c = 2 、 a = 0, b = 2, c = 1 等)

如果您能提供解决上述问题的示例 C 代码，我将不胜感激。

非常感谢您抽出时间。

最好，李。

Answer 1

引用这个答案:Z3: finding all satisfying models

将 and 替换为 or，然后它应该生成其他模型。

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 是不饱和的，因为由于第一个原因 b 不能为 0 和。