From 0f602d652a6e38d93767adc14c47c53bd2eef46a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Nov 2015 13:47:41 -0800 Subject: [PATCH 1/4] remove deprecated API functionality Signed-off-by: Nikolaj Bjorner --- examples/c/test_capi.c | 489 +++++++++++++--------- examples/interp/iz3.cpp | 35 +- examples/maxsat/maxsat.c | 98 +++-- src/api/api_ast.cpp | 14 - src/api/api_context.cpp | 25 +- src/api/api_context.h | 2 +- src/api/api_model.cpp | 260 +----------- src/api/api_quant.cpp | 36 -- src/api/api_solver.cpp | 2 + src/api/api_solver_old.cpp | 325 --------------- src/api/c++/z3++.h | 9 + src/api/dotnet/Deprecated.cs | 75 ---- src/api/z3_api.h | 770 ----------------------------------- 13 files changed, 368 insertions(+), 1772 deletions(-) diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index 11306a98b..385035361 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -83,6 +83,18 @@ Z3_context mk_context_custom(Z3_config cfg, Z3_error_handler err) return ctx; } +Z3_solver mk_solver(Z3_context ctx) +{ + Z3_solver s = Z3_mk_solver(ctx); + Z3_solver_inc_ref(ctx, s); + return s; +} + +void del_solver(Z3_context ctx, Z3_solver s) +{ + Z3_solver_dec_ref(ctx, s); +} + /** \brief Create a logical context. @@ -184,28 +196,30 @@ Z3_ast mk_binary_app(Z3_context ctx, Z3_func_decl f, Z3_ast x, Z3_ast y) \brief Check whether the logical context is satisfiable, and compare the result with the expected result. If the context is satisfiable, then display the model. */ -void check(Z3_context ctx, Z3_lbool expected_result) +void check(Z3_context ctx, Z3_solver s, Z3_lbool expected_result) { Z3_model m = 0; - Z3_lbool result = Z3_check_and_get_model(ctx, &m); + Z3_lbool result = Z3_solver_check(ctx, s); switch (result) { case Z3_L_FALSE: printf("unsat\n"); break; case Z3_L_UNDEF: - printf("unknown\n"); + printf("unknown\n"); + m = Z3_solver_get_model(ctx, s); + if (m) Z3_model_inc_ref(ctx, m); printf("potential model:\n%s\n", Z3_model_to_string(ctx, m)); break; case Z3_L_TRUE: + m = Z3_solver_get_model(ctx, s); + if (m) Z3_model_inc_ref(ctx, m); printf("sat\n%s\n", Z3_model_to_string(ctx, m)); break; } - if (m) { - Z3_del_model(ctx, m); - } if (result != expected_result) { exitf("unexpected result"); } + if (m) Z3_model_dec_ref(ctx, m); } /** @@ -218,20 +232,18 @@ void check(Z3_context ctx, Z3_lbool expected_result) The context \c ctx is not modified by this function. */ -void prove(Z3_context ctx, Z3_ast f, Z3_bool is_valid) +void prove(Z3_context ctx, Z3_solver s, Z3_ast f, Z3_bool is_valid) { - Z3_model m; + Z3_model m = 0; Z3_ast not_f; /* save the current state of the context */ - Z3_push(ctx); + Z3_solver_push(ctx, s); not_f = Z3_mk_not(ctx, f); - Z3_assert_cnstr(ctx, not_f); - - m = 0; - - switch (Z3_check_and_get_model(ctx, &m)) { + Z3_solver_assert(ctx, s, not_f); + + switch (Z3_solver_check(ctx, s)) { case Z3_L_FALSE: /* proved */ printf("valid\n"); @@ -242,9 +254,11 @@ void prove(Z3_context ctx, Z3_ast f, Z3_bool is_valid) case Z3_L_UNDEF: /* Z3 failed to prove/disprove f. */ printf("unknown\n"); + m = Z3_solver_get_model(ctx, s); if (m != 0) { + Z3_model_inc_ref(ctx, m); /* m should be viewed as a potential counterexample. */ - printf("potential counterexample:\n%s\n", Z3_model_to_string(ctx, m)); + printf("potential counterexample:\n%s\n", Z3_model_to_string(ctx, m)); } if (is_valid) { exitf("unexpected result"); @@ -253,7 +267,9 @@ void prove(Z3_context ctx, Z3_ast f, Z3_bool is_valid) case Z3_L_TRUE: /* disproved */ printf("invalid\n"); + m = Z3_solver_get_model(ctx, s); if (m) { + Z3_model_inc_ref(ctx, m); /* the model returned by Z3 is a counterexample */ printf("counterexample:\n%s\n", Z3_model_to_string(ctx, m)); } @@ -262,13 +278,10 @@ void prove(Z3_context ctx, Z3_ast f, Z3_bool is_valid) } break; } + if (m) Z3_model_dec_ref(ctx, m); - if (m) { - Z3_del_model(ctx, m); - } - - /* restore context */ - Z3_pop(ctx, 1); + /* restore scope */ + Z3_solver_pop(ctx, s, 1); } /** @@ -281,7 +294,7 @@ void prove(Z3_context ctx, Z3_ast f, Z3_bool is_valid) Where, \c finv is a fresh function declaration. */ -void assert_inj_axiom(Z3_context ctx, Z3_func_decl f, unsigned i) +void assert_inj_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f, unsigned i) { unsigned sz, j; Z3_sort finv_domain, finv_range; @@ -339,7 +352,7 @@ void assert_inj_axiom(Z3_context ctx, Z3_func_decl f, unsigned i) names, eq); printf("assert axiom:\n%s\n", Z3_ast_to_string(ctx, q)); - Z3_assert_cnstr(ctx, q); + Z3_solver_assert(ctx, s, q); /* free temporary arrays */ free(types); @@ -352,7 +365,7 @@ void assert_inj_axiom(Z3_context ctx, Z3_func_decl f, unsigned i) This example uses the SMT-LIB parser to simplify the axiom construction. */ -void assert_comm_axiom(Z3_context ctx, Z3_func_decl f) +void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f) { Z3_sort t; Z3_symbol f_name, t_name; @@ -379,7 +392,7 @@ void assert_comm_axiom(Z3_context ctx, Z3_func_decl f) 1, &f_name, &f); q = Z3_get_smtlib_formula(ctx, 0); printf("assert axiom:\n%s\n", Z3_ast_to_string(ctx, q)); - Z3_assert_cnstr(ctx, q); + Z3_solver_assert(ctx, s, q); } /** @@ -554,42 +567,50 @@ void display_function_interpretations(Z3_context c, FILE * out, Z3_model m) fprintf(out, "function interpretations:\n"); - num_functions = Z3_get_model_num_funcs(c, m); + num_functions = Z3_model_get_num_funcs(c, m); for (i = 0; i < num_functions; i++) { Z3_func_decl fdecl; Z3_symbol name; Z3_ast func_else; - unsigned num_entries, j; + unsigned num_entries = 0, j; + Z3_func_interp_opt finterp; - fdecl = Z3_get_model_func_decl(c, m, i); + fdecl = Z3_model_get_func_decl(c, m, i); + finterp = Z3_model_get_func_interp(c, m, fdecl); + Z3_func_interp_inc_ref(c, finterp); name = Z3_get_decl_name(c, fdecl); display_symbol(c, out, name); fprintf(out, " = {"); - num_entries = Z3_get_model_func_num_entries(c, m, i); + if (finterp) + num_entries = Z3_func_interp_get_num_entries(c, finterp); for (j = 0; j < num_entries; j++) { unsigned num_args, k; + Z3_func_entry fentry = Z3_func_interp_get_entry(c, finterp, j); + Z3_func_entry_inc_ref(c, fentry); if (j > 0) { fprintf(out, ", "); } - num_args = Z3_get_model_func_entry_num_args(c, m, i, j); + num_args = Z3_func_entry_get_num_args(c, fentry); fprintf(out, "("); for (k = 0; k < num_args; k++) { if (k > 0) { fprintf(out, ", "); } - display_ast(c, out, Z3_get_model_func_entry_arg(c, m, i, j, k)); + display_ast(c, out, Z3_func_entry_get_arg(c, fentry, k)); } fprintf(out, "|->"); - display_ast(c, out, Z3_get_model_func_entry_value(c, m, i, j)); + display_ast(c, out, Z3_func_entry_get_value(c, fentry)); fprintf(out, ")"); + Z3_func_entry_dec_ref(c, fentry); } if (num_entries > 0) { fprintf(out, ", "); } fprintf(out, "(else|->"); - func_else = Z3_get_model_func_else(c, m, i); + func_else = Z3_func_interp_get_else(c, finterp); display_ast(c, out, func_else); fprintf(out, ")}\n"); + Z3_func_interp_dec_ref(c, finterp); } } @@ -601,10 +622,12 @@ void display_model(Z3_context c, FILE * out, Z3_model m) unsigned num_constants; unsigned i; - num_constants = Z3_get_model_num_constants(c, m); + if (!m) return; + + num_constants = Z3_model_get_num_consts(c, m); for (i = 0; i < num_constants; i++) { Z3_symbol name; - Z3_func_decl cnst = Z3_get_model_constant(c, m, i); + Z3_func_decl cnst = Z3_model_get_const_decl(c, m, i); Z3_ast a, v; Z3_bool ok; name = Z3_get_decl_name(c, cnst); @@ -612,7 +635,7 @@ void display_model(Z3_context c, FILE * out, Z3_model m) fprintf(out, " = "); a = Z3_mk_app(c, cnst, 0, 0); v = a; - ok = Z3_eval(c, m, a, &v); + ok = Z3_model_eval(c, m, a, 1, &v); display_ast(c, out, v); fprintf(out, "\n"); } @@ -622,10 +645,10 @@ void display_model(Z3_context c, FILE * out, Z3_model m) /** \brief Similar to #check, but uses #display_model instead of #Z3_model_to_string. */ -void check2(Z3_context ctx, Z3_lbool expected_result) +void check2(Z3_context ctx, Z3_solver s, Z3_lbool expected_result) { Z3_model m = 0; - Z3_lbool result = Z3_check_and_get_model(ctx, &m); + Z3_lbool result = Z3_solver_check(ctx, s); switch (result) { case Z3_L_FALSE: printf("unsat\n"); @@ -633,19 +656,22 @@ void check2(Z3_context ctx, Z3_lbool expected_result) case Z3_L_UNDEF: printf("unknown\n"); printf("potential model:\n"); + m = Z3_solver_get_model(ctx, s); + if (m) Z3_model_inc_ref(ctx, m); display_model(ctx, stdout, m); break; case Z3_L_TRUE: printf("sat\n"); + m = Z3_solver_get_model(ctx, s); + if (m) Z3_model_inc_ref(ctx, m); display_model(ctx, stdout, m); break; } - if (m) { - Z3_del_model(ctx, m); - } if (result != expected_result) { exitf("unexpected result"); } + if (m) Z3_model_dec_ref(ctx, m); + } /** @@ -674,9 +700,6 @@ void simple_example() ctx = mk_context(); - /* do something with the context */ - printf("CONTEXT:\n%sEND OF CONTEXT\n", Z3_context_to_string(ctx)); - /* delete logical context */ Z3_del_context(ctx); } @@ -689,6 +712,7 @@ void demorgan() { Z3_config cfg; Z3_context ctx; + Z3_solver s; Z3_sort bool_sort; Z3_symbol symbol_x, symbol_y; Z3_ast x, y, not_x, not_y, x_and_y, ls, rs, conjecture, negated_conjecture; @@ -719,9 +743,10 @@ void demorgan() rs = Z3_mk_or(ctx, 2, args); conjecture = Z3_mk_iff(ctx, ls, rs); negated_conjecture = Z3_mk_not(ctx, conjecture); - - Z3_assert_cnstr(ctx, negated_conjecture); - switch (Z3_check(ctx)) { + + s = mk_solver(ctx); + Z3_solver_assert(ctx, s, negated_conjecture); + switch (Z3_solver_check(ctx, s)) { case Z3_L_FALSE: /* The negated conjecture was unsatisfiable, hence the conjecture is valid */ printf("DeMorgan is valid\n"); @@ -735,6 +760,7 @@ void demorgan() printf("DeMorgan is not valid\n"); break; } + del_solver(ctx, s); Z3_del_context(ctx); } @@ -745,21 +771,24 @@ void find_model_example1() { Z3_context ctx; Z3_ast x, y, x_xor_y; + Z3_solver s; printf("\nfind_model_example1\n"); LOG_MSG("find_model_example1"); ctx = mk_context(); + s = mk_solver(ctx); x = mk_bool_var(ctx, "x"); y = mk_bool_var(ctx, "y"); x_xor_y = Z3_mk_xor(ctx, x, y); - Z3_assert_cnstr(ctx, x_xor_y); + Z3_solver_assert(ctx, s, x_xor_y); printf("model for: x xor y\n"); - check(ctx, Z3_L_TRUE); + check(ctx, s, Z3_L_TRUE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -774,11 +803,13 @@ void find_model_example2() Z3_ast x_eq_y; Z3_ast args[2]; Z3_ast c1, c2, c3; + Z3_solver s; printf("\nfind_model_example2\n"); LOG_MSG("find_model_example2"); ctx = mk_context(); + s = mk_solver(ctx); x = mk_int_var(ctx, "x"); y = mk_int_var(ctx, "y"); one = mk_int(ctx, 1); @@ -791,20 +822,21 @@ void find_model_example2() c1 = Z3_mk_lt(ctx, x, y_plus_one); c2 = Z3_mk_gt(ctx, x, two); - Z3_assert_cnstr(ctx, c1); - Z3_assert_cnstr(ctx, c2); + Z3_solver_assert(ctx, s, c1); + Z3_solver_assert(ctx, s, c2); printf("model for: x < y + 1, x > 2\n"); - check(ctx, Z3_L_TRUE); + check(ctx, s, Z3_L_TRUE); /* assert not(x = y) */ x_eq_y = Z3_mk_eq(ctx, x, y); c3 = Z3_mk_not(ctx, x_eq_y); - Z3_assert_cnstr(ctx, c3); + Z3_solver_assert(ctx, s,c3); printf("model for: x < y + 1, x > 2, not(x = y)\n"); - check(ctx, Z3_L_TRUE); + check(ctx, s, Z3_L_TRUE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -818,6 +850,7 @@ void find_model_example2() void prove_example1() { Z3_context ctx; + Z3_solver s; Z3_symbol U_name, g_name, x_name, y_name; Z3_sort U; Z3_sort g_domain[1]; @@ -829,7 +862,8 @@ void prove_example1() LOG_MSG("prove_example1"); ctx = mk_context(); - + s = mk_solver(ctx); + /* create uninterpreted type. */ U_name = Z3_mk_string_symbol(ctx, "U"); U = Z3_mk_uninterpreted_sort(ctx, U_name); @@ -850,12 +884,12 @@ void prove_example1() /* assert x = y */ eq = Z3_mk_eq(ctx, x, y); - Z3_assert_cnstr(ctx, eq); + Z3_solver_assert(ctx, s, eq); /* prove g(x) = g(y) */ f = Z3_mk_eq(ctx, gx, gy); printf("prove: x = y implies g(x) = g(y)\n"); - prove(ctx, f, Z3_TRUE); + prove(ctx, s, f, Z3_TRUE); /* create g(g(x)) */ ggx = mk_unary_app(ctx, g, gx); @@ -863,8 +897,9 @@ 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, f, Z3_FALSE); + prove(ctx, s, f, Z3_FALSE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -877,6 +912,7 @@ void prove_example1() void prove_example2() { Z3_context ctx; + Z3_solver s; Z3_sort int_sort; Z3_symbol g_name; Z3_sort g_domain[1]; @@ -889,6 +925,7 @@ void prove_example2() LOG_MSG("prove_example2"); ctx = mk_context(); + s = mk_solver(ctx); /* declare function g */ int_sort = Z3_mk_int_sort(ctx); @@ -916,30 +953,31 @@ void prove_example2() ggx_gy = mk_unary_app(ctx, g, gx_gy); eq = Z3_mk_eq(ctx, ggx_gy, gz); c1 = Z3_mk_not(ctx, eq); - Z3_assert_cnstr(ctx, c1); + Z3_solver_assert(ctx, s, c1); /* assert x + z <= y */ args[0] = x; args[1] = z; x_plus_z = Z3_mk_add(ctx, 2, args); c2 = Z3_mk_le(ctx, x_plus_z, y); - Z3_assert_cnstr(ctx, c2); + Z3_solver_assert(ctx, s, c2); /* assert y <= x */ c3 = Z3_mk_le(ctx, y, x); - Z3_assert_cnstr(ctx, c3); + Z3_solver_assert(ctx, s, c3); /* 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, f, Z3_TRUE); + prove(ctx, s, f, Z3_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, f, Z3_FALSE); + prove(ctx, s, f, Z3_FALSE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -952,6 +990,7 @@ void prove_example2() void push_pop_example1() { Z3_context ctx; + Z3_solver s; Z3_sort int_sort; Z3_symbol x_sym, y_sym; Z3_ast x, y, big_number, three; @@ -961,6 +1000,7 @@ void push_pop_example1() LOG_MSG("push_pop_example1"); ctx = mk_context(); + s = mk_solver(ctx); /* create a big number */ int_sort = Z3_mk_int_sort(ctx); @@ -976,32 +1016,32 @@ void push_pop_example1() /* assert x >= "big number" */ c1 = Z3_mk_ge(ctx, x, big_number); printf("assert: x >= 'big number'\n"); - Z3_assert_cnstr(ctx, c1); + Z3_solver_assert(ctx, s, c1); /* create a backtracking point */ printf("push\n"); - Z3_push(ctx); + Z3_solver_push(ctx, s); - printf("number of scopes: %d\n", Z3_get_num_scopes(ctx)); + printf("number of scopes: %d\n", Z3_solver_get_num_scopes(ctx, s)); /* assert x <= 3 */ c2 = Z3_mk_le(ctx, x, three); printf("assert: x <= 3\n"); - Z3_assert_cnstr(ctx, c2); + Z3_solver_assert(ctx, s, c2); /* context is inconsistent at this point */ - check2(ctx, Z3_L_FALSE); + check2(ctx, s, Z3_L_FALSE); /* backtrack: the constraint x <= 3 will be removed, since it was - asserted after the last Z3_push. */ + asserted after the last Z3_solver_push. */ printf("pop\n"); - Z3_pop(ctx, 1); + Z3_solver_pop(ctx, s, 1); - printf("number of scopes: %d\n", Z3_get_num_scopes(ctx)); + printf("number of scopes: %d\n", Z3_solver_get_num_scopes(ctx, s)); /* the context is consistent again. */ - check2(ctx, Z3_L_TRUE); + check2(ctx, s, Z3_L_TRUE); /* new constraints can be asserted... */ @@ -1012,11 +1052,12 @@ void push_pop_example1() /* assert y > x */ c3 = Z3_mk_gt(ctx, y, x); printf("assert: y > x\n"); - Z3_assert_cnstr(ctx, c3); + Z3_solver_assert(ctx, s, c3); /* the context is still consistent. */ - check2(ctx, Z3_L_TRUE); + check2(ctx, s, Z3_L_TRUE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1030,6 +1071,7 @@ void quantifier_example1() { Z3_config cfg; Z3_context ctx; + Z3_solver s; Z3_sort int_sort; Z3_symbol f_name; Z3_sort f_domain[2]; @@ -1052,6 +1094,7 @@ void quantifier_example1() Z3_global_param_set("smt.mbqi.max_iterations", "10"); ctx = mk_context_custom(cfg, error_handler); Z3_del_config(cfg); + s = mk_solver(ctx); /* declare function f */ int_sort = Z3_mk_int_sort(ctx); @@ -1061,7 +1104,7 @@ void quantifier_example1() f = Z3_mk_func_decl(ctx, f_name, 2, f_domain, int_sort); /* assert that f is injective in the second argument. */ - assert_inj_axiom(ctx, f, 1); + assert_inj_axiom(ctx, s, f, 1); /* create x, y, v, w, fxy, fwv */ x = mk_int_var(ctx, "x"); @@ -1073,26 +1116,23 @@ void quantifier_example1() /* assert f(x, y) = f(w, v) */ p1 = Z3_mk_eq(ctx, fxy, fwv); - Z3_assert_cnstr(ctx, p1); + Z3_solver_assert(ctx, s, p1); /* 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, p2, Z3_TRUE); + prove(ctx, s, p2, Z3_TRUE); /* disprove f(x, y) = f(w, v) implies x = w */ /* using check2 instead of prove */ p3 = Z3_mk_eq(ctx, x, w); not_p3 = Z3_mk_not(ctx, p3); - Z3_assert_cnstr(ctx, not_p3); + Z3_solver_assert(ctx, s, not_p3); printf("disprove: f(x, y) = f(w, v) implies x = w\n"); printf("that is: not(f(x, y) = f(w, v) implies x = w) is satisfiable\n"); - check2(ctx, Z3_L_UNDEF); - printf("reason for last failure: %d (7 = quantifiers)\n", - Z3_get_search_failure(ctx)); - if (Z3_get_search_failure(ctx) != Z3_QUANTIFIERS) { - exitf("unexpected result"); - } + check2(ctx, s, Z3_L_UNDEF); + printf("reason for last failure: %s\n", Z3_solver_get_reason_unknown(ctx, s)); + del_solver(ctx, s); Z3_del_context(ctx); /* reset global parameters set by this function */ Z3_global_param_reset_all(); @@ -1105,7 +1145,8 @@ void quantifier_example1() */ void array_example1() { - Z3_context ctx; + Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_sort int_sort, array_sort; Z3_ast a1, a2, i1, v1, i2, v2, i3; Z3_ast st1, st2, sel1, sel2; @@ -1116,7 +1157,6 @@ void array_example1() printf("\narray_example1\n"); LOG_MSG("array_example1"); - ctx = mk_context(); int_sort = Z3_mk_int_sort(ctx); array_sort = Z3_mk_array_sort(ctx, int_sort, int_sort); @@ -1148,8 +1188,9 @@ 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, thm, Z3_TRUE); + prove(ctx, s, thm, Z3_TRUE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1163,6 +1204,7 @@ void array_example1() void array_example2() { Z3_context ctx; + Z3_solver s; Z3_sort bool_sort, array_sort; Z3_ast a[5]; Z3_ast d; @@ -1174,6 +1216,7 @@ void array_example2() for (n = 2; n <= 5; n++) { printf("n = %d\n", n); ctx = mk_context(); + s = mk_solver(ctx); bool_sort = Z3_mk_bool_sort(ctx); array_sort = Z3_mk_array_sort(ctx, bool_sort, bool_sort); @@ -1187,11 +1230,12 @@ void array_example2() /* assert distinct(a[0], ..., a[n]) */ d = Z3_mk_distinct(ctx, n, a); printf("%s\n", Z3_ast_to_string(ctx, d)); - Z3_assert_cnstr(ctx, d); + Z3_solver_assert(ctx, s, d); /* context is satisfiable if n < 5 */ - check2(ctx, n < 5 ? Z3_L_TRUE : Z3_L_FALSE); + check2(ctx, s, n < 5 ? Z3_L_TRUE : Z3_L_FALSE); + del_solver(ctx, s); Z3_del_context(ctx); } } @@ -1201,13 +1245,13 @@ void array_example2() */ void array_example3() { - Z3_context ctx; + Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_sort bool_sort, int_sort, array_sort; Z3_sort domain, range; printf("\narray_example3\n"); LOG_MSG("array_example3"); - ctx = mk_context(); bool_sort = Z3_mk_bool_sort(ctx); int_sort = Z3_mk_int_sort(ctx); @@ -1231,6 +1275,7 @@ void array_example3() exitf("invalid array type"); } + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1239,7 +1284,8 @@ void array_example3() */ void tuple_example1() { - Z3_context ctx; + Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_sort real_sort, pair_sort; Z3_symbol mk_tuple_name; Z3_func_decl mk_tuple_decl; @@ -1251,7 +1297,6 @@ void tuple_example1() printf("\ntuple_example1\n"); LOG_MSG("tuple_example1"); - ctx = mk_context(); real_sort = Z3_mk_real_sort(ctx); @@ -1284,13 +1329,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, thm, Z3_TRUE); + prove(ctx, s, thm, Z3_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, thm, Z3_FALSE); + prove(ctx, s, thm, Z3_FALSE); } { @@ -1311,12 +1356,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, thm, Z3_TRUE); + prove(ctx, s, thm, Z3_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, thm, Z3_FALSE); + prove(ctx, s, thm, Z3_FALSE); } { @@ -1335,16 +1380,17 @@ 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, thm, Z3_TRUE); + prove(ctx, s, thm, Z3_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, thm, Z3_FALSE); + prove(ctx, s, thm, Z3_FALSE); } + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1353,14 +1399,14 @@ void tuple_example1() */ void bitvector_example1() { - Z3_context ctx; + Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_sort bv_sort; Z3_ast x, zero, ten, x_minus_ten, c1, c2, thm; printf("\nbitvector_example1\n"); LOG_MSG("bitvector_example1"); - ctx = mk_context(); bv_sort = Z3_mk_bv_sort(ctx, 32); @@ -1373,8 +1419,9 @@ 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, thm, Z3_FALSE); + prove(ctx, s, thm, Z3_FALSE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1384,6 +1431,7 @@ void bitvector_example1() void bitvector_example2() { Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); /* construct x ^ y - 103 == x * y */ Z3_sort bv_sort = Z3_mk_bv_sort(ctx, 32); @@ -1400,11 +1448,12 @@ void bitvector_example2() printf("find values of x and y, such that x ^ y - 103 == x * y\n"); /* add the constraint x ^ y - 103 == x * y<\tt> to the logical context */ - Z3_assert_cnstr(ctx, ctr); + Z3_solver_assert(ctx, s, ctr); /* find a model (i.e., values for x an y that satisfy the constraint */ - check(ctx, Z3_L_TRUE); + check(ctx, s, Z3_L_TRUE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1413,36 +1462,38 @@ void bitvector_example2() */ void eval_example1() { - Z3_context ctx; + Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_ast x, y, two; Z3_ast c1, c2; - Z3_model m; + Z3_model m = 0; printf("\neval_example1\n"); LOG_MSG("eval_example1"); - ctx = mk_context(); x = mk_int_var(ctx, "x"); y = mk_int_var(ctx, "y"); two = mk_int(ctx, 2); /* assert x < y */ c1 = Z3_mk_lt(ctx, x, y); - Z3_assert_cnstr(ctx, c1); + Z3_solver_assert(ctx, s, c1); /* assert x > 2 */ c2 = Z3_mk_gt(ctx, x, two); - Z3_assert_cnstr(ctx, c2); + Z3_solver_assert(ctx, s, c2); /* find model for the constraints above */ - if (Z3_check_and_get_model(ctx, &m) == Z3_L_TRUE) { + if (Z3_solver_check(ctx, s) == Z3_L_TRUE) { Z3_ast x_plus_y; Z3_ast args[2] = {x, y}; Z3_ast v; + m = Z3_solver_get_model(ctx, s); + if (m) Z3_model_inc_ref(ctx, m); printf("MODEL:\n%s", Z3_model_to_string(ctx, m)); x_plus_y = Z3_mk_add(ctx, 2, args); printf("\nevaluating x+y\n"); - if (Z3_eval(ctx, m, x_plus_y, &v)) { + if (Z3_model_eval(ctx, m, x_plus_y, 1, &v)) { printf("result = "); display_ast(ctx, stdout, v); printf("\n"); @@ -1450,12 +1501,13 @@ void eval_example1() else { exitf("failed to evaluate: x+y"); } - Z3_del_model(ctx, m); } else { exitf("the constraints are satisfiable"); } + if (m) Z3_model_dec_ref(ctx, m); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1492,6 +1544,7 @@ void error_code_example1() { Z3_config cfg; Z3_context ctx; + Z3_solver s; Z3_ast x; Z3_model m; Z3_ast v; @@ -1505,16 +1558,19 @@ void error_code_example1() cfg = Z3_mk_config(); ctx = mk_context_custom(cfg, NULL); Z3_del_config(cfg); + s = mk_solver(ctx); x = mk_bool_var(ctx, "x"); x_decl = Z3_get_app_decl(ctx, Z3_to_app(ctx, x)); - Z3_assert_cnstr(ctx, x); + Z3_solver_assert(ctx, s, x); - if (Z3_check_and_get_model(ctx, &m) != Z3_L_TRUE) { + if (Z3_solver_check(ctx, s) != Z3_L_TRUE) { exitf("unexpected result"); } - if (!Z3_eval_func_decl(ctx, m, x_decl, &v)) { + m = Z3_solver_get_model(ctx, s); + if (m) Z3_model_inc_ref(ctx, m); + if (!Z3_model_eval(ctx, m, x, 1, &v)) { exitf("did not obtain value for declaration.\n"); } if (Z3_get_error_code(ctx) == Z3_OK) { @@ -1525,7 +1581,8 @@ void error_code_example1() if (Z3_get_error_code(ctx) != Z3_OK) { printf("last call failed.\n"); } - Z3_del_model(ctx, m); + if (m) Z3_model_dec_ref(ctx, m); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1558,7 +1615,7 @@ void error_code_example2() { Z3_del_context(ctx); } else { - printf("Z3 error: %s.\n", Z3_get_error_msg((Z3_error_code)r)); + printf("Z3 error: %s.\n", Z3_get_error_msg_ex(ctx, (Z3_error_code)r)); if (ctx != NULL) { Z3_del_context(ctx); } @@ -1570,13 +1627,13 @@ void error_code_example2() { */ void parser_example1() { - Z3_context ctx; + Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); unsigned i, num_formulas; printf("\nparser_example1\n"); LOG_MSG("parser_example1"); - ctx = mk_context(); Z3_parse_smtlib_string(ctx, "(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))", @@ -1586,11 +1643,12 @@ void parser_example1() for (i = 0; i < num_formulas; i++) { Z3_ast f = Z3_get_smtlib_formula(ctx, i); printf("formula %d: %s\n", i, Z3_ast_to_string(ctx, f)); - Z3_assert_cnstr(ctx, f); + Z3_solver_assert(ctx, s, f); } - check(ctx, Z3_L_TRUE); + check(ctx, s, Z3_L_TRUE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1599,7 +1657,8 @@ void parser_example1() */ void parser_example2() { - Z3_context ctx; + Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_ast x, y; Z3_symbol names[2]; Z3_func_decl decls[2]; @@ -1608,7 +1667,6 @@ void parser_example2() printf("\nparser_example2\n"); LOG_MSG("parser_example2"); - ctx = mk_context(); /* Z3_enable_arithmetic doesn't need to be invoked in this example because it will be implicitly invoked by mk_int_var. @@ -1629,9 +1687,10 @@ void parser_example2() 2, names, decls); f = Z3_get_smtlib_formula(ctx, 0); printf("formula: %s\n", Z3_ast_to_string(ctx, f)); - Z3_assert_cnstr(ctx, f); - check(ctx, Z3_L_TRUE); + Z3_solver_assert(ctx, s, f); + check(ctx, s, Z3_L_TRUE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1642,6 +1701,7 @@ void parser_example3() { Z3_config cfg; Z3_context ctx; + Z3_solver s; Z3_sort int_sort; Z3_symbol g_name; Z3_sort g_domain[2]; @@ -1656,6 +1716,7 @@ void parser_example3() Z3_set_param_value(cfg, "model", "true"); ctx = mk_context_custom(cfg, error_handler); Z3_del_config(cfg); + s = mk_solver(ctx); /* declare function g */ int_sort = Z3_mk_int_sort(ctx); @@ -1664,7 +1725,7 @@ void parser_example3() g_domain[1] = int_sort; g = Z3_mk_func_decl(ctx, g_name, 2, g_domain, int_sort); - assert_comm_axiom(ctx, g); + assert_comm_axiom(ctx, s, g); Z3_parse_smtlib_string(ctx, "(benchmark tst :formula (forall (x Int) (y Int) (implies (= x y) (= (g x 0) (g 0 y)))))", @@ -1672,8 +1733,9 @@ void parser_example3() 1, &g_name, &g); thm = Z3_get_smtlib_formula(ctx, 0); printf("formula: %s\n", Z3_ast_to_string(ctx, thm)); - prove(ctx, thm, Z3_TRUE); + prove(ctx, s, thm, Z3_TRUE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1718,6 +1780,7 @@ void parser_example4() void parser_example5() { Z3_config cfg; Z3_context ctx = NULL; + Z3_solver s = NULL; int r; printf("\nparser_example5\n"); @@ -1727,6 +1790,7 @@ void parser_example5() { if (r == 0) { cfg = Z3_mk_config(); ctx = mk_context_custom(cfg, throw_z3_error); + s = mk_solver(ctx); Z3_del_config(cfg); Z3_parse_smtlib_string(ctx, @@ -1735,12 +1799,14 @@ void parser_example5() { 0, 0, 0, 0, 0, 0); unreachable(); + del_solver(ctx, s); Z3_del_context(ctx); } else { - printf("Z3 error: %s.\n", Z3_get_error_msg((Z3_error_code)r)); + printf("Z3 error: %s.\n", Z3_get_error_msg_ex(ctx, (Z3_error_code)r)); if (ctx != NULL) { printf("Error message: '%s'.\n",Z3_get_smtlib_error(ctx)); + del_solver(ctx, s); Z3_del_context(ctx); } } @@ -1751,24 +1817,28 @@ void parser_example5() { */ void numeral_example() { Z3_context ctx; + Z3_solver s; Z3_ast n1, n2; Z3_sort real_ty; printf("\nnumeral_example\n"); LOG_MSG("numeral_example"); ctx = mk_context(); + s = mk_solver(ctx); + real_ty = Z3_mk_real_sort(ctx); n1 = Z3_mk_numeral(ctx, "1/2", real_ty); 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, Z3_mk_eq(ctx, n1, n2), Z3_TRUE); + prove(ctx, s, Z3_mk_eq(ctx, n1, n2), Z3_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, 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)), Z3_TRUE); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1801,6 +1871,7 @@ void ite_example() */ void enum_example() { Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_sort fruit; Z3_symbol name = Z3_mk_string_symbol(ctx, "fruit"); Z3_symbol enum_names[3]; @@ -1831,14 +1902,14 @@ void enum_example() { orange = Z3_mk_app(ctx, enum_consts[2], 0, 0); /* Apples are different from oranges */ - prove(ctx, 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)), Z3_TRUE); /* Apples pass the apple test */ - prove(ctx, Z3_mk_app(ctx, enum_testers[0], 1, &apple), Z3_TRUE); + prove(ctx, s, Z3_mk_app(ctx, enum_testers[0], 1, &apple), Z3_TRUE); /* Oranges fail the apple test */ - prove(ctx, Z3_mk_app(ctx, enum_testers[0], 1, &orange), Z3_FALSE); - prove(ctx, 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), Z3_FALSE); + prove(ctx, s, Z3_mk_not(ctx, Z3_mk_app(ctx, enum_testers[0], 1, &orange)), Z3_TRUE); fruity = mk_var(ctx, "fruity", fruit); @@ -1847,9 +1918,10 @@ void enum_example() { ors[1] = Z3_mk_eq(ctx, fruity, banana); ors[2] = Z3_mk_eq(ctx, fruity, orange); - prove(ctx, Z3_mk_or(ctx, 3, ors), Z3_TRUE); + prove(ctx, s, Z3_mk_or(ctx, 3, ors), Z3_TRUE); /* delete logical context */ + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1858,6 +1930,7 @@ void enum_example() { */ void list_example() { Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_sort int_ty, int_list; Z3_func_decl nil_decl, is_nil_decl, cons_decl, is_cons_decl, head_decl, tail_decl; Z3_ast nil, l1, l2, x, y, u, v, fml, fml1; @@ -1877,43 +1950,44 @@ void list_example() { l2 = mk_binary_app(ctx, cons_decl, mk_int(ctx, 2), nil); /* nil != cons(1, nil) */ - prove(ctx, 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)), Z3_TRUE); /* cons(2,nil) != cons(1, nil) */ - prove(ctx, 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)), Z3_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, 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)), Z3_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, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE); - prove(ctx, 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)), Z3_TRUE); + prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_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, Z3_mk_or(ctx, 2, ors), Z3_TRUE); + prove(ctx, s, Z3_mk_or(ctx, 2, ors), Z3_TRUE); /* occurs check u != cons(x,u) */ - prove(ctx, 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)), Z3_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, fml, Z3_TRUE); + prove(ctx, s, fml, Z3_TRUE); - prove(ctx, fml1, Z3_FALSE); + prove(ctx, s, fml1, Z3_FALSE); /* delete logical context */ + del_solver(ctx, s); Z3_del_context(ctx); } @@ -1922,6 +1996,7 @@ void list_example() { */ void tree_example() { Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_sort cell; Z3_func_decl nil_decl, is_nil_decl, cons_decl, is_cons_decl, car_decl, cdr_decl; Z3_ast nil, l1, l2, x, y, u, v, fml, fml1; @@ -1957,7 +2032,7 @@ void tree_example() { l2 = mk_binary_app(ctx, cons_decl, l1, nil); /* nil != cons(nil, nil) */ - prove(ctx, 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)), Z3_TRUE); /* cons(x,u) = cons(x, v) => u = v */ u = mk_var(ctx, "u", cell); @@ -1966,26 +2041,27 @@ 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, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE); - prove(ctx, 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)), Z3_TRUE); + prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_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, Z3_mk_or(ctx, 2, ors), Z3_TRUE); + prove(ctx, s, Z3_mk_or(ctx, 2, ors), Z3_TRUE); /* occurs check u != cons(x,u) */ - prove(ctx, 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)), Z3_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, fml, Z3_TRUE); + prove(ctx, s, fml, Z3_TRUE); - prove(ctx, fml1, Z3_FALSE); + prove(ctx, s, fml1, Z3_FALSE); /* delete logical context */ + del_solver(ctx, s); Z3_del_context(ctx); @@ -2000,6 +2076,7 @@ void tree_example() { void forest_example() { Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_sort tree, forest; Z3_func_decl nil1_decl, is_nil1_decl, cons1_decl, is_cons1_decl, car1_decl, cdr1_decl; Z3_func_decl nil2_decl, is_nil2_decl, cons2_decl, is_cons2_decl, car2_decl, cdr2_decl; @@ -2073,8 +2150,8 @@ void forest_example() { /* nil != cons(nil,nil) */ - prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil1, f1)), Z3_TRUE); - prove(ctx, 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)), Z3_TRUE); + prove(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil2, t1)), Z3_TRUE); /* cons(x,u) = cons(x, v) => u = v */ @@ -2084,18 +2161,19 @@ 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, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE); - prove(ctx, 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)), Z3_TRUE); + prove(ctx, s, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_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, Z3_mk_or(ctx, 2, ors), Z3_TRUE); + prove(ctx, s, Z3_mk_or(ctx, 2, ors), Z3_TRUE); /* occurs check u != cons(x,u) */ - prove(ctx, 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)), Z3_TRUE); /* delete logical context */ + del_solver(ctx, s); Z3_del_context(ctx); } @@ -2108,6 +2186,7 @@ void forest_example() { */ void binary_tree_example() { Z3_context ctx = mk_context(); + Z3_solver s = mk_solver(ctx); Z3_sort cell; Z3_func_decl nil_decl, /* nil : BinTree (constructor) */ @@ -2164,22 +2243,23 @@ void binary_tree_example() { Z3_ast node3 = Z3_mk_app(ctx, node_decl, 3, args3); /* prove that nil != node1 */ - prove(ctx, 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)), Z3_TRUE); /* prove that nil = left(node1) */ - prove(ctx, 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)), Z3_TRUE); /* prove that node1 = right(node3) */ - prove(ctx, 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)), Z3_TRUE); /* prove that !is-nil(node2) */ - prove(ctx, 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)), Z3_TRUE); /* prove that value(node2) >= 0 */ - prove(ctx, 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)), Z3_TRUE); } /* delete logical context */ + del_solver(ctx, s); Z3_del_context(ctx); } @@ -2190,6 +2270,7 @@ void binary_tree_example() { */ void unsat_core_and_proof_example() { Z3_context ctx = mk_proof_context(); + Z3_solver s = mk_solver(ctx); Z3_ast pa = mk_bool_var(ctx, "PredA"); Z3_ast pb = mk_bool_var(ctx, "PredB"); Z3_ast pc = mk_bool_var(ctx, "PredC"); @@ -2210,49 +2291,53 @@ void unsat_core_and_proof_example() { Z3_ast g2[2] = { f2, p2 }; Z3_ast g3[2] = { f3, p3 }; Z3_ast g4[2] = { f4, p4 }; - Z3_ast core[4] = { 0, 0, 0, 0 }; - unsigned core_size = 4; - Z3_ast proof; - Z3_model m = 0; Z3_lbool result; + Z3_ast proof; + Z3_model m = 0; unsigned i; + Z3_ast_vector core; printf("\nunsat_core_and_proof_example\n"); LOG_MSG("unsat_core_and_proof_example"); - Z3_assert_cnstr(ctx, Z3_mk_or(ctx, 2, g1)); - Z3_assert_cnstr(ctx, Z3_mk_or(ctx, 2, g2)); - Z3_assert_cnstr(ctx, Z3_mk_or(ctx, 2, g3)); - Z3_assert_cnstr(ctx, Z3_mk_or(ctx, 2, g4)); + Z3_solver_assert(ctx, s, Z3_mk_or(ctx, 2, g1)); + Z3_solver_assert(ctx, s, Z3_mk_or(ctx, 2, g2)); + Z3_solver_assert(ctx, s, Z3_mk_or(ctx, 2, g3)); + Z3_solver_assert(ctx, s, Z3_mk_or(ctx, 2, g4)); - result = Z3_check_assumptions(ctx, 4, assumptions, &m, &proof, &core_size, core); + result = Z3_solver_check_assumptions(ctx, s, 4, assumptions); switch (result) { case Z3_L_FALSE: + core = Z3_solver_get_unsat_core(ctx, s); + proof = Z3_solver_get_proof(ctx, s); printf("unsat\n"); printf("proof: %s\n", Z3_ast_to_string(ctx, proof)); printf("\ncore:\n"); - for (i = 0; i < core_size; ++i) { - printf("%s\n", Z3_ast_to_string(ctx, core[i])); + for (i = 0; i < Z3_ast_vector_size(ctx, core); ++i) { + printf("%s\n", Z3_ast_to_string(ctx, Z3_ast_vector_get(ctx, core, i))); } printf("\n"); break; case Z3_L_UNDEF: printf("unknown\n"); printf("potential model:\n"); + m = Z3_solver_get_model(ctx, s); + if (m) Z3_model_inc_ref(ctx, m); display_model(ctx, stdout, m); break; case Z3_L_TRUE: printf("sat\n"); + m = Z3_solver_get_model(ctx, s); + if (m) Z3_model_inc_ref(ctx, m); display_model(ctx, stdout, m); break; } - if (m) { - Z3_del_model(ctx, m); - } /* delete logical context */ + if (m) Z3_model_dec_ref(ctx, m); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -2264,6 +2349,7 @@ void unsat_core_and_proof_example() { */ typedef struct { Z3_context m_context; + Z3_solver m_solver; // 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]; @@ -2279,6 +2365,7 @@ typedef Z3_ext_context_struct * Z3_ext_context; Z3_ext_context mk_ext_context() { Z3_ext_context ctx = (Z3_ext_context) malloc(sizeof(Z3_ext_context_struct)); ctx->m_context = mk_context(); + ctx->m_solver = mk_solver(ctx->m_context); ctx->m_num_answer_literals = 0; return ctx; } @@ -2287,6 +2374,7 @@ Z3_ext_context mk_ext_context() { \brief Delete the given logical context wrapper. */ void del_ext_context(Z3_ext_context ctx) { + del_solver(ctx->m_context, ctx->m_solver); Z3_del_context(ctx->m_context); free(ctx); } @@ -2313,7 +2401,7 @@ unsigned assert_retractable_cnstr(Z3_ext_context ctx, Z3_ast c) { // assert: c OR (not ans_lit) args[0] = c; args[1] = Z3_mk_not(ctx->m_context, ans_lit); - Z3_assert_cnstr(ctx->m_context, Z3_mk_or(ctx->m_context, 2, args)); + Z3_solver_assert(ctx->m_context, ctx->m_solver, Z3_mk_or(ctx->m_context, 2, args)); return result; } @@ -2344,10 +2432,8 @@ Z3_lbool ext_check(Z3_ext_context ctx) { Z3_lbool result; unsigned num_assumptions = 0; Z3_ast assumptions[MAX_RETRACTABLE_ASSERTIONS]; - Z3_ast core[MAX_RETRACTABLE_ASSERTIONS]; + Z3_ast_vector core; unsigned core_size; - Z3_ast dummy_proof = 0; // we don't care about the proof in this example. - Z3_model dummy_model = 0; // we don't care about the model in this example. unsigned i; for (i = 0; i < ctx->m_num_answer_literals; i++) { if (ctx->m_retracted[i] == Z3_FALSE) { @@ -2358,15 +2444,18 @@ Z3_lbool ext_check(Z3_ext_context ctx) { num_assumptions ++; } } - result = Z3_check_assumptions(ctx->m_context, num_assumptions, assumptions, &dummy_model, &dummy_proof, &core_size, core); + result = Z3_solver_check_assumptions(ctx->m_context, ctx->m_solver, num_assumptions, assumptions); if (result == Z3_L_FALSE) { // Display the UNSAT core printf("unsat core: "); + core = Z3_solver_get_unsat_core(ctx->m_context, ctx->m_solver); + core_size = Z3_ast_vector_size(ctx->m_context, core); for (i = 0; i < core_size; i++) { + // In this example, we display the core based on the assertion ids. unsigned j; for (j = 0; j < ctx->m_num_answer_literals; j++) { - if (core[i] == ctx->m_answer_literals[j]) { + if (Z3_ast_vector_get(ctx->m_context, core, i) == ctx->m_answer_literals[j]) { printf("%d ", j); break; } @@ -2378,10 +2467,6 @@ Z3_lbool ext_check(Z3_ext_context ctx) { printf("\n"); } - if (dummy_model) { - Z3_del_model(ctx->m_context, dummy_model); - } - return result; } @@ -2452,6 +2537,7 @@ void incremental_example1() { void reference_counter_example() { Z3_config cfg; Z3_context ctx; + Z3_solver s; Z3_sort ty; Z3_ast x, y, x_xor_y; Z3_symbol sx, sy; @@ -2465,6 +2551,8 @@ void reference_counter_example() { // Z3_ast reference counters. ctx = Z3_mk_context_rc(cfg); Z3_del_config(cfg); + s = mk_solver(ctx); + Z3_solver_inc_ref(ctx, s); ty = Z3_mk_bool_sort(ctx); Z3_inc_ref(ctx, Z3_sort_to_ast(ctx, ty)); // Z3_sort_to_ast(ty) is just syntax sugar for ((Z3_ast) ty) @@ -2482,17 +2570,19 @@ void reference_counter_example() { // x and y are not needed anymore. Z3_dec_ref(ctx, x); Z3_dec_ref(ctx, y); - Z3_assert_cnstr(ctx, x_xor_y); + Z3_solver_assert(ctx, s, x_xor_y); // x_or_y is not needed anymore. Z3_dec_ref(ctx, x_xor_y); printf("model for: x xor y\n"); - check(ctx, Z3_L_TRUE); + check(ctx, s, Z3_L_TRUE); // Test push & pop - Z3_push(ctx); - Z3_pop(ctx, 1); + Z3_solver_push(ctx, s); + Z3_solver_pop(ctx, s, 1); + Z3_solver_dec_ref(ctx, s); + del_solver(ctx, s); Z3_del_context(ctx); } @@ -2608,6 +2698,7 @@ void substitute_vars_example() { void fpa_example() { Z3_config cfg; Z3_context ctx; + Z3_solver s; Z3_sort double_sort, rm_sort; Z3_symbol s_rm, s_x, s_y, s_x_plus_y; Z3_ast rm, x, y, n, x_plus_y, c1, c2, c3, c4, c5; @@ -2618,6 +2709,7 @@ void fpa_example() { cfg = Z3_mk_config(); ctx = Z3_mk_context(cfg); + s = mk_solver(ctx); Z3_del_config(cfg); double_sort = Z3_mk_fpa_sort(ctx, 11, 53); @@ -2652,10 +2744,10 @@ void fpa_example() { c4 = Z3_mk_and(ctx, 2, (Z3_ast*)&args3); printf("c4: %s\n", Z3_ast_to_string(ctx, c4)); - Z3_push(ctx); - Z3_assert_cnstr(ctx, c4); - check(ctx, Z3_L_TRUE); - Z3_pop(ctx, 1); + Z3_solver_push(ctx, s); + Z3_solver_assert(ctx, s, c4); + check(ctx, s, Z3_L_TRUE); + Z3_solver_pop(ctx, s, 1); // Show that the following are equal: // (fp #b0 #b10000000001 #xc000000000000) @@ -2663,7 +2755,7 @@ void fpa_example() { // ((_ to_fp 11 53) RTZ 1.75 2))) // ((_ to_fp 11 53) RTZ 7.0))) - Z3_push(ctx); + Z3_solver_push(ctx, s); c1 = Z3_mk_fpa_fp(ctx, Z3_mk_numeral(ctx, "0", Z3_mk_bv_sort(ctx, 1)), Z3_mk_numeral(ctx, "3377699720527872", Z3_mk_bv_sort(ctx, 52)), @@ -2686,10 +2778,11 @@ void fpa_example() { c5 = Z3_mk_and(ctx, 3, args3); printf("c5: %s\n", Z3_ast_to_string(ctx, c5)); - Z3_assert_cnstr(ctx, c5); - check(ctx, Z3_L_TRUE); - Z3_pop(ctx, 1); + Z3_solver_assert(ctx, s, c5); + check(ctx, s, Z3_L_TRUE); + Z3_solver_pop(ctx, s, 1); + del_solver(ctx, s); Z3_del_context(ctx); } diff --git a/examples/interp/iz3.cpp b/examples/interp/iz3.cpp index 21ea518a6..915d3ba54 100755 --- a/examples/interp/iz3.cpp +++ b/examples/interp/iz3.cpp @@ -9,7 +9,7 @@ Copyright (c) 2015 Microsoft Corporation #include #include #include -#include "z3.h" +#include "z3++.h" @@ -40,7 +40,7 @@ int main(int argc, const char **argv) { bool anonymize = false; bool write = false; - Z3_config cfg = Z3_mk_config(); + z3::config cfg; // Z3_interpolation_options options = Z3_mk_interpolation_options(); // Z3_params options = 0; @@ -87,7 +87,7 @@ int main(int argc, const char **argv) { /* Create a Z3 context to contain formulas */ - Z3_context ctx = Z3_mk_interpolation_context(cfg); + z3::context ctx(cfg, z3::context::interpolation()); if(write || anonymize) Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB2_COMPLIANT); @@ -145,12 +145,12 @@ int main(int argc, const char **argv) { /* Compute an interpolant, or get a model. */ Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast)); - Z3_model model = 0; + Z3_model z3model = 0; Z3_lbool result; if(!incremental_mode){ /* In non-incremental mode, we just pass the constraints. */ - result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, constraints, parents, options, interpolants, &model, 0, false, num_theory, theory); + result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, constraints, parents, options, interpolants, &z3model, 0, false, num_theory, theory); } else { @@ -159,28 +159,26 @@ int main(int argc, const char **argv) { iZ3 in an array, so iZ3 knows the sequence. Note it's safe to pass "true", even though we haven't techically asserted if. */ - Z3_push(ctx); - std::vector asserted(num); + z3::solver s(ctx); + z3::expr_vector asserted(ctx), saved_interpolants(ctx); /* We start with nothing asserted. */ - for(unsigned i = 0; i < num; i++) - asserted[i] = Z3_mk_true(ctx); + for(unsigned i = 0; i < num; i++) asserted.push_back(ctx.bool_val(true)); /* Now we assert the constrints one at a time until UNSAT. */ for(unsigned i = 0; i < num; i++){ - asserted[i] = constraints[i]; - Z3_assert_cnstr(ctx,constraints[i]); // assert one constraint - result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, &asserted[0], parents, options, interpolants, &model, 0, true, 0, 0); + asserted[i] = z3::expr(ctx, constraints[i]); + s.add(asserted[i]); + result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, &asserted[0], parents, options, interpolants, &z3model, 0, true, 0, 0); if(result == Z3_L_FALSE){ for(unsigned j = 0; j < num-1; j++) /* Since we want the interpolant formulas to survive a "pop", we "persist" them here. */ - Z3_persist_ast(ctx,interpolants[j],1); + saved_interpolants.push_back(z3::expr(ctx, interpolants[j])); break; } } - Z3_pop(ctx,1); } switch (result) { @@ -219,21 +217,14 @@ int main(int argc, const char **argv) { break; case Z3_L_TRUE: printf("sat\n"); - printf("model:\n%s\n", Z3_model_to_string(ctx, model)); + printf("model:\n%s\n", Z3_model_to_string(ctx, z3model)); break; } if(profile_mode) std::cout << Z3_interpolation_profile(ctx); - /* Delete the model if there is one */ - if (model) - Z3_del_model(ctx, model); - - /* Delete logical context. */ - - Z3_del_context(ctx); free(interpolants); return 0; diff --git a/examples/maxsat/maxsat.c b/examples/maxsat/maxsat.c index 8f747cb98..dc79357b9 100644 --- a/examples/maxsat/maxsat.c +++ b/examples/maxsat/maxsat.c @@ -163,11 +163,11 @@ void free_cnstr_array(Z3_ast * cnstrs) /** \brief Assert hard constraints stored in the given array. */ -void assert_hard_constraints(Z3_context ctx, unsigned num_cnstrs, Z3_ast * cnstrs) +void assert_hard_constraints(Z3_context ctx, Z3_solver s, unsigned num_cnstrs, Z3_ast * cnstrs) { unsigned i; for (i = 0; i < num_cnstrs; i++) { - Z3_assert_cnstr(ctx, cnstrs[i]); + Z3_solver_assert(ctx, s, cnstrs[i]); } } @@ -176,14 +176,14 @@ void assert_hard_constraints(Z3_context ctx, unsigned num_cnstrs, Z3_ast * cnstr This funtion 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, unsigned num_cnstrs, Z3_ast * cnstrs) +Z3_ast * assert_soft_constraints(Z3_context ctx, Z3_solver s, unsigned num_cnstrs, Z3_ast * cnstrs) { unsigned i; Z3_ast * aux_vars; aux_vars = mk_fresh_bool_var_array(ctx, num_cnstrs); for (i = 0; i < num_cnstrs; i++) { Z3_ast assumption = cnstrs[i]; - Z3_assert_cnstr(ctx, mk_binary_or(ctx, assumption, aux_vars[i])); + Z3_solver_assert(ctx, s, mk_binary_or(ctx, assumption, aux_vars[i])); } return aux_vars; } @@ -299,7 +299,7 @@ int get_bit(unsigned val, unsigned idx) /** \brief Given an integer val encoded in n bits (boolean variables), assert the constraint that val <= k. */ -void assert_le_k(Z3_context ctx, unsigned n, Z3_ast * val, unsigned k) +void assert_le_k(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * val, unsigned k) { Z3_ast i1, i2, not_val, out; unsigned idx; @@ -321,7 +321,7 @@ void assert_le_k(Z3_context ctx, unsigned n, Z3_ast * val, unsigned k) out = mk_ternary_or(ctx, i1, i2, mk_binary_and(ctx, not_val, out)); } // printf("at-most-k:\n%s\n", Z3_ast_to_string(ctx, out)); - Z3_assert_cnstr(ctx, out); + Z3_solver_assert(ctx, s, out); } /** @@ -331,14 +331,14 @@ void assert_le_k(Z3_context ctx, unsigned n, Z3_ast * val, unsigned k) We use a simple encoding using an adder (counter). An interesting exercise consists in implementing more sophisticated encodings. */ -void assert_at_most_k(Z3_context ctx, unsigned n, Z3_ast * lits, unsigned k) +void assert_at_most_k(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * lits, unsigned k) { Z3_ast * counter_bits; unsigned counter_bits_sz; if (k >= n || n <= 1) return; /* nothing to be done */ counter_bits = mk_counter_circuit(ctx, n, lits, &counter_bits_sz); - assert_le_k(ctx, counter_bits_sz, counter_bits, k); + assert_le_k(ctx, s, counter_bits_sz, counter_bits, k); del_bool_var_array(counter_bits); } @@ -346,9 +346,9 @@ void assert_at_most_k(Z3_context ctx, unsigned n, Z3_ast * lits, unsigned k) \brief Assert that at most one literal in \c lits can be true, where \c n is the number of literals in lits. */ -void assert_at_most_one(Z3_context ctx, unsigned n, Z3_ast * lits) +void assert_at_most_one(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * lits) { - assert_at_most_k(ctx, n, lits, 1); + assert_at_most_k(ctx, s, n, lits, 1); } /** @@ -357,6 +357,7 @@ void assert_at_most_one(Z3_context ctx, unsigned n, Z3_ast * lits) void tst_at_most_one() { Z3_context ctx = mk_context(); + Z3_solver s = Z3_mk_solver(ctx); Z3_ast k1 = mk_bool_var(ctx, "k1"); Z3_ast k2 = mk_bool_var(ctx, "k2"); Z3_ast k3 = mk_bool_var(ctx, "k3"); @@ -368,29 +369,25 @@ void tst_at_most_one() Z3_model m = 0; Z3_lbool result; printf("testing at-most-one constraint\n"); - assert_at_most_one(ctx, 5, args1); - assert_at_most_one(ctx, 3, args2); + assert_at_most_one(ctx, s, 5, args1); + assert_at_most_one(ctx, s, 3, args2); printf("it must be sat...\n"); - result = Z3_check_and_get_model(ctx, &m); + result = Z3_solver_check(ctx, s); if (result != Z3_L_TRUE) error("BUG"); + m = Z3_solver_get_model(ctx, s); printf("model:\n%s\n", Z3_model_to_string(ctx, m)); - if (m) { - Z3_del_model(ctx, m); - } - Z3_assert_cnstr(ctx, mk_binary_or(ctx, k2, k3)); - Z3_assert_cnstr(ctx, mk_binary_or(ctx, k1, k6)); + Z3_solver_assert(ctx, s, mk_binary_or(ctx, k2, k3)); + Z3_solver_assert(ctx, s, mk_binary_or(ctx, k1, k6)); printf("it must be sat...\n"); - result = Z3_check_and_get_model(ctx, &m); + result = Z3_solver_check(ctx, s); if (result != Z3_L_TRUE) error("BUG"); + m = Z3_solver_get_model(ctx, s); printf("model:\n%s\n", Z3_model_to_string(ctx, m)); - if (m) { - Z3_del_model(ctx, m); - } - Z3_assert_cnstr(ctx, mk_binary_or(ctx, k4, k5)); + Z3_solver_assert(ctx, s, mk_binary_or(ctx, k4, k5)); printf("it must be unsat...\n"); - result = Z3_check_and_get_model(ctx, &m); + result = Z3_solver_check(ctx, s); if (result != Z3_L_FALSE) error("BUG"); Z3_del_context(ctx); @@ -407,7 +404,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_eval(ctx, m, aux_vars[i], &val) == Z3_TRUE) { + if (Z3_model_eval(ctx, m, aux_vars[i], 1, &val) == Z3_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)) { @@ -428,21 +425,21 @@ unsigned get_num_disabled_soft_constraints(Z3_context ctx, Z3_model m, unsigned Exercise: use binary search to implement MaxSAT. Hint: you will need to use an answer literal to retract the at-most-k constraint. */ -int naive_maxsat(Z3_context ctx, unsigned num_hard_cnstrs, Z3_ast * hard_cnstrs, unsigned num_soft_cnstrs, Z3_ast * soft_cnstrs) +int naive_maxsat(Z3_context ctx, Z3_solver s, unsigned num_hard_cnstrs, Z3_ast * hard_cnstrs, unsigned num_soft_cnstrs, Z3_ast * soft_cnstrs) { Z3_ast * aux_vars; Z3_lbool is_sat; unsigned r, k; - assert_hard_constraints(ctx, num_hard_cnstrs, hard_cnstrs); + assert_hard_constraints(ctx, s, num_hard_cnstrs, hard_cnstrs); printf("checking whether hard constraints are satisfiable...\n"); - is_sat = Z3_check(ctx); + is_sat = Z3_solver_check(ctx, s); if (is_sat == Z3_L_FALSE) { // It is not possible to make the formula satisfiable even when ignoring all soft constraints. return -1; } if (num_soft_cnstrs == 0) return 0; // nothing to be done... - aux_vars = assert_soft_constraints(ctx, num_soft_cnstrs, soft_cnstrs); + aux_vars = assert_soft_constraints(ctx, s, num_soft_cnstrs, soft_cnstrs); // Perform linear search. r = 0; k = num_soft_cnstrs - 1; @@ -451,19 +448,17 @@ int naive_maxsat(Z3_context ctx, unsigned num_hard_cnstrs, Z3_ast * hard_cnstrs, unsigned num_disabled; // at most k soft-constraints can be ignored. printf("checking whether at-most %d soft-constraints can be ignored.\n", k); - assert_at_most_k(ctx, num_soft_cnstrs, aux_vars, k); - is_sat = Z3_check_and_get_model(ctx, &m); + assert_at_most_k(ctx, s, num_soft_cnstrs, aux_vars, k); + is_sat = Z3_solver_check(ctx, s); if (is_sat == Z3_L_FALSE) { printf("unsat\n"); return num_soft_cnstrs - k - 1; } + m = Z3_solver_get_model(ctx, s); num_disabled = get_num_disabled_soft_constraints(ctx, m, num_soft_cnstrs, aux_vars); if (num_disabled > k) { error("BUG"); } - if (m) { - Z3_del_model(ctx, m); - } printf("sat\n"); k = num_disabled; if (k == 0) { @@ -489,28 +484,27 @@ int naive_maxsat(Z3_context ctx, unsigned num_hard_cnstrs, Z3_ast * hard_cnstrs, - replace aux-var with a new one * add at-most-one constraint with blocking */ -int fu_malik_maxsat_step(Z3_context ctx, unsigned num_soft_cnstrs, Z3_ast * soft_cnstrs, Z3_ast * aux_vars) +int fu_malik_maxsat_step(Z3_context ctx, Z3_solver s, unsigned num_soft_cnstrs, Z3_ast * soft_cnstrs, Z3_ast * aux_vars) { // create assumptions Z3_ast * assumptions = (Z3_ast*) malloc(sizeof(Z3_ast) * num_soft_cnstrs); - Z3_ast * core = (Z3_ast*) malloc(sizeof(Z3_ast) * num_soft_cnstrs); - unsigned core_size; - Z3_ast dummy_proof; // we don't care about proofs in this example - Z3_model m; Z3_lbool is_sat; + Z3_ast_vector core; + unsigned core_size; unsigned i = 0; for (i = 0; i < num_soft_cnstrs; i++) { // Recall that we asserted (soft_cnstrs[i] \/ aux_vars[i]) // So using (NOT aux_vars[i]) as an assumption we are actually forcing the soft_cnstrs[i] to be considered. assumptions[i] = Z3_mk_not(ctx, aux_vars[i]); - core[i] = 0; } - is_sat = Z3_check_assumptions(ctx, num_soft_cnstrs, assumptions, &m, &dummy_proof, &core_size, core); + is_sat = Z3_solver_check_assumptions(ctx, s, num_soft_cnstrs, assumptions); if (is_sat != Z3_L_FALSE) { return 1; // done } else { + core = Z3_solver_get_unsat_core(ctx, s); + core_size = Z3_ast_vector_size(ctx, core); Z3_ast * block_vars = (Z3_ast*) malloc(sizeof(Z3_ast) * core_size); unsigned k = 0; // update soft-constraints and aux_vars @@ -518,7 +512,7 @@ int fu_malik_maxsat_step(Z3_context ctx, unsigned num_soft_cnstrs, Z3_ast * soft unsigned j; // check whether assumption[i] is in the core or not for (j = 0; j < core_size; j++) { - if (assumptions[i] == core[j]) + if (assumptions[i] == Z3_ast_vector_get(ctx, core, j)) break; } if (j < core_size) { @@ -531,10 +525,10 @@ int fu_malik_maxsat_step(Z3_context ctx, unsigned num_soft_cnstrs, Z3_ast * soft k++; // Add new constraint containing the block variable. // Note that we are using the new auxiliary variable to be able to use it as an assumption. - Z3_assert_cnstr(ctx, mk_binary_or(ctx, soft_cnstrs[i], new_aux_var)); + Z3_solver_assert(ctx, s, mk_binary_or(ctx, soft_cnstrs[i], new_aux_var)); } } - assert_at_most_one(ctx, k, block_vars); + assert_at_most_one(ctx, s, k, block_vars); return 0; // not done. } } @@ -553,14 +547,14 @@ int fu_malik_maxsat_step(Z3_context ctx, unsigned num_soft_cnstrs, Z3_ast * soft Z. Fu and S. Malik, On solving the partial MAX-SAT problem, in International Conference on Theory and Applications of Satisfiability Testing, 2006. */ -int fu_malik_maxsat(Z3_context ctx, unsigned num_hard_cnstrs, Z3_ast * hard_cnstrs, unsigned num_soft_cnstrs, Z3_ast * soft_cnstrs) +int fu_malik_maxsat(Z3_context ctx, Z3_solver s, unsigned num_hard_cnstrs, Z3_ast * hard_cnstrs, unsigned num_soft_cnstrs, Z3_ast * soft_cnstrs) { Z3_ast * aux_vars; Z3_lbool is_sat; unsigned k; - assert_hard_constraints(ctx, num_hard_cnstrs, hard_cnstrs); + assert_hard_constraints(ctx, s, num_hard_cnstrs, hard_cnstrs); printf("checking whether hard constraints are satisfiable...\n"); - is_sat = Z3_check(ctx); + is_sat = Z3_solver_check(ctx, s); if (is_sat == Z3_L_FALSE) { // It is not possible to make the formula satisfiable even when ignoring all soft constraints. return -1; @@ -571,11 +565,11 @@ int fu_malik_maxsat(Z3_context ctx, unsigned num_hard_cnstrs, Z3_ast * hard_cnst Fu&Malik algorithm is based on UNSAT-core extraction. We accomplish that using auxiliary variables (aka answer literals). */ - aux_vars = assert_soft_constraints(ctx, num_soft_cnstrs, soft_cnstrs); + aux_vars = assert_soft_constraints(ctx, s, num_soft_cnstrs, soft_cnstrs); k = 0; for (;;) { printf("iteration %d\n", k); - if (fu_malik_maxsat_step(ctx, num_soft_cnstrs, soft_cnstrs, aux_vars)) { + if (fu_malik_maxsat_step(ctx, s, num_soft_cnstrs, soft_cnstrs, aux_vars)) { return num_soft_cnstrs - k; } k++; @@ -596,19 +590,21 @@ int fu_malik_maxsat(Z3_context ctx, unsigned num_hard_cnstrs, Z3_ast * hard_cnst int smtlib_maxsat(char * file_name, int approach) { Z3_context ctx; + Z3_solver s; unsigned num_hard_cnstrs, num_soft_cnstrs; Z3_ast * hard_cnstrs, * soft_cnstrs; unsigned result = 0; ctx = mk_context(); + s = Z3_mk_solver(ctx); Z3_parse_smtlib_file(ctx, file_name, 0, 0, 0, 0, 0, 0); hard_cnstrs = get_hard_constraints(ctx, &num_hard_cnstrs); soft_cnstrs = get_soft_constraints(ctx, &num_soft_cnstrs); switch (approach) { case NAIVE_MAXSAT: - result = naive_maxsat(ctx, num_hard_cnstrs, hard_cnstrs, num_soft_cnstrs, soft_cnstrs); + result = naive_maxsat(ctx, s, num_hard_cnstrs, hard_cnstrs, num_soft_cnstrs, soft_cnstrs); break; case FU_MALIK_MAXSAT: - result = fu_malik_maxsat(ctx, num_hard_cnstrs, hard_cnstrs, num_soft_cnstrs, soft_cnstrs); + result = fu_malik_maxsat(ctx, s, num_hard_cnstrs, hard_cnstrs, num_soft_cnstrs, soft_cnstrs); break; default: /* Exercise: implement your own MaxSAT algorithm.*/ diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 200b483cf..4087b1639 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -136,20 +136,6 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_label(Z3_context c, Z3_symbol s, Z3_bool is_pos, Z3_ast f) { - Z3_TRY; - LOG_Z3_mk_label(c, s, is_pos, f); - RESET_ERROR_CODE(); - expr* _f = to_expr(f); - if (!mk_c(c)->m().is_bool(_f)) { - SET_ERROR_CODE(Z3_SORT_ERROR); - return f; - } - expr* a = mk_c(c)->m().mk_label(is_pos != 0, to_symbol(s), _f); - mk_c(c)->save_ast_trail(a); - RETURN_Z3(of_ast(a)); - Z3_CATCH_RETURN(0); - } Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, const char * prefix, unsigned domain_size, Z3_sort const domain[], Z3_sort range) { diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index f17a296fa..9c1701c44 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -32,8 +32,8 @@ void install_tactics(tactic_manager & ctx); namespace api { - static void default_error_handler(Z3_context, Z3_error_code c) { - printf("Error: %s\n", Z3_get_error_msg(c)); + static void default_error_handler(Z3_context ctx, Z3_error_code c) { + printf("Error: %s\n", Z3_get_error_msg_ex(ctx, c)); exit(1); } @@ -209,6 +209,7 @@ namespace api { } } } +#if 0 void context::persist_ast(ast * n, unsigned num_scopes) { // persist_ast is irrelevant when m_user_ref_count == true if (m_user_ref_count) @@ -223,6 +224,7 @@ namespace api { } m_replay_stack[j]->push_back(n); } +#endif void context::save_ast_trail(ast * n) { SASSERT(m().contains(n)); @@ -478,13 +480,6 @@ extern "C" { Z3_CATCH; } - Z3_bool Z3_API Z3_set_logic(Z3_context c, Z3_string logic) { - Z3_TRY; - LOG_Z3_set_logic(c, logic); - RESET_ERROR_CODE(); - return mk_c(c)->get_smt_kernel().set_logic(symbol(logic)); - Z3_CATCH_RETURN(Z3_FALSE); - } void Z3_API Z3_get_version(unsigned * major, unsigned * minor, @@ -555,24 +550,12 @@ extern "C" { } } - Z3_API char const * Z3_get_error_msg(Z3_error_code err) { - LOG_Z3_get_error_msg(err); - return _get_error_msg_ex(0, err); - } Z3_API char const * Z3_get_error_msg_ex(Z3_context c, Z3_error_code err) { LOG_Z3_get_error_msg_ex(c, err); return _get_error_msg_ex(c, err); } - void Z3_API Z3_persist_ast(Z3_context c, Z3_ast n, unsigned num_scopes) { - Z3_TRY; - LOG_Z3_persist_ast(c, n, num_scopes); - RESET_ERROR_CODE(); - CHECK_VALID_AST(to_ast(n), ); - mk_c(c)->persist_ast(to_ast(n), num_scopes); - Z3_CATCH; - } void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode) { Z3_TRY; diff --git a/src/api/api_context.h b/src/api/api_context.h index 3d5f0c2bf..d8331e2f8 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -155,7 +155,7 @@ namespace api { expr * mk_and(unsigned num_exprs, expr * const * exprs); // Hack for preventing an AST for being GC when ref-count is not used - void persist_ast(ast * n, unsigned num_scopes); + // void persist_ast(ast * n, unsigned num_scopes); // "Save" an AST that will exposed to the "external" world. void save_ast_trail(ast * n); diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index 633d51fab..370e639b9 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -140,7 +140,7 @@ extern "C" { Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i) { Z3_TRY; - LOG_Z3_get_model_func_decl(c, m, i); + LOG_Z3_model_get_func_decl(c, m, i); RESET_ERROR_CODE(); Z3_func_decl r = get_model_func_decl_core(c, m, i); RETURN_Z3(r); @@ -368,26 +368,6 @@ extern "C" { return Z3_model_get_func_decl(c, m, i); } - Z3_ast Z3_API Z3_get_model_func_else(Z3_context c, Z3_model m, unsigned i) { - Z3_TRY; - LOG_Z3_get_model_func_else(c, m, i); - RESET_ERROR_CODE(); - CHECK_NON_NULL(m, 0); - Z3_func_decl d = get_model_func_decl_core(c, m, i); - if (d) { - model * _m = to_model_ref(m); - func_interp * g = _m->get_func_interp(to_func_decl(d)); - if (g) { - expr * e = g->get_else(); - mk_c(c)->save_ast_trail(e); - RETURN_Z3(of_ast(e)); - } - SET_ERROR_CODE(Z3_IOB); - RETURN_Z3(0); - } - RETURN_Z3(0); - Z3_CATCH_RETURN(0); - } unsigned get_model_func_num_entries_core(Z3_context c, Z3_model m, unsigned i) { RESET_ERROR_CODE(); @@ -405,12 +385,6 @@ extern "C" { return 0; } - unsigned Z3_API Z3_get_model_func_num_entries(Z3_context c, Z3_model m, unsigned i) { - Z3_TRY; - LOG_Z3_get_model_func_num_entries(c, m, i); - return get_model_func_num_entries_core(c, m, i); - Z3_CATCH_RETURN(0); - } unsigned get_model_func_entry_num_args_core(Z3_context c, Z3_model m, @@ -431,238 +405,6 @@ extern "C" { return 0; } - unsigned Z3_API Z3_get_model_func_entry_num_args(Z3_context c, - Z3_model m, - unsigned i, - unsigned j) { - Z3_TRY; - LOG_Z3_get_model_func_entry_num_args(c, m, i, j); - return get_model_func_entry_num_args_core(c, m, i, j); - Z3_CATCH_RETURN(0); - } - - Z3_ast Z3_API Z3_get_model_func_entry_arg(Z3_context c, - Z3_model m, - unsigned i, - unsigned j, - unsigned k) { - Z3_TRY; - LOG_Z3_get_model_func_entry_arg(c, m, i, j, k); - RESET_ERROR_CODE(); - CHECK_NON_NULL(m, 0); - if (j >= get_model_func_num_entries_core(c, m, i) || k >= get_model_func_entry_num_args_core(c, m, i, j)) { - SET_ERROR_CODE(Z3_IOB); - RETURN_Z3(0); - } - Z3_func_decl d = get_model_func_decl_core(c, m, i); - if (d) { - model * _m = to_model_ref(m); - func_interp * g = _m->get_func_interp(to_func_decl(d)); - if (g && j < g->num_entries()) { - func_entry const * e = g->get_entry(j); - if (k < g->get_arity()) { - expr * a = e->get_arg(k); - mk_c(c)->save_ast_trail(a); - RETURN_Z3(of_ast(a)); - } - } - SET_ERROR_CODE(Z3_IOB); - RETURN_Z3(0); - } - RETURN_Z3(0); - Z3_CATCH_RETURN(0); - } - - Z3_ast Z3_API Z3_get_model_func_entry_value(Z3_context c, - Z3_model m, - unsigned i, - unsigned j) { - Z3_TRY; - LOG_Z3_get_model_func_entry_value(c, m, i, j); - RESET_ERROR_CODE(); - CHECK_NON_NULL(m, 0); - if (j >= get_model_func_num_entries_core(c, m, i)) { - SET_ERROR_CODE(Z3_IOB); - RETURN_Z3(0); - } - Z3_func_decl d = get_model_func_decl_core(c, m, i); - if (d) { - model * _m = to_model_ref(m); - func_interp * g = _m->get_func_interp(to_func_decl(d)); - if (g && j < g->num_entries()) { - func_entry const* e = g->get_entry(j); - expr* a = e->get_result(); - mk_c(c)->save_ast_trail(a); - RETURN_Z3(of_ast(a)); - } - SET_ERROR_CODE(Z3_IOB); - RETURN_Z3(0); - } - RETURN_Z3(0); - Z3_CATCH_RETURN(0); - } - - Z3_bool Z3_API Z3_eval(Z3_context c, - Z3_model m, - Z3_ast t, - Z3_ast * v) { - model_evaluator_params p; - return Z3_model_eval(c, m, t, p.completion(), v); - } - - Z3_bool Z3_API Z3_eval_func_decl(Z3_context c, - Z3_model m, - Z3_func_decl decl, - Z3_ast* v) { - Z3_TRY; - LOG_Z3_eval_func_decl(c, m, decl, v); - RESET_ERROR_CODE(); - CHECK_NON_NULL(m, Z3_FALSE); - ast_manager & mgr = mk_c(c)->m(); - model * _m = to_model_ref(m); - expr_ref result(mgr); - if( _m->eval(to_func_decl(decl), result)) { - mk_c(c)->save_ast_trail(result.get()); - *v = of_ast(result.get()); - RETURN_Z3_eval_func_decl Z3_TRUE; - } - else { - return Z3_FALSE; - } - Z3_CATCH_RETURN(Z3_FALSE); - } - - - Z3_bool Z3_API Z3_is_array_value(Z3_context c, Z3_model _m, Z3_ast _v, unsigned* size) { - Z3_TRY; - LOG_Z3_is_array_value(c, _m, _v, size); - RESET_ERROR_CODE(); - CHECK_NON_NULL(_v, Z3_FALSE); - CHECK_NON_NULL(_m, Z3_FALSE); - model * m = to_model_ref(_m); - expr * v = to_expr(_v); - ast_manager& mgr = mk_c(c)->m(); - family_id afid = mk_c(c)->get_array_fid(); - unsigned sz = 0; - array_util pl(mgr); - if (pl.is_as_array(v)) { - func_decl* f = pl.get_as_array_func_decl(to_app(v)); - func_interp* g = m->get_func_interp(f); - sz = g->num_entries(); - if (sz > 0 && g->get_arity() != 1) { - return Z3_FALSE; - } - } - else { - while (pl.is_store(v)) { - if (to_app(v)->get_num_args() != 3) { - return Z3_FALSE; - } - v = to_app(v)->get_arg(0); - ++sz; - } - if (!is_app_of(v, afid, OP_CONST_ARRAY)) { - return Z3_FALSE; - } - } - if (size) { - *size = sz; - } - return Z3_TRUE; - Z3_CATCH_RETURN(Z3_FALSE); - } - - - void Z3_API Z3_get_array_value(Z3_context c, - Z3_model _m, - Z3_ast _v, - unsigned num_entries, - Z3_ast indices[], - Z3_ast values[], - Z3_ast* else_value) { - Z3_TRY; - LOG_Z3_get_array_value(c, _m, _v, num_entries, indices, values, else_value); - RESET_ERROR_CODE(); - CHECK_NON_NULL(_m, ); - model * m = to_model_ref(_m); - - expr* v = to_expr(_v); - family_id afid = mk_c(c)->get_array_fid(); - ast_manager& mgr = mk_c(c)->m(); - array_util pl(mgr); - - // - // note: _v is already reference counted. - // saving the trail for the returned values - // is redundant. - // - unsigned sz = 0; - if (pl.is_as_array(v)) { - func_decl* f = pl.get_as_array_func_decl(to_app(v)); - func_interp* g = m->get_func_interp(f); - sz = g->num_entries(); - if (g->get_arity() != 1) { - SET_ERROR_CODE(Z3_INVALID_ARG); - return; - } - for (unsigned i = 0; i < sz && i < num_entries; ++i) { - indices[i] = of_ast(g->get_entry(i)->get_arg(0)); - values[i] = of_ast(g->get_entry(i)->get_result()); - } - if (else_value) { - *else_value = of_ast(g->get_else()); - } - } - else { - while (sz <= num_entries && is_app_of(v, afid, OP_STORE)) { - app* a = to_app(v); - if (a->get_num_args() != 3) { - SET_ERROR_CODE(Z3_INVALID_ARG); - return; - } - expr* idx = a->get_arg(1); - expr* val = a->get_arg(2); - indices[sz] = of_ast(idx); - values[sz] = of_ast(val); - v = to_app(v)->get_arg(0); - ++sz; - } - - if (is_app_of(v, afid, OP_CONST_ARRAY)) { - if (else_value) { - *else_value = of_ast(to_app(v)->get_arg(0)); - } - } - else { - SET_ERROR_CODE(Z3_INVALID_ARG); - return; - } - } - RETURN_Z3_get_array_value; - Z3_CATCH; - } - - Z3_bool Z3_API Z3_eval_decl(Z3_context c, - Z3_model m, - Z3_func_decl d, - unsigned num_args, - Z3_ast const args[], - Z3_ast* v) { - Z3_TRY; - LOG_Z3_eval_decl(c, m, d, num_args, args, v); - RESET_ERROR_CODE(); - CHECK_NON_NULL(m, Z3_FALSE); - ast_manager & mgr = mk_c(c)->m(); - model * _m = to_model_ref(m); - app_ref app(mgr); - app = mgr.mk_app(to_func_decl(d), num_args, to_exprs(args)); - expr_ref result(mgr); - _m->eval(app.get(), result); - mk_c(c)->save_ast_trail(result.get()); - *v = of_ast(result.get()); - RETURN_Z3_eval_decl Z3_TRUE; - Z3_CATCH_RETURN(Z3_FALSE); - } Z3_API char const * Z3_model_to_string(Z3_context c, Z3_model m) { Z3_TRY; diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp index 727005186..cfaf5b6df 100644 --- a/src/api/api_quant.cpp +++ b/src/api/api_quant.cpp @@ -466,42 +466,6 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_func_decl Z3_API Z3_mk_injective_function(Z3_context c, - Z3_symbol s, - unsigned domain_size, - Z3_sort const domain[], - Z3_sort range) { - Z3_TRY; - LOG_Z3_mk_injective_function(c, s, domain_size, domain, range); - RESET_ERROR_CODE(); - ast_manager & m = mk_c(c)->m(); - mk_c(c)->reset_last_result(); - sort* range_ = to_sort(range); - func_decl* d = m.mk_func_decl(to_symbol(s), domain_size, to_sorts(domain), range_); - expr_ref_vector args(m); - expr_ref fn(m), body(m); - vector names; - for (unsigned i = 0; i < domain_size; ++i) { - unsigned idx = domain_size-i-1; - args.push_back(m.mk_var(idx, to_sort(domain[i]))); - names.push_back(symbol(idx)); - } - fn = m.mk_app(d, args.size(), args.c_ptr()); - - for (unsigned i = 0; i < domain_size; ++i) { - expr* arg = args[i].get(); - sort* dom = m.get_sort(arg); - func_decl* inv = m.mk_fresh_func_decl(symbol("inv"), to_symbol(s), 1, &range_, dom); - body = m.mk_eq(m.mk_app(inv, fn.get()), arg); - body = m.mk_forall(args.size(), to_sorts(domain), names.c_ptr(), body.get()); - mk_c(c)->save_multiple_ast_trail(body.get()); - mk_c(c)->assert_cnstr(body.get()); - } - mk_c(c)->save_multiple_ast_trail(d); - RETURN_Z3(of_func_decl(d)); - Z3_CATCH_RETURN(0); - } - Z3_ast Z3_API Z3_pattern_to_ast(Z3_context c, Z3_pattern p) { RESET_ERROR_CODE(); return (Z3_ast)(p); diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 6112a8cd2..77848900e 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -391,6 +391,7 @@ extern "C" { } +#if 0 Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c, Z3_solver s, unsigned num_terms, @@ -406,5 +407,6 @@ extern "C" { return static_cast(result); Z3_CATCH_RETURN(Z3_L_UNDEF); } +#endif }; diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp index fbd57ad97..b4911698c 100644 --- a/src/api/api_solver_old.cpp +++ b/src/api/api_solver_old.cpp @@ -21,332 +21,7 @@ Revision History: #include"z3.h" #include"api_log_macros.h" #include"api_context.h" -#include"api_model.h" -#include"cancel_eh.h" -#include"scoped_timer.h" -#include"rlimit.h" -extern "C" { - - void Z3_API Z3_push(Z3_context c) { - Z3_TRY; - LOG_Z3_push(c); - RESET_ERROR_CODE(); - CHECK_SEARCHING(c); - mk_c(c)->push(); - Z3_CATCH; - } - - void Z3_API Z3_pop(Z3_context c, unsigned num_scopes) { - Z3_TRY; - LOG_Z3_pop(c, num_scopes); - RESET_ERROR_CODE(); - CHECK_SEARCHING(c); - if (num_scopes > mk_c(c)->get_num_scopes()) { - SET_ERROR_CODE(Z3_IOB); - return; - } - if (num_scopes > 0) { - mk_c(c)->pop(num_scopes); - } - Z3_CATCH; - } - - unsigned Z3_API Z3_get_num_scopes(Z3_context c) { - Z3_TRY; - LOG_Z3_get_num_scopes(c); - RESET_ERROR_CODE(); - return mk_c(c)->get_num_scopes(); - Z3_CATCH_RETURN(0); - } - - void Z3_API Z3_assert_cnstr(Z3_context c, Z3_ast a) { - Z3_TRY; - LOG_Z3_assert_cnstr(c, a); - RESET_ERROR_CODE(); - CHECK_FORMULA(a,); - mk_c(c)->assert_cnstr(to_expr(a)); - Z3_CATCH; - } - - Z3_lbool Z3_API Z3_check_and_get_model(Z3_context c, Z3_model * m) { - Z3_TRY; - LOG_Z3_check_and_get_model(c, m); - RESET_ERROR_CODE(); - CHECK_SEARCHING(c); - cancel_eh eh(mk_c(c)->get_smt_kernel()); - api::context::set_interruptable si(*(mk_c(c)), eh); - flet _model(mk_c(c)->fparams().m_model, true); - unsigned timeout = mk_c(c)->params().m_timeout; - unsigned rlimit = mk_c(c)->params().m_rlimit; - lbool result; - try { - scoped_timer timer(timeout, &eh); - scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); - - model_ref _m; - result = mk_c(c)->check(_m); - if (m) { - if (_m) { - Z3_model_ref * m_ref = alloc(Z3_model_ref); - m_ref->m_model = _m; - // Must bump reference counter for backward compatibility reasons. - // Don't need to invoke save_object, since the counter was bumped - m_ref->inc_ref(); - *m = of_model(m_ref); - } - else { - *m = 0; - } - } - } - catch (z3_exception & ex) { - mk_c(c)->handle_exception(ex); - RETURN_Z3_check_and_get_model static_cast(l_undef); - } - RETURN_Z3_check_and_get_model static_cast(result); - Z3_CATCH_RETURN(Z3_L_UNDEF); - } - - Z3_lbool Z3_API Z3_check(Z3_context c) { - Z3_TRY; - // This is just syntax sugar... - RESET_ERROR_CODE(); - CHECK_SEARCHING(c); - Z3_lbool r = Z3_check_and_get_model(c, 0); - return r; - Z3_CATCH_RETURN(Z3_L_UNDEF); - } - - - Z3_lbool Z3_API Z3_check_assumptions(Z3_context c, - unsigned num_assumptions, Z3_ast const assumptions[], - Z3_model * m, Z3_ast* proof, - unsigned* core_size, Z3_ast core[]) { - Z3_TRY; - LOG_Z3_check_assumptions(c, num_assumptions, assumptions, m, proof, core_size, core); - RESET_ERROR_CODE(); - CHECK_SEARCHING(c); - expr * const* _assumptions = to_exprs(assumptions); - flet _model(mk_c(c)->fparams().m_model, true); - cancel_eh eh(mk_c(c)->get_smt_kernel()); - api::context::set_interruptable si(*(mk_c(c)), eh); - lbool result; - result = mk_c(c)->get_smt_kernel().check(num_assumptions, _assumptions); - if (result != l_false && m) { - model_ref _m; - mk_c(c)->get_smt_kernel().get_model(_m); - if (_m) { - Z3_model_ref * m_ref = alloc(Z3_model_ref); - m_ref->m_model = _m; - // Must bump reference counter for backward compatibility reasons. - // Don't need to invoke save_object, since the counter was bumped - m_ref->inc_ref(); - *m = of_model(m_ref); - } - else { - *m = 0; - } - } - if (result == l_false && core_size) { - *core_size = mk_c(c)->get_smt_kernel().get_unsat_core_size(); - if (*core_size > num_assumptions) { - SET_ERROR_CODE(Z3_INVALID_ARG); - } - for (unsigned i = 0; i < *core_size; ++i) { - core[i] = of_ast(mk_c(c)->get_smt_kernel().get_unsat_core_expr(i)); - } - } - else if (core_size) { - *core_size = 0; - } - if (result == l_false && proof) { - *proof = of_ast(mk_c(c)->get_smt_kernel().get_proof()); - } - else if (proof) { - *proof = 0; // breaks abstraction. - } - RETURN_Z3_check_assumptions static_cast(result); - Z3_CATCH_RETURN(Z3_L_UNDEF); - } - - Z3_search_failure Z3_API Z3_get_search_failure(Z3_context c) { - Z3_TRY; - LOG_Z3_get_search_failure(c); - RESET_ERROR_CODE(); - CHECK_SEARCHING(c); - smt::failure f = mk_c(c)->get_smt_kernel().last_failure(); - return api::mk_Z3_search_failure(f); - Z3_CATCH_RETURN(Z3_UNKNOWN); - } - - class labeled_literal { - expr_ref m_literal; - symbol m_label; - bool m_enabled; - public: - labeled_literal(ast_manager& m, expr* l, symbol const& n) : m_literal(l,m), m_label(n), m_enabled(true) {} - labeled_literal(ast_manager& m, expr* l) : m_literal(l,m), m_label(), m_enabled(true) {} - bool is_enabled() const { return m_enabled; } - void disable() { m_enabled = false; } - symbol const& get_label() const { return m_label; } - expr* get_literal() { return m_literal.get(); } - }; - - typedef vector labels; - - Z3_literals Z3_API Z3_get_relevant_labels(Z3_context c) { - Z3_TRY; - LOG_Z3_get_relevant_labels(c); - RESET_ERROR_CODE(); - buffer labl_syms; - ast_manager& m = mk_c(c)->m(); - expr_ref_vector lits(m); - mk_c(c)->get_smt_kernel().get_relevant_labels(0, labl_syms); - mk_c(c)->get_smt_kernel().get_relevant_labeled_literals(mk_c(c)->fparams().m_at_labels_cex, lits); - labels* lbls = alloc(labels); - SASSERT(labl_syms.size() == lits.size()); - for (unsigned i = 0; i < lits.size(); ++i) { - lbls->push_back(labeled_literal(m,lits[i].get(), labl_syms[i])); - } - RETURN_Z3(reinterpret_cast(lbls)); - Z3_CATCH_RETURN(0); - } - - Z3_literals Z3_API Z3_get_relevant_literals(Z3_context c) { - Z3_TRY; - LOG_Z3_get_relevant_literals(c); - RESET_ERROR_CODE(); - ast_manager& m = mk_c(c)->m(); - expr_ref_vector lits(m); - mk_c(c)->get_smt_kernel().get_relevant_literals(lits); - labels* lbls = alloc(labels); - for (unsigned i = 0; i < lits.size(); ++i) { - lbls->push_back(labeled_literal(m,lits[i].get())); - } - RETURN_Z3(reinterpret_cast(lbls)); - Z3_CATCH_RETURN(0); - } - - Z3_literals Z3_API Z3_get_guessed_literals(Z3_context c) { - Z3_TRY; - LOG_Z3_get_guessed_literals(c); - RESET_ERROR_CODE(); - ast_manager& m = mk_c(c)->m(); - expr_ref_vector lits(m); - mk_c(c)->get_smt_kernel().get_guessed_literals(lits); - labels* lbls = alloc(labels); - for (unsigned i = 0; i < lits.size(); ++i) { - lbls->push_back(labeled_literal(m,lits[i].get())); - } - RETURN_Z3(reinterpret_cast(lbls)); - Z3_CATCH_RETURN(0); - } - - void Z3_API Z3_del_literals(Z3_context c, Z3_literals lbls) { - Z3_TRY; - LOG_Z3_del_literals(c, lbls); - RESET_ERROR_CODE(); - dealloc(reinterpret_cast(lbls)); - Z3_CATCH; - } - - unsigned Z3_API Z3_get_num_literals(Z3_context c,Z3_literals lbls) { - Z3_TRY; - LOG_Z3_get_num_literals(c, lbls); - RESET_ERROR_CODE(); - return reinterpret_cast(lbls)->size(); - Z3_CATCH_RETURN(0); - } - - Z3_symbol Z3_API Z3_get_label_symbol(Z3_context c,Z3_literals lbls, unsigned idx) { - Z3_TRY; - LOG_Z3_get_label_symbol(c, lbls, idx); - RESET_ERROR_CODE(); - return of_symbol((*reinterpret_cast(lbls))[idx].get_label()); - Z3_CATCH_RETURN(0); - } - - Z3_ast Z3_API Z3_get_literal(Z3_context c,Z3_literals lbls, unsigned idx) { - Z3_TRY; - LOG_Z3_get_literal(c, lbls, idx); - RESET_ERROR_CODE(); - expr* e = (*reinterpret_cast(lbls))[idx].get_literal(); - mk_c(c)->save_ast_trail(e); - RETURN_Z3(of_ast(e)); - Z3_CATCH_RETURN(0); - } - - void Z3_API Z3_disable_literal(Z3_context c, Z3_literals lbls, unsigned idx) { - Z3_TRY; - LOG_Z3_disable_literal(c, lbls, idx); - RESET_ERROR_CODE(); - (*reinterpret_cast(lbls))[idx].disable(); - Z3_CATCH; - } - - void Z3_API Z3_block_literals(Z3_context c, Z3_literals lbls) { - Z3_TRY; - LOG_Z3_block_literals(c, lbls); - RESET_ERROR_CODE(); - labels* _lbls = reinterpret_cast(lbls); - ast_manager& m = mk_c(c)->m(); - expr_ref_vector lits(m); - for (unsigned i = 0; i < _lbls->size(); ++i) { - if ((*_lbls)[i].is_enabled()) { - lits.push_back(m.mk_not((*_lbls)[i].get_literal())); - } - } - expr_ref clause(m); - clause = m.mk_or(lits.size(), lits.c_ptr()); - mk_c(c)->save_ast_trail(clause.get()); - mk_c(c)->assert_cnstr(clause.get()); - Z3_CATCH; - } - - Z3_API char const * Z3_context_to_string(Z3_context c) { - Z3_TRY; - LOG_Z3_context_to_string(c); - RESET_ERROR_CODE(); - std::ostringstream buffer; - mk_c(c)->get_smt_kernel().display(buffer); - return mk_c(c)->mk_external_string(buffer.str()); - Z3_CATCH_RETURN(0); - } - - Z3_ast Z3_API Z3_get_context_assignment(Z3_context c) { - Z3_TRY; - LOG_Z3_get_context_assignment(c); - RESET_ERROR_CODE(); - ast_manager& m = mk_c(c)->m(); - expr_ref result(m); - expr_ref_vector assignment(m); - mk_c(c)->get_smt_kernel().get_assignments(assignment); - result = mk_c(c)->mk_and(assignment.size(), assignment.c_ptr()); - RETURN_Z3(of_ast(result.get())); - Z3_CATCH_RETURN(0); - } - - Z3_string Z3_API Z3_statistics_to_string(Z3_context c) { - Z3_TRY; - LOG_Z3_statistics_to_string(c); - RESET_ERROR_CODE(); - std::ostringstream buffer; - mk_c(c)->get_smt_kernel().display_statistics(buffer); - memory::display_max_usage(buffer); - return mk_c(c)->mk_external_string(buffer.str()); - Z3_CATCH_RETURN(0); - } - - void Z3_API Z3_soft_check_cancel(Z3_context c) { - Z3_TRY; - LOG_Z3_soft_check_cancel(c); - RESET_ERROR_CODE(); - mk_c(c)->interrupt(); - Z3_CATCH; - } - -}; void Z3_display_statistics(Z3_context c, std::ostream& s) { mk_c(c)->get_smt_kernel().display_statistics(s); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 9cfad3415..591b82b43 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -128,11 +128,20 @@ namespace z3 { Z3_set_error_handler(m_ctx, error_handler); Z3_set_ast_print_mode(m_ctx, Z3_PRINT_SMTLIB2_COMPLIANT); } + + void init_interp(config & c) { + m_ctx = Z3_mk_interpolation_context(c); + Z3_set_error_handler(m_ctx, error_handler); + Z3_set_ast_print_mode(m_ctx, Z3_PRINT_SMTLIB2_COMPLIANT); + } + context(context const & s); context & operator=(context const & s); public: + struct interpolation {}; context() { config c; init(c); } context(config & c) { init(c); } + context(config & c, interpolation) { init_interp(c); } ~context() { Z3_del_context(m_ctx); } operator Z3_context() const { return m_ctx; } diff --git a/src/api/dotnet/Deprecated.cs b/src/api/dotnet/Deprecated.cs index aa6dffb45..feb5b1555 100644 --- a/src/api/dotnet/Deprecated.cs +++ b/src/api/dotnet/Deprecated.cs @@ -31,81 +31,6 @@ namespace Microsoft.Z3 public class Deprecated { - /// - /// Creates a backtracking point. - /// - /// - public static void Push(Context ctx) { - Native.Z3_push(ctx.nCtx); - } - - /// - /// Backtracks backtracking points. - /// - /// Note that an exception is thrown if is not smaller than NumScopes - /// - public static void Pop(Context ctx, uint n = 1) { - Native.Z3_pop(ctx.nCtx, n); - } - - /// - /// Assert a constraint (or multiple) into the solver. - /// - public static void Assert(Context ctx, params BoolExpr[] constraints) - { - Contract.Requires(constraints != null); - Contract.Requires(Contract.ForAll(constraints, c => c != null)); - - ctx.CheckContextMatch(constraints); - foreach (BoolExpr a in constraints) - { - Native.Z3_assert_cnstr(ctx.nCtx, a.NativeObject); - } - } - /// - /// Checks whether the assertions in the context are consistent or not. - /// - public static Status Check(Context ctx, List core, ref Model model, ref Expr proof, params Expr[] assumptions) - { - Z3_lbool r; - model = null; - proof = null; - if (assumptions == null || assumptions.Length == 0) - r = (Z3_lbool)Native.Z3_check(ctx.nCtx); - else { - IntPtr mdl = IntPtr.Zero, prf = IntPtr.Zero; - uint core_size = 0; - IntPtr[] native_core = new IntPtr[assumptions.Length]; - r = (Z3_lbool)Native.Z3_check_assumptions(ctx.nCtx, - (uint)assumptions.Length, AST.ArrayToNative(assumptions), - ref mdl, ref prf, ref core_size, native_core); - - for (uint i = 0; i < core_size; i++) - core.Add((BoolExpr)Expr.Create(ctx, native_core[i])); - if (mdl != IntPtr.Zero) { - model = new Model(ctx, mdl); - } - if (prf != IntPtr.Zero) { - proof = Expr.Create(ctx, prf); - } - - } - switch (r) - { - case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE; - case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE; - default: return Status.UNKNOWN; - } - } - - /// - /// Retrieves an assignment to atomic propositions for a satisfiable context. - /// - public static BoolExpr GetAssignment(Context ctx) - { - IntPtr x = Native.Z3_get_context_assignment(ctx.nCtx); - return (BoolExpr)Expr.Create(ctx, x); - } } } \ No newline at end of file diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 927aad930..798ffe2cf 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5318,16 +5318,6 @@ END_MLAPI_EXCLUDE */ void Z3_API Z3_set_error(Z3_context c, Z3_error_code e); -#ifdef Conly - /** - \brief Return a string describing the given error code. - - \deprecated Use #Z3_get_error_msg_ex instead. - - def_API('Z3_get_error_msg', STRING, (_in(ERROR_CODE),)) - */ - Z3_string Z3_API Z3_get_error_msg(Z3_error_code err); -#endif BEGIN_MLAPI_EXCLUDE /** @@ -7372,769 +7362,9 @@ END_MLAPI_EXCLUDE #endif -#ifdef CorML3 - /** - @name Deprecated Injective functions API - */ - /*@{*/ - /** - \brief Create injective function declaration - \deprecated This method just asserts a (universally quantified) formula that asserts that - the new function is injective. It is compatible with the old interface for solving: - #Z3_assert_cnstr, #Z3_check_assumptions, etc. - - def_API('Z3_mk_injective_function', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT))) - */ - Z3_func_decl Z3_API Z3_mk_injective_function( - Z3_context c, - Z3_symbol s, - unsigned domain_size, Z3_sort const domain[], - Z3_sort range - ); - - /*@}*/ -#endif - - - /** - @name Deprecated Constraints API - */ - /*@{*/ - -#ifdef CorML3 - /** - \brief Set the SMTLIB logic to be used in the given logical context. - It is incorrect to invoke this function after invoking - #Z3_check, #Z3_check_and_get_model, #Z3_check_assumptions and #Z3_push. - Return \c Z3_TRUE if the logic was changed successfully, and \c Z3_FALSE otherwise. - - \deprecated Subsumed by #Z3_mk_solver_for_logic - - def_API('Z3_set_logic', VOID, (_in(CONTEXT), _in(STRING))) - */ - Z3_bool Z3_API Z3_set_logic(Z3_context c, Z3_string logic); - - /** - \brief Create a backtracking point. - - The logical context can be viewed as a stack of contexts. The - scope level is the number of elements on this stack. The stack - of contexts is simulated using trail (undo) stacks. - - \sa Z3_pop - - \deprecated Subsumed by #Z3_solver_push - - def_API('Z3_push', VOID, (_in(CONTEXT),)) - */ - void Z3_API Z3_push(Z3_context c); - - /** - \brief Backtrack. - - Restores the context from the top of the stack, and pops it off the - stack. Any changes to the logical context (by #Z3_assert_cnstr or - other functions) between the matching #Z3_push and \c Z3_pop - operators are flushed, and the context is completely restored to - what it was right before the #Z3_push. - - \sa Z3_push - - \deprecated Subsumed by #Z3_solver_pop - - def_API('Z3_pop', VOID, (_in(CONTEXT), _in(UINT))) - */ - void Z3_API Z3_pop(Z3_context c, unsigned num_scopes); - - /** - \brief Retrieve the current scope level. - - It retrieves the number of scopes that have been pushed, but not yet popped. - - \sa Z3_push - \sa Z3_pop - - \deprecated Subsumed by #Z3_solver_get_num_scopes. - - def_API('Z3_get_num_scopes', UINT, (_in(CONTEXT),)) - */ - unsigned Z3_API Z3_get_num_scopes(Z3_context c); - - /** - \conly \brief Persist AST through num_scopes pops. - \conly This function is only relevant if \c c was created using #Z3_mk_context. - \conly If \c c was created using #Z3_mk_context_rc, this function is a NOOP. - - \conly Normally, for contexts created using #Z3_mk_context, - \conly references to terms are no longer valid when - \conly popping scopes beyond the level where the terms are created. - \conly If you want to reference a term below the scope where it - \conly was created, use this method to specify how many pops - \conly the term should survive. - \conly The num_scopes should be at most equal to the number of - \conly calls to Z3_push subtracted with the calls to Z3_pop. - - \conly \deprecated Z3 users should move to #Z3_mk_context_rc and use the - \conly reference counting APIs for managing AST nodes. - - \mlonly \deprecated This function has no effect. \endmlonly - - def_API('Z3_persist_ast', VOID, (_in(CONTEXT), _in(AST), _in(UINT))) - */ - void Z3_API Z3_persist_ast(Z3_context c, Z3_ast a, unsigned num_scopes); - - /** - \brief Assert a constraint into the logical context. - - After one assertion, the logical context may become - inconsistent. - - The functions #Z3_check or #Z3_check_and_get_model should be - used to check whether the logical context is consistent or not. - - \sa Z3_check - \sa Z3_check_and_get_model - - \deprecated Subsumed by #Z3_solver_assert - - def_API('Z3_assert_cnstr', VOID, (_in(CONTEXT), _in(AST))) - */ - void Z3_API Z3_assert_cnstr(Z3_context c, Z3_ast a); - - /** - \brief Check whether the given logical context is consistent or not. - - If the logical context is not unsatisfiable (i.e., the return value is different from \c Z3_L_FALSE) - and model construction is enabled (see #Z3_mk_config), - \conly then a model is stored in \c m. Otherwise, the value \c NULL is stored in \c m. - \mlonly then a valid model is returned. Otherwise, it is unsafe to use the returned model.\endmlonly - \conly The caller is responsible for deleting the model using the function #Z3_del_model. - - \conly \remark In contrast with the rest of the Z3 API, the reference counter of the - \conly model is incremented. This is to guarantee backward compatibility. In previous - \conly versions, models did not support reference counting. - - \remark Model construction must be enabled using configuration - parameters (See, #Z3_mk_config). - - \sa Z3_check - \conly \sa Z3_del_model - - \deprecated Subsumed by #Z3_solver_check - - def_API('Z3_check_and_get_model', INT, (_in(CONTEXT), _out(MODEL))) - */ - Z3_lbool Z3_API Z3_check_and_get_model(Z3_context c, Z3_model * m); - - /** - \brief Check whether the given logical context is consistent or not. - - The function #Z3_check_and_get_model should be used when models are needed. - - \sa Z3_check_and_get_model - - \deprecated Subsumed by #Z3_solver_check - - def_API('Z3_check', INT, (_in(CONTEXT),)) - */ - Z3_lbool Z3_API Z3_check(Z3_context c); - - /** - \brief Check whether the given logical context and optional assumptions is consistent or not. - - If the logical context is not unsatisfiable (i.e., the return value is different from \c Z3_L_FALSE), - \conly a non-NULL model argument is passed in, - and model construction is enabled (see #Z3_mk_config), - \conly then a model is stored in \c m. Otherwise, \c m is left unchanged. - \mlonly then a valid model is returned. Otherwise, it is unsafe to use the returned model.\endmlonly - \conly The caller is responsible for deleting the model using the function #Z3_del_model. - - \conly \remark If the model argument is non-NULL, then model construction must be enabled using configuration - \conly parameters (See, #Z3_mk_config). - - \param c logical context. - \param num_assumptions number of auxiliary assumptions. - \param assumptions array of auxiliary assumptions - \param m optional pointer to a model. - \param proof optional pointer to a proof term. - \param core_size size of unsatisfiable core. - \param core pointer to an array receiving unsatisfiable core. - The unsatisfiable core is a subset of the assumptions, so the array has the same size as the assumptions. - The \c core array is not populated if \c core_size is set to 0. - - \pre assumptions comprises of propositional literals. - In other words, you cannot use compound formulas for assumptions, - but should use propositional variables or negations of propositional variables. - - \conly \remark In constrast with the rest of the Z3 API, the reference counter of the - \conly model is incremented. This is to guarantee backward compatibility. In previous - \conly versions, models did not support reference counting. - - \sa Z3_check - \conly \sa Z3_del_model - - \deprecated Subsumed by #Z3_solver_check_assumptions - - def_API('Z3_check_assumptions', INT, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _out(MODEL), _out(AST), _out(UINT), _out_array2(1, 5, AST))) - */ - Z3_lbool Z3_API Z3_check_assumptions( - Z3_context c, - unsigned num_assumptions, Z3_ast const assumptions[], - Z3_model * m, Z3_ast* proof, - unsigned* core_size, Z3_ast core[] - ); -#endif - -#ifdef CorML4 - /** - \brief Retrieve congruence class representatives for terms. - - The function can be used for relying on Z3 to identify equal terms under the current - set of assumptions. The array of terms and array of class identifiers should have - the same length. The class identifiers are numerals that are assigned to the same - value for their corresponding terms if the current context forces the terms to be - equal. You cannot deduce that terms corresponding to different numerals must be all different, - (especially when using non-convex theories). - All implied equalities are returned by this call. - This means that two terms map to the same class identifier if and only if - the current context implies that they are equal. - - A side-effect of the function is a satisfiability check on the assertions on the solver that is passed in. - The function return Z3_L_FALSE if the current assertions are not satisfiable. - - \sa Z3_check_and_get_model - \sa Z3_check - - \deprecated To be moved outside of API. - - def_API('Z3_get_implied_equalities', INT, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST), _out_array(2, UINT))) - */ - Z3_lbool Z3_API Z3_get_implied_equalities( - Z3_context c, - Z3_solver s, - unsigned num_terms, - Z3_ast const terms[], - unsigned class_ids[] - ); -#endif - -#ifdef CorML3 - /** - \brief Delete a model object. - - \sa Z3_check_and_get_model - - \conly \remark The Z3_check_and_get_model automatically increments a reference count on the model. - \conly The expected usage is that models created by that method are deleted using Z3_del_model. - \conly This is for backwards compatibility and in contrast to the rest of the API where - \conly callers are responsible for managing reference counts. - - \deprecated Subsumed by Z3_solver API - - def_API('Z3_del_model', VOID, (_in(CONTEXT), _in(MODEL))) - */ - void Z3_API Z3_del_model(Z3_context c, Z3_model m); - - /*@}*/ - - /** - @name Deprecated Search control API - */ - /*@{*/ - - /** - \brief Cancel an ongoing check. - - Notifies the current check to abort and return. - This method should be called from a different thread - than the one performing the check. - - \deprecated Use #Z3_interrupt instead. - - def_API('Z3_soft_check_cancel', VOID, (_in(CONTEXT), )) - */ - void Z3_API Z3_soft_check_cancel(Z3_context c); - - /** - \brief Retrieve reason for search failure. - - If a call to #Z3_check or #Z3_check_and_get_model returns Z3_L_UNDEF, - use this facility to determine the more detailed cause of search failure. - - \deprecated Subsumed by #Z3_solver_get_reason_unknown - - def_API('Z3_get_search_failure', UINT, (_in(CONTEXT), )) - */ - Z3_search_failure Z3_API Z3_get_search_failure(Z3_context c); - - /*@}*/ - - /** - @name Deprecated Labels API - */ - /*@{*/ - - /** - \brief Create a labeled formula. - - \param c logical context. - \param s name of the label. - \param is_pos label polarity. - \param f formula being labeled. - - A label behaves as an identity function, so the truth value of the - labeled formula is unchanged. Labels are used for identifying - useful sub-formulas when generating counter-examples. - - \deprecated Labels are only supported by the old Solver API. - This feature is not essential (it can be simulated using auxiliary Boolean variables). - It is only available for backward compatibility. - - def_API('Z3_mk_label', AST, (_in(CONTEXT), _in(SYMBOL), _in(BOOL), _in(AST))) - */ - Z3_ast Z3_API Z3_mk_label(Z3_context c, Z3_symbol s, Z3_bool is_pos, Z3_ast f); - - /** - \brief Retrieve the set of labels that were relevant in - the context of the current satisfied context. - - \sa Z3_del_literals - \sa Z3_get_num_literals - \sa Z3_get_label_symbol - \sa Z3_get_literal - - \deprecated This procedure is based on the old Solver API. - - def_API('Z3_get_relevant_labels', LITERALS, (_in(CONTEXT), )) - */ - Z3_literals Z3_API Z3_get_relevant_labels(Z3_context c); - - /** - \brief Retrieve the set of literals that satisfy the current context. - - \sa Z3_del_literals - \sa Z3_get_num_literals - \sa Z3_get_label_symbol - \sa Z3_get_literal - - \deprecated This procedure is based on the old Solver API. - - def_API('Z3_get_relevant_literals', LITERALS, (_in(CONTEXT), )) - */ - Z3_literals Z3_API Z3_get_relevant_literals(Z3_context c); - - /** - \brief Retrieve the set of literals that whose assignment were - guess, but not propagated during the search. - - \sa Z3_del_literals - \sa Z3_get_num_literals - \sa Z3_get_label_symbol - \sa Z3_get_literal - - \deprecated This procedure is based on the old Solver API. - - def_API('Z3_get_guessed_literals', LITERALS, (_in(CONTEXT), )) - */ - Z3_literals Z3_API Z3_get_guessed_literals(Z3_context c); - - /** - \brief Delete a labels context. - - \sa Z3_get_relevant_labels - - \deprecated This procedure is based on the old Solver API. - - def_API('Z3_del_literals', VOID, (_in(CONTEXT), _in(LITERALS))) - */ - void Z3_API Z3_del_literals(Z3_context c, Z3_literals lbls); - - /** - \brief Retrieve the number of label symbols that were returned. - - \sa Z3_get_relevant_labels - - \deprecated This procedure is based on the old Solver API. - - def_API('Z3_get_num_literals', UINT, (_in(CONTEXT), _in(LITERALS))) - */ - unsigned Z3_API Z3_get_num_literals(Z3_context c, Z3_literals lbls); - - /** - \brief Retrieve label symbol at idx. - - \deprecated This procedure is based on the old Solver API. - - def_API('Z3_get_label_symbol', SYMBOL, (_in(CONTEXT), _in(LITERALS), _in(UINT))) - */ - Z3_symbol Z3_API Z3_get_label_symbol(Z3_context c, Z3_literals lbls, unsigned idx); - - /** - \brief Retrieve literal expression at idx. - - \deprecated This procedure is based on the old Solver API. - - def_API('Z3_get_literal', AST, (_in(CONTEXT), _in(LITERALS), _in(UINT))) - */ - Z3_ast Z3_API Z3_get_literal(Z3_context c, Z3_literals lbls, unsigned idx); - - /** - \brief Disable label. - - The disabled label is not going to be used when blocking the subsequent search. - - \sa Z3_block_literals - - \deprecated This procedure is based on the old Solver API. - - def_API('Z3_disable_literal', VOID, (_in(CONTEXT), _in(LITERALS), _in(UINT))) - */ - void Z3_API Z3_disable_literal(Z3_context c, Z3_literals lbls, unsigned idx); - - /** - \brief Block subsequent checks using the remaining enabled labels. - - \deprecated This procedure is based on the old Solver API. - - def_API('Z3_block_literals', VOID, (_in(CONTEXT), _in(LITERALS))) - */ - void Z3_API Z3_block_literals(Z3_context c, Z3_literals lbls); - - /*@}*/ - - /** - @name Deprecated Model API - */ - /*@{*/ - - /** - \brief Return the number of constants assigned by the given model. - - \mlonly \remark Consider using {!get_model_constants}. \endmlonly - - \sa Z3_get_model_constant - - \deprecated use #Z3_model_get_num_consts - - def_API('Z3_get_model_num_constants', UINT, (_in(CONTEXT), _in(MODEL))) - */ - unsigned Z3_API Z3_get_model_num_constants(Z3_context c, Z3_model m); - - /** - \brief \mlh get_model_constant c m i \endmlh - Return the i-th constant in the given model. - - \mlonly \remark Consider using {!get_model_constants}. \endmlonly - - \pre i < Z3_get_model_num_constants(c, m) - - \deprecated use #Z3_model_get_const_decl - - def_API('Z3_get_model_constant', FUNC_DECL, (_in(CONTEXT), _in(MODEL), _in(UINT))) - */ - Z3_func_decl Z3_API Z3_get_model_constant(Z3_context c, Z3_model m, unsigned i); - - /** - \brief Return the number of function interpretations in the given model. - - A function interpretation is represented as a finite map and an 'else' value. - Each entry in the finite map represents the value of a function given a set of arguments. - - \deprecated use #Z3_model_get_num_funcs - - def_API('Z3_get_model_num_funcs', UINT, (_in(CONTEXT), _in(MODEL))) - */ - unsigned Z3_API Z3_get_model_num_funcs(Z3_context c, Z3_model m); - - /** - \brief \mlh get_model_func_decl c m i \endmlh - Return the declaration of the i-th function in the given model. - - \pre i < Z3_get_model_num_funcs(c, m) - - \sa Z3_get_model_num_funcs - - \deprecated use #Z3_model_get_func_decl - - def_API('Z3_get_model_func_decl', FUNC_DECL, (_in(CONTEXT), _in(MODEL), _in(UINT))) - */ - Z3_func_decl Z3_API Z3_get_model_func_decl(Z3_context c, Z3_model m, unsigned i); - - /** - \brief Return the value of the given constant or function - in the given model. - - \deprecated Consider using #Z3_model_eval or #Z3_model_get_func_interp - - def_API('Z3_eval_func_decl', BOOL, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL), _out(AST))) - */ - Z3_bool Z3_API Z3_eval_func_decl(Z3_context c, Z3_model m, Z3_func_decl decl, Z3_ast* v); - - /** - \brief \mlh is_array_value c v \endmlh - Determine whether the term encodes an array value. - A term encodes an array value if it is a nested sequence of - applications of store on top of a constant array. - The indices to the stores have to be values (for example, integer constants) - so that equality between the indices can be evaluated. - Array values are useful for representing interpretations for arrays. - - Return the number of entries mapping to non-default values of the array. - - \deprecated Use #Z3_is_as_array - - def_API('Z3_is_array_value', BOOL, (_in(CONTEXT), _in(MODEL), _in(AST), _out(UINT))) - */ - Z3_bool Z3_API Z3_is_array_value(Z3_context c, Z3_model m, Z3_ast v, unsigned* num_entries); - - /** - \brief \mlh get_array_value c v \endmlh - An array values is represented as a dictionary plus a - default (else) value. This function returns the array graph. - - \pre Z3_TRUE == Z3_is_array_value(c, v, &num_entries) - - \deprecated Use Z3_func_interp objects and #Z3_get_as_array_func_decl - - def_API('Z3_get_array_value', VOID, (_in(CONTEXT), _in(MODEL), _in(AST), _in(UINT), _out_array(3, AST), _out_array(3, AST), _out (AST))) - */ - void Z3_API Z3_get_array_value(Z3_context c, - Z3_model m, - Z3_ast v, - unsigned num_entries, - Z3_ast indices[], - Z3_ast values[], - Z3_ast* else_value - ); - - /** - \brief \mlh get_model_func_else c m i \endmlh - Return the 'else' value of the i-th function interpretation in the given model. - - A function interpretation is represented as a finite map and an 'else' value. - - \mlonly \remark Consider using {!get_model_funcs}. \endmlonly - - \pre i < Z3_get_model_num_funcs(c, m) - - \sa Z3_get_model_num_funcs - \sa Z3_get_model_func_num_entries - \sa Z3_get_model_func_entry_num_args - \sa Z3_get_model_func_entry_arg - - \deprecated Use Z3_func_interp objects - - def_API('Z3_get_model_func_else', AST, (_in(CONTEXT), _in(MODEL), _in(UINT))) - */ - Z3_ast Z3_API Z3_get_model_func_else(Z3_context c, Z3_model m, unsigned i); - - /** - \brief \mlh get_model_func_num_entries c m i \endmlh - Return the number of entries of the i-th function interpretation in the given model. - - A function interpretation is represented as a finite map and an 'else' value. - - \mlonly \remark Consider using {!get_model_funcs}. \endmlonly - - \pre i < Z3_get_model_num_funcs(c, m) - - \sa Z3_get_model_num_funcs - \sa Z3_get_model_func_else - \sa Z3_get_model_func_entry_num_args - \sa Z3_get_model_func_entry_arg - - \deprecated Use Z3_func_interp objects - - def_API('Z3_get_model_func_num_entries', UINT, (_in(CONTEXT), _in(MODEL), _in(UINT))) - */ - unsigned Z3_API Z3_get_model_func_num_entries(Z3_context c, Z3_model m, unsigned i); - - /** - \brief \mlh get_model_func_entry_num_args c m i j \endmlh - Return the number of arguments of the j-th entry of the i-th function interpretation in the given - model. - - A function interpretation is represented as a finite map and an 'else' value. - This function returns the j-th entry of this map. - - An entry represents the value of a function given a set of arguments. - \conly That is: it has the following format f(args[0],...,args[num_args - 1]) = val. - - \mlonly \remark Consider using {!get_model_funcs}. \endmlonly - - \pre i < Z3_get_model_num_funcs(c, m) - \pre j < Z3_get_model_func_num_entries(c, m, i) - - \sa Z3_get_model_num_funcs - \sa Z3_get_model_func_num_entries - \sa Z3_get_model_func_entry_arg - - \deprecated Use Z3_func_interp objects - - def_API('Z3_get_model_func_entry_num_args', UINT, (_in(CONTEXT), _in(MODEL), _in(UINT), _in(UINT))) - */ - unsigned Z3_API Z3_get_model_func_entry_num_args(Z3_context c, - Z3_model m, - unsigned i, - unsigned j); - - /** - \brief \mlh get_model_func_entry_arg c m i j k \endmlh - Return the k-th argument of the j-th entry of the i-th function interpretation in the given - model. - - A function interpretation is represented as a finite map and an 'else' value. - This function returns the j-th entry of this map. - - An entry represents the value of a function given a set of arguments. - \conly That is: it has the following format f(args[0],...,args[num_args - 1]) = val. - - \mlonly \remark Consider using {!get_model_funcs}. \endmlonly - - \pre i < Z3_get_model_num_funcs(c, m) - \pre j < Z3_get_model_func_num_entries(c, m, i) - \pre k < Z3_get_model_func_entry_num_args(c, m, i, j) - - \sa Z3_get_model_num_funcs - \sa Z3_get_model_func_num_entries - \sa Z3_get_model_func_entry_num_args - - \deprecated Use Z3_func_interp objects - - def_API('Z3_get_model_func_entry_arg', AST, (_in(CONTEXT), _in(MODEL), _in(UINT), _in(UINT), _in(UINT))) - */ - Z3_ast Z3_API Z3_get_model_func_entry_arg(Z3_context c, - Z3_model m, - unsigned i, - unsigned j, - unsigned k); - - /** - \brief \mlh get_model_func_entry_value c m i j \endmlh - Return the return value of the j-th entry of the i-th function interpretation in the given - model. - - A function interpretation is represented as a finite map and an 'else' value. - This function returns the j-th entry of this map. - - An entry represents the value of a function given a set of arguments. - \conly That is: it has the following format f(args[0],...,args[num_args - 1]) = val. - - \mlonly \remark Consider using {!get_model_funcs}. \endmlonly - - \pre i < Z3_get_model_num_funcs(c, m) - \pre j < Z3_get_model_func_num_entries(c, m, i) - - \sa Z3_get_model_num_funcs - \sa Z3_get_model_func_num_entries - - \deprecated Use Z3_func_interp objects - - def_API('Z3_get_model_func_entry_value', AST, (_in(CONTEXT), _in(MODEL), _in(UINT), _in(UINT))) - */ - Z3_ast Z3_API Z3_get_model_func_entry_value(Z3_context c, - Z3_model m, - unsigned i, - unsigned j); - - /** - \brief \mlh eval c m t \endmlh - Evaluate the AST node \c t in the given model. - \conly Return \c Z3_TRUE if succeeded, and store the result in \c v. - \mlonly Return a pair: Boolean and value. The Boolean is true if the term was successfully evaluated. \endmlonly - - The evaluation may fail for the following reasons: - - - \c t contains a quantifier. - - - the model \c m is partial, that is, it doesn't have a complete interpretation for uninterpreted functions. - That is, the option MODEL_PARTIAL=true was used. - - - \c t is type incorrect. - - \deprecated Use #Z3_model_eval - - def_API('Z3_eval', BOOL, (_in(CONTEXT), _in(MODEL), _in(AST), _out(AST))) - */ - Z3_bool Z3_API Z3_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_ast * v); - - /** - \brief Evaluate declaration given values. - - Provides direct way to evaluate declarations - without going over terms. - - \deprecated Consider using #Z3_model_eval and #Z3_substitute_vars - - def_API('Z3_eval_decl', BOOL, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL), _in(UINT), _in_array(3, AST), _out(AST))) - */ - Z3_bool Z3_API Z3_eval_decl(Z3_context c, Z3_model m, - Z3_func_decl d, - unsigned num_args, - Z3_ast const args[], - Z3_ast* v); - - /*@}*/ - - /** - @name Deprecated String conversion API - */ - /*@{*/ - - /** - \brief Convert the given logical context into a string. - - This function is mainly used for debugging purposes. It displays - the internal structure of a logical context. - - \conly \warning The result buffer is statically allocated by Z3. It will - \conly be automatically deallocated when #Z3_del_context is invoked. - \conly So, the buffer is invalidated in the next call to \c Z3_context_to_string. - - \deprecated This method is obsolete. It just displays the internal representation of - the global solver available for backward compatibility reasons. - - def_API('Z3_context_to_string', STRING, (_in(CONTEXT),)) - */ - Z3_string Z3_API Z3_context_to_string(Z3_context c); - - /** - \brief Return runtime statistics as a string. - - This function is mainly used for debugging purposes. It displays - statistics of the search activity. - - \conly \warning The result buffer is statically allocated by Z3. It will - \conly be automatically deallocated when #Z3_del_context is invoked. - \conly So, the buffer is invalidated in the next call to \c Z3_context_to_string. - - \deprecated This method is based on the old solver API. - Use #Z3_stats_to_string when using the new solver API. - - def_API('Z3_statistics_to_string', STRING, (_in(CONTEXT),)) - */ - Z3_string Z3_API Z3_statistics_to_string(Z3_context c); - - /** - \brief Extract satisfying assignment from context as a conjunction. - - This function can be used for debugging purposes. It returns a conjunction - of formulas that are assigned to true in the current context. - This conjunction will contain not only the assertions that are set to true - under the current assignment, but will also include additional literals - if there has been a call to #Z3_check or #Z3_check_and_get_model. - - \deprecated This method is based on the old solver API. - - def_API('Z3_get_context_assignment', AST, (_in(CONTEXT),)) - */ - Z3_ast Z3_API Z3_get_context_assignment(Z3_context c); - - /*@}*/ -#endif #ifndef CAMLIDL From bea68cd194b05fb5584d769c83c92040c61e6915 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Nov 2015 17:05:15 -0800 Subject: [PATCH 2/4] remove deprecated API functionality Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 10 +++++----- src/api/api_context.cpp | 10 +++++----- src/api/api_solver.cpp | 2 -- src/api/z3_api.h | 35 +++++++++++++++++++++++++++++++++-- src/muz/pdr/pdr_context.cpp | 13 +++++++++---- src/muz/pdr/pdr_context.h | 2 +- 6 files changed, 53 insertions(+), 19 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index bb5935a1e..86f6ceee8 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -57,7 +57,7 @@ log_h.write('inline void SetR(void * obj) { *g_z3_log << "= " << obj << "\\n"; } log_h.write('#define RETURN_Z3(Z3RES) if (_LOG_CTX.enabled()) { SetR(Z3RES); } return Z3RES\n') log_h.write('void _Z3_append_log(char const * msg);\n') ## -exe_c.write('void Z3_replacer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg_ex(ctx, c)); }\n') +exe_c.write('void Z3_replacer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg(ctx, c)); }\n') ## core_py.write('# Automatically generated file\n') core_py.write('import sys, os\n') @@ -404,7 +404,7 @@ def mk_py_wrappers(): if len(params) > 0 and param_type(params[0]) == CONTEXT: core_py.write(" err = lib().Z3_get_error_code(a0)\n") core_py.write(" if err != Z3_OK:\n") - core_py.write(" raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))\n") + core_py.write(" raise Z3Exception(lib().Z3_get_error_msg(a0, err))\n") if result == STRING: core_py.write(" return _to_pystr(r)\n") elif result != VOID: @@ -477,7 +477,7 @@ def mk_dotnet_wrappers(): dotnet.write(" LIB.Z3_set_error_handler(a0, a1);\n") dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n") dotnet.write(" if (err != Z3_error_code.Z3_OK)\n") - dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n") + dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg(a0, (uint)err)));\n") dotnet.write(" }\n\n") for name, result, params in _dotnet_decls: if result == STRING: @@ -525,7 +525,7 @@ def mk_dotnet_wrappers(): if len(params) > 0 and param_type(params[0]) == CONTEXT: dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n") dotnet.write(" if (err != Z3_error_code.Z3_OK)\n") - dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n") + dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg(a0, (uint)err)));\n") if result == STRING: dotnet.write(" return Marshal.PtrToStringAnsi(r);\n") elif result != VOID: @@ -1276,7 +1276,7 @@ def mk_ml(): if name not in Unwrapped and len(params) > 0 and param_type(params[0]) == CONTEXT: ml_native.write(' let err = (error_code_of_int (ML2C.n_get_error_code a0)) in \n') ml_native.write(' if err <> OK then\n') - ml_native.write(' raise (Exception (ML2C.n_get_error_msg_ex a0 (int_of_error_code err)))\n') + ml_native.write(' raise (Exception (ML2C.n_get_error_msg a0 (int_of_error_code err)))\n') ml_native.write(' else\n') if result == VOID and len(op) == 0: ml_native.write(' ()\n') diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 9c1701c44..c1f982997 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -33,7 +33,7 @@ void install_tactics(tactic_manager & ctx); namespace api { static void default_error_handler(Z3_context ctx, Z3_error_code c) { - printf("Error: %s\n", Z3_get_error_msg_ex(ctx, c)); + printf("Error: %s\n", Z3_get_error_msg(ctx, c)); exit(1); } @@ -531,7 +531,7 @@ extern "C" { SET_ERROR_CODE(e); } - static char const * _get_error_msg_ex(Z3_context c, Z3_error_code err) { + static char const * _get_error_msg(Z3_context c, Z3_error_code err) { switch(err) { case Z3_OK: return "ok"; case Z3_SORT_ERROR: return "type error"; @@ -551,9 +551,9 @@ extern "C" { } - Z3_API char const * Z3_get_error_msg_ex(Z3_context c, Z3_error_code err) { - LOG_Z3_get_error_msg_ex(c, err); - return _get_error_msg_ex(c, err); + Z3_API char const * Z3_get_error_msg(Z3_context c, Z3_error_code err) { + LOG_Z3_get_error_msg(c, err); + return _get_error_msg(c, err); } diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 77848900e..6112a8cd2 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -391,7 +391,6 @@ extern "C" { } -#if 0 Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c, Z3_solver s, unsigned num_terms, @@ -407,6 +406,5 @@ extern "C" { return static_cast(result); Z3_CATCH_RETURN(Z3_L_UNDEF); } -#endif }; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 798ffe2cf..4492a4c0f 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5323,9 +5323,9 @@ BEGIN_MLAPI_EXCLUDE /** \brief Return a string describing the given error code. - def_API('Z3_get_error_msg_ex', STRING, (_in(CONTEXT), _in(ERROR_CODE))) + def_API('Z3_get_error_msg', STRING, (_in(CONTEXT), _in(ERROR_CODE))) */ - Z3_string Z3_API Z3_get_error_msg_ex(Z3_context c, Z3_error_code err); + Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err); END_MLAPI_EXCLUDE #ifdef ML4only #include @@ -7216,6 +7216,37 @@ END_MLAPI_EXCLUDE Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[]); + + +#ifdef CorML4 + /** + \brief Retrieve congruence class representatives for terms. + + The function can be used for relying on Z3 to identify equal terms under the current + set of assumptions. The array of terms and array of class identifiers should have + the same length. The class identifiers are numerals that are assigned to the same + value for their corresponding terms if the current context forces the terms to be + equal. You cannot deduce that terms corresponding to different numerals must be all different, + (especially when using non-convex theories). + All implied equalities are returned by this call. + This means that two terms map to the same class identifier if and only if + the current context implies that they are equal. + + A side-effect of the function is a satisfiability check on the assertions on the solver that is passed in. + The function return Z3_L_FALSE if the current assertions are not satisfiable. + + + + def_API('Z3_get_implied_equalities', INT, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST), _out_array(2, UINT))) + */ + Z3_lbool Z3_API Z3_get_implied_equalities( + Z3_context c, + Z3_solver s, + unsigned num_terms, + Z3_ast const terms[], + unsigned class_ids[] + ); +#endif /** \brief Retrieve the model for the last #Z3_solver_check or #Z3_solver_check_assumptions diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index d349da4ec..39e519863 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -738,6 +738,7 @@ namespace pdr { // model_node void model_node::set_closed() { + TRACE("pdr", tout << state() << "\n";); pt().close(state()); m_closed = true; } @@ -1149,17 +1150,21 @@ namespace pdr { ast_manager& m = n->pt().get_manager(); if (!n->get_model_ptr()) { if (models.find(n->state(), md)) { - TRACE("pdr", tout << mk_pp(n->state(), m) << "\n";); + TRACE("pdr", tout << n->state() << "\n";); model_ref mr(md); n->set_model(mr); datalog::rule const* rule = rules.find(n->state()); n->set_rule(rule); } else { + TRACE("pdr", tout << "no model for " << n->state() << "\n";); IF_VERBOSE(1, n->display(verbose_stream() << "no model:\n", 0); - verbose_stream() << mk_pp(n->state(), m) << "\n";); + verbose_stream() << n->state() << "\n";); } } + else { + TRACE("pdr", tout << n->state() << "\n";); + } todo.pop_back(); todo.append(n->children().size(), n->children().c_ptr()); } @@ -2027,11 +2032,11 @@ namespace pdr { switch (expand_state(n, cube, uses_level)) { case l_true: if (n.level() == 0) { - TRACE("pdr", tout << "reachable at level 0\n";); + TRACE("pdr", n.display(tout << "reachable at level 0\n", 0);); close_node(n); } else { - TRACE("pdr", tout << "node: " << &n << "\n";); + TRACE("pdr", n.display(tout, 0);); create_children(n); } break; diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h index 7cba1e0c5..35b9067b2 100644 --- a/src/muz/pdr/pdr_context.h +++ b/src/muz/pdr/pdr_context.h @@ -240,7 +240,7 @@ namespace pdr { void check_pre_closed(); void set_closed(); void set_open(); - void set_pre_closed() { m_closed = true; } + void set_pre_closed() { TRACE("pdr", tout << state() << "\n";); m_closed = true; } void reset() { m_children.reset(); } void set_rule(datalog::rule const* r) { m_rule = r; } From cb85b60160c7a6d368a957ca2ea4376ede6104df Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Nov 2015 18:13:14 -0800 Subject: [PATCH 3/4] Fix issue #311 Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_context.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index 39e519863..a55d0e648 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -929,7 +929,7 @@ namespace pdr { model_node* p = n.parent(); while (p) { if (p->state() == n.state()) { - TRACE("pdr", tout << "repeated\n";); + TRACE("pdr", tout << n.state() << "repeated\n";); return true; } p = p->parent(); @@ -1019,6 +1019,11 @@ namespace pdr { SASSERT(n1->children().empty()); enqueue_leaf(n1); } + + if (!nodes.empty() && n.get_model_ptr() && backtrack) { + model_ref mr(n.get_model_ptr()); + nodes[0]->set_model(mr); + } if (nodes.empty()) { cache(n).remove(n.state()); } From ab4033133f64c3a8fe8f1405e1c6288ec10ede3a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Nov 2015 18:46:49 -0800 Subject: [PATCH 4/4] remove solver_old Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 16 ---------------- src/api/api_solver.cpp | 3 ++- src/api/api_solver_old.cpp | 33 --------------------------------- src/api/z3_api.h | 2 -- 4 files changed, 2 insertions(+), 52 deletions(-) delete mode 100644 src/api/api_solver_old.cpp diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index c1f982997..8451c00c5 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -209,22 +209,6 @@ namespace api { } } } -#if 0 - void context::persist_ast(ast * n, unsigned num_scopes) { - // persist_ast is irrelevant when m_user_ref_count == true - if (m_user_ref_count) - return; - if (num_scopes > m_ast_lim.size()) { - num_scopes = m_ast_lim.size(); - } - SASSERT(m_replay_stack.size() > num_scopes); - unsigned j = m_replay_stack.size() - num_scopes - 1; - if (!m_replay_stack[j]) { - m_replay_stack[j] = alloc(ast_ref_vector, m()); - } - m_replay_stack[j]->push_back(n); - } -#endif void context::save_ast_trail(ast * n) { SASSERT(m().contains(n)); diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 6112a8cd2..b568f3613 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -6,7 +6,8 @@ Module Name: api_solver.cpp Abstract: - New solver API + + Solver API Author: diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp deleted file mode 100644 index b4911698c..000000000 --- a/src/api/api_solver_old.cpp +++ /dev/null @@ -1,33 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - api_solver_old.cpp - -Abstract: - OLD API for using solvers. - - This has been deprecated - -Author: - - Leonardo de Moura (leonardo) 2012-02-29. - -Revision History: - ---*/ -#include -#include"z3.h" -#include"api_log_macros.h" -#include"api_context.h" - - -void Z3_display_statistics(Z3_context c, std::ostream& s) { - mk_c(c)->get_smt_kernel().display_statistics(s); -} - -void Z3_display_istatistics(Z3_context c, std::ostream& s) { - mk_c(c)->get_smt_kernel().display_istatistics(s); -} - diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 4492a4c0f..cc72aaa4c 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1552,8 +1552,6 @@ extern "C" { \conly \sa Z3_del_context - \conly \deprecated Use #Z3_mk_context_rc - def_API('Z3_mk_context', CONTEXT, (_in(CONFIG),)) */ #ifdef CorML3