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/scripts/update_api.py b/scripts/update_api.py index 6e7b6d5f7..ae0761056 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: @@ -632,7 +632,7 @@ def mk_java(): if len(params) > 0 and param_type(params[0]) == CONTEXT: java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n') java_native.write(' if (err != Z3_error_code.Z3_OK)\n') - java_native.write(' throw new Z3Exception(INTERNALgetErrorMsgEx(a0, err.toInt()));\n') + java_native.write(' throw new Z3Exception(INTERNALgetErrorMsg(a0, err.toInt()));\n') if result != VOID: java_native.write(' return res;\n') java_native.write(' }\n\n') @@ -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_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 6749f1525..79a2fd965 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(ctx, c)); exit(1); } @@ -207,20 +207,6 @@ namespace api { } } } - 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); - } void context::save_ast_trail(ast * n) { SASSERT(m().contains(n)); @@ -476,13 +462,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, @@ -534,7 +513,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"; @@ -553,24 +532,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(Z3_context c, Z3_error_code err) { + LOG_Z3_get_error_msg(c, err); + return _get_error_msg(c, 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..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 fbd57ad97..000000000 --- a/src/api/api_solver_old.cpp +++ /dev/null @@ -1,358 +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" -#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); -} - -void Z3_display_istatistics(Z3_context c, std::ostream& s) { - mk_c(c)->get_smt_kernel().display_istatistics(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..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 @@ -5318,24 +5316,14 @@ 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 /** \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 @@ -7226,6 +7214,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 @@ -7372,769 +7391,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 diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 1b33c2cf1..369c6e2b1 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -241,27 +241,37 @@ namespace opt { TRACE("opt", model_smt2_pp(tout, m, *m_model, 0);); m_optsmt.setup(*m_opt_solver.get()); update_lower(); + switch (m_objectives.size()) { case 0: - return is_sat; + break; case 1: - return execute(m_objectives[0], true, false); + is_sat = execute(m_objectives[0], true, false); + break; default: { opt_params optp(m_params); symbol pri = optp.priority(); if (pri == symbol("pareto")) { - return execute_pareto(); + is_sat = execute_pareto(); } else if (pri == symbol("box")) { - return execute_box(); + is_sat = execute_box(); } else { - return execute_lex(); + is_sat = execute_lex(); } + break; } } + return adjust_unknown(is_sat); } + lbool context::adjust_unknown(lbool r) { + if (r == l_true && m_opt_solver.get() && m_opt_solver->was_unknown()) { + r = l_undef; + } + return r; + } bool context::print_model() const { opt_params optp(m_params); diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index dc180e8e6..946c2a5a3 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -229,6 +229,7 @@ namespace opt { lbool execute_lex(); lbool execute_box(); lbool execute_pareto(); + lbool adjust_unknown(lbool r); bool scoped_lex(); expr_ref to_expr(inf_eps const& n); diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index d7e3c8590..195567a29 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -44,7 +44,8 @@ namespace opt { m_fm(fm), m_objective_terms(m), m_dump_benchmarks(false), - m_first(true) { + m_first(true), + m_was_unknown(false) { m_params.updt_params(p); if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) { m_params.m_relevancy_lvl = 0; @@ -173,6 +174,7 @@ namespace opt { else { r = m_context.check(num_assumptions, assumptions); } + r = adjust_result(r); m_first = false; if (dump_benchmarks()) { w.stop(); @@ -242,6 +244,7 @@ namespace opt { TRACE("opt", tout << ge << "\n";); assert_expr(ge); lbool is_sat = m_context.check(0, 0); + is_sat = adjust_result(is_sat); if (is_sat == l_true) { set_model(i); } @@ -261,6 +264,13 @@ namespace opt { } + lbool opt_solver::adjust_result(lbool r) { + if (r == l_undef && m_context.last_failure() == smt::QUANTIFIERS) { + r = l_true; + m_was_unknown = true; + } + return r; + } void opt_solver::get_unsat_core(ptr_vector & r) { unsigned sz = m_context.get_unsat_core_size(); diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 0e53e07c6..a12c7ffb0 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -82,6 +82,7 @@ namespace opt { static unsigned m_dump_count; statistics m_stats; bool m_first; + bool m_was_unknown; public: opt_solver(ast_manager & m, params_ref const & p, filter_model_converter& fm); virtual ~opt_solver(); @@ -117,6 +118,8 @@ namespace opt { return m_valid_objectives[obj_index]; } + bool was_unknown() const { return m_was_unknown; } + vector const& get_objective_values(); expr_ref mk_ge(unsigned obj_index, inf_eps const& val); @@ -136,6 +139,7 @@ namespace opt { private: lbool decrement_value(unsigned i, inf_eps& val); void set_model(unsigned i); + lbool adjust_result(lbool r); }; }