Z3:使用 C API 寻找所有可能的解决方案 [英] Z3: finding all possible solutions using C API
问题描述
我是 Z3 求解器的新手，使用 Windows 10，VS2013 命令提示符.
I am a newcomer in Z3 solver, and using Windows 10, VS2013 command prompt.
我正在尝试使用 C，并且尝试使用 Z3 求解器解决以下问题.
I am trying to use C and I have tried to solve the below problem using Z3 solver.
问题集:满足的?a、b、c的可能组合是什么?a + 2*b + 3*c = 7
Problem set: What is the possible combination of a, b, c that satisfies a + 2*b + 3*c = 7?
所以我根据Z3的C代码示例编写了以下C代码:
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;
}
结果，我得到了以下结果(在构建和运行 c_example.exe 之后)
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
<小时>
但是我想问一下如何修改我的c代码以获得a、b、c的所有可能组合?
(例如:a = 1, b = 0, c = 2, a = 0, b = 2, c = 1 等等)
如果您能提供解决上述问题的示例 C 代码，我将不胜感激.
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.
最好的，李.
推荐答案
参考这个答案:Z3:找到所有满意的模型
用 or 替换你的 and，然后它应该生成其他模型.
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)
模型: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 由于第一个和.
So, e.g., a=1,b=0,c=2 is unsat since b cannot be 0 due to the first And.
这篇关于Z3:使用 C API 寻找所有可能的解决方案的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
