mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 00:55:31 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
Yatao Li
commit
f5b874e0a3
587 changed files with 16270 additions and 9645 deletions
|
|
@ -7,8 +7,8 @@ find_package(Z3
|
|||
REQUIRED
|
||||
CONFIG
|
||||
# `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3.
|
||||
# This should prevent us from accidently picking up an installed
|
||||
# copy of Z3. This is here to benefit Z3's build sytem when building
|
||||
# This should prevent us from accidentally picking up an installed
|
||||
# copy of Z3. This is here to benefit Z3's build system when building
|
||||
# this project. When making your own project you probably shouldn't
|
||||
# use this option.
|
||||
NO_DEFAULT_PATH
|
||||
|
|
|
|||
|
|
@ -5,6 +5,6 @@ in the build directory.
|
|||
|
||||
This command will create the executable cpp_example.
|
||||
On Windows, you can just execute it.
|
||||
On OSX and Linux, you must install z3 first using
|
||||
On macOS and Linux, you must install z3 first using
|
||||
sudo make install
|
||||
OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX) with the build directory. You need that to be able to find the Z3 shared library.
|
||||
OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (macOS) with the build directory. You need that to be able to find the Z3 shared library.
|
||||
|
|
|
|||
|
|
@ -835,6 +835,17 @@ void tst_visit() {
|
|||
visit(f);
|
||||
}
|
||||
|
||||
void tst_numeral() {
|
||||
context c;
|
||||
expr x = c.real_val("1/3");
|
||||
double d = 0;
|
||||
if (!x.is_numeral(d)) {
|
||||
std::cout << x << " is not recognized as a numeral\n";
|
||||
return;
|
||||
}
|
||||
std::cout << x << " is " << d << "\n";
|
||||
}
|
||||
|
||||
void incremental_example1() {
|
||||
std::cout << "incremental example1\n";
|
||||
context c;
|
||||
|
|
@ -1179,6 +1190,20 @@ void mk_model_example() {
|
|||
std::cout << m.eval(a + b < 2)<< std::endl;
|
||||
}
|
||||
|
||||
void recfun_example() {
|
||||
std::cout << "recfun example\n";
|
||||
context c;
|
||||
expr x = c.int_const("x");
|
||||
expr y = c.int_const("y");
|
||||
expr b = c.bool_const("b");
|
||||
sort I = c.int_sort();
|
||||
sort B = c.bool_sort();
|
||||
func_decl f = recfun("f", I, B, I);
|
||||
expr_vector args(c);
|
||||
args.push_back(x); args.push_back(b);
|
||||
c.recdef(f, args, ite(b, x, f(x + 1, !b)));
|
||||
prove(f(x,c.bool_val(false)) > x);
|
||||
}
|
||||
|
||||
int main() {
|
||||
|
||||
|
|
@ -1212,6 +1237,7 @@ int main() {
|
|||
tactic_example9(); std::cout << "\n";
|
||||
tactic_qe(); std::cout << "\n";
|
||||
tst_visit(); std::cout << "\n";
|
||||
tst_numeral(); std::cout << "\n";
|
||||
incremental_example1(); std::cout << "\n";
|
||||
incremental_example2(); std::cout << "\n";
|
||||
incremental_example3(); std::cout << "\n";
|
||||
|
|
@ -1227,6 +1253,7 @@ int main() {
|
|||
consequence_example(); std::cout << "\n";
|
||||
parse_example(); std::cout << "\n";
|
||||
mk_model_example(); std::cout << "\n";
|
||||
recfun_example(); std::cout << "\n";
|
||||
std::cout << "done\n";
|
||||
}
|
||||
catch (exception & ex) {
|
||||
|
|
|
|||
|
|
@ -24,8 +24,8 @@ find_package(Z3
|
|||
REQUIRED
|
||||
CONFIG
|
||||
# `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3.
|
||||
# This should prevent us from accidently picking up an installed
|
||||
# copy of Z3. This is here to benefit Z3's build sytem when building
|
||||
# This should prevent us from accidentally picking up an installed
|
||||
# copy of Z3. This is here to benefit Z3's build system when building
|
||||
# this project. When making your own project you probably shouldn't
|
||||
# use this option.
|
||||
NO_DEFAULT_PATH
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ in the build directory.
|
|||
|
||||
This command will create the executable c_example.
|
||||
On Windows, you can just execute it.
|
||||
On OSX and Linux, you must install z3 first using
|
||||
On macOS and Linux, you must install z3 first using
|
||||
sudo make install
|
||||
OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX) with the build directory. You need that to be able to find the Z3 shared library.
|
||||
OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (macOS) with the build directory. You need that to be able to find the Z3 shared library.
|
||||
|
||||
|
|
|
|||
|
|
@ -241,7 +241,7 @@ void check(Z3_context ctx, Z3_solver s, Z3_lbool expected_result)
|
|||
|
||||
The context \c ctx is not modified by this function.
|
||||
*/
|
||||
void prove(Z3_context ctx, Z3_solver s, Z3_ast f, Z3_bool is_valid)
|
||||
void prove(Z3_context ctx, Z3_solver s, Z3_ast f, bool is_valid)
|
||||
{
|
||||
Z3_model m = 0;
|
||||
Z3_ast not_f;
|
||||
|
|
@ -379,6 +379,7 @@ void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f)
|
|||
Z3_sort t;
|
||||
Z3_symbol f_name, t_name;
|
||||
Z3_ast_vector q;
|
||||
unsigned i;
|
||||
|
||||
t = Z3_get_range(ctx, f);
|
||||
|
||||
|
|
@ -399,7 +400,7 @@ void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f)
|
|||
1, &t_name, &t,
|
||||
1, &f_name, &f);
|
||||
printf("assert axiom:\n%s\n", Z3_ast_vector_to_string(ctx, q));
|
||||
for (unsigned i = 0; i < Z3_ast_vector_size(ctx, q); ++i) {
|
||||
for (i = 0; i < Z3_ast_vector_size(ctx, q); ++i) {
|
||||
Z3_solver_assert(ctx, s, Z3_ast_vector_get(ctx, q, i));
|
||||
}
|
||||
}
|
||||
|
|
@ -638,7 +639,7 @@ void display_model(Z3_context c, FILE * out, Z3_model m)
|
|||
Z3_symbol name;
|
||||
Z3_func_decl cnst = Z3_model_get_const_decl(c, m, i);
|
||||
Z3_ast a, v;
|
||||
Z3_bool ok;
|
||||
bool ok;
|
||||
name = Z3_get_decl_name(c, cnst);
|
||||
display_symbol(c, out, name);
|
||||
fprintf(out, " = ");
|
||||
|
|
@ -898,7 +899,7 @@ void prove_example1()
|
|||
/* prove g(x) = g(y) */
|
||||
f = Z3_mk_eq(ctx, gx, gy);
|
||||
printf("prove: x = y implies g(x) = g(y)\n");
|
||||
prove(ctx, s, f, Z3_TRUE);
|
||||
prove(ctx, s, f, true);
|
||||
|
||||
/* create g(g(x)) */
|
||||
ggx = mk_unary_app(ctx, g, gx);
|
||||
|
|
@ -906,7 +907,7 @@ void prove_example1()
|
|||
/* disprove g(g(x)) = g(y) */
|
||||
f = Z3_mk_eq(ctx, ggx, gy);
|
||||
printf("disprove: x = y implies g(g(x)) = g(y)\n");
|
||||
prove(ctx, s, f, Z3_FALSE);
|
||||
prove(ctx, s, f, false);
|
||||
|
||||
del_solver(ctx, s);
|
||||
Z3_del_context(ctx);
|
||||
|
|
@ -978,13 +979,13 @@ void prove_example2()
|
|||
/* prove z < 0 */
|
||||
f = Z3_mk_lt(ctx, z, zero);
|
||||
printf("prove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0\n");
|
||||
prove(ctx, s, f, Z3_TRUE);
|
||||
prove(ctx, s, f, true);
|
||||
|
||||
/* disprove z < -1 */
|
||||
minus_one = mk_int(ctx, -1);
|
||||
f = Z3_mk_lt(ctx, z, minus_one);
|
||||
printf("disprove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < -1\n");
|
||||
prove(ctx, s, f, Z3_FALSE);
|
||||
prove(ctx, s, f, false);
|
||||
|
||||
del_solver(ctx, s);
|
||||
Z3_del_context(ctx);
|
||||
|
|
@ -1130,7 +1131,7 @@ void quantifier_example1()
|
|||
/* prove f(x, y) = f(w, v) implies y = v */
|
||||
p2 = Z3_mk_eq(ctx, y, v);
|
||||
printf("prove: f(x, y) = f(w, v) implies y = v\n");
|
||||
prove(ctx, s, p2, Z3_TRUE);
|
||||
prove(ctx, s, p2, true);
|
||||
|
||||
/* disprove f(x, y) = f(w, v) implies x = w */
|
||||
/* using check2 instead of prove */
|
||||
|
|
@ -1197,7 +1198,7 @@ void array_example1()
|
|||
thm = Z3_mk_implies(ctx, antecedent, consequent);
|
||||
printf("prove: store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3))\n");
|
||||
printf("%s\n", Z3_ast_to_string(ctx, thm));
|
||||
prove(ctx, s, thm, Z3_TRUE);
|
||||
prove(ctx, s, thm, true);
|
||||
|
||||
del_solver(ctx, s);
|
||||
Z3_del_context(ctx);
|
||||
|
|
@ -1338,13 +1339,13 @@ void tuple_example1()
|
|||
eq2 = Z3_mk_eq(ctx, x, one);
|
||||
thm = Z3_mk_implies(ctx, eq1, eq2);
|
||||
printf("prove: get_x(mk_pair(x, y)) = 1 implies x = 1\n");
|
||||
prove(ctx, s, thm, Z3_TRUE);
|
||||
prove(ctx, s, thm, true);
|
||||
|
||||
/* disprove that get_x(mk_pair(x,y)) == 1 implies y = 1*/
|
||||
eq3 = Z3_mk_eq(ctx, y, one);
|
||||
thm = Z3_mk_implies(ctx, eq1, eq3);
|
||||
printf("disprove: get_x(mk_pair(x, y)) = 1 implies y = 1\n");
|
||||
prove(ctx, s, thm, Z3_FALSE);
|
||||
prove(ctx, s, thm, false);
|
||||
}
|
||||
|
||||
{
|
||||
|
|
@ -1365,12 +1366,12 @@ void tuple_example1()
|
|||
consequent = Z3_mk_eq(ctx, p1, p2);
|
||||
thm = Z3_mk_implies(ctx, antecedent, consequent);
|
||||
printf("prove: get_x(p1) = get_x(p2) and get_y(p1) = get_y(p2) implies p1 = p2\n");
|
||||
prove(ctx, s, thm, Z3_TRUE);
|
||||
prove(ctx, s, thm, true);
|
||||
|
||||
/* disprove that get_x(p1) = get_x(p2) implies p1 = p2 */
|
||||
thm = Z3_mk_implies(ctx, antecedents[0], consequent);
|
||||
printf("disprove: get_x(p1) = get_x(p2) implies p1 = p2\n");
|
||||
prove(ctx, s, thm, Z3_FALSE);
|
||||
prove(ctx, s, thm, false);
|
||||
}
|
||||
|
||||
{
|
||||
|
|
@ -1389,14 +1390,14 @@ void tuple_example1()
|
|||
consequent = Z3_mk_eq(ctx, x, ten);
|
||||
thm = Z3_mk_implies(ctx, antecedent, consequent);
|
||||
printf("prove: p2 = update(p1, 0, 10) implies get_x(p2) = 10\n");
|
||||
prove(ctx, s, thm, Z3_TRUE);
|
||||
prove(ctx, s, thm, true);
|
||||
|
||||
/* disprove that p2 = update(p1, 0, 10) implies get_y(p2) = 10 */
|
||||
y = mk_unary_app(ctx, get_y_decl, p2);
|
||||
consequent = Z3_mk_eq(ctx, y, ten);
|
||||
thm = Z3_mk_implies(ctx, antecedent, consequent);
|
||||
printf("disprove: p2 = update(p1, 0, 10) implies get_y(p2) = 10\n");
|
||||
prove(ctx, s, thm, Z3_FALSE);
|
||||
prove(ctx, s, thm, false);
|
||||
}
|
||||
|
||||
del_solver(ctx, s);
|
||||
|
|
@ -1428,7 +1429,7 @@ void bitvector_example1()
|
|||
c2 = Z3_mk_bvsle(ctx, x_minus_ten, zero);
|
||||
thm = Z3_mk_iff(ctx, c1, c2);
|
||||
printf("disprove: x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers\n");
|
||||
prove(ctx, s, thm, Z3_FALSE);
|
||||
prove(ctx, s, thm, false);
|
||||
|
||||
del_solver(ctx, s);
|
||||
Z3_del_context(ctx);
|
||||
|
|
@ -1644,6 +1645,7 @@ void parser_example2()
|
|||
Z3_symbol names[2];
|
||||
Z3_func_decl decls[2];
|
||||
Z3_ast_vector f;
|
||||
unsigned i;
|
||||
|
||||
printf("\nparser_example2\n");
|
||||
LOG_MSG("parser_example2");
|
||||
|
|
@ -1668,7 +1670,7 @@ void parser_example2()
|
|||
2, names, decls);
|
||||
printf("formula: %s\n", Z3_ast_vector_to_string(ctx, f));
|
||||
printf("assert axiom:\n%s\n", Z3_ast_vector_to_string(ctx, f));
|
||||
for (unsigned i = 0; i < Z3_ast_vector_size(ctx, f); ++i) {
|
||||
for (i = 0; i < Z3_ast_vector_size(ctx, f); ++i) {
|
||||
Z3_solver_assert(ctx, s, Z3_ast_vector_get(ctx, f, i));
|
||||
}
|
||||
check(ctx, s, Z3_L_TRUE);
|
||||
|
|
@ -1695,7 +1697,7 @@ void parser_example3()
|
|||
LOG_MSG("parser_example3");
|
||||
|
||||
cfg = Z3_mk_config();
|
||||
/* See quantifer_example1 */
|
||||
/* See quantifier_example1 */
|
||||
Z3_set_param_value(cfg, "model", "true");
|
||||
ctx = mk_context_custom(cfg, error_handler);
|
||||
Z3_del_config(cfg);
|
||||
|
|
@ -1715,7 +1717,7 @@ void parser_example3()
|
|||
0, 0, 0,
|
||||
1, &g_name, &g);
|
||||
printf("formula: %s\n", Z3_ast_vector_to_string(ctx, thm));
|
||||
prove(ctx, s, Z3_ast_vector_get(ctx, thm, 0), Z3_TRUE);
|
||||
prove(ctx, s, Z3_ast_vector_get(ctx, thm, 0), true);
|
||||
|
||||
del_solver(ctx, s);
|
||||
Z3_del_context(ctx);
|
||||
|
|
@ -1779,13 +1781,13 @@ void numeral_example() {
|
|||
n2 = Z3_mk_numeral(ctx, "0.5", real_ty);
|
||||
printf("Numerals n1:%s", Z3_ast_to_string(ctx, n1));
|
||||
printf(" n2:%s\n", Z3_ast_to_string(ctx, n2));
|
||||
prove(ctx, s, Z3_mk_eq(ctx, n1, n2), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_eq(ctx, n1, n2), true);
|
||||
|
||||
n1 = Z3_mk_numeral(ctx, "-1/3", real_ty);
|
||||
n2 = Z3_mk_numeral(ctx, "-0.33333333333333333333333333333333333333333333333333", real_ty);
|
||||
printf("Numerals n1:%s", Z3_ast_to_string(ctx, n1));
|
||||
printf(" n2:%s\n", Z3_ast_to_string(ctx, n2));
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, n1, n2)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, n1, n2)), true);
|
||||
del_solver(ctx, s);
|
||||
Z3_del_context(ctx);
|
||||
}
|
||||
|
|
@ -1850,14 +1852,14 @@ void enum_example() {
|
|||
orange = Z3_mk_app(ctx, enum_consts[2], 0, 0);
|
||||
|
||||
/* Apples are different from oranges */
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, apple, orange)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, apple, orange)), true);
|
||||
|
||||
/* Apples pass the apple test */
|
||||
prove(ctx, s, Z3_mk_app(ctx, enum_testers[0], 1, &apple), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_app(ctx, enum_testers[0], 1, &apple), true);
|
||||
|
||||
/* Oranges fail the apple test */
|
||||
prove(ctx, s, Z3_mk_app(ctx, enum_testers[0], 1, &orange), Z3_FALSE);
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_app(ctx, enum_testers[0], 1, &orange)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_app(ctx, enum_testers[0], 1, &orange), false);
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_app(ctx, enum_testers[0], 1, &orange)), true);
|
||||
|
||||
fruity = mk_var(ctx, "fruity", fruit);
|
||||
|
||||
|
|
@ -1866,7 +1868,7 @@ void enum_example() {
|
|||
ors[1] = Z3_mk_eq(ctx, fruity, banana);
|
||||
ors[2] = Z3_mk_eq(ctx, fruity, orange);
|
||||
|
||||
prove(ctx, s, Z3_mk_or(ctx, 3, ors), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_or(ctx, 3, ors), true);
|
||||
|
||||
/* delete logical context */
|
||||
del_solver(ctx, s);
|
||||
|
|
@ -1898,41 +1900,41 @@ void list_example() {
|
|||
l2 = mk_binary_app(ctx, cons_decl, mk_int(ctx, 2), nil);
|
||||
|
||||
/* nil != cons(1, nil) */
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, l1)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, l1)), true);
|
||||
|
||||
/* cons(2,nil) != cons(1, nil) */
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, l1, l2)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, l1, l2)), true);
|
||||
|
||||
/* cons(x,nil) = cons(y, nil) => x = y */
|
||||
x = mk_var(ctx, "x", int_ty);
|
||||
y = mk_var(ctx, "y", int_ty);
|
||||
l1 = mk_binary_app(ctx, cons_decl, x, nil);
|
||||
l2 = mk_binary_app(ctx, cons_decl, y, nil);
|
||||
prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), true);
|
||||
|
||||
/* cons(x,u) = cons(x, v) => u = v */
|
||||
u = mk_var(ctx, "u", int_list);
|
||||
v = mk_var(ctx, "v", int_list);
|
||||
l1 = mk_binary_app(ctx, cons_decl, x, u);
|
||||
l2 = mk_binary_app(ctx, cons_decl, y, v);
|
||||
prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), true);
|
||||
prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), true);
|
||||
|
||||
/* is_nil(u) or is_cons(u) */
|
||||
ors[0] = Z3_mk_app(ctx, is_nil_decl, 1, &u);
|
||||
ors[1] = Z3_mk_app(ctx, is_cons_decl, 1, &u);
|
||||
prove(ctx, s, Z3_mk_or(ctx, 2, ors), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_or(ctx, 2, ors), true);
|
||||
|
||||
/* occurs check u != cons(x,u) */
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), true);
|
||||
|
||||
/* destructors: is_cons(u) => u = cons(head(u),tail(u)) */
|
||||
fml1 = Z3_mk_eq(ctx, u, mk_binary_app(ctx, cons_decl, mk_unary_app(ctx, head_decl, u), mk_unary_app(ctx, tail_decl, u)));
|
||||
fml = Z3_mk_implies(ctx, Z3_mk_app(ctx, is_cons_decl, 1, &u), fml1);
|
||||
printf("Formula %s\n", Z3_ast_to_string(ctx, fml));
|
||||
prove(ctx, s, fml, Z3_TRUE);
|
||||
prove(ctx, s, fml, true);
|
||||
|
||||
prove(ctx, s, fml1, Z3_FALSE);
|
||||
prove(ctx, s, fml1, false);
|
||||
|
||||
/* delete logical context */
|
||||
del_solver(ctx, s);
|
||||
|
|
@ -1980,7 +1982,7 @@ void tree_example() {
|
|||
l2 = mk_binary_app(ctx, cons_decl, l1, nil);
|
||||
|
||||
/* nil != cons(nil, nil) */
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, l1)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, l1)), true);
|
||||
|
||||
/* cons(x,u) = cons(x, v) => u = v */
|
||||
u = mk_var(ctx, "u", cell);
|
||||
|
|
@ -1989,24 +1991,24 @@ void tree_example() {
|
|||
y = mk_var(ctx, "y", cell);
|
||||
l1 = mk_binary_app(ctx, cons_decl, x, u);
|
||||
l2 = mk_binary_app(ctx, cons_decl, y, v);
|
||||
prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), true);
|
||||
prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), true);
|
||||
|
||||
/* is_nil(u) or is_cons(u) */
|
||||
ors[0] = Z3_mk_app(ctx, is_nil_decl, 1, &u);
|
||||
ors[1] = Z3_mk_app(ctx, is_cons_decl, 1, &u);
|
||||
prove(ctx, s, Z3_mk_or(ctx, 2, ors), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_or(ctx, 2, ors), true);
|
||||
|
||||
/* occurs check u != cons(x,u) */
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), true);
|
||||
|
||||
/* destructors: is_cons(u) => u = cons(car(u),cdr(u)) */
|
||||
fml1 = Z3_mk_eq(ctx, u, mk_binary_app(ctx, cons_decl, mk_unary_app(ctx, car_decl, u), mk_unary_app(ctx, cdr_decl, u)));
|
||||
fml = Z3_mk_implies(ctx, Z3_mk_app(ctx, is_cons_decl, 1, &u), fml1);
|
||||
printf("Formula %s\n", Z3_ast_to_string(ctx, fml));
|
||||
prove(ctx, s, fml, Z3_TRUE);
|
||||
prove(ctx, s, fml, true);
|
||||
|
||||
prove(ctx, s, fml1, Z3_FALSE);
|
||||
prove(ctx, s, fml1, false);
|
||||
|
||||
/* delete logical context */
|
||||
del_solver(ctx, s);
|
||||
|
|
@ -2098,8 +2100,8 @@ void forest_example() {
|
|||
|
||||
|
||||
/* nil != cons(nil,nil) */
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil1, f1)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil2, t1)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil1, f1)), true);
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil2, t1)), true);
|
||||
|
||||
|
||||
/* cons(x,u) = cons(x, v) => u = v */
|
||||
|
|
@ -2109,16 +2111,16 @@ void forest_example() {
|
|||
y = mk_var(ctx, "y", tree);
|
||||
l1 = mk_binary_app(ctx, cons1_decl, x, u);
|
||||
l2 = mk_binary_app(ctx, cons1_decl, y, v);
|
||||
prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), true);
|
||||
prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), true);
|
||||
|
||||
/* is_nil(u) or is_cons(u) */
|
||||
ors[0] = Z3_mk_app(ctx, is_nil1_decl, 1, &u);
|
||||
ors[1] = Z3_mk_app(ctx, is_cons1_decl, 1, &u);
|
||||
prove(ctx, s, Z3_mk_or(ctx, 2, ors), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_or(ctx, 2, ors), true);
|
||||
|
||||
/* occurs check u != cons(x,u) */
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), true);
|
||||
|
||||
/* delete logical context */
|
||||
del_solver(ctx, s);
|
||||
|
|
@ -2191,19 +2193,19 @@ void binary_tree_example() {
|
|||
Z3_ast node3 = Z3_mk_app(ctx, node_decl, 3, args3);
|
||||
|
||||
/* prove that nil != node1 */
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, node1)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, node1)), true);
|
||||
|
||||
/* prove that nil = left(node1) */
|
||||
prove(ctx, s, Z3_mk_eq(ctx, nil, mk_unary_app(ctx, left_decl, node1)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_eq(ctx, nil, mk_unary_app(ctx, left_decl, node1)), true);
|
||||
|
||||
/* prove that node1 = right(node3) */
|
||||
prove(ctx, s, Z3_mk_eq(ctx, node1, mk_unary_app(ctx, right_decl, node3)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_eq(ctx, node1, mk_unary_app(ctx, right_decl, node3)), true);
|
||||
|
||||
/* prove that !is-nil(node2) */
|
||||
prove(ctx, s, Z3_mk_not(ctx, mk_unary_app(ctx, is_nil_decl, node2)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_not(ctx, mk_unary_app(ctx, is_nil_decl, node2)), true);
|
||||
|
||||
/* prove that value(node2) >= 0 */
|
||||
prove(ctx, s, Z3_mk_ge(ctx, mk_unary_app(ctx, value_decl, node2), mk_int(ctx, 0)), Z3_TRUE);
|
||||
prove(ctx, s, Z3_mk_ge(ctx, mk_unary_app(ctx, value_decl, node2), mk_int(ctx, 0)), true);
|
||||
}
|
||||
|
||||
/* delete logical context */
|
||||
|
|
@ -2302,7 +2304,7 @@ typedef struct {
|
|||
// IMPORTANT: the fields m_answer_literals, m_retracted and m_num_answer_literals must be saved/restored
|
||||
// if push/pop operations are performed on m_context.
|
||||
Z3_ast m_answer_literals[MAX_RETRACTABLE_ASSERTIONS];
|
||||
Z3_bool m_retracted[MAX_RETRACTABLE_ASSERTIONS]; // true if the assertion was retracted.
|
||||
bool m_retracted[MAX_RETRACTABLE_ASSERTIONS]; // true if the assertion was retracted.
|
||||
unsigned m_num_answer_literals;
|
||||
} Z3_ext_context_struct;
|
||||
|
||||
|
|
@ -2345,7 +2347,7 @@ unsigned assert_retractable_cnstr(Z3_ext_context ctx, Z3_ast c) {
|
|||
ans_lit = Z3_mk_fresh_const(ctx->m_context, "k", ty);
|
||||
result = ctx->m_num_answer_literals;
|
||||
ctx->m_answer_literals[result] = ans_lit;
|
||||
ctx->m_retracted[result] = Z3_FALSE;
|
||||
ctx->m_retracted[result] = false;
|
||||
ctx->m_num_answer_literals++;
|
||||
// assert: c OR (not ans_lit)
|
||||
args[0] = c;
|
||||
|
|
@ -2361,7 +2363,7 @@ void retract_cnstr(Z3_ext_context ctx, unsigned id) {
|
|||
if (id >= ctx->m_num_answer_literals) {
|
||||
exitf("invalid constraint id.");
|
||||
}
|
||||
ctx->m_retracted[id] = Z3_TRUE;
|
||||
ctx->m_retracted[id] = true;
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -2371,7 +2373,7 @@ void reassert_cnstr(Z3_ext_context ctx, unsigned id) {
|
|||
if (id >= ctx->m_num_answer_literals) {
|
||||
exitf("invalid constraint id.");
|
||||
}
|
||||
ctx->m_retracted[id] = Z3_FALSE;
|
||||
ctx->m_retracted[id] = false;
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -2385,7 +2387,7 @@ Z3_lbool ext_check(Z3_ext_context ctx) {
|
|||
unsigned core_size;
|
||||
unsigned i;
|
||||
for (i = 0; i < ctx->m_num_answer_literals; i++) {
|
||||
if (ctx->m_retracted[i] == Z3_FALSE) {
|
||||
if (ctx->m_retracted[i] == false) {
|
||||
// Since the answer literal was not retracted, we added it as an assumption.
|
||||
// Recall that we assert (C \/ (not ans_lit)). Therefore, adding ans_lit as an assumption has the effect of "asserting" C.
|
||||
// If the constraint was "retracted" (ctx->m_retracted[i] == Z3_true), then we don't really need to add (not ans_lit) as an assumption.
|
||||
|
|
@ -2870,19 +2872,19 @@ void mk_model_example() {
|
|||
/*num_args=*/2,
|
||||
/*args=*/addArgs);
|
||||
Z3_ast aPlusBEval = NULL;
|
||||
Z3_bool aPlusBEvalSuccess =
|
||||
bool aPlusBEvalSuccess =
|
||||
Z3_model_eval(ctx, m, aPlusB,
|
||||
/*model_completion=*/Z3_FALSE, &aPlusBEval);
|
||||
if (aPlusBEvalSuccess != Z3_TRUE) {
|
||||
/*model_completion=*/false, &aPlusBEval);
|
||||
if (aPlusBEvalSuccess != true) {
|
||||
printf("Failed to evaluate model\n");
|
||||
exit(1);
|
||||
}
|
||||
|
||||
{
|
||||
int aPlusBValue = 0;
|
||||
Z3_bool getAPlusBValueSuccess =
|
||||
bool getAPlusBValueSuccess =
|
||||
Z3_get_numeral_int(ctx, aPlusBEval, &aPlusBValue);
|
||||
if (getAPlusBValueSuccess != Z3_TRUE) {
|
||||
if (getAPlusBValueSuccess != true) {
|
||||
printf("Failed to get integer value for a+b\n");
|
||||
exit(1);
|
||||
}
|
||||
|
|
@ -2904,18 +2906,18 @@ void mk_model_example() {
|
|||
/*num_args=*/3,
|
||||
/*args=*/arrayAddArgs);
|
||||
Z3_ast arrayAddEval = NULL;
|
||||
Z3_bool arrayAddEvalSuccess =
|
||||
bool arrayAddEvalSuccess =
|
||||
Z3_model_eval(ctx, m, arrayAdd,
|
||||
/*model_completion=*/Z3_FALSE, &arrayAddEval);
|
||||
if (arrayAddEvalSuccess != Z3_TRUE) {
|
||||
/*model_completion=*/false, &arrayAddEval);
|
||||
if (arrayAddEvalSuccess != true) {
|
||||
printf("Failed to evaluate model\n");
|
||||
exit(1);
|
||||
}
|
||||
{
|
||||
int arrayAddValue = 0;
|
||||
Z3_bool getArrayAddValueSuccess =
|
||||
bool getArrayAddValueSuccess =
|
||||
Z3_get_numeral_int(ctx, arrayAddEval, &arrayAddValue);
|
||||
if (getArrayAddValueSuccess != Z3_TRUE) {
|
||||
if (getArrayAddValueSuccess != true) {
|
||||
printf("Failed to get integer value for c[0] + c[1] + c[2]\n");
|
||||
exit(1);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -363,10 +363,10 @@ namespace test_mapi
|
|||
|
||||
Console.WriteLine("Model = " + s.Model);
|
||||
|
||||
Console.WriteLine("Interpretation of MyArray:\n" + s.Model.FuncInterp(aex.FuncDecl));
|
||||
//Console.WriteLine("Interpretation of MyArray:\n" + s.Model.ConstInterp(aex.FuncDecl));
|
||||
Console.WriteLine("Interpretation of x:\n" + s.Model.ConstInterp(xc));
|
||||
Console.WriteLine("Interpretation of f:\n" + s.Model.FuncInterp(fd));
|
||||
Console.WriteLine("Interpretation of MyArray as Term:\n" + s.Model.FuncInterp(aex.FuncDecl));
|
||||
//Console.WriteLine("Interpretation of MyArray as Term:\n" + s.Model.ConstInterp(aex.FuncDecl));
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
|
|||
|
|
@ -10,5 +10,5 @@ which can be run on Windows via
|
|||
|
||||
On Linux and FreeBSD, we must use
|
||||
LD_LIBRARY_PATH=. java -cp com.microsoft.z3.jar:. JavaExample
|
||||
On OSX, the corresponding option is DYLD_LIBRARY_PATH:
|
||||
On macOS, the corresponding option is DYLD_LIBRARY_PATH:
|
||||
DYLD_LIBRARY_PATH=. java -cp com.microsoft.z3.jar:. JavaExample
|
||||
|
|
|
|||
|
|
@ -11,8 +11,8 @@ find_package(Z3
|
|||
REQUIRED
|
||||
CONFIG
|
||||
# `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3.
|
||||
# This should prevent us from accidently picking up an installed
|
||||
# copy of Z3. This is here to benefit Z3's build sytem when building
|
||||
# This should prevent us from accidentally picking up an installed
|
||||
# copy of Z3. This is here to benefit Z3's build system when building
|
||||
# this project. When making your own project you probably shouldn't
|
||||
# use this option.
|
||||
NO_DEFAULT_PATH
|
||||
|
|
|
|||
|
|
@ -5,8 +5,8 @@ in the build directory.
|
|||
|
||||
This command will create the executable maxsat.
|
||||
On Windows, you can just execute it.
|
||||
On OSX and Linux, you must install z3 first using
|
||||
On macOS and Linux, you must install z3 first using
|
||||
sudo make install
|
||||
OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX) with the build directory. You need that to be able to find the Z3 shared library.
|
||||
OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (macOS) with the build directory. You need that to be able to find the Z3 shared library.
|
||||
|
||||
This directory contains a test file (ex.smt) that can be used as input for the maxsat test application.
|
||||
|
|
|
|||
|
|
@ -138,7 +138,7 @@ void assert_hard_constraints(Z3_context ctx, Z3_solver s, unsigned num_cnstrs, Z
|
|||
|
||||
/**
|
||||
\brief Assert soft constraints stored in the given array.
|
||||
This funtion will assert each soft-constraint C_i as (C_i or k_i) where k_i is a fresh boolean variable.
|
||||
This function will assert each soft-constraint C_i as (C_i or k_i) where k_i is a fresh boolean variable.
|
||||
It will also return an array containing these fresh variables.
|
||||
*/
|
||||
Z3_ast * assert_soft_constraints(Z3_context ctx, Z3_solver s, unsigned num_cnstrs, Z3_ast * cnstrs)
|
||||
|
|
@ -382,7 +382,7 @@ unsigned get_num_disabled_soft_constraints(Z3_context ctx, Z3_model m, unsigned
|
|||
Z3_ast t = Z3_mk_true(ctx);
|
||||
for (i = 0; i < num_soft_cnstrs; i++) {
|
||||
Z3_ast val;
|
||||
if (Z3_model_eval(ctx, m, aux_vars[i], 1, &val) == Z3_TRUE) {
|
||||
if (Z3_model_eval(ctx, m, aux_vars[i], 1, &val) == true) {
|
||||
// printf("%s", Z3_ast_to_string(ctx, aux_vars[i]));
|
||||
// printf(" -> %s\n", Z3_ast_to_string(ctx, val));
|
||||
if (Z3_is_eq_ast(ctx, val, t)) {
|
||||
|
|
@ -565,7 +565,7 @@ int fu_malik_maxsat(Z3_context ctx, Z3_solver s, unsigned num_hard_cnstrs, Z3_as
|
|||
|
||||
/**
|
||||
\brief Finds the maximal number of assumptions that can be satisfied.
|
||||
An assumption is any formula preceeded with the :assumption keyword.
|
||||
An assumption is any formula preceded with the :assumption keyword.
|
||||
"Hard" constraints can be supported by using the :formula keyword.
|
||||
|
||||
Input: file in SMT-LIB format, and MaxSAT algorithm to be used: 0 - Naive, 1 - Fu&Malik's algo.
|
||||
|
|
|
|||
|
|
@ -20,4 +20,4 @@ ocamlfind ocamlopt -o ml_example -package Z3 -linkpkg ml_example.ml
|
|||
|
||||
Note that the resulting binaries depend on the shared z3 library
|
||||
(libz3.dll/.so/.dylb), which needs to be in the PATH (Windows), LD_LIBRARY_PATH
|
||||
(Linux), or DYLD_LIBRARY_PATH (OSX).
|
||||
(Linux), or DYLD_LIBRARY_PATH (macOS).
|
||||
|
|
|
|||
|
|
@ -226,7 +226,7 @@ namespace Microsoft.SolverFoundation.Plugin.Z3
|
|||
}
|
||||
|
||||
/// <summary>
|
||||
/// Adds a MSF variable with the coresponding assertion to the Z3 variables.
|
||||
/// Adds a MSF variable with the corresponding assertion to the Z3 variables.
|
||||
/// </summary>
|
||||
/// <param name="vid">The MSF id of the variable</param>
|
||||
internal void AddVariable(int vid)
|
||||
|
|
|
|||
|
|
@ -33,14 +33,14 @@ namespace Microsoft.SolverFoundation.Plugin.Z3
|
|||
|
||||
#region Solver construction and destruction
|
||||
|
||||
/// <summary>Constructor that initializes the base clases</summary>
|
||||
/// <summary>Constructor that initializes the base classes</summary>
|
||||
public Z3MILPSolver() : base(null)
|
||||
{
|
||||
_result = LinearResult.Feasible;
|
||||
_solver = new Z3BaseSolver(this);
|
||||
}
|
||||
|
||||
/// <summary>Constructor that initializes the base clases</summary>
|
||||
/// <summary>Constructor that initializes the base classes</summary>
|
||||
public Z3MILPSolver(ISolverEnvironment context) : this() { }
|
||||
|
||||
/// <summary>
|
||||
|
|
|
|||
|
|
@ -29,13 +29,13 @@ namespace Microsoft.SolverFoundation.Plugin.Z3
|
|||
private NonlinearResult _result;
|
||||
private Z3BaseSolver _solver;
|
||||
|
||||
/// <summary>Constructor that initializes the base clases</summary>
|
||||
/// <summary>Constructor that initializes the base classes</summary>
|
||||
public Z3TermSolver() : base(null)
|
||||
{
|
||||
_solver = new Z3BaseSolver(this);
|
||||
}
|
||||
|
||||
/// <summary>Constructor that initializes the base clases</summary>
|
||||
/// <summary>Constructor that initializes the base classes</summary>
|
||||
public Z3TermSolver(ISolverEnvironment context) : this() { }
|
||||
|
||||
/// <summary>
|
||||
|
|
|
|||
50
examples/python/data/horn1.smt2
Normal file
50
examples/python/data/horn1.smt2
Normal file
|
|
@ -0,0 +1,50 @@
|
|||
(declare-rel Goal (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
|
||||
(declare-rel Invariant (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
|
||||
(declare-var A Bool)
|
||||
(declare-var B Bool)
|
||||
(declare-var C Bool)
|
||||
(declare-var D Bool)
|
||||
(declare-var E Bool)
|
||||
(declare-var F Bool)
|
||||
(declare-var G Bool)
|
||||
(declare-var H Bool)
|
||||
(declare-var I Bool)
|
||||
(declare-var J Bool)
|
||||
(declare-var K Bool)
|
||||
(declare-var L Bool)
|
||||
(declare-var M Bool)
|
||||
(declare-var N Bool)
|
||||
(declare-var O Bool)
|
||||
(declare-var P Bool)
|
||||
(declare-var Q Bool)
|
||||
(declare-var R Bool)
|
||||
(declare-var S Bool)
|
||||
(declare-var T Bool)
|
||||
(declare-var U Bool)
|
||||
(declare-var V Bool)
|
||||
(declare-var W Bool)
|
||||
(declare-var X Bool)
|
||||
(rule (=> (not (or L K J I H G F E D C B A)) (Invariant L K J I H G F E D C B A)))
|
||||
(rule (let ((a!1 (and (Invariant X W V U T S R Q P O N M)
|
||||
(=> (not (and true)) (not F))
|
||||
(=> (not (and true)) (not E))
|
||||
(=> (not (and W)) (not D))
|
||||
(=> (not (and W)) (not C))
|
||||
(=> (not (and U)) (not B))
|
||||
(=> (not (and U)) (not A))
|
||||
(= L (xor F X))
|
||||
(= K (xor E W))
|
||||
(= J (xor D V))
|
||||
(= I (xor C U))
|
||||
(= H (xor B T))
|
||||
(= G (xor A S))
|
||||
(=> D (not E))
|
||||
(=> C (not E))
|
||||
(=> B (not C))
|
||||
(=> A (not C))
|
||||
((_ at-most 5) L K J I H G))))
|
||||
(=> a!1 (Invariant L K J I H G F E D C B A))))
|
||||
(rule (=> (and (Invariant L K J I H G F E D C B A) L (not K) J (not I) H G)
|
||||
(Goal L K J I H G F E D C B A)))
|
||||
|
||||
(query Goal)
|
||||
44
examples/python/data/horn2.smt2
Normal file
44
examples/python/data/horn2.smt2
Normal file
|
|
@ -0,0 +1,44 @@
|
|||
(declare-rel Invariant (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
|
||||
(declare-rel Goal (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
|
||||
(declare-var A Bool)
|
||||
(declare-var B Bool)
|
||||
(declare-var C Bool)
|
||||
(declare-var D Bool)
|
||||
(declare-var E Bool)
|
||||
(declare-var F Bool)
|
||||
(declare-var G Bool)
|
||||
(declare-var H Bool)
|
||||
(declare-var I Bool)
|
||||
(declare-var J Bool)
|
||||
(declare-var K Bool)
|
||||
(declare-var L Bool)
|
||||
(declare-var M Bool)
|
||||
(declare-var N Bool)
|
||||
(declare-var O Bool)
|
||||
(declare-var P Bool)
|
||||
(declare-var Q Bool)
|
||||
(declare-var R Bool)
|
||||
(declare-var S Bool)
|
||||
(declare-var T Bool)
|
||||
(rule (=> (not (or J I H G F E D C B A)) (Invariant J I H G F E D C B A)))
|
||||
(rule (let ((a!1 (and (Invariant T S R Q P O N M L K)
|
||||
(=> (not (and true)) (not E))
|
||||
(=> (not (and T)) (not D))
|
||||
(=> (not (and S)) (not C))
|
||||
(=> (not (and R)) (not B))
|
||||
(=> (not (and Q)) (not A))
|
||||
(= J (xor E T))
|
||||
(= I (xor D S))
|
||||
(= H (xor C R))
|
||||
(= G (xor B Q))
|
||||
(= F (xor A P))
|
||||
(=> D (not E))
|
||||
(=> C (not D))
|
||||
(=> B (not C))
|
||||
(=> A (not B))
|
||||
((_ at-most 3) J I H G F))))
|
||||
(=> a!1 (Invariant J I H G F E D C B A))))
|
||||
(rule (=> (and (Invariant J I H G F E D C B A) (not J) (not I) (not H) (not G) F)
|
||||
(Goal J I H G F E D C B A)))
|
||||
|
||||
(query Goal)
|
||||
17
examples/python/data/horn3.smt2
Normal file
17
examples/python/data/horn3.smt2
Normal file
|
|
@ -0,0 +1,17 @@
|
|||
(declare-rel Invariant (Bool))
|
||||
(declare-rel Goal ())
|
||||
(declare-var l0 Bool)
|
||||
(declare-var l2 Bool)
|
||||
(declare-var l4 Bool)
|
||||
(declare-var l6 Bool)
|
||||
(declare-var l8 Bool)
|
||||
(declare-var l10 Bool)
|
||||
(rule (=> (not (or l4)) (Invariant l4)))
|
||||
(rule (=> (and (Invariant l4)
|
||||
(= (and (not l4) (not l2)) l6)
|
||||
(= (and l4 l2) l8)
|
||||
(= (and (not l8) (not l6)) l10)
|
||||
) (Invariant l10)))
|
||||
(rule (=> (and (Invariant l4)
|
||||
l4) Goal))
|
||||
(query Goal)
|
||||
99
examples/python/data/horn4.smt2
Normal file
99
examples/python/data/horn4.smt2
Normal file
|
|
@ -0,0 +1,99 @@
|
|||
(declare-rel Invariant (Bool Bool Bool Bool Bool Bool))
|
||||
(declare-rel Goal ())
|
||||
(declare-var l0 Bool)
|
||||
(declare-var l2 Bool)
|
||||
(declare-var l4 Bool)
|
||||
(declare-var l6 Bool)
|
||||
(declare-var l8 Bool)
|
||||
(declare-var l10 Bool)
|
||||
(declare-var l12 Bool)
|
||||
(declare-var l14 Bool)
|
||||
(declare-var l16 Bool)
|
||||
(declare-var l18 Bool)
|
||||
(declare-var l20 Bool)
|
||||
(declare-var l22 Bool)
|
||||
(declare-var l24 Bool)
|
||||
(declare-var l26 Bool)
|
||||
(declare-var l28 Bool)
|
||||
(declare-var l30 Bool)
|
||||
(declare-var l32 Bool)
|
||||
(declare-var l34 Bool)
|
||||
(declare-var l36 Bool)
|
||||
(declare-var l38 Bool)
|
||||
(declare-var l40 Bool)
|
||||
(declare-var l42 Bool)
|
||||
(declare-var l44 Bool)
|
||||
(declare-var l46 Bool)
|
||||
(declare-var l48 Bool)
|
||||
(declare-var l50 Bool)
|
||||
(declare-var l52 Bool)
|
||||
(declare-var l54 Bool)
|
||||
(declare-var l56 Bool)
|
||||
(declare-var l58 Bool)
|
||||
(declare-var l60 Bool)
|
||||
(declare-var l62 Bool)
|
||||
(declare-var l64 Bool)
|
||||
(declare-var l66 Bool)
|
||||
(declare-var l68 Bool)
|
||||
(declare-var l70 Bool)
|
||||
(declare-var l72 Bool)
|
||||
(declare-var l74 Bool)
|
||||
(declare-var l76 Bool)
|
||||
(declare-var l78 Bool)
|
||||
(declare-var l80 Bool)
|
||||
(declare-var l82 Bool)
|
||||
(declare-var l84 Bool)
|
||||
(declare-var l86 Bool)
|
||||
(rule (=> (not (or l4 l6 l8 l10 l12 l14)) (Invariant l4 l6 l8 l10 l12 l14)))
|
||||
(rule (=> (and (Invariant l4 l6 l8 l10 l12 l14)
|
||||
(= (and l6 (not l4)) l16)
|
||||
(= (and l10 (not l8)) l18)
|
||||
(= (and l18 l16) l20)
|
||||
(= (and (not l14) (not l12)) l22)
|
||||
(= (and l22 l20) l24)
|
||||
(= (and (not l24) (not l4)) l26)
|
||||
(= (and (not l6) l4) l28)
|
||||
(= (and (not l28) (not l16)) l30)
|
||||
(= (and (not l30) (not l24)) l32)
|
||||
(= (and l6 l4) l34)
|
||||
(= (and (not l34) l8) l36)
|
||||
(= (and l34 (not l8)) l38)
|
||||
(= (and (not l38) (not l36)) l40)
|
||||
(= (and (not l40) (not l24)) l42)
|
||||
(= (and l34 l8) l44)
|
||||
(= (and (not l44) l10) l46)
|
||||
(= (and l44 (not l10)) l48)
|
||||
(= (and (not l48) (not l46)) l50)
|
||||
(= (and (not l50) (not l24)) l52)
|
||||
(= (and l10 l8) l54)
|
||||
(= (and l54 l34) l56)
|
||||
(= (and (not l56) l12) l58)
|
||||
(= (and l56 (not l12)) l60)
|
||||
(= (and (not l60) (not l58)) l62)
|
||||
(= (and (not l62) (not l24)) l64)
|
||||
(= (and l56 l12) l66)
|
||||
(= (and (not l66) l14) l68)
|
||||
(= (and l66 (not l14)) l70)
|
||||
(= (and (not l70) (not l68)) l72)
|
||||
(= (and (not l72) (not l24)) l74)
|
||||
(= (and l6 l4) l76)
|
||||
(= (and (not l76) l18) l78)
|
||||
(= (and (not l78) l10) l80)
|
||||
(= (and (not l80) l22) l82)
|
||||
(= (and (not l82) (not l24)) l84)
|
||||
(= (and l84 (not l0)) l86)
|
||||
) (Invariant l26 l32 l42 l52 l64 l74)))
|
||||
(rule (=> (and (Invariant l4 l6 l8 l10 l12 l14)
|
||||
(= (and l84 (not l0)) l86)
|
||||
(= (and (not l82) (not l24)) l84)
|
||||
(= (and (not l80) l22) l82)
|
||||
(= (and (not l78) l10) l80)
|
||||
(= (and (not l76) l18) l78)
|
||||
(= (and l6 l4) l76)
|
||||
(= (and l10 (not l8)) l18)
|
||||
(= (and (not l14) (not l12)) l22)
|
||||
(= (and l22 l20) l24)
|
||||
(= (and l18 l16) l20)
|
||||
(= (and l6 (not l4)) l16)
|
||||
l86) Goal))
|
||||
(query Goal)
|
||||
21
examples/python/data/horn5.smt2
Normal file
21
examples/python/data/horn5.smt2
Normal file
|
|
@ -0,0 +1,21 @@
|
|||
(declare-rel Invariant (Bool Bool Bool Bool))
|
||||
(declare-rel Goal ())
|
||||
(declare-var l0 Bool)
|
||||
(declare-var l2 Bool)
|
||||
(declare-var l4 Bool)
|
||||
(declare-var l6 Bool)
|
||||
(declare-var l8 Bool)
|
||||
(declare-var l10 Bool)
|
||||
(declare-var l12 Bool)
|
||||
(declare-var l14 Bool)
|
||||
(declare-var l16 Bool)
|
||||
(rule (=> (not (or l4 l6 l8 l10)) (Invariant l4 l6 l8 l10)))
|
||||
(rule (=> (and (Invariant l4 l6 l8 l10)
|
||||
(= (and l6 l4) l12)
|
||||
(= (and l12 l8) l14)
|
||||
(= (and l10 (not l0)) l16)
|
||||
) (Invariant l12 l8 l0 l14)))
|
||||
(rule (=> (and (Invariant l4 l6 l8 l10)
|
||||
(= (and l10 (not l0)) l16)
|
||||
l16) Goal))
|
||||
(query Goal)
|
||||
292
examples/python/data/horn6.smt2
Normal file
292
examples/python/data/horn6.smt2
Normal file
|
|
@ -0,0 +1,292 @@
|
|||
(declare-rel Invariant (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
|
||||
(declare-rel Goal ())
|
||||
(declare-var l0 Bool)
|
||||
(declare-var l2 Bool)
|
||||
(declare-var l4 Bool)
|
||||
(declare-var l6 Bool)
|
||||
(declare-var l8 Bool)
|
||||
(declare-var l10 Bool)
|
||||
(declare-var l12 Bool)
|
||||
(declare-var l14 Bool)
|
||||
(declare-var l16 Bool)
|
||||
(declare-var l18 Bool)
|
||||
(declare-var l20 Bool)
|
||||
(declare-var l22 Bool)
|
||||
(declare-var l24 Bool)
|
||||
(declare-var l26 Bool)
|
||||
(declare-var l28 Bool)
|
||||
(declare-var l30 Bool)
|
||||
(declare-var l32 Bool)
|
||||
(declare-var l34 Bool)
|
||||
(declare-var l36 Bool)
|
||||
(declare-var l38 Bool)
|
||||
(declare-var l40 Bool)
|
||||
(declare-var l42 Bool)
|
||||
(declare-var l44 Bool)
|
||||
(declare-var l46 Bool)
|
||||
(declare-var l48 Bool)
|
||||
(declare-var l50 Bool)
|
||||
(declare-var l52 Bool)
|
||||
(declare-var l54 Bool)
|
||||
(declare-var l56 Bool)
|
||||
(declare-var l58 Bool)
|
||||
(declare-var l60 Bool)
|
||||
(declare-var l62 Bool)
|
||||
(declare-var l64 Bool)
|
||||
(declare-var l66 Bool)
|
||||
(declare-var l68 Bool)
|
||||
(declare-var l70 Bool)
|
||||
(declare-var l72 Bool)
|
||||
(declare-var l74 Bool)
|
||||
(declare-var l76 Bool)
|
||||
(declare-var l78 Bool)
|
||||
(declare-var l80 Bool)
|
||||
(declare-var l82 Bool)
|
||||
(declare-var l84 Bool)
|
||||
(declare-var l86 Bool)
|
||||
(declare-var l88 Bool)
|
||||
(declare-var l90 Bool)
|
||||
(declare-var l92 Bool)
|
||||
(declare-var l94 Bool)
|
||||
(declare-var l96 Bool)
|
||||
(declare-var l98 Bool)
|
||||
(declare-var l100 Bool)
|
||||
(declare-var l102 Bool)
|
||||
(declare-var l104 Bool)
|
||||
(declare-var l106 Bool)
|
||||
(declare-var l108 Bool)
|
||||
(declare-var l110 Bool)
|
||||
(declare-var l112 Bool)
|
||||
(declare-var l114 Bool)
|
||||
(declare-var l116 Bool)
|
||||
(declare-var l118 Bool)
|
||||
(declare-var l120 Bool)
|
||||
(declare-var l122 Bool)
|
||||
(declare-var l124 Bool)
|
||||
(declare-var l126 Bool)
|
||||
(declare-var l128 Bool)
|
||||
(declare-var l130 Bool)
|
||||
(declare-var l132 Bool)
|
||||
(declare-var l134 Bool)
|
||||
(declare-var l136 Bool)
|
||||
(declare-var l138 Bool)
|
||||
(declare-var l140 Bool)
|
||||
(declare-var l142 Bool)
|
||||
(declare-var l144 Bool)
|
||||
(declare-var l146 Bool)
|
||||
(declare-var l148 Bool)
|
||||
(declare-var l150 Bool)
|
||||
(declare-var l152 Bool)
|
||||
(declare-var l154 Bool)
|
||||
(declare-var l156 Bool)
|
||||
(declare-var l158 Bool)
|
||||
(declare-var l160 Bool)
|
||||
(declare-var l162 Bool)
|
||||
(declare-var l164 Bool)
|
||||
(declare-var l166 Bool)
|
||||
(declare-var l168 Bool)
|
||||
(declare-var l170 Bool)
|
||||
(declare-var l172 Bool)
|
||||
(declare-var l174 Bool)
|
||||
(declare-var l176 Bool)
|
||||
(declare-var l178 Bool)
|
||||
(declare-var l180 Bool)
|
||||
(declare-var l182 Bool)
|
||||
(declare-var l184 Bool)
|
||||
(declare-var l186 Bool)
|
||||
(declare-var l188 Bool)
|
||||
(declare-var l190 Bool)
|
||||
(declare-var l192 Bool)
|
||||
(declare-var l194 Bool)
|
||||
(declare-var l196 Bool)
|
||||
(declare-var l198 Bool)
|
||||
(declare-var l200 Bool)
|
||||
(declare-var l202 Bool)
|
||||
(declare-var l204 Bool)
|
||||
(declare-var l206 Bool)
|
||||
(declare-var l208 Bool)
|
||||
(declare-var l210 Bool)
|
||||
(declare-var l212 Bool)
|
||||
(declare-var l214 Bool)
|
||||
(declare-var l216 Bool)
|
||||
(declare-var l218 Bool)
|
||||
(declare-var l220 Bool)
|
||||
(declare-var l222 Bool)
|
||||
(declare-var l224 Bool)
|
||||
(declare-var l226 Bool)
|
||||
(declare-var l228 Bool)
|
||||
(declare-var l230 Bool)
|
||||
(declare-var l232 Bool)
|
||||
(declare-var l234 Bool)
|
||||
(declare-var l236 Bool)
|
||||
(declare-var l238 Bool)
|
||||
(declare-var l240 Bool)
|
||||
(declare-var l242 Bool)
|
||||
(declare-var l244 Bool)
|
||||
(declare-var l246 Bool)
|
||||
(declare-var l248 Bool)
|
||||
(declare-var l250 Bool)
|
||||
(declare-var l252 Bool)
|
||||
(declare-var l254 Bool)
|
||||
(declare-var l256 Bool)
|
||||
(declare-var l258 Bool)
|
||||
(declare-var l260 Bool)
|
||||
(declare-var l262 Bool)
|
||||
(declare-var l264 Bool)
|
||||
(declare-var l266 Bool)
|
||||
(declare-var l268 Bool)
|
||||
(declare-var l270 Bool)
|
||||
(declare-var l272 Bool)
|
||||
(declare-var l274 Bool)
|
||||
(declare-var l276 Bool)
|
||||
(declare-var l278 Bool)
|
||||
(declare-var l280 Bool)
|
||||
(declare-var l282 Bool)
|
||||
(declare-var l284 Bool)
|
||||
(declare-var l286 Bool)
|
||||
(declare-var l288 Bool)
|
||||
(declare-var l290 Bool)
|
||||
(declare-var l292 Bool)
|
||||
(declare-var l294 Bool)
|
||||
(declare-var l296 Bool)
|
||||
(declare-var l298 Bool)
|
||||
(declare-var l300 Bool)
|
||||
(declare-var l302 Bool)
|
||||
(declare-var l304 Bool)
|
||||
(declare-var l306 Bool)
|
||||
(declare-var l308 Bool)
|
||||
(declare-var l310 Bool)
|
||||
(declare-var l312 Bool)
|
||||
(declare-var l314 Bool)
|
||||
(declare-var l316 Bool)
|
||||
(rule (=> (not (or l8 l10 l12 l14 l16 l18 l20 l22 l24 l26 l28 l30 l32 l34 l36 l38 l40 l42 l44 l46 l48 l50 l52 l54 l56 l58 l60 l62 l64 l66 l68 l70 l72 l74)) (Invariant l8 l10 l12 l14 l16 l18 l20 l22 l24 l26 l28 l30 l32 l34 l36 l38 l40 l42 l44 l46 l48 l50 l52 l54 l56 l58 l60 l62 l64 l66 l68 l70 l72 l74)))
|
||||
(rule (=> (and (Invariant l8 l10 l12 l14 l16 l18 l20 l22 l24 l26 l28 l30 l32 l34 l36 l38 l40 l42 l44 l46 l48 l50 l52 l54 l56 l58 l60 l62 l64 l66 l68 l70 l72 l74)
|
||||
(= (and (not l20) (not l14)) l76)
|
||||
(= (and (not l76) l8) l78)
|
||||
(= (and l20 l14) l80)
|
||||
(= (and (not l80) (not l78)) l82)
|
||||
(= (and (not l28) l8) l84)
|
||||
(= (and (not l84) l10) l86)
|
||||
(= (and l18 l12) l88)
|
||||
(= (and l88 l38) l90)
|
||||
(= (and (not l24) (not l8)) l92)
|
||||
(= (and l92 (not l26)) l94)
|
||||
(= (and l94 l28) l96)
|
||||
(= (and l96 (not l90)) l98)
|
||||
(= (and (not l98) (not l86)) l100)
|
||||
(= (and l38 l18) l102)
|
||||
(= (and l102 l12) l104)
|
||||
(= (and (not l104) (not l26)) l106)
|
||||
(= (and l24 (not l16)) l108)
|
||||
(= (and l108 (not l32)) l110)
|
||||
(= (and l110 l106) l112)
|
||||
(= (and (not l32) l14) l114)
|
||||
(= (and (not l114) (not l112)) l116)
|
||||
(= (and (not l114) l16) l118)
|
||||
(= (and l32 (not l14)) l120)
|
||||
(= (and l120 l106) l122)
|
||||
(= (and l122 l24) l124)
|
||||
(= (and (not l124) (not l118)) l126)
|
||||
(= (and l26 (not l22)) l128)
|
||||
(= (and l128 (not l36)) l130)
|
||||
(= (and (not l36) l20) l132)
|
||||
(= (and l130 (not l90)) l134)
|
||||
(= (and (not l134) (not l132)) l136)
|
||||
(= (and (not l132) l22) l138)
|
||||
(= (and l26 (not l20)) l140)
|
||||
(= (and l140 l36) l142)
|
||||
(= (and l142 (not l90)) l144)
|
||||
(= (and (not l144) (not l138)) l146)
|
||||
(= (and (not l106) l24) l148)
|
||||
(= (and l106 (not l24)) l150)
|
||||
(= (and (not l150) (not l148)) l152)
|
||||
(= (and (not l90) l24) l154)
|
||||
(= (and l90 l26) l156)
|
||||
(= (and (not l156) (not l154)) l158)
|
||||
(= (and (not l30) l2) l160)
|
||||
(= (and l28 (not l2)) l162)
|
||||
(= (and (not l162) (not l160)) l164)
|
||||
(= (and l28 l2) l166)
|
||||
(= (and (not l166) l30) l168)
|
||||
(= (and (not l30) l28) l170)
|
||||
(= (and l170 l8) l172)
|
||||
(= (and (not l172) (not l168)) l174)
|
||||
(= (and (not l34) l4) l176)
|
||||
(= (and l32 (not l4)) l178)
|
||||
(= (and (not l178) (not l176)) l180)
|
||||
(= (and l32 l4) l182)
|
||||
(= (and (not l182) l34) l184)
|
||||
(= (and (not l34) l32) l186)
|
||||
(= (and l186 l14) l188)
|
||||
(= (and (not l188) (not l184)) l190)
|
||||
(= (and (not l40) l6) l192)
|
||||
(= (and l36 (not l6)) l194)
|
||||
(= (and (not l194) (not l192)) l196)
|
||||
(= (and (not l24) (not l10)) l198)
|
||||
(= (and l198 (not l26)) l200)
|
||||
(= (and l200 (not l28)) l202)
|
||||
(= (and l202 (not l90)) l204)
|
||||
(= (and (not l204) (not l84)) l206)
|
||||
(= (and l36 l6) l208)
|
||||
(= (and (not l208) l40) l210)
|
||||
(= (and (not l40) l36) l212)
|
||||
(= (and l212 l20) l214)
|
||||
(= (and (not l214) (not l210)) l216)
|
||||
(= (and l62 l44) l218)
|
||||
(= (and l52 l46) l220)
|
||||
(= (and l220 l72) l222)
|
||||
(= (and (not l60) (not l58)) l224)
|
||||
(= (and l224 l62) l226)
|
||||
(= (and l226 (not l222)) l228)
|
||||
(= (and (not l228) (not l218)) l230)
|
||||
(= (and (not l222) (not l60)) l232)
|
||||
(= (and (not l66) l58) l234)
|
||||
(= (and (not l66) l48) l236)
|
||||
(= (and l234 l232) l238)
|
||||
(= (and (not l238) (not l236)) l240)
|
||||
(= (and l66 l50) l242)
|
||||
(= (and l66 (not l48)) l244)
|
||||
(= (and l244 l232) l246)
|
||||
(= (and l246 l58) l248)
|
||||
(= (and (not l248) (not l242)) l250)
|
||||
(= (and (not l70) l60) l252)
|
||||
(= (and (not l70) l54) l254)
|
||||
(= (and l252 (not l222)) l256)
|
||||
(= (and (not l256) (not l254)) l258)
|
||||
(= (and l70 l56) l260)
|
||||
(= (and l70 l60) l262)
|
||||
(= (and l262 (not l222)) l264)
|
||||
(= (and (not l264) (not l260)) l266)
|
||||
(= (and (not l232) l58) l268)
|
||||
(= (and l232 (not l58)) l270)
|
||||
(= (and (not l270) (not l268)) l272)
|
||||
(= (and l222 l60) l274)
|
||||
(= (and (not l222) l58) l276)
|
||||
(= (and (not l276) (not l274)) l278)
|
||||
(= (and l62 (not l2)) l280)
|
||||
(= (and (not l64) l2) l282)
|
||||
(= (and (not l282) (not l280)) l284)
|
||||
(= (and l62 l42) l286)
|
||||
(= (and l286 (not l284)) l288)
|
||||
(= (and l66 (not l4)) l290)
|
||||
(= (and (not l68) l4) l292)
|
||||
(= (and (not l292) (not l290)) l294)
|
||||
(= (and (not l244) l66) l296)
|
||||
(= (and l296 (not l294)) l298)
|
||||
(= (and l70 (not l6)) l300)
|
||||
(= (and (not l74) l6) l302)
|
||||
(= (and (not l302) (not l300)) l304)
|
||||
(= (and l224 (not l62)) l306)
|
||||
(= (and (not l62) l42) l308)
|
||||
(= (and l306 (not l222)) l310)
|
||||
(= (and (not l310) (not l308)) l312)
|
||||
(= (and l70 l54) l314)
|
||||
(= (and l314 (not l304)) l316)
|
||||
) (Invariant l86 l100 l116 l118 l126 l136 l138 l146 l152 l158 l164 l174 l180 l190 l196 l206 l216 l218 l230 l240 l242 l250 l258 l260 l266 l272 l278 l284 l288 l294 l298 l304 l312 l316)))
|
||||
(rule (=> (and (Invariant l8 l10 l12 l14 l16 l18 l20 l22 l24 l26 l28 l30 l32 l34 l36 l38 l40 l42 l44 l46 l48 l50 l52 l54 l56 l58 l60 l62 l64 l66 l68 l70 l72 l74)
|
||||
(= (and (not l80) (not l78)) l82)
|
||||
(= (and l20 l14) l80)
|
||||
(= (and (not l76) l8) l78)
|
||||
(= (and (not l20) (not l14)) l76)
|
||||
(not l82)) Goal))
|
||||
(query Goal)
|
||||
|
|
@ -20,7 +20,7 @@
|
|||
# export PYTHONPATH=MYZ3/bin/python
|
||||
# python example.py
|
||||
|
||||
# Running this example on OSX:
|
||||
# Running this example on macOS:
|
||||
# export DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH:MYZ3/bin
|
||||
# export PYTHONPATH=MYZ3/bin/python
|
||||
# python example.py
|
||||
|
|
|
|||
469
examples/python/mini_ic3.py
Normal file
469
examples/python/mini_ic3.py
Normal file
|
|
@ -0,0 +1,469 @@
|
|||
from z3 import *
|
||||
import heapq
|
||||
|
||||
|
||||
# Simplistic (and fragile) converter from
|
||||
# a class of Horn clauses corresponding to
|
||||
# a transition system into a transition system
|
||||
# representation as <init, trans, goal>
|
||||
# It assumes it is given three Horn clauses
|
||||
# of the form:
|
||||
# init(x) => Invariant(x)
|
||||
# Invariant(x) and trans(x,x') => Invariant(x')
|
||||
# Invariant(x) and goal(x) => Goal(x)
|
||||
# where Invariant and Goal are uninterpreted predicates
|
||||
|
||||
class Horn2Transitions:
|
||||
def __init__(self):
|
||||
self.trans = True
|
||||
self.init = True
|
||||
self.inputs = []
|
||||
self.goal = True
|
||||
self.index = 0
|
||||
|
||||
def parse(self, file):
|
||||
fp = Fixedpoint()
|
||||
goals = fp.parse_file(file)
|
||||
for r in fp.get_rules():
|
||||
if not is_quantifier(r):
|
||||
continue
|
||||
b = r.body()
|
||||
if not is_implies(b):
|
||||
continue
|
||||
f = b.arg(0)
|
||||
g = b.arg(1)
|
||||
if self.is_goal(f, g):
|
||||
continue
|
||||
if self.is_transition(f, g):
|
||||
continue
|
||||
if self.is_init(f, g):
|
||||
continue
|
||||
|
||||
def is_pred(self, p, name):
|
||||
return is_app(p) and p.decl().name() == name
|
||||
|
||||
def is_goal(self, body, head):
|
||||
if not self.is_pred(head, "Goal"):
|
||||
return False
|
||||
pred, inv = self.is_body(body)
|
||||
if pred is None:
|
||||
return False
|
||||
self.goal = self.subst_vars("x", inv, pred)
|
||||
self.goal = self.subst_vars("i", self.goal, self.goal)
|
||||
self.inputs += self.vars
|
||||
self.inputs = list(set(self.inputs))
|
||||
return True
|
||||
|
||||
def is_body(self, body):
|
||||
if not is_and(body):
|
||||
return None, None
|
||||
fmls = [f for f in body.children() if self.is_inv(f) is None]
|
||||
inv = None
|
||||
for f in body.children():
|
||||
if self.is_inv(f) is not None:
|
||||
inv = f;
|
||||
break
|
||||
return And(fmls), inv
|
||||
|
||||
def is_inv(self, f):
|
||||
if self.is_pred(f, "Invariant"):
|
||||
return f
|
||||
return None
|
||||
|
||||
def is_transition(self, body, head):
|
||||
pred, inv0 = self.is_body(body)
|
||||
if pred is None:
|
||||
return False
|
||||
inv1 = self.is_inv(head)
|
||||
if inv1 is None:
|
||||
return False
|
||||
pred = self.subst_vars("x", inv0, pred)
|
||||
self.xs = self.vars
|
||||
pred = self.subst_vars("xn", inv1, pred)
|
||||
self.xns = self.vars
|
||||
pred = self.subst_vars("i", pred, pred)
|
||||
self.inputs += self.vars
|
||||
self.inputs = list(set(self.inputs))
|
||||
self.trans = pred
|
||||
return True
|
||||
|
||||
def is_init(self, body, head):
|
||||
for f in body.children():
|
||||
if self.is_inv(f) is not None:
|
||||
return False
|
||||
inv = self.is_inv(head)
|
||||
if inv is None:
|
||||
return False
|
||||
self.init = self.subst_vars("x", inv, body)
|
||||
return True
|
||||
|
||||
def subst_vars(self, prefix, inv, fml):
|
||||
subst = self.mk_subst(prefix, inv)
|
||||
self.vars = [ v for (k,v) in subst ]
|
||||
return substitute(fml, subst)
|
||||
|
||||
def mk_subst(self, prefix, inv):
|
||||
self.index = 0
|
||||
if self.is_inv(inv) is not None:
|
||||
return [(f, self.mk_bool(prefix)) for f in inv.children()]
|
||||
else:
|
||||
vars = self.get_vars(inv)
|
||||
return [(f, self.mk_bool(prefix)) for f in vars]
|
||||
|
||||
def mk_bool(self, prefix):
|
||||
self.index += 1
|
||||
return Bool("%s%d" % (prefix, self.index))
|
||||
|
||||
def get_vars(self, f, rs=[]):
|
||||
if is_var(f):
|
||||
return z3util.vset(rs + [f], str)
|
||||
else:
|
||||
for f_ in f.children():
|
||||
rs = self.get_vars(f_, rs)
|
||||
return z3util.vset(rs, str)
|
||||
|
||||
# Produce a finite domain solver.
|
||||
# The theory QF_FD covers bit-vector formulas
|
||||
# and pseudo-Boolean constraints.
|
||||
# By default cardinality and pseudo-Boolean
|
||||
# constraints are converted to clauses. To override
|
||||
# this default for cardinality constraints
|
||||
# we set sat.cardinality.solver to True
|
||||
|
||||
def fd_solver():
|
||||
s = SolverFor("QF_FD")
|
||||
s.set("sat.cardinality.solver", True)
|
||||
return s
|
||||
|
||||
|
||||
# negate, avoid double negation
|
||||
def negate(f):
|
||||
if is_not(f):
|
||||
return f.arg(0)
|
||||
else:
|
||||
return Not(f)
|
||||
|
||||
def cube2clause(cube):
|
||||
return Or([negate(f) for f in cube])
|
||||
|
||||
class State:
|
||||
def __init__(self, s):
|
||||
self.R = set([])
|
||||
self.solver = s
|
||||
|
||||
def add(self, clause):
|
||||
if clause not in self.R:
|
||||
self.R |= { clause }
|
||||
self.solver.add(clause)
|
||||
|
||||
class Goal:
|
||||
def __init__(self, cube, parent, level):
|
||||
self.level = level
|
||||
self.cube = cube
|
||||
self.parent = parent
|
||||
|
||||
def is_seq(f):
|
||||
return isinstance(f, list) or isinstance(f, tuple) or isinstance(f, AstVector)
|
||||
|
||||
# Check if the initial state is bad
|
||||
def check_disjoint(a, b):
|
||||
s = fd_solver()
|
||||
s.add(a)
|
||||
s.add(b)
|
||||
return unsat == s.check()
|
||||
|
||||
|
||||
# Remove clauses that are subsumed
|
||||
def prune(R):
|
||||
removed = set([])
|
||||
s = fd_solver()
|
||||
for f1 in R:
|
||||
s.push()
|
||||
for f2 in R:
|
||||
if f2 not in removed:
|
||||
s.add(Not(f2) if f1.eq(f2) else f2)
|
||||
if s.check() == unsat:
|
||||
removed |= { f1 }
|
||||
s.pop()
|
||||
return R - removed
|
||||
|
||||
class MiniIC3:
|
||||
def __init__(self, init, trans, goal, x0, inputs, xn):
|
||||
self.x0 = x0
|
||||
self.inputs = inputs
|
||||
self.xn = xn
|
||||
self.init = init
|
||||
self.bad = goal
|
||||
self.trans = trans
|
||||
self.min_cube_solver = fd_solver()
|
||||
self.min_cube_solver.add(Not(trans))
|
||||
self.goals = []
|
||||
s = State(fd_solver())
|
||||
s.add(init)
|
||||
s.solver.add(trans)
|
||||
self.states = [s]
|
||||
self.s_bad = fd_solver()
|
||||
self.s_good = fd_solver()
|
||||
self.s_bad.add(self.bad)
|
||||
self.s_good.add(Not(self.bad))
|
||||
|
||||
def next(self, f):
|
||||
if is_seq(f):
|
||||
return [self.next(f1) for f1 in f]
|
||||
return substitute(f, zip(self.x0, self.xn))
|
||||
|
||||
def prev(self, f):
|
||||
if is_seq(f):
|
||||
return [self.prev(f1) for f1 in f]
|
||||
return substitute(f, zip(self.xn, self.x0))
|
||||
|
||||
def add_solver(self):
|
||||
s = fd_solver()
|
||||
s.add(self.trans)
|
||||
self.states += [State(s)]
|
||||
|
||||
def R(self, i):
|
||||
return And(self.states[i].R)
|
||||
|
||||
# Check if there are two states next to each other that have the same clauses.
|
||||
def is_valid(self):
|
||||
i = 1
|
||||
while i + 1 < len(self.states):
|
||||
if not (self.states[i].R - self.states[i+1].R):
|
||||
return And(prune(self.states[i].R))
|
||||
i += 1
|
||||
return None
|
||||
|
||||
def value2literal(self, m, x):
|
||||
value = m.eval(x)
|
||||
if is_true(value):
|
||||
return x
|
||||
if is_false(value):
|
||||
return Not(x)
|
||||
return None
|
||||
|
||||
def values2literals(self, m, xs):
|
||||
p = [self.value2literal(m, x) for x in xs]
|
||||
return [x for x in p if x is not None]
|
||||
|
||||
def project0(self, m):
|
||||
return self.values2literals(m, self.x0)
|
||||
|
||||
def projectI(self, m):
|
||||
return self.values2literals(m, self.inputs)
|
||||
|
||||
def projectN(self, m):
|
||||
return self.values2literals(m, self.xn)
|
||||
|
||||
# Determine if there is a cube for the current state
|
||||
# that is potentially reachable.
|
||||
def unfold(self):
|
||||
core = []
|
||||
self.s_bad.push()
|
||||
R = self.R(len(self.states)-1)
|
||||
self.s_bad.add(R)
|
||||
is_sat = self.s_bad.check()
|
||||
if is_sat == sat:
|
||||
m = self.s_bad.model()
|
||||
cube = self.project0(m)
|
||||
props = cube + self.projectI(m)
|
||||
self.s_good.push()
|
||||
self.s_good.add(R)
|
||||
is_sat2 = self.s_good.check(props)
|
||||
assert is_sat2 == unsat
|
||||
core = self.s_good.unsat_core()
|
||||
core = [c for c in core if c in set(cube)]
|
||||
self.s_good.pop()
|
||||
self.s_bad.pop()
|
||||
return is_sat, core
|
||||
|
||||
# Block a cube by asserting the clause corresponding to its negation
|
||||
def block_cube(self, i, cube):
|
||||
self.assert_clause(i, cube2clause(cube))
|
||||
|
||||
# Add a clause to levels 0 until i
|
||||
def assert_clause(self, i, clause):
|
||||
for j in range(i + 1):
|
||||
self.states[j].add(clause)
|
||||
|
||||
# minimize cube that is core of Dual solver.
|
||||
# this assumes that props & cube => Trans
|
||||
def minimize_cube(self, cube, inputs, lits):
|
||||
is_sat = self.min_cube_solver.check(lits + [c for c in cube] + [i for i in inputs])
|
||||
assert is_sat == unsat
|
||||
core = self.min_cube_solver.unsat_core()
|
||||
assert core
|
||||
return [c for c in core if c in set(cube)]
|
||||
|
||||
# push a goal on a heap
|
||||
def push_heap(self, goal):
|
||||
heapq.heappush(self.goals, (goal.level, goal))
|
||||
|
||||
# A state s0 and level f0 such that
|
||||
# not(s0) is f0-1 inductive
|
||||
def ic3_blocked(self, s0, f0):
|
||||
self.push_heap(Goal(self.next(s0), None, f0))
|
||||
while self.goals:
|
||||
f, g = heapq.heappop(self.goals)
|
||||
sys.stdout.write("%d." % f)
|
||||
sys.stdout.flush()
|
||||
# Not(g.cube) is f-1 invariant
|
||||
if f == 0:
|
||||
print("")
|
||||
return g
|
||||
cube, f, is_sat = self.is_inductive(f, g.cube)
|
||||
if is_sat == unsat:
|
||||
self.block_cube(f, self.prev(cube))
|
||||
if f < f0:
|
||||
self.push_heap(Goal(g.cube, g.parent, f + 1))
|
||||
elif is_sat == sat:
|
||||
self.push_heap(Goal(cube, g, f - 1))
|
||||
self.push_heap(g)
|
||||
else:
|
||||
return is_sat
|
||||
print("")
|
||||
return None
|
||||
|
||||
# Rudimentary generalization:
|
||||
# If the cube is already unsat with respect to transition relation
|
||||
# extract a core (not necessarily minimal)
|
||||
# otherwise, just return the cube.
|
||||
def generalize(self, cube, f):
|
||||
s = self.states[f - 1].solver
|
||||
if unsat == s.check(cube):
|
||||
core = s.unsat_core()
|
||||
if not check_disjoint(self.init, self.prev(And(core))):
|
||||
return core, f
|
||||
return cube, f
|
||||
|
||||
# Check if the negation of cube is inductive at level f
|
||||
def is_inductive(self, f, cube):
|
||||
s = self.states[f - 1].solver
|
||||
s.push()
|
||||
s.add(self.prev(Not(And(cube))))
|
||||
is_sat = s.check(cube)
|
||||
if is_sat == sat:
|
||||
m = s.model()
|
||||
s.pop()
|
||||
if is_sat == sat:
|
||||
cube = self.next(self.minimize_cube(self.project0(m), self.projectI(m), self.projectN(m)))
|
||||
elif is_sat == unsat:
|
||||
cube, f = self.generalize(cube, f)
|
||||
return cube, f, is_sat
|
||||
|
||||
def run(self):
|
||||
if not check_disjoint(self.init, self.bad):
|
||||
return "goal is reached in initial state"
|
||||
level = 0
|
||||
while True:
|
||||
inv = self.is_valid()
|
||||
if inv is not None:
|
||||
return inv
|
||||
is_sat, cube = self.unfold()
|
||||
if is_sat == unsat:
|
||||
level += 1
|
||||
print("Unfold %d" % level)
|
||||
sys.stdout.flush()
|
||||
self.add_solver()
|
||||
elif is_sat == sat:
|
||||
cex = self.ic3_blocked(cube, level)
|
||||
if cex is not None:
|
||||
return cex
|
||||
else:
|
||||
return is_sat
|
||||
|
||||
def test(file):
|
||||
h2t = Horn2Transitions()
|
||||
h2t.parse(file)
|
||||
mp = MiniIC3(h2t.init, h2t.trans, h2t.goal, h2t.xs, h2t.inputs, h2t.xns)
|
||||
result = mp.run()
|
||||
if isinstance(result, Goal):
|
||||
g = result
|
||||
print("Trace")
|
||||
while g:
|
||||
print(g.level, g.cube)
|
||||
g = g.parent
|
||||
return
|
||||
if isinstance(result, ExprRef):
|
||||
print("Invariant:\n%s " % result)
|
||||
return
|
||||
print(result)
|
||||
|
||||
test("data/horn1.smt2")
|
||||
test("data/horn2.smt2")
|
||||
test("data/horn3.smt2")
|
||||
test("data/horn4.smt2")
|
||||
test("data/horn5.smt2")
|
||||
test("data/horn6.smt2")
|
||||
|
||||
|
||||
|
||||
"""
|
||||
# TBD: Quip variant of IC3
|
||||
|
||||
must = True
|
||||
may = False
|
||||
|
||||
class QGoal:
|
||||
def __init__(self, cube, parent, level, must):
|
||||
self.level = level
|
||||
self.cube = cube
|
||||
self.parent = parent
|
||||
self.must = must
|
||||
|
||||
class Quip(MiniIC3):
|
||||
|
||||
# prev & tras -> r', such that r' intersects with cube
|
||||
def add_reachable(self, prev, cube):
|
||||
s = fd_solver()
|
||||
s.add(self.trans)
|
||||
s.add(prev)
|
||||
s.add(Or(cube))
|
||||
is_sat = s.check()
|
||||
assert is_sat == sat
|
||||
m = s.model();
|
||||
result = self.values2literals(m, cube)
|
||||
assert result
|
||||
self.reachable.add(result)
|
||||
|
||||
# A state s0 and level f0 such that
|
||||
# not(s0) is f0-1 inductive
|
||||
def quip_blocked(self, s0, f0):
|
||||
self.push_heap(QGoal(self.next(s0), None, f0, must))
|
||||
while self.goals:
|
||||
f, g = heapq.heappop(self.goals)
|
||||
sys.stdout.write("%d." % f)
|
||||
sys.stdout.flush()
|
||||
if f == 0:
|
||||
if g.must:
|
||||
print("")
|
||||
return g
|
||||
self.add_reachable(self.init, p.parent.cube)
|
||||
continue
|
||||
|
||||
# TBD
|
||||
return None
|
||||
|
||||
|
||||
def run(self):
|
||||
if not check_disjoint(self.init, self.bad):
|
||||
return "goal is reached in initial state"
|
||||
level = 0
|
||||
while True:
|
||||
inv = self.is_valid()
|
||||
if inv is not None:
|
||||
return inv
|
||||
is_sat, cube = self.unfold()
|
||||
if is_sat == unsat:
|
||||
level += 1
|
||||
print("Unfold %d" % level)
|
||||
sys.stdout.flush()
|
||||
self.add_solver()
|
||||
elif is_sat == sat:
|
||||
cex = self.quipie_blocked(cube, level)
|
||||
if cex is not None:
|
||||
return cex
|
||||
else:
|
||||
return is_sat
|
||||
|
||||
"""
|
||||
149
examples/python/rc2.py
Normal file
149
examples/python/rc2.py
Normal file
|
|
@ -0,0 +1,149 @@
|
|||
# RC2 algorithm
|
||||
# basic version with some optimizations
|
||||
# - process soft constraints in order of highest values first.
|
||||
# - extract multiple cores, not just one
|
||||
# - use built-in cardinality constraints, cheap core minimization.
|
||||
#
|
||||
# See also https://github.com/pysathq/pysat and papers in CP 2014, JSAT 2015.
|
||||
|
||||
from z3 import *
|
||||
|
||||
def tt(s, f):
|
||||
return is_true(s.model().eval(f))
|
||||
|
||||
def add(Ws, f, w):
|
||||
Ws[f] = w + (Ws[f] if f in Ws else 0)
|
||||
|
||||
def sub(Ws, f, w):
|
||||
w1 = Ws[f]
|
||||
if w1 > w:
|
||||
Ws[f] = w1 - w
|
||||
else:
|
||||
del(Ws[f])
|
||||
|
||||
class RC2:
|
||||
|
||||
def __init__(self, s):
|
||||
self.bounds = {}
|
||||
self.names = {}
|
||||
self.solver = s
|
||||
self.solver.set("sat.cardinality.solver", True)
|
||||
self.solver.set("sat.core.minimize", True)
|
||||
self.solver.set("sat.core.minimize_partial", True)
|
||||
|
||||
def at_most(self, S, k):
|
||||
fml = simplify(AtMost(S + [k]))
|
||||
if fml in self.names:
|
||||
return self.names[fml]
|
||||
name = Bool("%s" % fml)
|
||||
self.solver.add(Implies(name, fml))
|
||||
self.bounds[name] = (S, k)
|
||||
sel.names[fml] = name
|
||||
return name
|
||||
|
||||
def print_cost(self):
|
||||
print("cost [", self.min_cost, ":", self.max_cost, "]")
|
||||
|
||||
def update_max_cost(self):
|
||||
self.max_cost = min(self.max_cost, self.get_cost())
|
||||
self.print_cost()
|
||||
|
||||
# sort W, and incrementally add elements of W
|
||||
# in sorted order to prefer cores with high weight.
|
||||
def check(self, Ws):
|
||||
ws = sorted(list(Ws), lambda f,w : -w)
|
||||
# print(ws)
|
||||
i = 0
|
||||
while i < len(ws):
|
||||
j = i
|
||||
# increment j until making 5% progress or exhausting equal weight entries
|
||||
while (j < len(ws) and ws[j][1] == ws[i][1]) or (i > 0 and (i - j)*20 < len(ws)):
|
||||
j += 1
|
||||
i = j
|
||||
r = self.solver.check(ws[j][0] for j in range(i))
|
||||
if r == sat:
|
||||
self.update_max_cost()
|
||||
else:
|
||||
return r
|
||||
return sat
|
||||
|
||||
def get_cost(self):
|
||||
return sum(self.Ws0[c] for c in self.Ws0 if not tt(self.solver, c))
|
||||
|
||||
# Retrieve independendent cores from Ws
|
||||
def get_cores(self, Ws):
|
||||
cores = []
|
||||
while unsat == self.check(Ws):
|
||||
core = list(self.solver.unsat_core())
|
||||
print (self.solver.statistics())
|
||||
if not core:
|
||||
return unsat
|
||||
w = min([Ws[c] for c in core])
|
||||
for f in core:
|
||||
sub(Ws, f, w)
|
||||
cores += [(core, w)]
|
||||
self.update_max_cost()
|
||||
return cores
|
||||
|
||||
# Add new soft constraints to replace core
|
||||
# with weight w. Allow to weaken at most
|
||||
# one element of core. Elements that are
|
||||
# cardinality constraints are weakened by
|
||||
# increasing their bounds. Non-cardinality
|
||||
# constraints are weakened to "true". They
|
||||
# correspond to the constraint Not(s) <= 0,
|
||||
# so weakening produces Not(s) <= 1, which
|
||||
# is a tautology.
|
||||
def update_bounds(self, Ws, core, w):
|
||||
for f in core:
|
||||
if f in self.bounds:
|
||||
S, k = self.bounds[f]
|
||||
if k + 1 < len(S):
|
||||
add(Ws, self.at_most(S, k + 1), w)
|
||||
add(Ws, self.at_most([mk_not(f) for f in core], 1), w)
|
||||
|
||||
# Ws are weighted soft constraints
|
||||
# Whenever there is an unsatisfiable core over ws
|
||||
# increase the limit of each soft constraint from a bound
|
||||
# and create a soft constraint that limits the number of
|
||||
# increased bounds to be at most one.
|
||||
def maxsat(self, Ws):
|
||||
self.min_cost = 0
|
||||
self.max_cost = sum(Ws[c] for c in Ws)
|
||||
self.Ws0 = Ws.copy()
|
||||
while True:
|
||||
cores = self.get_cores(Ws)
|
||||
if not cores:
|
||||
break
|
||||
if cores == unsat:
|
||||
return unsat
|
||||
for (core, w) in cores:
|
||||
self.min_cost += w
|
||||
self.print_cost()
|
||||
self.update_bounds(Ws, core, w)
|
||||
return sel.min_cost, { f for f in self.Ws0 if not tt(self.solver, f) }
|
||||
|
||||
def from_file(self, file):
|
||||
opt = Optimize()
|
||||
opt.from_file(file)
|
||||
self.solver.add(opt.assertions())
|
||||
obj = opt.objectives()[0]
|
||||
Ws = {}
|
||||
for f in obj.children():
|
||||
assert(f.arg(1).as_long() == 0)
|
||||
add(Ws, f.arg(0), f.arg(2).as_long())
|
||||
return self.maxsat(Ws)
|
||||
|
||||
def main(file):
|
||||
s = SolverFor("QF_FD")
|
||||
rc2 = RC2(s)
|
||||
set_param(verbose=0)
|
||||
cost, falses = rc2.from_file(file)
|
||||
print(cost)
|
||||
print(s.statistics())
|
||||
|
||||
if len(sys.argv) > 1:
|
||||
main(sys.argv[1])
|
||||
|
||||
# main(<myfile>)
|
||||
|
||||
|
|
@ -7,8 +7,8 @@ find_package(Z3
|
|||
REQUIRED
|
||||
CONFIG
|
||||
# `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3.
|
||||
# This should prevent us from accidently picking up an installed
|
||||
# copy of Z3. This is here to benefit Z3's build sytem when building
|
||||
# This should prevent us from accidentally picking up an installed
|
||||
# copy of Z3. This is here to benefit Z3's build system when building
|
||||
# this project. When making your own project you probably shouldn't
|
||||
# use this option.
|
||||
NO_DEFAULT_PATH
|
||||
|
|
|
|||
|
|
@ -5,9 +5,9 @@ in the build directory.
|
|||
|
||||
This command will create the executable tptp.
|
||||
On Windows, you can just execute it.
|
||||
On OSX and Linux, you must install z3 first using
|
||||
On macOS and Linux, you must install z3 first using
|
||||
sudo make install
|
||||
OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX)
|
||||
OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (macOS)
|
||||
with the build directory. You need that to be able to
|
||||
find the Z3 shared library.
|
||||
|
||||
|
|
|
|||
|
|
@ -233,7 +233,7 @@ class env {
|
|||
|
||||
void check_arity(unsigned num_args, unsigned arity) {
|
||||
if (num_args != arity) {
|
||||
throw failure_ex("arity missmatch");
|
||||
throw failure_ex("arity mismatch");
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1337,7 +1337,7 @@ public:
|
|||
}
|
||||
}
|
||||
else if (e.is_quantifier()) {
|
||||
Z3_bool is_forall = Z3_is_quantifier_forall(ctx, e);
|
||||
bool is_forall = Z3_is_quantifier_forall(ctx, e);
|
||||
unsigned nb = Z3_get_quantifier_num_bound(ctx, e);
|
||||
|
||||
out << (is_forall?"!":"?") << "[";
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue