diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 469282e40..09092dbc2 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -633,6 +633,32 @@ void tactic_example9() { std::cout << t(g) << "\n"; } +void tactic_qe() { + std::cout << "tactic example using quantifier elimination\n"; + context c; + + // Create a solver using "qe" and "smt" tactics + solver s = + (tactic(c, "qe") & + tactic(c, "smt")).mk_solver(); + + expr a = c.int_const("a"); + expr b = c.int_const("b"); + expr x = c.int_const("x"); + expr f = implies(x <= a, x < b); + + // We have to use the C API directly for creating quantified formulas. + Z3_app vars[] = {(Z3_app) x}; + expr qf = to_expr(c, Z3_mk_forall_const(c, 0, 1, vars, + 0, 0, // no pattern + f)); + std::cout << qf << "\n"; + + s.add(qf); + std::cout << s.check() << "\n"; + std::cout << s.get_model() << "\n"; +} + void visit(expr const & e) { if (e.is_app()) { unsigned num = e.num_args(); @@ -691,6 +717,7 @@ int main() { tactic_example7(); std::cout << "\n"; tactic_example8(); std::cout << "\n"; tactic_example9(); std::cout << "\n"; + tactic_qe(); std::cout << "\n"; tst_visit(); std::cout << "\n"; std::cout << "done\n"; } diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index c80b55fd9..ba8d2ae64 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -333,28 +333,28 @@ namespace api { // // ------------------------ - smt::solver & context::get_solver() { + smt::kernel & context::get_smt_kernel() { if (!m_solver) { - m_solver = alloc(smt::solver, m_manager, m_params); + m_solver = alloc(smt::kernel, m_manager, m_params); } return *m_solver; } void context::assert_cnstr(expr * a) { - get_solver().assert_expr(a); + get_smt_kernel().assert_expr(a); } lbool context::check(model_ref & m) { flet searching(m_searching, true); lbool r; - r = get_solver().check(); + r = get_smt_kernel().check(); if (r != l_false) - get_solver().get_model(m); + get_smt_kernel().get_model(m); return r; } void context::push() { - get_solver().push(); + get_smt_kernel().push(); if (!m_user_ref_count) { m_ast_lim.push_back(m_ast_trail.size()); m_replay_stack.push_back(0); @@ -373,7 +373,7 @@ namespace api { } } } - get_solver().pop(num_scopes); + get_smt_kernel().pop(num_scopes); } // ------------------------ @@ -476,7 +476,7 @@ extern "C" { Z3_TRY; LOG_Z3_set_logic(c, logic); RESET_ERROR_CODE(); - return mk_c(c)->get_solver().set_logic(symbol(logic)); + return mk_c(c)->get_smt_kernel().set_logic(symbol(logic)); Z3_CATCH_RETURN(Z3_FALSE); } diff --git a/src/api/api_context.h b/src/api/api_context.h index 4bb0b6d18..3da506b54 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -27,7 +27,7 @@ Revision History: #include"bv_decl_plugin.h" #include"datatype_decl_plugin.h" #include"dl_decl_plugin.h" -#include"smt_solver.h" +#include"smt_kernel.h" #include"front_end_params.h" #include"event_handler.h" #include"tactic_manager.h" @@ -62,7 +62,7 @@ namespace api { bv_util m_bv_util; datalog::dl_decl_util m_datalog_util; - smt::solver * m_solver; // General purpose solver for backward compatibility + smt::kernel * m_solver; // General purpose solver for backward compatibility ast_ref_vector m_last_result; //!< used when m_user_ref_count == true ast_ref_vector m_ast_trail; //!< used when m_user_ref_count == false @@ -175,7 +175,7 @@ namespace api { // ------------------------ bool has_solver() const { return m_solver != 0; } - smt::solver & get_solver(); + smt::kernel & get_smt_kernel(); void assert_cnstr(expr * a); lbool check(model_ref & m); void push(); diff --git a/src/api/api_datalog.h b/src/api/api_datalog.h index fad44de87..1d6bb995a 100644 --- a/src/api/api_datalog.h +++ b/src/api/api_datalog.h @@ -24,7 +24,7 @@ Revision History: #include"front_end_params.h" #include"dl_external_relation.h" #include"dl_decl_plugin.h" -#include"smt_solver.h" +#include"smt_kernel.h" #include"api_util.h" #include"dl_context.h" diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index 0a76c710e..b6d18096f 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -23,6 +23,7 @@ Revision History: #include"cmd_context.h" #include"smt2parser.h" #include"smtparser.h" +#include"solver_na2as.h" extern "C" { @@ -251,20 +252,19 @@ extern "C" { // --------------- // Support for SMTLIB2 - class z3_context_solver : public solver { + class z3_context_solver : public solver_na2as { api::context & m_ctx; - smt::solver & ctx() const { return m_ctx.get_solver(); } + smt::kernel & ctx() const { return m_ctx.get_smt_kernel(); } public: virtual ~z3_context_solver() {} z3_context_solver(api::context& c) : m_ctx(c) {} - virtual void init(ast_manager & m, symbol const & logic) {} + virtual void init_core(ast_manager & m, symbol const & logic) {} virtual void collect_statistics(statistics & st) const {} - virtual void reset() { ctx().reset(); } + virtual void reset_core() { ctx().reset(); } virtual void assert_expr(expr * t) { ctx().assert_expr(t); } - virtual void push() { ctx().push(); } - virtual void pop(unsigned n) { ctx().pop(n); } - virtual unsigned get_scope_level() const { return ctx().get_scope_level(); } - virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) { + virtual void push_core() { ctx().push(); } + virtual void pop_core(unsigned n) { ctx().pop(n); } + virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) { return ctx().check(num_assumptions, assumptions); } virtual void get_unsat_core(ptr_vector & r) { diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 9b3619a6e..6d1becb4d 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -29,18 +29,33 @@ Revision History: #include"cancel_eh.h" #include"scoped_timer.h" #include"smt_strategic_solver.h" -#include"default_solver.h" +#include"smt_solver.h" extern "C" { + static void init_solver_core(Z3_context c, Z3_solver _s) { + ast_manager & m = mk_c(c)->m(); + Z3_solver_ref * s = to_solver(_s); + s->m_solver->set_produce_proofs(m.proofs_enabled()); + s->m_solver->set_produce_unsat_cores(s->m_params.get_bool(":unsat-core", false)); + s->m_solver->set_produce_models(s->m_params.get_bool(":model", true)); + s->m_solver->set_front_end_params(mk_c(c)->fparams()); + s->m_solver->updt_params(s->m_params); + s->m_solver->init(m, s->m_logic); + s->m_initialized = true; + } + + static void init_solver(Z3_context c, Z3_solver s) { + if (!to_solver(s)->m_initialized) + init_solver_core(c, s); + } + Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c) { Z3_TRY; LOG_Z3_mk_simple_solver(c); RESET_ERROR_CODE(); Z3_solver_ref * s = alloc(Z3_solver_ref); - s->m_solver = mk_default_solver(); - s->m_solver->set_front_end_params(mk_c(c)->fparams()); - s->m_solver->init(mk_c(c)->m(), symbol::null); + s->m_solver = mk_smt_solver(); mk_c(c)->save_object(s); Z3_solver r = of_solver(s); RETURN_Z3(r); @@ -53,8 +68,6 @@ extern "C" { RESET_ERROR_CODE(); Z3_solver_ref * s = alloc(Z3_solver_ref); s->m_solver = mk_smt_strategic_solver(); - s->m_solver->set_front_end_params(mk_c(c)->fparams()); - s->m_solver->init(mk_c(c)->m(), symbol::null); mk_c(c)->save_object(s); Z3_solver r = of_solver(s); RETURN_Z3(r); @@ -65,10 +78,8 @@ extern "C" { Z3_TRY; LOG_Z3_mk_solver_for_logic(c, logic); RESET_ERROR_CODE(); - Z3_solver_ref * s = alloc(Z3_solver_ref); + Z3_solver_ref * s = alloc(Z3_solver_ref, to_symbol(logic)); s->m_solver = mk_smt_strategic_solver(true /* force solver to use tactics even when auto_config is disabled */); - s->m_solver->set_front_end_params(mk_c(c)->fparams()); - s->m_solver->init(mk_c(c)->m(), to_symbol(logic)); mk_c(c)->save_object(s); Z3_solver r = of_solver(s); RETURN_Z3(r); @@ -81,8 +92,6 @@ extern "C" { RESET_ERROR_CODE(); Z3_solver_ref * s = alloc(Z3_solver_ref); s->m_solver = alloc(tactic2solver, to_tactic_ref(t)); - s->m_solver->set_front_end_params(mk_c(c)->fparams()); - s->m_solver->init(mk_c(c)->m(), symbol::null); mk_c(c)->save_object(s); Z3_solver r = of_solver(s); RETURN_Z3(r); @@ -117,7 +126,13 @@ extern "C" { Z3_TRY; LOG_Z3_solver_set_params(c, s, p); RESET_ERROR_CODE(); - to_solver_ref(s)->updt_params(to_param_ref(p)); + if (to_solver(s)->m_initialized) { + bool old_model = to_solver(s)->m_params.get_bool(":model", true); + bool new_model = to_param_ref(p).get_bool(":model", true); + if (old_model != new_model) + to_solver_ref(s)->set_produce_models(new_model); + to_solver_ref(s)->updt_params(to_param_ref(p)); + } to_solver(s)->m_params = to_param_ref(p); Z3_CATCH; } @@ -142,6 +157,7 @@ extern "C" { Z3_TRY; LOG_Z3_solver_push(c, s); RESET_ERROR_CODE(); + init_solver(c, s); to_solver_ref(s)->push(); Z3_CATCH; } @@ -150,6 +166,7 @@ extern "C" { Z3_TRY; LOG_Z3_solver_pop(c, s, n); RESET_ERROR_CODE(); + init_solver(c, s); if (n > to_solver_ref(s)->get_scope_level()) { SET_ERROR_CODE(Z3_IOB); return; @@ -164,7 +181,7 @@ extern "C" { LOG_Z3_solver_reset(c, s); RESET_ERROR_CODE(); to_solver_ref(s)->reset(); - to_solver_ref(s)->init(mk_c(c)->m(), symbol::null); + to_solver(s)->m_initialized = false; Z3_CATCH; } @@ -172,6 +189,7 @@ extern "C" { Z3_TRY; LOG_Z3_solver_get_num_scopes(c, s); RESET_ERROR_CODE(); + init_solver(c, s); return to_solver_ref(s)->get_scope_level(); Z3_CATCH_RETURN(0); } @@ -180,7 +198,8 @@ extern "C" { Z3_TRY; LOG_Z3_solver_assert(c, s, a); RESET_ERROR_CODE(); - CHECK_FORMULA(a,); + init_solver(c, s); + CHECK_FORMULA(a,); to_solver_ref(s)->assert_expr(to_expr(a)); Z3_CATCH; } @@ -189,6 +208,7 @@ extern "C" { Z3_TRY; LOG_Z3_solver_get_assertions(c, s); RESET_ERROR_CODE(); + init_solver(c, s); Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m()); mk_c(c)->save_object(v); unsigned sz = to_solver_ref(s)->get_num_assertions(); @@ -207,9 +227,6 @@ extern "C" { } } expr * const * _assumptions = to_exprs(assumptions); - to_solver_ref(s)->set_produce_models(to_solver(s)->m_params.get_bool(":model", true)); - to_solver_ref(s)->set_produce_proofs(mk_c(c)->m().proofs_enabled()); - to_solver_ref(s)->set_produce_unsat_cores(num_assumptions > 0); unsigned timeout = to_solver(s)->m_params.get_uint(":timeout", UINT_MAX); bool use_ctrl_c = to_solver(s)->m_params.get_bool(":ctrl-c", false); cancel_eh eh(*to_solver_ref(s)); @@ -233,6 +250,7 @@ extern "C" { Z3_TRY; LOG_Z3_solver_check(c, s); RESET_ERROR_CODE(); + init_solver(c, s); return _solver_check(c, s, 0, 0); Z3_CATCH_RETURN(Z3_L_UNDEF); } @@ -241,6 +259,7 @@ extern "C" { Z3_TRY; LOG_Z3_solver_check_assumptions(c, s, num_assumptions, assumptions); RESET_ERROR_CODE(); + init_solver(c, s); return _solver_check(c, s, num_assumptions, assumptions); Z3_CATCH_RETURN(Z3_L_UNDEF); } @@ -249,6 +268,7 @@ extern "C" { Z3_TRY; LOG_Z3_solver_get_model(c, s); RESET_ERROR_CODE(); + init_solver(c, s); model_ref _m; to_solver_ref(s)->get_model(_m); if (!_m) { @@ -266,6 +286,7 @@ extern "C" { Z3_TRY; LOG_Z3_solver_get_proof(c, s); RESET_ERROR_CODE(); + init_solver(c, s); proof * p = to_solver_ref(s)->get_proof(); if (!p) { SET_ERROR_CODE(Z3_INVALID_USAGE); @@ -280,6 +301,7 @@ extern "C" { Z3_TRY; LOG_Z3_solver_get_unsat_core(c, s); RESET_ERROR_CODE(); + init_solver(c, s); ptr_vector core; to_solver_ref(s)->get_unsat_core(core); Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m()); @@ -295,6 +317,7 @@ extern "C" { Z3_TRY; LOG_Z3_solver_get_reason_unknown(c, s); RESET_ERROR_CODE(); + init_solver(c, s); return mk_c(c)->mk_external_string(to_solver_ref(s)->reason_unknown()); Z3_CATCH_RETURN(""); } @@ -303,6 +326,7 @@ extern "C" { Z3_TRY; LOG_Z3_solver_get_statistics(c, s); RESET_ERROR_CODE(); + init_solver(c, s); Z3_stats_ref * st = alloc(Z3_stats_ref); to_solver_ref(s)->collect_statistics(st->m_stats); mk_c(c)->save_object(st); @@ -315,6 +339,7 @@ extern "C" { Z3_TRY; LOG_Z3_solver_to_string(c, s); RESET_ERROR_CODE(); + init_solver(c, s); std::ostringstream buffer; to_solver_ref(s)->display(buffer); return mk_c(c)->mk_external_string(buffer.str()); diff --git a/src/api/api_solver.h b/src/api/api_solver.h index a39475bac..1569ef0da 100644 --- a/src/api/api_solver.h +++ b/src/api/api_solver.h @@ -24,7 +24,10 @@ Revision History: struct Z3_solver_ref : public api::object { solver * m_solver; params_ref m_params; - Z3_solver_ref():m_solver(0) {} + bool m_initialized; + symbol m_logic; + Z3_solver_ref():m_solver(0), m_initialized(false), m_logic(symbol::null) {} + Z3_solver_ref(symbol const & logic):m_solver(0), m_initialized(false), m_logic(logic) {} virtual ~Z3_solver_ref() { dealloc(m_solver); } }; diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp index bb083b7fc..cd4b797e3 100644 --- a/src/api/api_solver_old.cpp +++ b/src/api/api_solver_old.cpp @@ -41,7 +41,7 @@ extern "C" { LOG_Z3_pop(c, num_scopes); RESET_ERROR_CODE(); CHECK_SEARCHING(c); - if (num_scopes > mk_c(c)->get_solver().get_scope_level()) { + if (num_scopes > mk_c(c)->get_smt_kernel().get_scope_level()) { SET_ERROR_CODE(Z3_IOB); return; } @@ -73,7 +73,7 @@ extern "C" { LOG_Z3_check_and_get_model(c, m); RESET_ERROR_CODE(); CHECK_SEARCHING(c); - cancel_eh eh(mk_c(c)->get_solver()); + cancel_eh eh(mk_c(c)->get_smt_kernel()); api::context::set_interruptable(*(mk_c(c)), eh); flet _model(mk_c(c)->fparams().m_model, true); lbool result; @@ -120,7 +120,7 @@ extern "C" { LOG_Z3_get_implied_equalities(c, num_terms, terms, class_ids); RESET_ERROR_CODE(); CHECK_SEARCHING(c); - lbool result = smt::implied_equalities(mk_c(c)->get_solver(), num_terms, to_exprs(terms), class_ids); + lbool result = smt::implied_equalities(mk_c(c)->get_smt_kernel(), num_terms, to_exprs(terms), class_ids); return static_cast(result); Z3_CATCH_RETURN(Z3_L_UNDEF); } @@ -136,13 +136,13 @@ extern "C" { 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_solver()); + cancel_eh eh(mk_c(c)->get_smt_kernel()); api::context::set_interruptable(*(mk_c(c)), eh); lbool result; - result = mk_c(c)->get_solver().check(num_assumptions, _assumptions); + result = mk_c(c)->get_smt_kernel().check(num_assumptions, _assumptions); if (result != l_false && m) { model_ref _m; - mk_c(c)->get_solver().get_model(_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; @@ -156,19 +156,19 @@ extern "C" { } } if (result == l_false && core_size) { - *core_size = mk_c(c)->get_solver().get_unsat_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_solver().get_unsat_core_expr(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_solver().get_proof()); + *proof = of_ast(mk_c(c)->get_smt_kernel().get_proof()); } else if (proof) { *proof = 0; // breaks abstraction. @@ -182,7 +182,7 @@ extern "C" { LOG_Z3_get_search_failure(c); RESET_ERROR_CODE(); CHECK_SEARCHING(c); - smt::failure f = mk_c(c)->get_solver().last_failure(); + smt::failure f = mk_c(c)->get_smt_kernel().last_failure(); return api::mk_Z3_search_failure(f); Z3_CATCH_RETURN(Z3_UNKNOWN); } @@ -209,8 +209,8 @@ extern "C" { buffer labl_syms; ast_manager& m = mk_c(c)->m(); expr_ref_vector lits(m); - mk_c(c)->get_solver().get_relevant_labels(0, labl_syms); - mk_c(c)->get_solver().get_relevant_labeled_literals(mk_c(c)->fparams().m_at_labels_cex, lits); + 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) { @@ -226,7 +226,7 @@ extern "C" { RESET_ERROR_CODE(); ast_manager& m = mk_c(c)->m(); expr_ref_vector lits(m); - mk_c(c)->get_solver().get_relevant_literals(lits); + 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())); @@ -241,7 +241,7 @@ extern "C" { RESET_ERROR_CODE(); ast_manager& m = mk_c(c)->m(); expr_ref_vector lits(m); - mk_c(c)->get_solver().get_guessed_literals(lits); + 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())); @@ -316,7 +316,7 @@ extern "C" { LOG_Z3_context_to_string(c); RESET_ERROR_CODE(); std::ostringstream buffer; - mk_c(c)->get_solver().display(buffer); + mk_c(c)->get_smt_kernel().display(buffer); return mk_c(c)->mk_external_string(buffer.str()); Z3_CATCH_RETURN(0); } @@ -328,7 +328,7 @@ extern "C" { ast_manager& m = mk_c(c)->m(); expr_ref result(m); expr_ref_vector assignment(m); - mk_c(c)->get_solver().get_assignments(assignment); + 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); @@ -339,7 +339,7 @@ extern "C" { LOG_Z3_statistics_to_string(c); RESET_ERROR_CODE(); std::ostringstream buffer; - mk_c(c)->get_solver().display_statistics(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); @@ -356,10 +356,10 @@ extern "C" { }; void Z3_display_statistics(Z3_context c, std::ostream& s) { - mk_c(c)->get_solver().display_statistics(s); + mk_c(c)->get_smt_kernel().display_statistics(s); } void Z3_display_istatistics(Z3_context c, std::ostream& s) { - mk_c(c)->get_solver().display_istatistics(s); + mk_c(c)->get_smt_kernel().display_istatistics(s); } diff --git a/src/api/api_user_theory.cpp b/src/api/api_user_theory.cpp index bb0c582bf..fde34bbb2 100644 --- a/src/api/api_user_theory.cpp +++ b/src/api/api_user_theory.cpp @@ -35,11 +35,11 @@ extern "C" { Z3_theory Z3_mk_theory(Z3_context c, Z3_string th_name, void * ext_data) { Z3_TRY; RESET_ERROR_CODE(); - if (mk_c(c)->get_solver().get_scope_level() > 0) { + if (mk_c(c)->get_smt_kernel().get_scope_level() > 0) { SET_ERROR_CODE(Z3_INVALID_USAGE); return 0; } - return reinterpret_cast(mk_user_theory(mk_c(c)->get_solver(), c, ext_data, th_name)); + return reinterpret_cast(mk_user_theory(mk_c(c)->get_smt_kernel(), c, ext_data, th_name)); Z3_CATCH_RETURN(0); } diff --git a/src/ast/expr_substitution.cpp b/src/ast/expr_substitution.cpp index 00d741fda..8d6f0319c 100644 --- a/src/ast/expr_substitution.cpp +++ b/src/ast/expr_substitution.cpp @@ -139,6 +139,10 @@ bool expr_substitution::find(expr * c, expr * & def, proof * & def_pr, expr_depe return false; } +bool expr_substitution::contains(expr * s) { + return m_subst.contains(s); +} + void expr_substitution::reset() { dec_ref_map_key_values(m_manager, m_subst); if (proofs_enabled()) diff --git a/src/ast/expr_substitution.h b/src/ast/expr_substitution.h index 204a28cc1..507228f98 100644 --- a/src/ast/expr_substitution.h +++ b/src/ast/expr_substitution.h @@ -47,6 +47,7 @@ public: void erase(expr * s); bool find(expr * s, expr * & def, proof * & def_pr); bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep); + bool contains(expr * s); void reset(); void cleanup(); }; diff --git a/src/ast/macros/macro_substitution.cpp b/src/ast/macro_substitution.cpp similarity index 100% rename from src/ast/macros/macro_substitution.cpp rename to src/ast/macro_substitution.cpp diff --git a/src/ast/macros/macro_substitution.h b/src/ast/macro_substitution.h similarity index 100% rename from src/ast/macros/macro_substitution.h rename to src/ast/macro_substitution.h diff --git a/src/ast/rewriter/expr_replacer.cpp b/src/ast/rewriter/expr_replacer.cpp index 829e82092..4265fc1ad 100644 --- a/src/ast/rewriter/expr_replacer.cpp +++ b/src/ast/rewriter/expr_replacer.cpp @@ -114,6 +114,10 @@ public: virtual unsigned get_num_steps() const { return m_replacer.get_num_steps(); } + + virtual void reset() { + m_replacer.reset(); + } }; expr_replacer * mk_default_expr_replacer(ast_manager & m) { @@ -149,6 +153,11 @@ public: virtual unsigned get_num_steps() const { return m_r.get_num_steps(); } + + virtual void reset() { + m_r.reset(); + } + }; expr_replacer * mk_expr_simp_replacer(ast_manager & m, params_ref const & p) { diff --git a/src/ast/rewriter/expr_replacer.h b/src/ast/rewriter/expr_replacer.h index 722c0ff12..5bd72dc76 100644 --- a/src/ast/rewriter/expr_replacer.h +++ b/src/ast/rewriter/expr_replacer.h @@ -43,8 +43,8 @@ public: void reset_cancel() { set_cancel(false); } virtual void set_cancel(bool f) = 0; virtual unsigned get_num_steps() const { return 0; } - - + virtual void reset() = 0; + void apply_substitution(expr * s, expr * def, proof * def_pr, expr_ref & t); void apply_substitution(expr * s, expr * def, expr_ref & t); }; diff --git a/src/ast/simplifier/poly_simplifier_plugin.h b/src/ast/simplifier/poly_simplifier_plugin.h index 66ecf4bb0..ec4aa336e 100644 --- a/src/ast/simplifier/poly_simplifier_plugin.h +++ b/src/ast/simplifier/poly_simplifier_plugin.h @@ -134,6 +134,10 @@ public: virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result); virtual bool reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result); + virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { + return simplifier_plugin::reduce(f, num_args, args, result); + } + expr * get_monomial_body(expr * m); int get_monomial_body_order(expr * m); diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index c6fa7718c..4c24b5ae6 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -359,14 +359,14 @@ class set_option_cmd : public set_get_option_cmd { } else if (m_option == m_produce_proofs) { check_not_initialized(ctx, m_produce_proofs); - ctx.params().m_proof_mode = to_bool(value) ? PGM_FINE : PGM_DISABLED; + ctx.set_produce_proofs(to_bool(value)); } else if (m_option == m_produce_unsat_cores) { check_not_initialized(ctx, m_produce_unsat_cores); ctx.set_produce_unsat_cores(to_bool(value)); } else if (m_option == m_produce_models) { - ctx.params().m_model = to_bool(value); + ctx.set_produce_models(to_bool(value)); } else if (m_option == m_produce_assignments) { ctx.set_produce_assignments(to_bool(value)); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index c56066827..2d0d349d7 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -348,6 +348,24 @@ cmd_context::~cmd_context() { } } +void cmd_context::set_produce_models(bool f) { + params().m_model = f; + if (m_solver) + m_solver->set_produce_models(f); +} + +void cmd_context::set_produce_unsat_cores(bool f) { + // can only be set before initialization + SASSERT(!has_manager()); + m_produce_unsat_cores = f; +} + +void cmd_context::set_produce_proofs(bool f) { + // can only be set before initialization + SASSERT(!has_manager()); + params().m_proof_mode = f ? PGM_FINE : PGM_DISABLED; +} + bool cmd_context::is_smtlib2_compliant() const { return params().m_smtlib2_compliant; } @@ -540,8 +558,12 @@ void cmd_context::init_manager_core(bool new_manager) { // it prevents clashes with builtin types. insert(pm().mk_plist_decl()); } - if (m_solver) + if (m_solver) { + m_solver->set_produce_unsat_cores(m_produce_unsat_cores); + m_solver->set_produce_models(params().m_model); + m_solver->set_produce_proofs(params().m_proof_mode == PGM_FINE); m_solver->init(m(), m_logic); + } m_check_logic.set_logic(m(), m_logic); } @@ -1076,7 +1098,6 @@ void cmd_context::reset(bool finalize) { reset_macros(); reset_func_decls(); restore_assertions(0); - restore_assumptions(0); if (m_solver) m_solver->reset(); m_pp_env = 0; @@ -1108,6 +1129,8 @@ void cmd_context::assert_expr(expr * t) { m_check_sat_result = 0; m().inc_ref(t); m_assertions.push_back(t); + if (m_produce_unsat_cores) + m_assertion_names.push_back(0); if (m_solver) m_solver->assert_expr(t); } @@ -1119,11 +1142,14 @@ void cmd_context::assert_expr(symbol const & name, expr * t) { assert_expr(t); return; } - app * proxy = m().mk_const(name, m().mk_bool_sort()); - expr * new_t = m().mk_implies(proxy, t); - m().inc_ref(proxy); - m_assumptions.push_back(proxy); - assert_expr(new_t); + m_check_sat_result = 0; + m().inc_ref(t); + m_assertions.push_back(t); + expr * ans = m().mk_const(name, m().mk_bool_sort()); + m().inc_ref(ans); + m_assertion_names.push_back(ans); + if (m_solver) + m_solver->assert_expr(t, ans); } void cmd_context::push() { @@ -1137,7 +1163,6 @@ void cmd_context::push() { s.m_macros_stack_lim = m_macros_stack.size(); s.m_aux_pdecls_lim = m_aux_pdecls.size(); s.m_assertions_lim = m_assertions.size(); - s.m_assumptions_lim = m_assumptions.size(); if (m_solver) m_solver->push(); } @@ -1200,29 +1225,25 @@ void cmd_context::restore_aux_pdecls(unsigned old_sz) { m_aux_pdecls.shrink(old_sz); } +static void restore(ast_manager & m, ptr_vector & c, unsigned old_sz) { + ptr_vector::iterator it = c.begin() + old_sz; + ptr_vector::iterator end = c.end(); + for (; it != end; ++it) { + m.dec_ref(*it); + } + c.shrink(old_sz); +} + void cmd_context::restore_assertions(unsigned old_sz) { SASSERT(old_sz <= m_assertions.size()); SASSERT(!m_interactive_mode || m_assertions.size() == m_assertion_strings.size()); - ptr_vector::iterator it = m_assertions.begin() + old_sz; - ptr_vector::iterator end = m_assertions.end(); - for (; it != end; ++it) { - m().dec_ref(*it); - } - m_assertions.shrink(old_sz); + restore(m(), m_assertions, old_sz); + if (m_produce_unsat_cores) + restore(m(), m_assertion_names, old_sz); if (m_interactive_mode) m_assertion_strings.shrink(old_sz); } -void cmd_context::restore_assumptions(unsigned old_sz) { - SASSERT(old_sz <= m_assumptions.size()); - ptr_vector::iterator it = m_assumptions.begin() + old_sz; - ptr_vector::iterator end = m_assumptions.end(); - for (; it != end; ++it) { - m().dec_ref(*it); - } - m_assumptions.shrink(old_sz); -} - void cmd_context::pop(unsigned n) { m_check_sat_result = 0; if (n == 0) @@ -1240,7 +1261,6 @@ void cmd_context::pop(unsigned n) { restore_macros(s.m_macros_stack_lim); restore_aux_pdecls(s.m_aux_pdecls_lim); restore_assertions(s.m_assertions_lim); - restore_assumptions(s.m_assumptions_lim); m_scopes.shrink(new_lvl); } @@ -1260,17 +1280,12 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions m_check_sat_result = m_solver.get(); // solver itself stores the result. m_solver->set_front_end_params(params()); m_solver->set_progress_callback(this); - m_solver->set_produce_proofs(produce_proofs()); - m_solver->set_produce_models(produce_models()); - m_solver->set_produce_unsat_cores(produce_unsat_cores()); scoped_watch sw(*this); cancel_eh eh(*m_solver); scoped_ctrl_c ctrlc(eh); - unsigned old_sz = m_assumptions.size(); - m_assumptions.append(num_assumptions, assumptions); lbool r; try { - r = m_solver->check_sat(m_assumptions.size(), m_assumptions.c_ptr()); + r = m_solver->check_sat(num_assumptions, assumptions); } catch (z3_error & ex) { throw ex; @@ -1278,7 +1293,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions catch (z3_exception & ex) { throw cmd_exception(ex.msg()); } - m_assumptions.shrink(old_sz); m_solver->set_status(r); display_sat_result(r); validate_check_sat_result(r); @@ -1410,6 +1424,9 @@ void cmd_context::set_solver(solver * s) { m_solver = s; m_solver->set_front_end_params(params()); if (has_manager() && s != 0) { + m_solver->set_produce_unsat_cores(m_produce_unsat_cores); + m_solver->set_produce_models(params().m_model); + m_solver->set_produce_proofs(params().m_proof_mode == PGM_FINE); m_solver->init(m(), m_logic); // assert formulas and create scopes in the new solver. unsigned lim = 0; diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 9296f0735..34a3375d7 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -175,16 +175,15 @@ protected: ptr_vector m_aux_pdecls; ptr_vector m_assertions; vector m_assertion_strings; - ptr_vector m_assumptions; // for unsat-core extraction + ptr_vector m_assertion_names; // named assertions are represented using boolean variables. struct scope { unsigned m_func_decls_stack_lim; unsigned m_psort_decls_stack_lim; unsigned m_macros_stack_lim; unsigned m_aux_pdecls_lim; - // only m_assertions_lim and m_assumptions_lim are relevant when m_global_decls = true + // only m_assertions_lim is relevant when m_global_decls = true unsigned m_assertions_lim; - unsigned m_assumptions_lim; }; svector m_scopes; @@ -225,7 +224,6 @@ protected: void restore_macros(unsigned old_sz); void restore_aux_pdecls(unsigned old_sz); void restore_assertions(unsigned old_sz); - void restore_assumptions(unsigned old_sz); void erase_func_decl_core(symbol const & s, func_decl * f); void erase_psort_decl_core(symbol const & s); @@ -272,7 +270,9 @@ public: bool produce_models() const; bool produce_proofs() const; bool produce_unsat_cores() const { return m_produce_unsat_cores; } - void set_produce_unsat_cores(bool flag) { m_produce_unsat_cores = flag; } + void set_produce_models(bool flag); + void set_produce_unsat_cores(bool flag); + void set_produce_proofs(bool flag); bool produce_assignments() const { return m_produce_assignments; } void set_produce_assignments(bool flag) { m_produce_assignments = flag; } void set_status(status st) { m_status = st; } @@ -369,8 +369,8 @@ public: ptr_vector::const_iterator begin_assertions() const { return m_assertions.begin(); } ptr_vector::const_iterator end_assertions() const { return m_assertions.end(); } - ptr_vector::const_iterator begin_assumptions() const { return m_assumptions.begin(); } - ptr_vector::const_iterator end_assumptions() const { return m_assumptions.end(); } + ptr_vector::const_iterator begin_assertion_names() const { return m_assertion_names.begin(); } + ptr_vector::const_iterator end_assertion_names() const { return m_assertion_names.end(); } /** \brief Hack: consume assertions if there are no scopes. @@ -380,7 +380,6 @@ public: if (num_scopes() > 0) return false; restore_assertions(0); - restore_assumptions(0); return true; } diff --git a/src/cmd_context/cmd_context_to_goal.cpp b/src/cmd_context/cmd_context_to_goal.cpp index 21f8445d5..26cb2766b 100644 --- a/src/cmd_context/cmd_context_to_goal.cpp +++ b/src/cmd_context/cmd_context_to_goal.cpp @@ -27,20 +27,22 @@ void assert_exprs_from(cmd_context const & ctx, goal & t) { throw cmd_exception("Frontend does not support simultaneous generation of proofs and unsat cores"); ast_manager & m = t.m(); bool proofs_enabled = t.proofs_enabled(); - ptr_vector::const_iterator it = ctx.begin_assertions(); - ptr_vector::const_iterator end = ctx.end_assertions(); - for (; it != end; ++it) { - t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : 0, 0); - } if (ctx.produce_unsat_cores()) { - SASSERT(!ctx.produce_proofs()); - it = ctx.begin_assumptions(); - end = ctx.end_assumptions(); - for (; it != end; ++it) { - t.assert_expr(*it, 0, m.mk_leaf(*it)); + ptr_vector::const_iterator it = ctx.begin_assertions(); + ptr_vector::const_iterator end = ctx.end_assertions(); + ptr_vector::const_iterator it2 = ctx.begin_assertion_names(); + ptr_vector::const_iterator end2 = ctx.end_assertion_names(); + SASSERT(end - it == end2 - it2); + for (; it != end; ++it, ++it2) { + t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : 0, m.mk_leaf(*it2)); } } else { - SASSERT(ctx.begin_assumptions() == ctx.end_assumptions()); + ptr_vector::const_iterator it = ctx.begin_assertions(); + ptr_vector::const_iterator end = ctx.end_assertions(); + for (; it != end; ++it) { + t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : 0, 0); + } + SASSERT(ctx.begin_assertion_names() == ctx.end_assertion_names()); } } diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h index 36b1dcd51..76ad2a020 100644 --- a/src/cmd_context/pdecl.h +++ b/src/cmd_context/pdecl.h @@ -181,6 +181,7 @@ class paccessor_decl : public pdecl { ptype const & get_type() const { return m_type; } virtual ~paccessor_decl() {} public: + virtual void display(std::ostream & out) const { pdecl::display(out); } void display(std::ostream & out, pdatatype_decl const * const * dts) const; }; @@ -201,6 +202,7 @@ class pconstructor_decl : public pdecl { constructor_decl * instantiate_decl(pdecl_manager & m, sort * const * s); virtual ~pconstructor_decl() {} public: + virtual void display(std::ostream & out) const { pdecl::display(out); } void display(std::ostream & out, pdatatype_decl const * const * dts) const; }; diff --git a/src/cmd_context/strategic_solver_cmd.cpp b/src/cmd_context/strategic_solver_cmd.cpp deleted file mode 100644 index 3bb820e0d..000000000 --- a/src/cmd_context/strategic_solver_cmd.cpp +++ /dev/null @@ -1,34 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - strategic_solver_cmd.h - -Abstract: - - Specialization of the strategic solver that - used cmd_context to access the assertion set. - -Author: - - Leonardo (leonardo) 2012-11-01 - -Notes: - ---*/ -#include"strategic_solver_cmd.h" -#include"cmd_context.h" - -strategic_solver_cmd::strategic_solver_cmd(cmd_context & ctx): - m_ctx(ctx) { -} - -unsigned strategic_solver_cmd::get_num_assertions() const { - return static_cast(m_ctx.end_assertions() - m_ctx.begin_assertions()); -} - -expr * strategic_solver_cmd::get_assertion(unsigned idx) const { - SASSERT(idx < get_num_assertions()); - return m_ctx.begin_assertions()[idx]; -} diff --git a/src/cmd_context/strategic_solver_cmd.h b/src/cmd_context/strategic_solver_cmd.h deleted file mode 100644 index 014d2dee6..000000000 --- a/src/cmd_context/strategic_solver_cmd.h +++ /dev/null @@ -1,40 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - strategic_solver_cmd.h - -Abstract: - - Specialization of the strategic solver that - used cmd_context to access the assertion set. - -Author: - - Leonardo (leonardo) 2012-11-01 - -Notes: - ---*/ -#ifndef _STRATEGIC_SOLVER_CMD_H_ -#define _STRATEGIC_SOLVER_CMD_H_ - -#include"strategic_solver.h" - -class cmd_context; - -/** - Specialization for the SMT 2.0 command language frontend. - - The strategic solver does not have to maintain a copy of the assertion set in the cmd_context. -*/ -class strategic_solver_cmd : public strategic_solver_core { - cmd_context & m_ctx; -public: - strategic_solver_cmd(cmd_context & ctx); - virtual unsigned get_num_assertions() const; - virtual expr * get_assertion(unsigned idx) const; -}; - -#endif diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp index 8e0e3b9b7..91c2d72ee 100644 --- a/src/muz_qe/dl_bmc_engine.cpp +++ b/src/muz_qe/dl_bmc_engine.cpp @@ -21,7 +21,7 @@ Revision History: #include "dl_rule_transformer.h" #include "dl_bmc_engine.h" #include "dl_mk_slice.h" -#include "smt_solver.h" +#include "smt_kernel.h" #include "datatype_decl_plugin.h" #include "dl_mk_rule_inliner.h" #include "dl_decl_plugin.h" diff --git a/src/muz_qe/dl_bmc_engine.h b/src/muz_qe/dl_bmc_engine.h index e0e8ff3da..b8bb2e1e0 100644 --- a/src/muz_qe/dl_bmc_engine.h +++ b/src/muz_qe/dl_bmc_engine.h @@ -22,7 +22,7 @@ Revision History: #include "params.h" #include "statistics.h" -#include "smt_solver.h" +#include "smt_kernel.h" #include "bv_decl_plugin.h" @@ -33,7 +33,7 @@ namespace datalog { context& m_ctx; ast_manager& m; front_end_params m_fparams; - smt::solver m_solver; + smt::kernel m_solver; obj_map m_pred2sort; obj_map m_sort2pred; obj_map m_pred2newpred; diff --git a/src/muz_qe/dl_smt_relation.cpp b/src/muz_qe/dl_smt_relation.cpp index 572894d05..381b8f434 100644 --- a/src/muz_qe/dl_smt_relation.cpp +++ b/src/muz_qe/dl_smt_relation.cpp @@ -23,7 +23,7 @@ Revision History: #include "dl_context.h" #include "dl_smt_relation.h" #include "expr_abstract.h" -#include "smt_solver.h" +#include "smt_kernel.h" #include "th_rewriter.h" #include "qe.h" #include "datatype_decl_plugin.h" @@ -131,7 +131,7 @@ namespace datalog { front_end_params& params = get_plugin().get_fparams(); flet flet2(params.m_der, true); - smt::solver ctx(m, params); + smt::kernel ctx(m, params); expr_ref tmp(m); instantiate(r, tmp); ctx.assert_expr(tmp); @@ -184,7 +184,7 @@ namespace datalog { flet flet0(params.m_quant_elim, true); flet flet1(params.m_nnf_cnf, false); flet flet2(params.m_der, true); - smt::solver ctx(m, params); + smt::kernel ctx(m, params); ctx.assert_expr(fml_inst); lbool result = ctx.check(); TRACE("smt_relation", @@ -242,7 +242,7 @@ namespace datalog { eqs.resize(num_vars); instantiate(r, tmp); flet flet4(params.m_model, true); - smt::solver ctx(m, params); + smt::kernel ctx(m, params); ctx.assert_expr(tmp); while (true) { diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 5481bf218..0f426b6fd 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -1867,7 +1867,7 @@ namespace pdr { } bool context::check_invariant(unsigned lvl, func_decl* fn) { - smt::solver ctx(m, m_fparams); + smt::kernel ctx(m, m_fparams); pred_transformer& pt = *m_rels.find(fn); expr_ref_vector conj(m); expr_ref inv = pt.get_formulas(next_level(lvl), false); diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h index 8b654e2fb..19b1a6570 100644 --- a/src/muz_qe/pdr_context.h +++ b/src/muz_qe/pdr_context.h @@ -274,7 +274,7 @@ namespace pdr { (*this)(n, new_cores.back().first, new_cores.back().second); } } - virtual void collect_statistics(statistics& st) {} + virtual void collect_statistics(statistics& st) const {} }; class context { diff --git a/src/muz_qe/pdr_farkas_learner.cpp b/src/muz_qe/pdr_farkas_learner.cpp index 00bb5d723..3206c64da 100644 --- a/src/muz_qe/pdr_farkas_learner.cpp +++ b/src/muz_qe/pdr_farkas_learner.cpp @@ -251,7 +251,7 @@ namespace pdr { o2p(outer_mgr, m_pr) { reg_decl_plugins(m_pr); - m_ctx = alloc(smt::solver, m_pr, m_proof_params); + m_ctx = alloc(smt::kernel, m_pr, m_proof_params); } front_end_params farkas_learner::get_proof_params(front_end_params& orig_params) { @@ -325,7 +325,7 @@ namespace pdr { if (!m_ctx) { - m_ctx = alloc(smt::solver, m_pr, m_proof_params); + m_ctx = alloc(smt::kernel, m_pr, m_proof_params); } m_ctx->push(); diff --git a/src/muz_qe/pdr_farkas_learner.h b/src/muz_qe/pdr_farkas_learner.h index 888947049..56cb3640c 100644 --- a/src/muz_qe/pdr_farkas_learner.h +++ b/src/muz_qe/pdr_farkas_learner.h @@ -23,7 +23,7 @@ Revision History: #include "arith_decl_plugin.h" #include "ast_translation.h" #include "bv_decl_plugin.h" -#include "smt_solver.h" +#include "smt_kernel.h" #include "bool_rewriter.h" #include "pdr_util.h" #include "front_end_params.h" @@ -41,7 +41,7 @@ class farkas_learner { front_end_params m_proof_params; ast_manager m_pr; - scoped_ptr m_ctx; + scoped_ptr m_ctx; static front_end_params get_proof_params(front_end_params& orig_params); diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp index e0d584f09..3105485e0 100644 --- a/src/muz_qe/pdr_generalizers.cpp +++ b/src/muz_qe/pdr_generalizers.cpp @@ -463,7 +463,7 @@ namespace pdr { imp imp(m_ctx); ast_manager& m = core.get_manager(); expr_ref goal = imp.mk_induction_goal(p->pt(), p->level(), depth); - smt::solver ctx(m, m_ctx.get_fparams(), m_ctx.get_params()); + smt::kernel ctx(m, m_ctx.get_fparams(), m_ctx.get_params()); ctx.assert_expr(goal); lbool r = ctx.check(); TRACE("pdr", tout << r << "\n"; diff --git a/src/muz_qe/pdr_manager.cpp b/src/muz_qe/pdr_manager.cpp index 29f299b91..87edbc618 100644 --- a/src/muz_qe/pdr_manager.cpp +++ b/src/muz_qe/pdr_manager.cpp @@ -329,7 +329,7 @@ namespace pdr { bool manager::implication_surely_holds(expr * lhs, expr * rhs, expr * bg) { - smt::solver sctx(m, get_fparams()); + smt::kernel sctx(m, get_fparams()); if(bg) { sctx.assert_expr(bg); } diff --git a/src/muz_qe/pdr_manager.h b/src/muz_qe/pdr_manager.h index 87eaa03bf..398f2716f 100644 --- a/src/muz_qe/pdr_manager.h +++ b/src/muz_qe/pdr_manager.h @@ -28,7 +28,7 @@ Revision History: #include "expr_substitution.h" #include "map.h" #include "ref_vector.h" -#include "smt_solver.h" +#include "smt_kernel.h" #include "pdr_util.h" #include "pdr_sym_mux.h" #include "pdr_farkas_learner.h" diff --git a/src/muz_qe/pdr_prop_solver.h b/src/muz_qe/pdr_prop_solver.h index 2b7c1af6d..da0a1b31e 100644 --- a/src/muz_qe/pdr_prop_solver.h +++ b/src/muz_qe/pdr_prop_solver.h @@ -25,7 +25,7 @@ Revision History: #include #include "ast.h" #include "obj_hashtable.h" -#include "smt_solver.h" +#include "smt_kernel.h" #include "util.h" #include "vector.h" #include "pdr_manager.h" diff --git a/src/muz_qe/pdr_quantifiers.cpp b/src/muz_qe/pdr_quantifiers.cpp index df3938acf..362575a8b 100644 --- a/src/muz_qe/pdr_quantifiers.cpp +++ b/src/muz_qe/pdr_quantifiers.cpp @@ -152,7 +152,7 @@ namespace pdr { bool found_instance = false; expr_ref C(m); front_end_params fparams; - smt::solver solver(m, fparams); + smt::kernel solver(m, fparams); solver.assert_expr(m_A); for (unsigned i = 0; i < m_Bs.size(); ++i) { expr_ref_vector fresh_vars(m); @@ -344,7 +344,7 @@ namespace pdr { for (unsigned i = 0; i < fmls.size(); ++i) { tout << mk_pp(fmls[i].get(), mp) << "\n"; }); - smt::solver solver(mp, fparams); + smt::kernel solver(mp, fparams); for (unsigned i = 0; i < fmls.size(); ++i) { solver.assert_expr(fmls[i].get()); } diff --git a/src/muz_qe/pdr_smt_context_manager.cpp b/src/muz_qe/pdr_smt_context_manager.cpp index ec813f606..36b8e2325 100644 --- a/src/muz_qe/pdr_smt_context_manager.cpp +++ b/src/muz_qe/pdr_smt_context_manager.cpp @@ -52,7 +52,7 @@ namespace pdr { } - _smt_context::_smt_context(smt::solver & ctx, smt_context_manager& p, app* pred): + _smt_context::_smt_context(smt::kernel & ctx, smt_context_manager& p, app* pred): smt_context(p, ctx.m(), pred), m_context(ctx) {} @@ -104,21 +104,21 @@ namespace pdr { smt_context_manager::~smt_context_manager() { TRACE("pdr",tout << "\n";); - std::for_each(m_contexts.begin(), m_contexts.end(), delete_proc()); + std::for_each(m_contexts.begin(), m_contexts.end(), delete_proc()); } smt_context* smt_context_manager::mk_fresh() { ++m_num_contexts; app_ref pred(m); - smt::solver * ctx = 0; + smt::kernel * ctx = 0; if (m_max_num_contexts == 0) { - m_contexts.push_back(alloc(smt::solver, m, m_fparams)); + m_contexts.push_back(alloc(smt::kernel, m, m_fparams)); pred = m.mk_true(); ctx = m_contexts[m_num_contexts-1]; } else { if (m_contexts.size() < m_max_num_contexts) { - m_contexts.push_back(alloc(smt::solver, m, m_fparams)); + m_contexts.push_back(alloc(smt::kernel, m, m_fparams)); } std::stringstream name; name << "#context" << m_num_contexts; diff --git a/src/muz_qe/pdr_smt_context_manager.h b/src/muz_qe/pdr_smt_context_manager.h index cdff26a19..d6aef9776 100644 --- a/src/muz_qe/pdr_smt_context_manager.h +++ b/src/muz_qe/pdr_smt_context_manager.h @@ -20,7 +20,7 @@ Revision History: #ifndef _PDR_SMT_CONTEXT_MANAGER_H_ #define _PDR_SMT_CONTEXT_MANAGER_H_ -#include "smt_solver.h" +#include "smt_kernel.h" #include "sat_solver.h" #include "func_decl_dependencies.h" @@ -56,9 +56,9 @@ namespace pdr { }; class _smt_context : public smt_context { - smt::solver & m_context; + smt::kernel & m_context; public: - _smt_context(smt::solver & ctx, smt_context_manager& p, app* pred); + _smt_context(smt::kernel & ctx, smt_context_manager& p, app* pred); virtual ~_smt_context() {} virtual void assert_expr(expr* e); virtual lbool check(expr_ref_vector& assumptions); @@ -74,7 +74,7 @@ namespace pdr { class sat_context : public smt_context { sat::solver m_solver; public: - sat_context(smt::solver & ctx, smt_context_manager& p, app* pred); + sat_context(smt::kernel & ctx, smt_context_manager& p, app* pred); virtual ~sat_context() {} virtual void assert_expr(expr* e); virtual lbool check(expr_ref_vector& assumptions); @@ -91,7 +91,7 @@ namespace pdr { front_end_params& m_fparams; ast_manager& m; unsigned m_max_num_contexts; - ptr_vector m_contexts; + ptr_vector m_contexts; unsigned m_num_contexts; app_ref_vector m_predicate_list; func_decl_set m_predicate_set; diff --git a/src/muz_qe/qe.cpp b/src/muz_qe/qe.cpp index 1b92aa6e8..77750ced6 100644 --- a/src/muz_qe/qe.cpp +++ b/src/muz_qe/qe.cpp @@ -38,7 +38,7 @@ Revision History: #include "bool_rewriter.h" #include "dl_util.h" #include "th_rewriter.h" -#include "smt_solver.h" +#include "smt_kernel.h" #include "model_evaluator.h" #include "has_free_vars.h" #include "rewriter_def.h" @@ -1288,7 +1288,7 @@ namespace qe { ast_manager& m; quant_elim& m_qe; th_rewriter m_rewriter; - smt::solver m_solver; + smt::kernel m_solver; bv_util m_bv; expr_ref_vector m_literals; diff --git a/src/muz_qe/qe_sat_tactic.cpp b/src/muz_qe/qe_sat_tactic.cpp index e5a57871a..1480a8ca0 100644 --- a/src/muz_qe/qe_sat_tactic.cpp +++ b/src/muz_qe/qe_sat_tactic.cpp @@ -23,7 +23,7 @@ Revision History: #include "qe_sat_tactic.h" #include "quant_hoist.h" #include "ast_pp.h" -#include "smt_solver.h" +#include "smt_kernel.h" #include "qe.h" #include "cooperate.h" #include "model_v2_pp.h" @@ -66,8 +66,8 @@ namespace qe { bool m_strong_context_simplify_param; bool m_ctx_simplify_local_param; vector m_vars; - ptr_vector m_solvers; - smt::solver m_solver; + ptr_vector m_solvers; + smt::kernel m_solver; expr_ref m_fml; expr_ref_vector m_Ms; expr_ref_vector m_assignments; @@ -80,7 +80,7 @@ namespace qe { ast_manager& m; sat_tactic& m_super; - smt::solver& m_solver; + smt::kernel& m_solver; atom_set m_pos; atom_set m_neg; app_ref_vector m_vars; @@ -322,10 +322,10 @@ namespace qe { void init_Ms() { for (unsigned i = 0; i < num_alternations(); ++i) { m_Ms.push_back(m.mk_true()); - m_solvers.push_back(alloc(smt::solver, m, m_fparams, m_params)); + m_solvers.push_back(alloc(smt::kernel, m, m_fparams, m_params)); } m_Ms.push_back(m_fml); - m_solvers.push_back(alloc(smt::solver, m, m_fparams, m_params)); + m_solvers.push_back(alloc(smt::kernel, m, m_fparams, m_params)); m_solvers.back()->assert_expr(m_fml); } @@ -333,7 +333,7 @@ namespace qe { app_ref_vector const& vars(unsigned i) { return m_vars[i]; } - smt::solver& solver(unsigned i) { return *m_solvers[i]; } + smt::kernel& solver(unsigned i) { return *m_solvers[i]; } void reset() { m_fml = 0; @@ -468,7 +468,7 @@ namespace qe { remove_duplicates(pos, neg); // Assumption: B is already asserted in solver[i]. - smt::solver& solver = *m_solvers[i]; + smt::kernel& solver = *m_solvers[i]; solver.push(); solver.assert_expr(A); nnf_strengthen(solver, pos, m.mk_false(), sub); @@ -506,7 +506,7 @@ namespace qe { return Bnnf; } - void nnf_strengthen(smt::solver& solver, atom_set& atoms, expr* value, expr_substitution& sub) { + void nnf_strengthen(smt::kernel& solver, atom_set& atoms, expr* value, expr_substitution& sub) { atom_set::iterator it = atoms.begin(), end = atoms.end(); for (; it != end; ++it) { solver.push(); @@ -565,7 +565,7 @@ namespace qe { return Bnnf; } - void nnf_weaken(smt::solver& solver, expr_ref& B, atom_set& atoms, expr* value, expr_substitution& sub) { + void nnf_weaken(smt::kernel& solver, expr_ref& B, atom_set& atoms, expr* value, expr_substitution& sub) { atom_set::iterator it = atoms.begin(), end = atoms.end(); for (; it != end; ++it) { solver.push(); @@ -678,7 +678,7 @@ namespace qe { } bool is_sat(unsigned i, expr* ctx, model_ref& model) { - smt::solver& solver = *m_solvers[i]; + smt::kernel& solver = *m_solvers[i]; solver.push(); solver.assert_expr(ctx); lbool r = solver.check(); diff --git a/src/parsers/smt/smtlib_solver.cpp b/src/parsers/smt/smtlib_solver.cpp index 77c2455dc..dd54de350 100644 --- a/src/parsers/smt/smtlib_solver.cpp +++ b/src/parsers/smt/smtlib_solver.cpp @@ -83,7 +83,7 @@ namespace smtlib { benchmark.add_formula(m_ast_manager.mk_true()); } m_ctx = alloc(cmd_context, &m_params, true, &m_ast_manager, benchmark.get_logic()); - m_ctx->set_solver(mk_smt_strategic_solver(*m_ctx)); + m_ctx->set_solver(mk_smt_strategic_solver(false)); theory::expr_iterator fit = benchmark.begin_formulas(); theory::expr_iterator fend = benchmark.end_formulas(); for (; fit != fend; ++fit) diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp index 6711158fd..08b070183 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/src/shell/smtlib_frontend.cpp @@ -106,7 +106,7 @@ unsigned read_smtlib2_commands(char const* file_name, front_end_params& front_en ctx.set_solver(s); } else { - solver * s = mk_smt_strategic_solver(ctx); + solver * s = mk_smt_strategic_solver(false); ctx.set_solver(s); } install_dl_cmds(ctx); diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 368889cdc..4a6cfd85d 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -60,7 +60,6 @@ asserted_formulas::asserted_formulas(ast_manager & m, front_end_params & p): m_macro_manager(m, m_simplifier), m_bit2int(m), m_bv_sharing(m), - m_user_rewriter(m), m_inconsistent(false), m_cancel_flag(false) { @@ -282,7 +281,6 @@ void asserted_formulas::reset() { } void asserted_formulas::set_cancel_flag(bool f) { - m_user_rewriter.set_cancel(f); m_cancel_flag = f; } @@ -341,7 +339,6 @@ void asserted_formulas::reduce() { TRACE("qbv_bug", tout << "after demod:\n"; display(tout);); INVOKE(m_params.m_quasi_macros && has_quantifiers(), apply_quasi_macros()); INVOKE(m_params.m_simplify_bit2int, apply_bit2int()); - INVOKE(m_user_rewriter.enabled(), apply_user_rewriter()); INVOKE(m_params.m_eliminate_bounds && has_quantifiers(), cheap_quant_fourier_motzkin()); INVOKE(!m_params.m_bb_eager && has_quantifiers() && m_params.m_ematching, infer_patterns()); INVOKE(m_params.m_max_bv_sharing && has_bv(), max_bv_sharing()); @@ -1414,8 +1411,6 @@ void asserted_formulas::refine_inj_axiom() { MK_SIMPLIFIER(apply_bit2int, bit2int& functor = m_bit2int, "bit2int", "propagate bit-vector over integers", true); -MK_SIMPLIFIER(apply_user_rewriter, user_rewriter& functor = m_user_rewriter, "user_rewriter", "apply user supplied rewriting", true); - MK_SIMPLIFIER(apply_der_core, der_star functor(m_manager), "der", "destructive equality resolution", true); void asserted_formulas::apply_der() { diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h index b08ac90d3..94bb41682 100644 --- a/src/smt/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -30,7 +30,6 @@ Revision History: #include"maximise_ac_sharing.h" #include"bit2int.h" #include"statistics.h" -#include"user_rewriter.h" #include"pattern_inference.h" class arith_simplifier_plugin; @@ -66,8 +65,6 @@ class asserted_formulas { maximise_bv_sharing m_bv_sharing; - user_rewriter m_user_rewriter; - bool m_inconsistent; // qe::expr_quant_elim_star1 m_quant_elim; @@ -98,7 +95,6 @@ class asserted_formulas { void apply_quasi_macros(); void nnf_cnf(); bool apply_eager_bit_blaster(); - bool apply_user_rewriter(); void infer_patterns(); void eliminate_term_ite(); void reduce_and_solve(); @@ -157,7 +153,6 @@ public: void init(unsigned num_formulas, expr * const * formulas, proof * const * prs); void register_simplifier_plugin(simplifier_plugin * p) { m_simplifier.register_plugin(p); } simplifier & get_simplifier() { return m_simplifier; } - void set_user_rewriter(void* ctx, user_rewriter::fn* rw) { m_user_rewriter.set_rewriter(ctx, rw); } void get_assertions(ptr_vector & result); bool empty() const { return m_asserted_formulas.empty(); } void collect_static_features(); diff --git a/src/smt/default_solver.cpp b/src/smt/default_solver.cpp deleted file mode 100644 index 73ce084f3..000000000 --- a/src/smt/default_solver.cpp +++ /dev/null @@ -1,181 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - default_solver.cpp - -Abstract: - - Wrapps smt::solver as a solver for cmd_context - -Author: - - Leonardo (leonardo) 2012-10-21 - -Notes: - ---*/ -#include"solver.h" -#include"smt_solver.h" -#include"reg_decl_plugins.h" -#include"front_end_params.h" - -class default_solver : public solver { - front_end_params * m_params; - smt::solver * m_context; -public: - default_solver():m_params(0), m_context(0) {} - - virtual ~default_solver() { - if (m_context != 0) - dealloc(m_context); - } - - virtual void set_front_end_params(front_end_params & p) { - m_params = &p; - } - - virtual void updt_params(params_ref const & p) { - if (m_context == 0) - return; - m_context->updt_params(p); - } - - virtual void collect_param_descrs(param_descrs & r) { - if (m_context == 0) { - ast_manager m; - reg_decl_plugins(m); - front_end_params p; - smt::solver s(m, p); - s.collect_param_descrs(r); - } - else { - m_context->collect_param_descrs(r); - } - } - - virtual void init(ast_manager & m, symbol const & logic) { - SASSERT(m_params); - reset(); - #pragma omp critical (solver) - { - m_context = alloc(smt::solver, m, *m_params); - } - if (logic != symbol::null) - m_context->set_logic(logic); - } - - virtual void collect_statistics(statistics & st) const { - if (m_context == 0) { - return; - } - else { - m_context->collect_statistics(st); - } - } - - virtual void reset() { - if (m_context != 0) { - #pragma omp critical (solver) - { - dealloc(m_context); - m_context = 0; - } - } - } - - virtual void assert_expr(expr * t) { - SASSERT(m_context); - m_context->assert_expr(t); - } - - virtual void push() { - SASSERT(m_context); - m_context->push(); - } - - virtual void pop(unsigned n) { - SASSERT(m_context); - m_context->pop(n); - } - - virtual unsigned get_scope_level() const { - if (m_context) - return m_context->get_scope_level(); - else - return 0; - } - - virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) { - SASSERT(m_context); - return m_context->check(num_assumptions, assumptions); - } - - virtual void get_unsat_core(ptr_vector & r) { - SASSERT(m_context); - unsigned sz = m_context->get_unsat_core_size(); - for (unsigned i = 0; i < sz; i++) - r.push_back(m_context->get_unsat_core_expr(i)); - } - - virtual void get_model(model_ref & m) { - SASSERT(m_context); - m_context->get_model(m); - } - - virtual proof * get_proof() { - SASSERT(m_context); - return m_context->get_proof(); - } - - virtual std::string reason_unknown() const { - SASSERT(m_context); - return m_context->last_failure_as_string(); - } - - virtual void get_labels(svector & r) { - SASSERT(m_context); - buffer tmp; - m_context->get_relevant_labels(0, tmp); - r.append(tmp.size(), tmp.c_ptr()); - } - - virtual void set_cancel(bool f) { - #pragma omp critical (solver) - { - if (m_context) - m_context->set_cancel(f); - } - } - - virtual void set_progress_callback(progress_callback * callback) { - SASSERT(m_context); - m_context->set_progress_callback(callback); - } - - virtual unsigned get_num_assertions() const { - if (m_context) - return m_context->size(); - else - return 0; - } - - virtual expr * get_assertion(unsigned idx) const { - SASSERT(m_context); - SASSERT(idx < get_num_assertions()); - return m_context->get_formulas()[idx]; - } - - virtual void display(std::ostream & out) const { - if (m_context) - m_context->display(out); - else - out << "(solver)"; - } - -}; - -solver * mk_default_solver() { - return alloc(default_solver); -} diff --git a/src/smt/default_solver.h b/src/smt/default_solver.h deleted file mode 100644 index 170a55e56..000000000 --- a/src/smt/default_solver.h +++ /dev/null @@ -1,26 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - default_solver.h - -Abstract: - - Wrapps smt::solver as a solver for cmd_context - -Author: - - Leonardo (leonardo) 2012-10-21 - -Notes: - ---*/ -#ifndef _DEFAULT_SOLVER_H_ -#define _DEFAULT_SOLVER_H_ - -class solver; - -solver * mk_default_solver(); - -#endif diff --git a/src/smt/expr_context_simplifier.cpp b/src/smt/expr_context_simplifier.cpp index a2a097ff5..b39e3fb9c 100644 --- a/src/smt/expr_context_simplifier.cpp +++ b/src/smt/expr_context_simplifier.cpp @@ -20,7 +20,7 @@ Revision History: #include "expr_context_simplifier.h" #include "ast_pp.h" #include "obj_hashtable.h" -#include "smt_solver.h" +#include "smt_kernel.h" #include "for_each_expr.h" // table lookup before/after simplification. diff --git a/src/smt/expr_context_simplifier.h b/src/smt/expr_context_simplifier.h index 758c3af8b..6e13dcf43 100644 --- a/src/smt/expr_context_simplifier.h +++ b/src/smt/expr_context_simplifier.h @@ -23,7 +23,7 @@ Revision History: #include "obj_hashtable.h" #include "basic_simplifier_plugin.h" #include "front_end_params.h" -#include "smt_solver.h" +#include "smt_kernel.h" #include "arith_decl_plugin.h" class expr_context_simplifier { @@ -61,7 +61,7 @@ class expr_strong_context_simplifier { arith_util m_arith; unsigned m_id; func_decl_ref m_fn; - smt::solver m_solver; + smt::kernel m_solver; void simplify(expr* e, expr_ref& result) { simplify_model_based(e, result); } void simplify_basic(expr* fml, expr_ref& result); diff --git a/src/smt/ni_solver.cpp b/src/smt/ni_solver.cpp deleted file mode 100644 index a0341cb32..000000000 --- a/src/smt/ni_solver.cpp +++ /dev/null @@ -1,236 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - ni_solver.cpp - -Abstract: - Wrappers for smt::solver that are non-incremental & (quasi-incremental). - -Author: - - Leonardo (leonardo) 2011-03-30 - -Notes: - ---*/ -#include"ni_solver.h" -#include"smt_solver.h" -#include"cmd_context.h" - -class ni_smt_solver : public solver { -protected: - cmd_context & m_cmd_ctx; - smt::solver * m_context; - progress_callback * m_callback; -public: - ni_smt_solver(cmd_context & ctx):m_cmd_ctx(ctx), m_context(0), m_callback(0) {} - - virtual ~ni_smt_solver() { - if (m_context != 0) - dealloc(m_context); - } - - virtual void init(ast_manager & m, symbol const & logic) { - // do nothing - } - - virtual void collect_statistics(statistics & st) const { - if (m_context == 0) { - return; - } - else { - m_context->collect_statistics(st); - } - } - - virtual void reset() { - if (m_context != 0) { - #pragma omp critical (ni_solver) - { - dealloc(m_context); - m_context = 0; - } - } - } - - virtual void assert_expr(expr * t) { - // do nothing - } - - virtual void push() { - // do nothing - } - - virtual void pop(unsigned n) { - // do nothing - } - - virtual unsigned get_scope_level() const { - return m_cmd_ctx.num_scopes(); - } - - void assert_exprs() { - ptr_vector::const_iterator it = m_cmd_ctx.begin_assertions(); - ptr_vector::const_iterator end = m_cmd_ctx.end_assertions(); - for (; it != end; ++it) { - m_context->assert_expr(*it); - } - } - - void init_solver() { - reset(); - #pragma omp critical (ni_solver) - { - m_context = alloc(smt::solver, m_cmd_ctx.m(), m_cmd_ctx.params()); - } - if (m_cmd_ctx.has_logic()) - m_context->set_logic(m_cmd_ctx.get_logic()); - if (m_callback) - m_context->set_progress_callback(m_callback); - assert_exprs(); - } - - virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) { - // erase current solver, and create a new one. - init_solver(); - - if (num_assumptions == 0) { - return m_context->setup_and_check(); - } - else { - return m_context->check(num_assumptions, assumptions); - } - } - - virtual void get_unsat_core(ptr_vector & r) { - SASSERT(m_context); - unsigned sz = m_context->get_unsat_core_size(); - for (unsigned i = 0; i < sz; i++) - r.push_back(m_context->get_unsat_core_expr(i)); - } - - virtual void get_model(model_ref & m) { - SASSERT(m_context); - m_context->get_model(m); - } - - virtual proof * get_proof() { - SASSERT(m_context); - return m_context->get_proof(); - } - - virtual std::string reason_unknown() const { - SASSERT(m_context); - return m_context->last_failure_as_string(); - } - - virtual void get_labels(svector & r) { - SASSERT(m_context); - buffer tmp; - m_context->get_relevant_labels(0, tmp); - r.append(tmp.size(), tmp.c_ptr()); - } - - virtual void set_cancel(bool f) { - #pragma omp critical (ni_solver) - { - if (m_context) - m_context->set_cancel(f); - } - } - - virtual void set_progress_callback(progress_callback * callback) { - m_callback = callback; - if (m_context) - m_context->set_progress_callback(callback); - } - - - virtual void collect_param_descrs(param_descrs & r) { - smt::solver::collect_param_descrs(r); - } - -}; - -solver * mk_non_incremental_smt_solver(cmd_context & ctx) { - return alloc(ni_smt_solver, ctx); -} - -class qi_smt_solver : public ni_smt_solver { - bool m_inc_mode; -public: - qi_smt_solver(cmd_context & ctx):ni_smt_solver(ctx), m_inc_mode(false) {} - - virtual ~qi_smt_solver() {} - - virtual void init(ast_manager & m, symbol const & logic) { - if (m_inc_mode) { - init_solver(); - m_inc_mode = true; - } - } - - virtual void reset() { - ni_smt_solver::reset(); - m_inc_mode = false; - } - - void switch_to_inc() { - if (!m_inc_mode) { - init_solver(); - m_inc_mode = true; - } - SASSERT(m_inc_mode); - } - - virtual void assert_expr(expr * t) { - if (m_context != 0 && !m_inc_mode) { - // solver was already created to solve a check_sat query... - switch_to_inc(); - } - if (m_inc_mode) { - SASSERT(m_context); - m_context->assert_expr(t); - } - } - - virtual void push() { - switch_to_inc(); - SASSERT(m_context); - m_context->push(); - SASSERT(m_inc_mode); - } - - virtual void pop(unsigned n) { - switch_to_inc(); - SASSERT(m_context); - m_context->pop(n); - SASSERT(m_inc_mode); - } - - virtual unsigned get_scope_level() const { - if (!m_inc_mode) - return 0; - else - return m_context->get_scope_level(); - } - - - virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) { - if (!m_inc_mode) { - lbool r = ni_smt_solver::check_sat(num_assumptions, assumptions); - SASSERT(!m_inc_mode); - return r; - } - else { - return m_context->check(num_assumptions, assumptions); - } - } -}; - - -solver * mk_quasi_incremental_smt_solver(cmd_context & ctx) { - return alloc(qi_smt_solver, ctx); -} diff --git a/src/smt/ni_solver.h b/src/smt/ni_solver.h deleted file mode 100644 index c78707319..000000000 --- a/src/smt/ni_solver.h +++ /dev/null @@ -1,30 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - ni_solver.h - -Abstract: - Wrappers for smt::context that are non-incremental & (quasi-incremental). - -Author: - - Leonardo (leonardo) 2011-03-30 - -Notes: - ---*/ -#ifndef _NI_SOLVER_H_ -#define _NI_SOLVER_H_ - -#include"solver.h" -class cmd_context; - -// Creates a solver that restarts from scratch for every call to check_sat -solver * mk_non_incremental_smt_solver(cmd_context & ctx); - -// Creates a solver that restarts from scratch for the first call to check_sat, and then moves to incremental behavior. -solver * mk_quasi_incremental_smt_solver(cmd_context & ctx); - -#endif diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 095bcff92..6137917f0 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -523,12 +523,6 @@ namespace smt { friend class set_var_theory_trail; void set_var_theory(bool_var v, theory_id tid); - /** - \brief set user-supplied rewriter. - */ - - void set_user_rewriter(void* ctx, user_rewriter::fn* rw) { m_asserted_formulas.set_user_rewriter(ctx, rw); } - // ----------------------------------- // // Backtracking support diff --git a/src/smt/smt_implied_equalities.cpp b/src/smt/smt_implied_equalities.cpp index 1dd0c412b..ef8d27e2f 100644 --- a/src/smt/smt_implied_equalities.cpp +++ b/src/smt/smt_implied_equalities.cpp @@ -36,7 +36,7 @@ namespace smt { class get_implied_equalities_impl { ast_manager& m; - smt::solver& m_solver; + smt::kernel& m_solver; union_find_default_ctx m_df; union_find m_uf; array_util m_array_util; @@ -357,7 +357,7 @@ namespace smt { public: - get_implied_equalities_impl(smt::solver& s) : m(s.m()), m_solver(s), m_uf(m_df), m_array_util(m), m_stats_calls(0) {} + get_implied_equalities_impl(smt::kernel& s) : m(s.m()), m_solver(s), m_uf(m_df), m_array_util(m), m_stats_calls(0) {} lbool operator()(unsigned num_terms, expr* const* terms, unsigned* class_ids) { params_ref p; @@ -410,7 +410,7 @@ namespace smt { stopwatch get_implied_equalities_impl::s_timer; stopwatch get_implied_equalities_impl::s_stats_val_eq_timer; - lbool implied_equalities(smt::solver& solver, unsigned num_terms, expr* const* terms, unsigned* class_ids) { + lbool implied_equalities(smt::kernel& solver, unsigned num_terms, expr* const* terms, unsigned* class_ids) { get_implied_equalities_impl gi(solver); return gi(num_terms, terms, class_ids); } diff --git a/src/smt/smt_implied_equalities.h b/src/smt/smt_implied_equalities.h index dfb9bf611..6fc002ff1 100644 --- a/src/smt/smt_implied_equalities.h +++ b/src/smt/smt_implied_equalities.h @@ -23,13 +23,13 @@ Revision History: #ifndef __SMT_IMPLIED_EQUALITIES_H__ #define __SMT_IMPLIED_EQUALITIES_H__ -#include"smt_solver.h" +#include"smt_kernel.h" namespace smt { lbool implied_equalities( - solver& solver, + kernel & solver, unsigned num_terms, expr* const* terms, unsigned* class_ids); diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp new file mode 100644 index 000000000..9d87b1363 --- /dev/null +++ b/src/smt/smt_kernel.cpp @@ -0,0 +1,353 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + smt_kernel.cpp + +Abstract: + + New frontend for smt::context. + +Author: + + Leonardo de Moura (leonardo) 2012-02-09. + +Revision History: + +--*/ +#include"smt_kernel.h" +#include"smt_context.h" +#include"ast_smt2_pp.h" +#include"params2front_end_params.h" + +namespace smt { + + struct kernel::imp { + smt::context m_kernel; + params_ref m_params; + + imp(ast_manager & m, front_end_params & fp, params_ref const & p): + m_kernel(m, fp, p), + m_params(p) { + } + + front_end_params & fparams() { + return m_kernel.get_fparams(); + } + + params_ref const & params() { + return m_params; + } + + ast_manager & m() const { + return m_kernel.get_manager(); + } + + bool set_logic(symbol logic) { + return m_kernel.set_logic(logic); + } + + void set_progress_callback(progress_callback * callback) { + return m_kernel.set_progress_callback(callback); + } + + void assert_expr(expr * e) { + TRACE("smt_kernel", tout << "assert:\n" << mk_ismt2_pp(e, m()) << "\n";); + m_kernel.assert_expr(e); + } + + void assert_expr(expr * e, proof * pr) { + m_kernel.assert_expr(e, pr); + } + + unsigned size() const { + return m_kernel.get_num_asserted_formulas(); + } + + expr * const * get_formulas() const { + return m_kernel.get_asserted_formulas(); + } + + bool reduce() { + return m_kernel.reduce_assertions(); + } + + void push() { + TRACE("smt_kernel", tout << "push()\n";); + m_kernel.push(); + } + + void pop(unsigned num_scopes) { + TRACE("smt_kernel", tout << "pop()\n";); + m_kernel.pop(num_scopes); + } + + unsigned get_scope_level() const { + return m_kernel.get_scope_level(); + } + + lbool setup_and_check() { + return m_kernel.setup_and_check(); + } + + bool inconsistent() { + return m_kernel.inconsistent(); + } + + lbool check(unsigned num_assumptions, expr * const * assumptions) { + return m_kernel.check(num_assumptions, assumptions); + } + + void get_model(model_ref & m) const { + m_kernel.get_model(m); + } + + proof * get_proof() { + return m_kernel.get_proof(); + } + + unsigned get_unsat_core_size() const { + return m_kernel.get_unsat_core_size(); + } + + expr * get_unsat_core_expr(unsigned idx) const { + return m_kernel.get_unsat_core_expr(idx); + } + + failure last_failure() const { + return m_kernel.get_last_search_failure(); + } + + std::string last_failure_as_string() const { + return m_kernel.last_failure_as_string(); + } + + void get_assignments(expr_ref_vector & result) { + m_kernel.get_assignments(result); + } + + void get_relevant_labels(expr * cnstr, buffer & result) { + m_kernel.get_relevant_labels(cnstr, result); + } + + void get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) { + m_kernel.get_relevant_labeled_literals(at_lbls, result); + } + + void get_relevant_literals(expr_ref_vector & result) { + m_kernel.get_relevant_literals(result); + } + + void get_guessed_literals(expr_ref_vector & result) { + m_kernel.get_guessed_literals(result); + } + + void display(std::ostream & out) const { + // m_kernel.display(out); <<< for external users it is just junk + // TODO: it will be replaced with assertion_stack.display + unsigned num = m_kernel.get_num_asserted_formulas(); + expr * const * fms = m_kernel.get_asserted_formulas(); + out << "(kernel"; + for (unsigned i = 0; i < num; i++) { + out << "\n " << mk_ismt2_pp(fms[i], m(), 2); + } + out << ")"; + } + + void collect_statistics(::statistics & st) const { + m_kernel.collect_statistics(st); + } + + void reset_statistics() { + } + + void display_statistics(std::ostream & out) const { + m_kernel.display_statistics(out); + } + + void display_istatistics(std::ostream & out) const { + m_kernel.display_istatistics(out); + } + + void set_cancel(bool f) { + m_kernel.set_cancel_flag(f); + } + + bool canceled() { + return m_kernel.get_cancel_flag(); + } + + void updt_params(params_ref const & p) { + params2front_end_params(p, fparams()); + } + }; + + kernel::kernel(ast_manager & m, front_end_params & fp, params_ref const & p) { + m_imp = alloc(imp, m, fp, p); + } + + kernel::~kernel() { + dealloc(m_imp); + } + + ast_manager & kernel::m() const { + return m_imp->m(); + } + + bool kernel::set_logic(symbol logic) { + return m_imp->set_logic(logic); + } + + void kernel::set_progress_callback(progress_callback * callback) { + m_imp->set_progress_callback(callback); + } + + void kernel::assert_expr(expr * e) { + m_imp->assert_expr(e); + } + + void kernel::assert_expr(expr * e, proof * pr) { + m_imp->assert_expr(e, pr); + } + + unsigned kernel::size() const { + return m_imp->size(); + } + + expr * const * kernel::get_formulas() const { + return m_imp->get_formulas(); + } + + bool kernel::reduce() { + return m_imp->reduce(); + } + + void kernel::push() { + m_imp->push(); + } + + void kernel::pop(unsigned num_scopes) { + m_imp->pop(num_scopes); + } + + unsigned kernel::get_scope_level() const { + return m_imp->get_scope_level(); + } + + void kernel::reset() { + ast_manager & _m = m(); + front_end_params & fps = m_imp->fparams(); + params_ref ps = m_imp->params(); + #pragma omp critical (smt_kernel) + { + dealloc(m_imp); + m_imp = alloc(imp, _m, fps, ps); + } + } + + bool kernel::inconsistent() { + return m_imp->inconsistent(); + } + + lbool kernel::setup_and_check() { + set_cancel(false); + return m_imp->setup_and_check(); + } + + lbool kernel::check(unsigned num_assumptions, expr * const * assumptions) { + set_cancel(false); + lbool r = m_imp->check(num_assumptions, assumptions); + TRACE("smt_kernel", tout << "check result: " << r << "\n";); + return r; + } + + void kernel::get_model(model_ref & m) const { + m_imp->get_model(m); + } + + proof * kernel::get_proof() { + return m_imp->get_proof(); + } + + unsigned kernel::get_unsat_core_size() const { + return m_imp->get_unsat_core_size(); + } + + expr * kernel::get_unsat_core_expr(unsigned idx) const { + return m_imp->get_unsat_core_expr(idx); + } + + failure kernel::last_failure() const { + return m_imp->last_failure(); + } + + std::string kernel::last_failure_as_string() const { + return m_imp->last_failure_as_string(); + } + + void kernel::get_assignments(expr_ref_vector & result) { + m_imp->get_assignments(result); + } + + void kernel::get_relevant_labels(expr * cnstr, buffer & result) { + m_imp->get_relevant_labels(cnstr, result); + } + + void kernel::get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) { + m_imp->get_relevant_labeled_literals(at_lbls, result); + } + + void kernel::get_relevant_literals(expr_ref_vector & result) { + m_imp->get_relevant_literals(result); + } + + void kernel::get_guessed_literals(expr_ref_vector & result) { + m_imp->get_guessed_literals(result); + } + + void kernel::display(std::ostream & out) const { + m_imp->display(out); + } + + void kernel::collect_statistics(::statistics & st) const { + m_imp->collect_statistics(st); + } + + void kernel::reset_statistics() { + m_imp->reset_statistics(); + } + + void kernel::display_statistics(std::ostream & out) const { + m_imp->display_statistics(out); + } + + void kernel::display_istatistics(std::ostream & out) const { + m_imp->display_istatistics(out); + } + + void kernel::set_cancel(bool f) { + #pragma omp critical (smt_kernel) + { + if (m_imp) + m_imp->set_cancel(f); + } + } + + bool kernel::canceled() const { + return m_imp->canceled(); + } + + void kernel::updt_params(params_ref const & p) { + return m_imp->updt_params(p); + } + + void kernel::collect_param_descrs(param_descrs & d) { + solver_front_end_params_descrs(d); + } + + context & kernel::get_context() { + return m_imp->m_kernel; + } + +}; diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h new file mode 100644 index 000000000..4c381e113 --- /dev/null +++ b/src/smt/smt_kernel.h @@ -0,0 +1,255 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + smt_kernel.h + +Abstract: + + New frontend for smt::context. + The "kernel" tries to hide details of the smt::context object. + From now on, clients (code outside of the smt module) should be use smt::kernel instead of smt::context. + +Author: + + Leonardo de Moura (leonardo) 2012-02-09. + +Revision History: + + I initially called it smt::solver. This was confusing to others since we have the abstract solver API, + and smt::kernel is not a subclass of ::solver. + To increase the confusion I had a class default_solver that implemented the solver API on top of smt::context. + To avoid this problem I renamed them in the following way: + smt::solver ---> smt::kernel + default_solver ---> smt::solver +--*/ +#ifndef _SMT_KERNEL_H_ +#define _SMT_KERNEL_H_ + +#include"ast.h" +#include"params.h" +#include"model.h" +#include"lbool.h" +#include"statistics.h" +#include"smt_failure.h" + +struct front_end_params; +class progress_callback; + +namespace smt { + + class enode; + class context; + + class kernel { + struct imp; + imp * m_imp; + public: + kernel(ast_manager & m, front_end_params & fp, params_ref const & p = params_ref()); + + ~kernel(); + + ast_manager & m() const; + + /** + \brief Set logic. It must be invoked before any assertions. + Return true if succeeded. + */ + bool set_logic(symbol logic); + + /** + brief Set progress meter. Kernel will invoke the callback from time to time. + */ + void set_progress_callback(progress_callback * callback); + + /** + \brief Assert the given assetion into the logical context. + This method uses the "asserted" proof as a justification for e. + */ + void assert_expr(expr * e); + + /** + \brief Assert the given assertion with the given proof as a justification. + */ + void assert_expr(expr * e, proof * pr); + + /** + \brief Return the number of asserted formulas in the kernel. + */ + unsigned size() const; + + /** + \brief Return the array of asserted formulas. + */ + expr * const * get_formulas() const; + + /** + \brief Reduce the set of asserted formulas using preprocessors. + Return true if an inconsistency is detected. + + \remark This is mainly used by dl_smt_relation. This method + seens to be misplaced. This is not the right place. + */ + bool reduce(); + + /** + \brief Create a backtracking point (aka scope level). + */ + void push(); + + /** + \brief Backtrack the given number of scope levels. + */ + void pop(unsigned num_scopes); + + /** + \brief Return the number of backtracking points. + */ + unsigned get_scope_level() const; + + /** + \brief Reset the kernel. + All assertions are erased. + */ + void reset(); + + /** + \brief Return true if the set of asserted formulas is known to be inconsistent. + */ + bool inconsistent(); + + /** + \brief Setup the logical context and invoke check. + */ + lbool setup_and_check(); + + /** + \brief Satisfiability check. + */ + lbool check(unsigned num_assumptions = 0, expr * const * assumptions = 0); + + /** + \brief Return the model associated with the last check command. + */ + void get_model(model_ref & m) const; + + /** + \brief Return the proof of unsatisfiability associated with the last check command. + */ + proof * get_proof(); + + /** + \brief Return the size of the unsat core associated with the last check command. + */ + unsigned get_unsat_core_size() const; + + /** + \brief Return the i-th expression in the unsat core associated with the last check command. + + \pre i < get_unsat_core_size() + */ + expr * get_unsat_core_expr(unsigned i) const; + + /** + \brief Return the reason for failure for the last check command. + Failure means, it returned l_undef + */ + failure last_failure() const; + + /** + \brief Return a string describing the failure. + */ + std::string last_failure_as_string() const; + + /** + \brief Return the set of formulas assigned by the kernel. + */ + void get_assignments(expr_ref_vector & result); + + /** + \brief Return the set of relevant labels in the last check command. + */ + void get_relevant_labels(expr * cnstr, buffer & result); + + /** + \brief Return the relevant labeled_literals in the last check command. + */ + void get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result); + + /** + \brief Return the relevant literals in the last check command. + */ + void get_relevant_literals(expr_ref_vector & result); + + /** + \brief Return the set of guessed literals (decisions) performed in the last check command. + */ + void get_guessed_literals(expr_ref_vector & result); + + /** + \brief (For debubbing purposes) Prints the state of the kernel + */ + void display(std::ostream & out) const; + + /** + \brief Collect runtime statistics. + */ + void collect_statistics(::statistics & st) const; + + /** + \brief Reset kernel statistics. + */ + void reset_statistics(); + + /** + \brief Display statistics. + */ + void display_statistics(std::ostream & out) const; + + /** + \brief Display statistics in low level format. + */ + void display_istatistics(std::ostream & out) const; + + /** + \brief Interrupt the kernel. + */ + void set_cancel(bool f = true); + void cancel() { set_cancel(true); } + + /** + \brief Reset interruption. + */ + void reset_cancel() { set_cancel(false); } + + /** + \brief Return true if the kernel was interrupted. + */ + bool canceled() const; + + /** + \brief Update configuration parameters. + */ + void updt_params(params_ref const & p); + + /** + \brief Collect a description of the configuration parameters. + */ + static void collect_param_descrs(param_descrs & d); + + /** + \brief Return a reference to smt::context. + This is a temporary hack to support user theories. + TODO: remove this hack. + We need to revamp user theories too. + + This method breaks the abstraction barrier. + + \warning We should not use this method + */ + context & get_context(); + }; +}; + +#endif diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 6e9cd01fc..58921bb35 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -56,7 +56,7 @@ namespace smt { SASSERT(m_qm == 0); SASSERT(m_context == 0); m_qm = &qm; - m_context = &(m_qm->kernel()); + m_context = &(m_qm->get_context()); } /** diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index b6ed70180..c11f226ed 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -248,7 +248,7 @@ namespace smt { dealloc(m_imp); } - context & quantifier_manager::kernel() const { + context & quantifier_manager::get_context() const { return m_imp->m_context; } @@ -414,7 +414,7 @@ namespace smt { virtual void set_manager(quantifier_manager & qm) { SASSERT(m_qm == 0); m_qm = &qm; - m_context = &(qm.kernel()); + m_context = &(qm.get_context()); m_fparams = &(m_context->get_fparams()); ast_manager & m = m_context->get_manager(); diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index 9c4129c0d..3873c9737 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -38,7 +38,7 @@ namespace smt { quantifier_manager(context & ctx, front_end_params & fp, params_ref const & p); ~quantifier_manager(); - context & kernel() const; + context & get_context() const; void set_plugin(quantifier_manager_plugin * plugin); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 6bdfd0524..888e1b34c 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -3,351 +3,181 @@ Copyright (c) 2012 Microsoft Corporation Module Name: - smt_solver.h + smt_solver.cpp Abstract: - New frontend for the incremental solver. - + Wraps smt::kernel as a solver for the external API and cmd_context. + Author: - Leonardo de Moura (leonardo) 2012-02-09. + Leonardo (leonardo) 2012-10-21 -Revision History: +Notes: --*/ -#include"smt_solver.h" -#include"smt_context.h" -#include"ast_smt2_pp.h" -#include"params2front_end_params.h" +#include"solver_na2as.h" +#include"smt_kernel.h" +#include"reg_decl_plugins.h" +#include"front_end_params.h" namespace smt { - struct solver::imp { - smt::context m_kernel; - params_ref m_params; - - imp(ast_manager & m, front_end_params & fp, params_ref const & p): - m_kernel(m, fp, p), - m_params(p) { + class solver : public solver_na2as { + front_end_params * m_params; + smt::kernel * m_context; + progress_callback * m_callback; + public: + solver():m_params(0), m_context(0), m_callback(0) {} + + virtual ~solver() { + if (m_context != 0) + dealloc(m_context); } - front_end_params & fparams() { - return m_kernel.get_fparams(); + virtual void set_front_end_params(front_end_params & p) { + m_params = &p; } - params_ref const & params() { - return m_params; - } - - ast_manager & m() const { - return m_kernel.get_manager(); + virtual void updt_params(params_ref const & p) { + if (m_context == 0) + return; + m_context->updt_params(p); } - bool set_logic(symbol logic) { - return m_kernel.set_logic(logic); - } - - void set_progress_callback(progress_callback * callback) { - return m_kernel.set_progress_callback(callback); - } - - void assert_expr(expr * e) { - TRACE("smt_solver", tout << "assert:\n" << mk_ismt2_pp(e, m()) << "\n";); - m_kernel.assert_expr(e); - } - - void assert_expr(expr * e, proof * pr) { - m_kernel.assert_expr(e, pr); - } - - unsigned size() const { - return m_kernel.get_num_asserted_formulas(); - } - - expr * const * get_formulas() const { - return m_kernel.get_asserted_formulas(); - } - - bool reduce() { - return m_kernel.reduce_assertions(); - } - - void push() { - TRACE("smt_solver", tout << "push()\n";); - m_kernel.push(); - } - - void pop(unsigned num_scopes) { - TRACE("smt_solver", tout << "pop()\n";); - m_kernel.pop(num_scopes); - } - - unsigned get_scope_level() const { - return m_kernel.get_scope_level(); - } - - lbool setup_and_check() { - return m_kernel.setup_and_check(); - } - - bool inconsistent() { - return m_kernel.inconsistent(); - } - - lbool check(unsigned num_assumptions, expr * const * assumptions) { - return m_kernel.check(num_assumptions, assumptions); - } - - void get_model(model_ref & m) const { - m_kernel.get_model(m); - } - - proof * get_proof() { - return m_kernel.get_proof(); - } - - unsigned get_unsat_core_size() const { - return m_kernel.get_unsat_core_size(); - } - - expr * get_unsat_core_expr(unsigned idx) const { - return m_kernel.get_unsat_core_expr(idx); - } - - failure last_failure() const { - return m_kernel.get_last_search_failure(); - } - - std::string last_failure_as_string() const { - return m_kernel.last_failure_as_string(); - } - - void get_assignments(expr_ref_vector & result) { - m_kernel.get_assignments(result); - } - - void get_relevant_labels(expr * cnstr, buffer & result) { - m_kernel.get_relevant_labels(cnstr, result); - } - - void get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) { - m_kernel.get_relevant_labeled_literals(at_lbls, result); - } - - void get_relevant_literals(expr_ref_vector & result) { - m_kernel.get_relevant_literals(result); - } - - void get_guessed_literals(expr_ref_vector & result) { - m_kernel.get_guessed_literals(result); - } - - void display(std::ostream & out) const { - // m_kernel.display(out); <<< for external users it is just junk - // TODO: it will be replaced with assertion_stack.display - unsigned num = m_kernel.get_num_asserted_formulas(); - expr * const * fms = m_kernel.get_asserted_formulas(); - out << "(solver"; - for (unsigned i = 0; i < num; i++) { - out << "\n " << mk_ismt2_pp(fms[i], m(), 2); + virtual void collect_param_descrs(param_descrs & r) { + if (m_context == 0) { + ast_manager m; + reg_decl_plugins(m); + front_end_params p; + smt::kernel s(m, p); + s.collect_param_descrs(r); + } + else { + m_context->collect_param_descrs(r); } - out << ")"; - } - - void collect_statistics(::statistics & st) const { - m_kernel.collect_statistics(st); - } - - void reset_statistics() { } - void display_statistics(std::ostream & out) const { - m_kernel.display_statistics(out); - } - - void display_istatistics(std::ostream & out) const { - m_kernel.display_istatistics(out); + virtual void init_core(ast_manager & m, symbol const & logic) { + SASSERT(m_params); + reset(); +#pragma omp critical (solver) + { + m_context = alloc(smt::kernel, m, *m_params); + if (m_callback) + m_context->set_progress_callback(m_callback); + } + if (logic != symbol::null) + m_context->set_logic(logic); } - void set_cancel(bool f) { - m_kernel.set_cancel_flag(f); - } - - bool canceled() { - return m_kernel.get_cancel_flag(); + virtual void collect_statistics(statistics & st) const { + if (m_context == 0) { + return; + } + else { + m_context->collect_statistics(st); + } } - void updt_params(params_ref const & p) { - params2front_end_params(p, fparams()); + virtual void reset_core() { + if (m_context != 0) { +#pragma omp critical (solver) + { + dealloc(m_context); + m_context = 0; + } + } } + + virtual void assert_expr(expr * t) { + SASSERT(m_context); + m_context->assert_expr(t); + } + + virtual void push_core() { + SASSERT(m_context); + m_context->push(); + } + + virtual void pop_core(unsigned n) { + SASSERT(m_context); + m_context->pop(n); + } + + virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) { + SASSERT(m_context); + TRACE("solver_na2as", tout << "smt_solver::check_sat_core: " << num_assumptions << "\n";); + return m_context->check(num_assumptions, assumptions); + } + + virtual void get_unsat_core(ptr_vector & r) { + SASSERT(m_context); + unsigned sz = m_context->get_unsat_core_size(); + for (unsigned i = 0; i < sz; i++) + r.push_back(m_context->get_unsat_core_expr(i)); + } + + virtual void get_model(model_ref & m) { + SASSERT(m_context); + m_context->get_model(m); + } + + virtual proof * get_proof() { + SASSERT(m_context); + return m_context->get_proof(); + } + + virtual std::string reason_unknown() const { + SASSERT(m_context); + return m_context->last_failure_as_string(); + } + + virtual void get_labels(svector & r) { + SASSERT(m_context); + buffer tmp; + m_context->get_relevant_labels(0, tmp); + r.append(tmp.size(), tmp.c_ptr()); + } + + virtual void set_cancel(bool f) { +#pragma omp critical (solver) + { + if (m_context) + m_context->set_cancel(f); + } + } + + virtual void set_progress_callback(progress_callback * callback) { + m_callback = callback; + if (m_context) + m_context->set_progress_callback(callback); + } + + virtual unsigned get_num_assertions() const { + if (m_context) + return m_context->size(); + else + return 0; + } + + virtual expr * get_assertion(unsigned idx) const { + SASSERT(m_context); + SASSERT(idx < get_num_assertions()); + return m_context->get_formulas()[idx]; + } + + virtual void display(std::ostream & out) const { + if (m_context) + m_context->display(out); + else + out << "(solver)"; + } + }; - solver::solver(ast_manager & m, front_end_params & fp, params_ref const & p) { - m_imp = alloc(imp, m, fp, p); - } - - solver::~solver() { - dealloc(m_imp); - } - - ast_manager & solver::m() const { - return m_imp->m(); - } - - bool solver::set_logic(symbol logic) { - return m_imp->set_logic(logic); - } - - void solver::set_progress_callback(progress_callback * callback) { - m_imp->set_progress_callback(callback); - } - - void solver::assert_expr(expr * e) { - m_imp->assert_expr(e); - } - - void solver::assert_expr(expr * e, proof * pr) { - m_imp->assert_expr(e, pr); - } - - unsigned solver::size() const { - return m_imp->size(); - } - - expr * const * solver::get_formulas() const { - return m_imp->get_formulas(); - } - - bool solver::reduce() { - return m_imp->reduce(); - } - - void solver::push() { - m_imp->push(); - } - - void solver::pop(unsigned num_scopes) { - m_imp->pop(num_scopes); - } - - unsigned solver::get_scope_level() const { - return m_imp->get_scope_level(); - } - - void solver::reset() { - ast_manager & _m = m(); - front_end_params & fps = m_imp->fparams(); - params_ref ps = m_imp->params(); - #pragma omp critical (smt_solver) - { - dealloc(m_imp); - m_imp = alloc(imp, _m, fps, ps); - } - } - - bool solver::inconsistent() { - return m_imp->inconsistent(); - } - - lbool solver::setup_and_check() { - set_cancel(false); - return m_imp->setup_and_check(); - } - - lbool solver::check(unsigned num_assumptions, expr * const * assumptions) { - set_cancel(false); - lbool r = m_imp->check(num_assumptions, assumptions); - TRACE("smt_solver", tout << "check result: " << r << "\n";); - return r; - } - - void solver::get_model(model_ref & m) const { - m_imp->get_model(m); - } - - proof * solver::get_proof() { - return m_imp->get_proof(); - } - - unsigned solver::get_unsat_core_size() const { - return m_imp->get_unsat_core_size(); - } - - expr * solver::get_unsat_core_expr(unsigned idx) const { - return m_imp->get_unsat_core_expr(idx); - } - - failure solver::last_failure() const { - return m_imp->last_failure(); - } - - std::string solver::last_failure_as_string() const { - return m_imp->last_failure_as_string(); - } - - void solver::get_assignments(expr_ref_vector & result) { - m_imp->get_assignments(result); - } - - void solver::get_relevant_labels(expr * cnstr, buffer & result) { - m_imp->get_relevant_labels(cnstr, result); - } - - void solver::get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) { - m_imp->get_relevant_labeled_literals(at_lbls, result); - } - - void solver::get_relevant_literals(expr_ref_vector & result) { - m_imp->get_relevant_literals(result); - } - - void solver::get_guessed_literals(expr_ref_vector & result) { - m_imp->get_guessed_literals(result); - } - - void solver::display(std::ostream & out) const { - m_imp->display(out); - } - - void solver::collect_statistics(::statistics & st) const { - m_imp->collect_statistics(st); - } - - void solver::reset_statistics() { - m_imp->reset_statistics(); - } - - void solver::display_statistics(std::ostream & out) const { - m_imp->display_statistics(out); - } - - void solver::display_istatistics(std::ostream & out) const { - m_imp->display_istatistics(out); - } - - void solver::set_cancel(bool f) { - #pragma omp critical (smt_solver) - { - if (m_imp) - m_imp->set_cancel(f); - } - } - - bool solver::canceled() const { - return m_imp->canceled(); - } - - void solver::updt_params(params_ref const & p) { - return m_imp->updt_params(p); - } - - void solver::collect_param_descrs(param_descrs & d) { - solver_front_end_params_descrs(d); - } - - context & solver::kernel() { - return m_imp->m_kernel; - } - }; + +solver * mk_smt_solver() { + return alloc(smt::solver); +} diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index 1d04df9ed..e9af9aafa 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -7,241 +7,22 @@ Module Name: Abstract: - New frontend for the incremental solver. - + Wraps smt::kernel as a solver for the external API and cmd_context. + Author: - Leonardo de Moura (leonardo) 2012-02-09. + Leonardo (leonardo) 2012-10-21 -Revision History: +Notes: + + This file was called default_solver.h. It was a bad name. --*/ #ifndef _SMT_SOLVER_H_ #define _SMT_SOLVER_H_ -#include"ast.h" -#include"params.h" -#include"model.h" -#include"lbool.h" -#include"statistics.h" -#include"smt_failure.h" +class solver; -struct front_end_params; -class progress_callback; - -namespace smt { - - class enode; - class context; - - class solver { - struct imp; - imp * m_imp; - public: - solver(ast_manager & m, front_end_params & fp, params_ref const & p = params_ref()); - - ~solver(); - - ast_manager & m() const; - - /** - \brief Set logic. It must be invoked before any assertions. - Return true if succeeded. - */ - bool set_logic(symbol logic); - - /** - brief Set progress meter. Solver will invoke the callback from time to time. - */ - void set_progress_callback(progress_callback * callback); - - /** - \brief Assert the given assetion into the logical context. - This method uses the "asserted" proof as a justification for e. - */ - void assert_expr(expr * e); - - /** - \brief Assert the given assertion with the given proof as a justification. - */ - void assert_expr(expr * e, proof * pr); - - /** - \brief Return the number of asserted formulas in the solver. - */ - unsigned size() const; - - /** - \brief Return the array of asserted formulas. - */ - expr * const * get_formulas() const; - - /** - \brief Reduce the set of asserted formulas using preprocessors. - Return true if an inconsistency is detected. - - \remark This is mainly used by dl_smt_relation. This method - seens to be misplaced. This is not the right place. - */ - bool reduce(); - - /** - \brief Create a backtracking point (aka scope level). - */ - void push(); - - /** - \brief Backtrack the given number of scope levels. - */ - void pop(unsigned num_scopes); - - /** - \brief Return the number of backtracking points. - */ - unsigned get_scope_level() const; - - /** - \brief Reset the solver. - All assertions are erased. - */ - void reset(); - - /** - \brief Return true if the set of asserted formulas is known to be inconsistent. - */ - bool inconsistent(); - - /** - \brief Setup the logical context and invoke check. - */ - lbool setup_and_check(); - - /** - \brief Satisfiability check. - */ - lbool check(unsigned num_assumptions = 0, expr * const * assumptions = 0); - - /** - \brief Return the model associated with the last check command. - */ - void get_model(model_ref & m) const; - - /** - \brief Return the proof of unsatisfiability associated with the last check command. - */ - proof * get_proof(); - - /** - \brief Return the size of the unsat core associated with the last check command. - */ - unsigned get_unsat_core_size() const; - - /** - \brief Return the i-th expression in the unsat core associated with the last check command. - - \pre i < get_unsat_core_size() - */ - expr * get_unsat_core_expr(unsigned i) const; - - /** - \brief Return the reason for failure for the last check command. - Failure means, it returned l_undef - */ - failure last_failure() const; - - /** - \brief Return a string describing the failure. - */ - std::string last_failure_as_string() const; - - /** - \brief Return the set of formulas assigned by the solver. - */ - void get_assignments(expr_ref_vector & result); - - /** - \brief Return the set of relevant labels in the last check command. - */ - void get_relevant_labels(expr * cnstr, buffer & result); - - /** - \brief Return the relevant labeled_literals in the last check command. - */ - void get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result); - - /** - \brief Return the relevant literals in the last check command. - */ - void get_relevant_literals(expr_ref_vector & result); - - /** - \brief Return the set of guessed literals (decisions) performed in the last check command. - */ - void get_guessed_literals(expr_ref_vector & result); - - /** - \brief (For debubbing purposes) Prints the state of the solver - */ - void display(std::ostream & out) const; - - /** - \brief Collect runtime statistics. - */ - void collect_statistics(::statistics & st) const; - - /** - \brief Reset solver statistics. - */ - void reset_statistics(); - - /** - \brief Display statistics. - */ - void display_statistics(std::ostream & out) const; - - /** - \brief Display statistics in low level format. - */ - void display_istatistics(std::ostream & out) const; - - /** - \brief Interrupt the solver. - */ - void set_cancel(bool f = true); - void cancel() { set_cancel(true); } - - /** - \brief Reset interruption. - */ - void reset_cancel() { set_cancel(false); } - - /** - \brief Return true if the solver was interrupted. - */ - bool canceled() const; - - /** - \brief Update configuration parameters. - */ - void updt_params(params_ref const & p); - - /** - \brief Collect a description of the configuration parameters. - */ - static void collect_param_descrs(param_descrs & d); - - /** - \brief Return a reference to the kernel. - This is a temporary hack to support user theories. - TODO: remove this hack. - We need to revamp user theories too. - - This method breaks the abstraction barrier. - - \warning We should not use this method - */ - context & kernel(); - }; -}; +solver * mk_smt_solver(); #endif diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index 76379e595..e5b625661 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -20,7 +20,7 @@ Notes: #include"ctx_solver_simplify_tactic.h" #include"arith_decl_plugin.h" #include"front_end_params.h" -#include"smt_solver.h" +#include"smt_kernel.h" #include"ast_pp.h" #include"mk_simplified_app.h" @@ -29,7 +29,7 @@ class ctx_solver_simplify_tactic : public tactic { ast_manager& m; params_ref m_params; front_end_params m_front_p; - smt::solver m_solver; + smt::kernel m_solver; arith_util m_arith; mk_simplified_app m_mk_app; func_decl_ref m_fn; diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 7afce667a..fd942d05c 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -18,7 +18,7 @@ Notes: --*/ #include"tactic.h" #include"tactical.h" -#include"smt_solver.h" +#include"smt_kernel.h" #include"front_end_params.h" #include"params2front_end_params.h" #include"rewriter_types.h" @@ -28,7 +28,7 @@ class smt_tactic : public tactic { params_ref m_params_ref; statistics m_stats; std::string m_failure; - smt::solver * m_ctx; + smt::kernel * m_ctx; symbol m_logic; progress_callback * m_callback; bool m_candidate_models; @@ -117,7 +117,7 @@ public: smt_tactic & m_owner; scoped_init_ctx(smt_tactic & o, ast_manager & m):m_owner(o) { - smt::solver * new_ctx = alloc(smt::solver, m, o.fparams()); + smt::kernel * new_ctx = alloc(smt::kernel, m, o.fparams()); TRACE("smt_tactic", tout << "logic: " << o.m_logic << "\n";); new_ctx->set_logic(o.m_logic); if (o.m_callback) { @@ -130,7 +130,7 @@ public: } ~scoped_init_ctx() { - smt::solver * d = m_owner.m_ctx; + smt::kernel * d = m_owner.m_ctx; #pragma omp critical (as_st_cancel) { m_owner.m_ctx = 0; diff --git a/src/smt/theory_diff_logic.cpp b/src/smt/theory_diff_logic.cpp index 86351e36f..a68b7782b 100644 --- a/src/smt/theory_diff_logic.cpp +++ b/src/smt/theory_diff_logic.cpp @@ -22,9 +22,11 @@ Revision History: #include"rational.h" #include"theory_diff_logic_def.h" +namespace smt { template class theory_diff_logic; template class theory_diff_logic; template class theory_diff_logic; template class theory_diff_logic; +}; diff --git a/src/smt/user_plugin/user_smt_theory.cpp b/src/smt/user_plugin/user_smt_theory.cpp index 19b25dcfa..d95346469 100644 --- a/src/smt/user_plugin/user_smt_theory.cpp +++ b/src/smt/user_plugin/user_smt_theory.cpp @@ -642,8 +642,8 @@ namespace smt { out << "Theory " << get_name() << ":\n"; } - user_theory * mk_user_theory(solver & _s, void * ext_context, void * ext_data, char const * name) { - context & ctx = _s.kernel(); // HACK + user_theory * mk_user_theory(kernel & _s, void * ext_context, void * ext_data, char const * name) { + context & ctx = _s.get_context(); // HACK symbol _name(name); ast_manager & m = ctx.get_manager(); family_id fid = m.get_family_id(_name); diff --git a/src/smt/user_plugin/user_smt_theory.h b/src/smt/user_plugin/user_smt_theory.h index a27b3af32..3dd664738 100644 --- a/src/smt/user_plugin/user_smt_theory.h +++ b/src/smt/user_plugin/user_smt_theory.h @@ -23,7 +23,7 @@ Revision History: #include"user_simplifier_plugin.h" #include"smt_theory.h" #include"union_find.h" -#include"smt_solver.h" +#include"smt_kernel.h" namespace smt { @@ -316,7 +316,7 @@ namespace smt { virtual void display(std::ostream & out) const; }; - user_theory * mk_user_theory(solver & s, void * ext_context, void * ext_data, char const * name); + user_theory * mk_user_theory(kernel & s, void * ext_context, void * ext_data, char const * name); }; diff --git a/src/smt/user_rewriter.cpp b/src/smt/user_rewriter.cpp deleted file mode 100644 index 94c6c3858..000000000 --- a/src/smt/user_rewriter.cpp +++ /dev/null @@ -1,24 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - user_rewriter.cpp - -Abstract: - - Rewriter for applying user-defined rewrite routine. - -Author: - - Nikolaj (nbjorner) 2012-01-08 - -Notes: - ---*/ - -#include "rewriter_def.h" -#include "user_rewriter.h" - - -template class rewriter_tpl; diff --git a/src/smt/user_rewriter.h b/src/smt/user_rewriter.h deleted file mode 100644 index 870425f89..000000000 --- a/src/smt/user_rewriter.h +++ /dev/null @@ -1,58 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - user_rewriter.h - -Abstract: - - Rewriter for applying user-defined rewrite routine. - -Author: - - Nikolaj (nbjorner) 2012-01-08 - -Notes: - ---*/ -#ifndef _USER_REWRITER_H_ -#define _USER_REWRITER_H_ - -#include "ast.h" -#include "rewriter.h" - - -class user_rewriter : public default_rewriter_cfg { -public: - typedef bool fn(void* context, expr* expr_in, expr** expr_out, proof** proof_out); -private: - ast_manager& m; - rewriter_tpl m_rw; - void* m_ctx; - fn* m_rewriter; - bool m_rec; - -public: - user_rewriter(ast_manager & m): m(m), m_rw(m, m.proofs_enabled(), *this), m_rewriter(0), m_rec(false) {} - ~user_rewriter() {} - - void set_rewriter(void * ctx, fn* rw) { m_ctx = ctx; m_rewriter = rw; } - bool enabled() { return m_rewriter != 0; } - - void operator()(expr_ref& term) { expr_ref tmp(m); (*this)(tmp, term); } - void operator()(expr * t, expr_ref & result) { proof_ref pr(m); (*this)(t, result, pr); } - void operator()(expr * t, expr_ref & result, proof_ref & result_pr) { m_rw(t, result, result_pr); } - - void cancel() { set_cancel(true); } - void reset_cancel() { set_cancel(false); } - void set_cancel(bool f) { m_rw.set_cancel(f); } - void cleanup() { if (!m_rec) { m_rec = true; m_rw.cleanup(); m_rec = false; } } - void reset() { if (!m_rec) { m_rec = true; m_rw.reset(); m_rec = false; } } - - bool get_subst(expr* s, expr*& t, proof*& t_pr) { - return enabled() && m_rewriter(m_ctx, s, &t, &t_pr); - } -}; - -#endif diff --git a/src/solver/solver.h b/src/solver/solver.h index e8823df4f..6f9887c1a 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -70,7 +70,8 @@ public: /** \brief Enable/Disable model generation for this solver object. - It is invoked before init(m, logic). + It is invoked before init(m, logic). + The user may optionally invoke it after init(m, logic). */ virtual void set_produce_models(bool f) {} /** @@ -95,6 +96,13 @@ public: */ virtual void assert_expr(expr * t) = 0; + /** + \brief Add a new formula \c t to the assertion stack, and "tag" it with \c a. + The propositional varialbe \c a is used to track the use of \c t in a proof + of unsatisfiability. + */ + virtual void assert_expr(expr * t, expr * a) = 0; + /** \brief Create a backtracking point. */ diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp new file mode 100644 index 000000000..f6d7414a5 --- /dev/null +++ b/src/solver/solver_na2as.cpp @@ -0,0 +1,101 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + solver_na2as.cpp + +Abstract: + + Solver that implements "named" assertions using assumptions (aka answer literals). + That is, a named assertion assert_expr(t, a) is mapped into + a implies t + and 'a' is used as an extra assumption for check_sat. + +Author: + + Leonardo (leonardo) 2012-11-02 + +Notes: + +--*/ +#include"solver_na2as.h" +#include"ast_smt2_pp.h" + +solver_na2as::solver_na2as() { + m_manager = 0; +} + +solver_na2as::~solver_na2as() { + restore_assumptions(0); +} + +void solver_na2as::assert_expr(expr * t, expr * a) { + SASSERT(m_manager != 0); + SASSERT(is_uninterp_const(a)); + SASSERT(m_manager->is_bool(a)); + TRACE("solver_na2as", tout << "asserting\n" << mk_ismt2_pp(t, *m_manager) << "\n" << mk_ismt2_pp(a, *m_manager) << "\n";); + m_manager->inc_ref(a); + m_assumptions.push_back(a); + expr_ref new_t(*m_manager); + new_t = m_manager->mk_implies(a, t); + assert_expr(new_t); +} + +void solver_na2as::init(ast_manager & m, symbol const & logic) { + SASSERT(m_assumptions.empty()); + m_manager = &m; + init_core(m, logic); +} + +struct append_assumptions { + ptr_vector & m_assumptions; + unsigned m_old_sz; + append_assumptions(ptr_vector & _m_assumptions, + unsigned num_assumptions, + expr * const * assumptions): + m_assumptions(_m_assumptions) { + m_old_sz = m_assumptions.size(); + m_assumptions.append(num_assumptions, assumptions); + } + + ~append_assumptions() { + m_assumptions.shrink(m_old_sz); + } +}; + +lbool solver_na2as::check_sat(unsigned num_assumptions, expr * const * assumptions) { + append_assumptions app(m_assumptions, num_assumptions, assumptions); + return check_sat_core(m_assumptions.size(), m_assumptions.c_ptr()); +} + +void solver_na2as::push() { + m_scopes.push_back(m_assumptions.size()); + push_core(); +} + +void solver_na2as::pop(unsigned n) { + pop_core(n); + unsigned lvl = m_scopes.size(); + SASSERT(n <= lvl); + unsigned new_lvl = lvl - n; + restore_assumptions(m_scopes[new_lvl]); + m_scopes.shrink(new_lvl); +} + +void solver_na2as::restore_assumptions(unsigned old_sz) { + SASSERT(old_sz == 0 || m_manager != 0); + for (unsigned i = old_sz; i < m_assumptions.size(); i++) { + m_manager->dec_ref(m_assumptions[i]); + } + m_assumptions.shrink(old_sz); +} + +unsigned solver_na2as::get_scope_level() const { + return m_scopes.size(); +} + +void solver_na2as::reset() { + reset_core(); + restore_assumptions(0); +} diff --git a/src/solver/solver_na2as.h b/src/solver/solver_na2as.h new file mode 100644 index 000000000..eb12479fc --- /dev/null +++ b/src/solver/solver_na2as.h @@ -0,0 +1,55 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + solver_na2as.h + +Abstract: + + Solver that implements "named" assertions using assumptions (aka answer literals). + That is, a named assertion assert_expr(t, a) is mapped into + a implies t + and 'a' is used as an extra assumption for check_sat. + +Author: + + Leonardo (leonardo) 2012-11-02 + +Notes: + +--*/ +#ifndef _SOLVER_NA2AS_H_ +#define _SOLVER_NA2AS_H_ + +#include"solver.h" + +class solver_na2as : public solver { + ast_manager * m_manager; + ptr_vector m_assumptions; + unsigned_vector m_scopes; + void restore_assumptions(unsigned old_sz); +public: + solver_na2as(); + virtual ~solver_na2as(); + + virtual void assert_expr(expr * t, expr * a); + virtual void assert_expr(expr * t) = 0; + + // Subclasses of solver_na2as should redefine the following *_core methods instead of these ones. + virtual void init(ast_manager & m, symbol const & logic); + virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions); + virtual void push(); + virtual void pop(unsigned n); + virtual unsigned get_scope_level() const; + virtual void reset(); +protected: + virtual void init_core(ast_manager & m, symbol const & logic) = 0; + virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) = 0; + virtual void push_core() = 0; + virtual void pop_core(unsigned n) = 0; + virtual void reset_core() = 0; +}; + + +#endif diff --git a/src/solver/strategic_solver.cpp b/src/solver/strategic_solver.cpp index a32aec2b1..616ec5342 100644 --- a/src/solver/strategic_solver.cpp +++ b/src/solver/strategic_solver.cpp @@ -25,7 +25,13 @@ Notes: // minimum verbosity level for portfolio verbose messages #define PS_VB_LVL 15 -strategic_solver_core::strategic_solver_core(): + +strategic_solver::ctx::ctx(ast_manager & m): + m_assertions(m), + m_assertion_names(m) { + } + +strategic_solver::strategic_solver(): m_manager(0), m_fparams(0), m_force_tactic(false), @@ -37,6 +43,7 @@ strategic_solver_core::strategic_solver_core(): m_default_fct(0), m_curr_tactic(0), m_proof(0), + m_core(0), m_callback(0) { m_use_inc_solver_results = false; DEBUG_CODE(m_num_scopes = 0;); @@ -45,7 +52,7 @@ strategic_solver_core::strategic_solver_core(): m_produce_unsat_cores = false; } -strategic_solver_core::~strategic_solver_core() { +strategic_solver::~strategic_solver() { SASSERT(!m_curr_tactic); dictionary::iterator it = m_logic2fct.begin(); dictionary::iterator end = m_logic2fct.end(); @@ -54,9 +61,11 @@ strategic_solver_core::~strategic_solver_core() { } if (m_proof) m().dec_ref(m_proof); + if (m_core) + m().dec_ref(m_core); } -bool strategic_solver_core::has_quantifiers() const { +bool strategic_solver::has_quantifiers() const { unsigned sz = get_num_assertions(); for (unsigned i = 0; i < sz; i++) { if (::has_quantifiers(get_assertion(i))) @@ -68,7 +77,7 @@ bool strategic_solver_core::has_quantifiers() const { /** \brief Return true if a tactic should be used when the incremental solver returns unknown. */ -bool strategic_solver_core::use_tactic_when_undef() const { +bool strategic_solver::use_tactic_when_undef() const { switch (m_inc_unknown_behavior) { case IUB_RETURN_UNDEF: return false; case IUB_USE_TACTIC_IF_QF: return !has_quantifiers(); @@ -79,7 +88,7 @@ bool strategic_solver_core::use_tactic_when_undef() const { } } -void strategic_solver_core::set_inc_solver(solver * s) { +void strategic_solver::set_inc_solver(solver * s) { SASSERT(m_inc_solver == 0); SASSERT(m_num_scopes == 0); m_inc_solver = s; @@ -87,7 +96,7 @@ void strategic_solver_core::set_inc_solver(solver * s) { m_inc_solver->set_progress_callback(m_callback); } -void strategic_solver_core::updt_params(params_ref const & p) { +void strategic_solver::updt_params(params_ref const & p) { if (m_inc_solver) m_inc_solver->updt_params(p); if (m_fparams) @@ -95,7 +104,7 @@ void strategic_solver_core::updt_params(params_ref const & p) { } -void strategic_solver_core::collect_param_descrs(param_descrs & r) { +void strategic_solver::collect_param_descrs(param_descrs & r) { if (m_inc_solver) m_inc_solver->collect_param_descrs(r); } @@ -105,7 +114,7 @@ void strategic_solver_core::collect_param_descrs(param_descrs & r) { timeout == UINT_MAX means infinite After the timeout a strategy is used. */ -void strategic_solver_core::set_inc_solver_timeout(unsigned timeout) { +void strategic_solver::set_inc_solver_timeout(unsigned timeout) { m_inc_solver_timeout = timeout; } @@ -113,14 +122,14 @@ void strategic_solver_core::set_inc_solver_timeout(unsigned timeout) { \brief Set the default tactic factory. It is used if there is no tactic for a given logic. */ -void strategic_solver_core::set_default_tactic(tactic_factory * fct) { +void strategic_solver::set_default_tactic(tactic_factory * fct) { m_default_fct = fct; } /** \brief Set a tactic factory for a given logic. */ -void strategic_solver_core::set_tactic_for(symbol const & logic, tactic_factory * fct) { +void strategic_solver::set_tactic_for(symbol const & logic, tactic_factory * fct) { tactic_factory * old_fct; if (m_logic2fct.find(logic, old_fct)) { dealloc(old_fct); @@ -128,31 +137,77 @@ void strategic_solver_core::set_tactic_for(symbol const & logic, tactic_factory m_logic2fct.insert(logic, fct); } -void strategic_solver_core::init(ast_manager & m, symbol const & logic) { +void strategic_solver::init(ast_manager & m, symbol const & logic) { m_manager = &m; m_logic = logic; if (m_inc_mode) { SASSERT(m_inc_solver); m_inc_solver->init(m, logic); } + m_ctx = alloc(ctx, m); + TRACE("strategic_solver", tout << "strategic_solver was initialized.\n";); +} + +unsigned strategic_solver::get_num_assertions() const { + if (m_ctx == 0) + return 0; + return m_ctx->m_assertions.size(); +} + +expr * strategic_solver::get_assertion(unsigned idx) const { + SASSERT(m_ctx); + return m_ctx->m_assertions.get(idx); +} + +expr * strategic_solver::get_assertion_name(unsigned idx) const { + SASSERT(m_ctx); + SASSERT(m_produce_unsat_cores); + return m_ctx->m_assertion_names.get(idx); +} + +void strategic_solver::set_produce_proofs(bool f) { + m_produce_proofs = f; + // do not need to propagate to inc_solver since flag cannot be changed after initialization +} + +void strategic_solver::set_produce_models(bool f) { + m_produce_models = f; + if (m_inc_solver) + m_inc_solver->set_produce_models(f); +} + +void strategic_solver::set_produce_unsat_cores(bool f) { + m_produce_unsat_cores = f; + // do not need to propagate to inc_solver since flag cannot be changed after initialization } // delayed inc solver initialization -void strategic_solver_core::init_inc_solver() { +void strategic_solver::init_inc_solver() { if (m_inc_mode) return; // solver was already initialized if (!m_inc_solver) return; // inc solver was not installed m_inc_mode = true; + m_inc_solver->set_produce_proofs(m_produce_proofs); + m_inc_solver->set_produce_models(m_produce_models); + m_inc_solver->set_produce_unsat_cores(m_produce_unsat_cores); m_inc_solver->set_front_end_params(*m_fparams); m_inc_solver->init(m(), m_logic); unsigned sz = get_num_assertions(); - for (unsigned i = 0; i < sz; i++) { - m_inc_solver->assert_expr(get_assertion(i)); + if (m_produce_unsat_cores) { + SASSERT(m_ctx->m_assertions.size() == m_ctx->m_assertion_names.size()); + for (unsigned i = 0; i < sz; i++) { + m_inc_solver->assert_expr(get_assertion(i), get_assertion_name(i)); + } + } + else { + for (unsigned i = 0; i < sz; i++) { + m_inc_solver->assert_expr(get_assertion(i)); + } } } -void strategic_solver_core::collect_statistics(statistics & st) const { +void strategic_solver::collect_statistics(statistics & st) const { if (m_use_inc_solver_results) { SASSERT(m_inc_solver); m_inc_solver->collect_statistics(st); @@ -165,7 +220,8 @@ void strategic_solver_core::collect_statistics(statistics & st) const { } } -void strategic_solver_core::reset() { +void strategic_solver::reset() { + m_ctx = 0; m_logic = symbol::null; m_inc_mode = false; m_check_sat_executed = false; @@ -176,18 +232,22 @@ void strategic_solver_core::reset() { reset_results(); } -void strategic_solver_core::reset_results() { +void strategic_solver::reset_results() { m_use_inc_solver_results = false; m_model = 0; if (m_proof) { m().dec_ref(m_proof); m_proof = 0; } + if (m_core) { + m().dec_ref(m_core); + m_core = 0; + } m_reason_unknown.clear(); m_stats.reset(); } -void strategic_solver_core::assert_expr(expr * t) { +void strategic_solver::assert_expr(expr * t) { if (m_check_sat_executed && !m_inc_mode) { // a check sat was already executed --> switch to incremental mode init_inc_solver(); @@ -197,16 +257,37 @@ void strategic_solver_core::assert_expr(expr * t) { SASSERT(m_inc_solver); m_inc_solver->assert_expr(t); } + SASSERT(m_ctx); + m_ctx->m_assertions.push_back(t); + if (m_produce_unsat_cores) + m_ctx->m_assertion_names.push_back(0); } -void strategic_solver_core::push() { +void strategic_solver::assert_expr(expr * t, expr * a) { + if (m_check_sat_executed && !m_inc_mode) { + // a check sat was already executed --> switch to incremental mode + init_inc_solver(); + SASSERT(m_inc_solver == 0 || m_inc_mode); + } + if (m_inc_mode) { + SASSERT(m_inc_solver); + m_inc_solver->assert_expr(t, a); + } + SASSERT(m_ctx); + m_ctx->m_assertions.push_back(t); + if (m_produce_unsat_cores) + m_ctx->m_assertion_names.push_back(a); +} + +void strategic_solver::push() { DEBUG_CODE(m_num_scopes++;); init_inc_solver(); if (m_inc_solver) m_inc_solver->push(); + m_ctx->m_scopes.push_back(m_ctx->m_assertions.size()); } -void strategic_solver_core::pop(unsigned n) { +void strategic_solver::pop(unsigned n) { DEBUG_CODE({ SASSERT(n <= m_num_scopes); m_num_scopes -= n; @@ -214,13 +295,20 @@ void strategic_solver_core::pop(unsigned n) { init_inc_solver(); if (m_inc_solver) m_inc_solver->pop(n); + + SASSERT(m_ctx); + unsigned new_lvl = m_ctx->m_scopes.size() - n; + unsigned old_sz = m_ctx->m_scopes[new_lvl]; + m_ctx->m_assertions.shrink(old_sz); + if (m_produce_unsat_cores) + m_ctx->m_assertion_names.shrink(old_sz); + m_ctx->m_scopes.shrink(new_lvl); } -unsigned strategic_solver_core::get_scope_level() const { - if (m_inc_solver) - return m_inc_solver->get_scope_level(); - else +unsigned strategic_solver::get_scope_level() const { + if (m_ctx == 0) return 0; + return m_ctx->m_assertions.size(); } struct aux_timeout_eh : public event_handler { @@ -233,10 +321,10 @@ struct aux_timeout_eh : public event_handler { } }; -struct strategic_solver_core::mk_tactic { - strategic_solver_core * m_solver; +struct strategic_solver::mk_tactic { + strategic_solver * m_solver; - mk_tactic(strategic_solver_core * s, tactic_factory * f):m_solver(s) { + mk_tactic(strategic_solver * s, tactic_factory * f):m_solver(s) { ast_manager & m = s->m(); params_ref p; front_end_params2params(*s->m_fparams, p); @@ -259,14 +347,14 @@ struct strategic_solver_core::mk_tactic { } }; -tactic_factory * strategic_solver_core::get_tactic_factory() const { +tactic_factory * strategic_solver::get_tactic_factory() const { tactic_factory * f = 0; if (m_logic2fct.find(m_logic, f)) return f; return m_default_fct.get(); } -lbool strategic_solver_core::check_sat_with_assumptions(unsigned num_assumptions, expr * const * assumptions) { +lbool strategic_solver::check_sat_with_assumptions(unsigned num_assumptions, expr * const * assumptions) { if (!m_inc_solver) { IF_VERBOSE(PS_VB_LVL, verbose_stream() << "incremental solver was not installed, returning unknown...\n";); m_use_inc_solver_results = false; @@ -275,10 +363,16 @@ lbool strategic_solver_core::check_sat_with_assumptions(unsigned num_assumptions } init_inc_solver(); m_use_inc_solver_results = true; + TRACE("strategic_solver", tout << "invoking inc_solver with " << num_assumptions << " assumptions\n";); return m_inc_solver->check_sat(num_assumptions, assumptions); } -lbool strategic_solver_core::check_sat(unsigned num_assumptions, expr * const * assumptions) { +lbool strategic_solver::check_sat(unsigned num_assumptions, expr * const * assumptions) { + TRACE("strategic_solver", tout << "assumptions at strategic_solver:\n"; + for (unsigned i = 0; i < num_assumptions; i++) { + tout << mk_ismt2_pp(assumptions[i], m()) << "\n"; + } + tout << "m_produce_unsat_cores: " << m_produce_unsat_cores << ", m_inc_mode: " << m_inc_mode << "\n";); reset_results(); m_check_sat_executed = true; if (num_assumptions > 0 || // assumptions were provided @@ -333,10 +427,18 @@ lbool strategic_solver_core::check_sat(unsigned num_assumptions, expr * const * goal_ref g = alloc(goal, m(), m_produce_proofs, m_produce_models, m_produce_unsat_cores); unsigned sz = get_num_assertions(); - for (unsigned i = 0; i < sz; i++) { - g->assert_expr(get_assertion(i)); + if (m_produce_unsat_cores) { + SASSERT(m_ctx->m_assertions.size() == m_ctx->m_assertion_names.size()); + for (unsigned i = 0; i < sz; i++) + g->assert_expr(get_assertion(i), get_assertion_name(i)); + } + else { + for (unsigned i = 0; i < sz; i++) + g->assert_expr(get_assertion(i)); } expr_dependency_ref core(m()); + + TRACE("strategic_solver", tout << "using goal...\n"; g->display_with_dependencies(tout);); mk_tactic tct_maker(this, factory); SASSERT(m_curr_tactic); @@ -348,10 +450,14 @@ lbool strategic_solver_core::check_sat(unsigned num_assumptions, expr * const * m_proof = pr; m().inc_ref(m_proof); } + if (core) { + m_core = core; + m().inc_ref(m_core); + } return r; } -void strategic_solver_core::set_cancel(bool f) { +void strategic_solver::set_cancel(bool f) { if (m_inc_solver) m_inc_solver->set_cancel(f); #pragma omp critical (strategic_solver) @@ -361,14 +467,18 @@ void strategic_solver_core::set_cancel(bool f) { } } -void strategic_solver_core::get_unsat_core(ptr_vector & r) { +void strategic_solver::get_unsat_core(ptr_vector & r) { + TRACE("strategic_solver", tout << "get_unsat_core, m_use_inc_solver_results: " << m_use_inc_solver_results << "\n";); if (m_use_inc_solver_results) { SASSERT(m_inc_solver); m_inc_solver->get_unsat_core(r); } + else { + m().linearize(m_core, r); + } } -void strategic_solver_core::get_model(model_ref & m) { +void strategic_solver::get_model(model_ref & m) { if (m_use_inc_solver_results) { SASSERT(m_inc_solver); m_inc_solver->get_model(m); @@ -378,7 +488,7 @@ void strategic_solver_core::get_model(model_ref & m) { } } -proof * strategic_solver_core::get_proof() { +proof * strategic_solver::get_proof() { if (m_use_inc_solver_results) { SASSERT(m_inc_solver); return m_inc_solver->get_proof(); @@ -388,7 +498,7 @@ proof * strategic_solver_core::get_proof() { } } -std::string strategic_solver_core::reason_unknown() const { +std::string strategic_solver::reason_unknown() const { if (m_use_inc_solver_results) { SASSERT(m_inc_solver); return m_inc_solver->reason_unknown(); @@ -396,20 +506,20 @@ std::string strategic_solver_core::reason_unknown() const { return m_reason_unknown; } -void strategic_solver_core::get_labels(svector & r) { +void strategic_solver::get_labels(svector & r) { if (m_use_inc_solver_results) { SASSERT(m_inc_solver); m_inc_solver->get_labels(r); } } -void strategic_solver_core::set_progress_callback(progress_callback * callback) { +void strategic_solver::set_progress_callback(progress_callback * callback) { m_callback = callback; if (m_inc_solver) m_inc_solver->set_progress_callback(callback); } -void strategic_solver_core::display(std::ostream & out) const { +void strategic_solver::display(std::ostream & out) const { if (m_manager) { unsigned num = get_num_assertions(); out << "(solver"; @@ -424,50 +534,7 @@ void strategic_solver_core::display(std::ostream & out) const { } -strategic_solver::ctx::ctx(ast_manager & m):m_assertions(m) { -} - -void strategic_solver::init(ast_manager & m, symbol const & logic) { - strategic_solver_core::init(m, logic); - m_ctx = alloc(ctx, m); -} - -unsigned strategic_solver::get_num_assertions() const { - if (m_ctx == 0) - return 0; - return m_ctx->m_assertions.size(); -} - -expr * strategic_solver::get_assertion(unsigned idx) const { - SASSERT(m_ctx); - return m_ctx->m_assertions.get(idx); -} - -void strategic_solver::assert_expr(expr * t) { - SASSERT(m_ctx); - strategic_solver_core::assert_expr(t); - m_ctx->m_assertions.push_back(t); -} - -void strategic_solver::push() { - SASSERT(m_ctx); - strategic_solver_core::push(); - m_ctx->m_scopes.push_back(m_ctx->m_assertions.size()); -} - -void strategic_solver::pop(unsigned n) { - SASSERT(m_ctx); - unsigned new_lvl = m_ctx->m_scopes.size() - n; - unsigned old_sz = m_ctx->m_scopes[new_lvl]; - m_ctx->m_assertions.shrink(old_sz); - m_ctx->m_scopes.shrink(new_lvl); - strategic_solver_core::pop(n); -} - -void strategic_solver::reset() { - m_ctx = 0; - strategic_solver_core::reset(); -} + diff --git a/src/solver/strategic_solver.h b/src/solver/strategic_solver.h index 4d4a47388..e903e9bd0 100644 --- a/src/solver/strategic_solver.h +++ b/src/solver/strategic_solver.h @@ -46,7 +46,7 @@ struct front_end_params; It goes back to non_incremental mode when: - reset is invoked. */ -class strategic_solver_core : public solver { +class strategic_solver : public solver { public: // Behavior when the incremental solver returns unknown. enum inc_unknown_behavior { @@ -73,9 +73,18 @@ private: bool m_use_inc_solver_results; model_ref m_model; proof * m_proof; + expr_dependency * m_core; std::string m_reason_unknown; statistics m_stats; + struct ctx { + expr_ref_vector m_assertions; + expr_ref_vector m_assertion_names; + unsigned_vector m_scopes; + ctx(ast_manager & m); + }; + scoped_ptr m_ctx; + #ifdef Z3DEBUG unsigned m_num_scopes; #endif @@ -97,8 +106,8 @@ private: bool use_tactic_when_undef() const; public: - strategic_solver_core(); - ~strategic_solver_core(); + strategic_solver(); + ~strategic_solver(); ast_manager & m() const { SASSERT(m_manager); return *m_manager; } @@ -114,19 +123,21 @@ public: virtual void updt_params(params_ref const & p); virtual void collect_param_descrs(param_descrs & r); - virtual void set_produce_proofs(bool f) { m_produce_proofs = f; } - virtual void set_produce_models(bool f) { m_produce_models = f; } - virtual void set_produce_unsat_cores(bool f) { m_produce_unsat_cores = f; } + virtual void set_produce_proofs(bool f); + virtual void set_produce_models(bool f); + virtual void set_produce_unsat_cores(bool f); + + unsigned get_num_assertions() const; + expr * get_assertion(unsigned idx) const; + expr * get_assertion_name(unsigned idx) const; - virtual unsigned get_num_assertions() const = 0; - virtual expr * get_assertion(unsigned idx) const = 0; - virtual void display(std::ostream & out) const; virtual void init(ast_manager & m, symbol const & logic); virtual void collect_statistics(statistics & st) const; virtual void reset(); virtual void assert_expr(expr * t); + virtual void assert_expr(expr * t, expr * a); virtual void push(); virtual void pop(unsigned n); virtual unsigned get_scope_level() const; @@ -140,30 +151,4 @@ public: virtual void set_progress_callback(progress_callback * callback); }; -/** - \brief Default implementation of strategic_solver_core -*/ -class strategic_solver : public strategic_solver_core { - struct ctx { - expr_ref_vector m_assertions; - unsigned_vector m_scopes; - ctx(ast_manager & m); - }; - scoped_ptr m_ctx; -public: - strategic_solver() {} - - virtual void init(ast_manager & m, symbol const & logic); - - virtual void assert_expr(expr * t); - virtual void push(); - virtual void pop(unsigned n); - virtual void reset(); - - virtual unsigned get_num_assertions() const; - virtual expr * get_assertion(unsigned idx) const; -}; - - - #endif diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 0747c7c9d..63308bd27 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -31,7 +31,7 @@ tactic2solver_core::ctx::ctx(ast_manager & m, symbol const & logic): tactic2solver_core::~tactic2solver_core() { } -void tactic2solver_core::init(ast_manager & m, symbol const & logic) { +void tactic2solver_core::init_core(ast_manager & m, symbol const & logic) { m_ctx = alloc(ctx, m, logic); } @@ -62,7 +62,7 @@ void tactic2solver_core::collect_param_descrs(param_descrs & r) { } } -void tactic2solver_core::reset() { +void tactic2solver_core::reset_core() { SASSERT(m_ctx); m_ctx->m_assertions.reset(); m_ctx->m_scopes.reset(); @@ -75,13 +75,13 @@ void tactic2solver_core::assert_expr(expr * t) { m_ctx->m_result = 0; } -void tactic2solver_core::push() { +void tactic2solver_core::push_core() { SASSERT(m_ctx); m_ctx->m_scopes.push_back(m_ctx->m_assertions.size()); m_ctx->m_result = 0; } -void tactic2solver_core::pop(unsigned n) { +void tactic2solver_core::pop_core(unsigned n) { SASSERT(m_ctx); unsigned new_lvl = m_ctx->m_scopes.size() - n; unsigned old_sz = m_ctx->m_scopes[new_lvl]; @@ -90,12 +90,7 @@ void tactic2solver_core::pop(unsigned n) { m_ctx->m_result = 0; } -unsigned tactic2solver_core::get_scope_level() const { - SASSERT(m_ctx); - return m_ctx->m_scopes.size(); -} - -lbool tactic2solver_core::check_sat(unsigned num_assumptions, expr * const * assumptions) { +lbool tactic2solver_core::check_sat_core(unsigned num_assumptions, expr * const * assumptions) { SASSERT(m_ctx); ast_manager & m = m_ctx->m(); params_ref p = m_params; diff --git a/src/solver/tactic2solver.h b/src/solver/tactic2solver.h index fe92f3a7d..8cf3551b4 100644 --- a/src/solver/tactic2solver.h +++ b/src/solver/tactic2solver.h @@ -22,7 +22,7 @@ Notes: #ifndef _TACTIC2SOLVER_H_ #define _TACTIC2SOLVER_H_ -#include"solver.h" +#include"solver_na2as.h" #include"tactic.h" /** @@ -32,7 +32,7 @@ Notes: option for applications trying to solve many easy queries that a similar to each other. */ -class tactic2solver_core : public solver { +class tactic2solver_core : public solver_na2as { struct ctx { symbol m_logic; expr_ref_vector m_assertions; @@ -63,13 +63,13 @@ public: virtual void set_produce_models(bool f) { m_produce_models = f; } virtual void set_produce_unsat_cores(bool f) { m_produce_unsat_cores = f; } - virtual void init(ast_manager & m, symbol const & logic); - virtual void reset(); virtual void assert_expr(expr * t); - virtual void push(); - virtual void pop(unsigned n); - virtual unsigned get_scope_level() const; - virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions); + + virtual void init_core(ast_manager & m, symbol const & logic); + virtual void reset_core(); + virtual void push_core(); + virtual void pop_core(unsigned n); + virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions); virtual void set_cancel(bool f); diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index 52637b1c3..9ab597dfa 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -209,6 +209,7 @@ class propagate_values_tactic : public tactic { result.push_back(m_goal); SASSERT(m_goal->is_well_sorted()); TRACE("propagate_values", m_goal->display(tout);); + TRACE("propagate_values_core", m_goal->display_with_dependencies(tout);); m_goal = 0; } }; diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index 6897097be..c6dad42b2 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -22,6 +22,13 @@ Revision History: #include"for_each_expr.h" #include"well_sorted.h" +goal::precision goal::mk_union(precision p1, precision p2) { + if (p1 == PRECISE) return p2; + if (p2 == PRECISE) return p1; + if (p1 != p2) return UNDER_OVER; + return p1; +} + std::ostream & operator<<(std::ostream & out, goal::precision p) { switch (p) { case goal::PRECISE: out << "precise"; break; @@ -32,6 +39,58 @@ std::ostream & operator<<(std::ostream & out, goal::precision p) { return out; } +goal::goal(ast_manager & m, bool models_enabled, bool core_enabled): + m_manager(m), + m_ref_count(0), + m_depth(0), + m_models_enabled(models_enabled), + m_proofs_enabled(m.proofs_enabled()), + m_core_enabled(core_enabled), + m_inconsistent(false), + m_precision(PRECISE) { + } + +goal::goal(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled): + m_manager(m), + m_ref_count(0), + m_depth(0), + m_models_enabled(models_enabled), + m_proofs_enabled(proofs_enabled), + m_core_enabled(core_enabled), + m_inconsistent(false), + m_precision(PRECISE) { + SASSERT(!proofs_enabled || m.proofs_enabled()); + } + +goal::goal(goal const & src): + m_manager(src.m()), + m_ref_count(0), + m_depth(0), + m_models_enabled(src.models_enabled()), + m_proofs_enabled(src.proofs_enabled()), + m_core_enabled(src.unsat_core_enabled()), + m_inconsistent(false), + m_precision(PRECISE) { + copy_from(src); + } + +// Copy configuration: depth, models/proofs/cores flags, and precision from src. +// The assertions are not copied +goal::goal(goal const & src, bool): + m_manager(src.m()), + m_ref_count(0), + m_depth(src.m_depth), + m_models_enabled(src.models_enabled()), + m_proofs_enabled(src.proofs_enabled()), + m_core_enabled(src.unsat_core_enabled()), + m_inconsistent(false), + m_precision(src.m_precision) { +} + +goal::~goal() { + reset_core(); +} + void goal::copy_to(goal & target) const { SASSERT(&m_manager == &(target.m_manager)); if (this == &target) @@ -174,6 +233,10 @@ void goal::assert_expr(expr * f, proof * pr, expr_dependency * d) { quick_process(false, f, d); } +void goal::assert_expr(expr * f, expr_dependency * d) { + assert_expr(f, proofs_enabled() ? m().mk_asserted(f) : 0, d); +} + void goal::get_formulas(ptr_vector & result) { unsigned sz = size(); for (unsigned i = 0; i < sz; i++) { @@ -570,6 +633,27 @@ goal * goal::translate(ast_translation & translator) const { return res; } + +bool goal::sat_preserved() const { + return prec() == PRECISE || prec() == UNDER; +} + +bool goal::unsat_preserved() const { + return prec() == PRECISE || prec() == OVER; +} + +bool goal::is_decided_sat() const { + return size() == 0 && sat_preserved(); +} + +bool goal::is_decided_unsat() const { + return inconsistent() && unsat_preserved(); +} + +bool goal::is_decided() const { + return is_decided_sat() || is_decided_unsat(); +} + bool is_equal(goal const & s1, goal const & s2) { if (s1.size() != s2.size()) return false; diff --git a/src/tactic/goal.h b/src/tactic/goal.h index c1dcaa6f6..294987699 100644 --- a/src/tactic/goal.h +++ b/src/tactic/goal.h @@ -45,12 +45,7 @@ public: UNDER_OVER // goal is garbage: the produce of combined under and over approximation steps. }; - static precision mk_union(precision p1, precision p2) { - if (p1 == PRECISE) return p2; - if (p2 == PRECISE) return p1; - if (p1 != p2) return UNDER_OVER; - return p1; - } + static precision mk_union(precision p1, precision p2); protected: ast_manager & m_manager; @@ -78,55 +73,13 @@ protected: void reset_core(); public: - goal(ast_manager & m, bool models_enabled = true, bool core_enabled = false): - m_manager(m), - m_ref_count(0), - m_depth(0), - m_models_enabled(models_enabled), - m_proofs_enabled(m.proofs_enabled()), - m_core_enabled(core_enabled), - m_inconsistent(false), - m_precision(PRECISE) { - } - - goal(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled): - m_manager(m), - m_ref_count(0), - m_depth(0), - m_models_enabled(models_enabled), - m_proofs_enabled(proofs_enabled), - m_core_enabled(core_enabled), - m_inconsistent(false), - m_precision(PRECISE) { - SASSERT(!proofs_enabled || m.proofs_enabled()); - } - - goal(goal const & src): - m_manager(src.m()), - m_ref_count(0), - m_depth(0), - m_models_enabled(src.models_enabled()), - m_proofs_enabled(src.proofs_enabled()), - m_core_enabled(src.unsat_core_enabled()), - m_inconsistent(false), - m_precision(PRECISE) { - copy_from(src); - } - + goal(ast_manager & m, bool models_enabled = true, bool core_enabled = false); + goal(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled); + goal(goal const & src); // Copy configuration: depth, models/proofs/cores flags, and precision from src. // The assertions are not copied - goal(goal const & src, bool): - m_manager(src.m()), - m_ref_count(0), - m_depth(src.m_depth), - m_models_enabled(src.models_enabled()), - m_proofs_enabled(src.proofs_enabled()), - m_core_enabled(src.unsat_core_enabled()), - m_inconsistent(false), - m_precision(src.m_precision) { - } - - ~goal() { reset_core(); } + goal(goal const & src, bool); + ~goal(); void inc_ref() { ++m_ref_count; } void dec_ref() { --m_ref_count; if (m_ref_count == 0) dealloc(this); } @@ -152,9 +105,9 @@ public: void copy_from(goal const & src) { src.copy_to(*this); } void assert_expr(expr * f, proof * pr, expr_dependency * d); - void assert_expr(expr * f) { - assert_expr(f, proofs_enabled() ? m().mk_asserted(f) : 0, 0); - } + void assert_expr(expr * f, expr_dependency * d); + void assert_expr(expr * f, expr * d) { assert_expr(f, m().mk_leaf(d)); } + void assert_expr(expr * f) { assert_expr(f, static_cast(0)); } unsigned size() const { return m().size(m_forms); } @@ -181,26 +134,11 @@ public: void display_with_dependencies(ast_printer_context & ctx) const; void display_with_dependencies(std::ostream & out) const; - bool sat_preserved() const { - return prec() == PRECISE || prec() == UNDER; - } - - bool unsat_preserved() const { - return prec() == PRECISE || prec() == OVER; - } - - bool is_decided_sat() const { - return size() == 0 && sat_preserved(); - } - - bool is_decided_unsat() const { - return inconsistent() && unsat_preserved(); - } - - bool is_decided() const { - return is_decided_sat() || is_decided_unsat(); - } - + bool sat_preserved() const; + bool unsat_preserved() const; + bool is_decided_sat() const; + bool is_decided_unsat() const; + bool is_decided() const; bool is_well_sorted() const; goal * translate(ast_translation & translator) const; diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 52762edc4..50d972a0d 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -18,8 +18,7 @@ Notes: --*/ #include"cmd_context.h" -#include"ni_solver.h" -#include"strategic_solver_cmd.h" +#include"strategic_solver.h" #include"qfbv_tactic.h" #include"qflia_tactic.h" #include"qfnia_tactic.h" @@ -34,7 +33,7 @@ Notes: #include"default_tactic.h" #include"ufbv_tactic.h" #include"qffpa_tactic.h" -#include"default_solver.h" +#include"smt_solver.h" MK_SIMPLE_TACTIC_FACTORY(qfuf_fct, mk_qfuf_tactic(m, p)); MK_SIMPLE_TACTIC_FACTORY(qfidl_fct, mk_qfidl_tactic(m, p)); @@ -56,7 +55,7 @@ MK_SIMPLE_TACTIC_FACTORY(qfnra_fct, mk_qfnra_tactic(m, p)); MK_SIMPLE_TACTIC_FACTORY(qffpa_fct, mk_qffpa_tactic(m, p)); MK_SIMPLE_TACTIC_FACTORY(ufbv_fct, mk_ufbv_tactic(m, p)); -static void init(strategic_solver_core * s) { +static void init(strategic_solver * s) { s->set_default_tactic(alloc(default_fct)); s->set_tactic_for(symbol("QF_UF"), alloc(qfuf_fct)); s->set_tactic_for(symbol("QF_BV"), alloc(qfbv_fct)); @@ -80,17 +79,10 @@ static void init(strategic_solver_core * s) { s->set_tactic_for(symbol("QF_FPA"), alloc(qffpa_fct)); } -solver * mk_smt_strategic_solver(cmd_context & ctx) { - strategic_solver_cmd * s = alloc(strategic_solver_cmd, ctx); - s->set_inc_solver(mk_quasi_incremental_smt_solver(ctx)); - init(s); - return s; -} - solver * mk_smt_strategic_solver(bool force_tactic) { strategic_solver * s = alloc(strategic_solver); s->force_tactic(force_tactic); - s->set_inc_solver(mk_default_solver()); + s->set_inc_solver(mk_smt_solver()); init(s); return s; } diff --git a/src/tactic/portfolio/smt_strategic_solver.h b/src/tactic/portfolio/smt_strategic_solver.h index f3cc2e0e0..060721e09 100644 --- a/src/tactic/portfolio/smt_strategic_solver.h +++ b/src/tactic/portfolio/smt_strategic_solver.h @@ -20,9 +20,7 @@ Notes: #ifndef _SMT_STRATEGIC_SOLVER_H_ #define _SMT_STRATEGIC_SOLVER_H_ -class cmd_context; -// Create a strategic solver for the SMT 2.0 frontend. -solver * mk_smt_strategic_solver(cmd_context & ctx); +class solver; // Create a strategic solver for the Z3 API solver * mk_smt_strategic_solver(bool force_tactic=false); diff --git a/src/test/quant_solve.cpp b/src/test/quant_solve.cpp index fe3454336..af6861af0 100644 --- a/src/test/quant_solve.cpp +++ b/src/test/quant_solve.cpp @@ -6,7 +6,7 @@ #include "lbool.h" #include #include "expr_replacer.h" -#include "smt_solver.h" +#include "smt_kernel.h" #include "reg_decl_plugins.h" #include "expr_abstract.h" #include "model_smt2_pp.h" @@ -29,7 +29,7 @@ static void validate_quant_solution(ast_manager& m, expr* fml, expr* guard, qe:: expr_ref tmp(m); tmp = m.mk_not(m.mk_implies(guard, fml1)); front_end_params fp; - smt::solver solver(m, fp); + smt::kernel solver(m, fp); solver.assert_expr(tmp); lbool res = solver.check(); //SASSERT(res == l_false); @@ -64,7 +64,7 @@ static void validate_quant_solutions(app* x, expr* fml, expr_ref_vector& guards) tmp = m.mk_not(m.mk_iff(fml2, tmp)); std::cout << mk_pp(tmp, m) << "\n"; front_end_params fp; - smt::solver solver(m, fp); + smt::kernel solver(m, fp); solver.assert_expr(tmp); lbool res = solver.check(); std::cout << "checked\n";