From 8198e62cbd0627ef698084a6fe2edf04b55101bc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 11 Dec 2012 17:47:27 -0800 Subject: [PATCH] solver factories, cleanup solver API, simplified strategic solver, added combined solver Signed-off-by: Leonardo de Moura --- src/api/api_solver.cpp | 37 +- src/api/api_solver.h | 15 +- src/cmd_context/cmd_context.cpp | 21 +- src/cmd_context/cmd_context.h | 6 +- src/cmd_context/context_params.cpp | 10 +- src/cmd_context/context_params.h | 9 +- src/parsers/smt/smtlib_solver.cpp | 2 +- src/shell/smtlib_frontend.cpp | 6 +- src/smt/smt_solver.cpp | 138 +++----- src/smt/smt_solver.h | 9 +- src/solver/combined_solver.cpp | 289 ++++++++++++++++ src/solver/combined_solver.h | 32 ++ src/solver/combined_solver_params.pyg | 9 + src/solver/solver.h | 31 +- src/solver/solver_na2as.cpp | 29 +- src/solver/solver_na2as.h | 8 +- src/solver/strategic_solver.cpp | 2 + src/solver/strategic_solver.h | 7 +- src/solver/tactic2solver.cpp | 326 ++++++++++-------- src/solver/tactic2solver.h | 96 +----- src/tactic/portfolio/smt_strategic_solver.cpp | 124 ++++--- src/tactic/portfolio/smt_strategic_solver.h | 6 +- 22 files changed, 720 insertions(+), 492 deletions(-) create mode 100644 src/solver/combined_solver.cpp create mode 100644 src/solver/combined_solver.h create mode 100644 src/solver/combined_solver_params.pyg diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 89bfd9519..6bf184708 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -34,15 +34,15 @@ Revision History: 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); - mk_c(c)->params().init_solver_params(mk_c(c)->m(), *(s->m_solver), s->m_params); - s->m_solver->init(m, s->m_logic); - s->m_initialized = true; + bool proofs_enabled, models_enabled, unsat_core_enabled; + params_ref p = s->m_params; + mk_c(c)->params().get_solver_params(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled); + s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic); } static void init_solver(Z3_context c, Z3_solver s) { - if (!to_solver(s)->m_initialized) + if (to_solver(s)->m_solver.get() == 0) init_solver_core(c, s); } @@ -50,8 +50,7 @@ extern "C" { Z3_TRY; LOG_Z3_mk_simple_solver(c); RESET_ERROR_CODE(); - Z3_solver_ref * s = alloc(Z3_solver_ref); - s->m_solver = mk_smt_solver(); + Z3_solver_ref * s = alloc(Z3_solver_ref, mk_smt_solver_factory()); mk_c(c)->save_object(s); Z3_solver r = of_solver(s); RETURN_Z3(r); @@ -62,8 +61,7 @@ extern "C" { Z3_TRY; LOG_Z3_mk_solver(c); RESET_ERROR_CODE(); - Z3_solver_ref * s = alloc(Z3_solver_ref); - s->m_solver = mk_smt_strategic_solver(); + Z3_solver_ref * s = alloc(Z3_solver_ref, mk_smt_strategic_solver_factory()); mk_c(c)->save_object(s); Z3_solver r = of_solver(s); RETURN_Z3(r); @@ -74,8 +72,7 @@ extern "C" { Z3_TRY; LOG_Z3_mk_solver_for_logic(c, logic); RESET_ERROR_CODE(); - 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 */); + Z3_solver_ref * s = alloc(Z3_solver_ref, mk_smt_strategic_solver_factory(to_symbol(logic))); mk_c(c)->save_object(s); Z3_solver r = of_solver(s); RETURN_Z3(r); @@ -86,8 +83,7 @@ extern "C" { Z3_TRY; LOG_Z3_mk_solver_from_tactic(c, t); RESET_ERROR_CODE(); - Z3_solver_ref * s = alloc(Z3_solver_ref); - s->m_solver = alloc(tactic2solver, to_tactic_ref(t)); + Z3_solver_ref * s = alloc(Z3_solver_ref, mk_tactic2solver_factory(to_tactic_ref(t))); mk_c(c)->save_object(s); Z3_solver r = of_solver(s); RETURN_Z3(r); @@ -100,7 +96,12 @@ extern "C" { RESET_ERROR_CODE(); std::ostringstream buffer; param_descrs descrs; + bool initialized = to_solver(s)->m_solver.get() != 0; + if (!initialized) + init_solver(c, s); to_solver_ref(s)->collect_param_descrs(descrs); + if (!initialized) + to_solver(s)->m_solver = 0; descrs.display(buffer); return mk_c(c)->mk_external_string(buffer.str()); Z3_CATCH_RETURN(""); @@ -112,7 +113,12 @@ extern "C" { RESET_ERROR_CODE(); Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref); mk_c(c)->save_object(d); + bool initialized = to_solver(s)->m_solver.get() != 0; + if (!initialized) + init_solver(c, s); to_solver_ref(s)->collect_param_descrs(d->m_descrs); + if (!initialized) + to_solver(s)->m_solver = 0; Z3_param_descrs r = of_param_descrs(d); RETURN_Z3(r); Z3_CATCH_RETURN(0); @@ -122,7 +128,7 @@ extern "C" { Z3_TRY; LOG_Z3_solver_set_params(c, s, p); RESET_ERROR_CODE(); - if (to_solver(s)->m_initialized) { + if (to_solver(s)->m_solver) { 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) @@ -176,8 +182,7 @@ extern "C" { Z3_TRY; LOG_Z3_solver_reset(c, s); RESET_ERROR_CODE(); - to_solver_ref(s)->reset(); - to_solver(s)->m_initialized = false; + to_solver(s)->m_solver = 0; Z3_CATCH; } diff --git a/src/api/api_solver.h b/src/api/api_solver.h index 1569ef0da..f11c9bfd8 100644 --- a/src/api/api_solver.h +++ b/src/api/api_solver.h @@ -22,17 +22,16 @@ Revision History: #include"solver.h" struct Z3_solver_ref : public api::object { - solver * m_solver; - params_ref m_params; - 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); } + scoped_ptr m_solver_factory; + ref m_solver; + params_ref m_params; + symbol m_logic; + Z3_solver_ref(solver_factory * f):m_solver_factory(f), m_solver(0), m_logic(symbol::null) {} + virtual ~Z3_solver_ref() {} }; inline Z3_solver_ref * to_solver(Z3_solver s) { return reinterpret_cast(s); } inline Z3_solver of_solver(Z3_solver_ref * s) { return reinterpret_cast(s); } -inline solver * to_solver_ref(Z3_solver s) { return to_solver(s)->m_solver; } +inline solver * to_solver_ref(Z3_solver s) { return to_solver(s)->m_solver.get(); } #endif diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 828cc3a68..e86e56b69 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -582,8 +582,8 @@ void cmd_context::init_manager_core(bool new_manager) { // it prevents clashes with builtin types. insert(pm().mk_plist_decl()); } - if (m_solver) { - init_solver_options(m_solver.get()); + if (m_solver_factory) { + mk_solver(); } m_check_logic.set_logic(m(), m_logic); } @@ -1119,7 +1119,7 @@ void cmd_context::reset(bool finalize) { reset_func_decls(); restore_assertions(0); if (m_solver) - m_solver->reset(); + m_solver = 0; m_pp_env = 0; m_dt_eh = 0; if (m_manager) { @@ -1441,17 +1441,18 @@ void cmd_context::validate_model() { } } -void cmd_context::init_solver_options(solver * s) { +void cmd_context::mk_solver() { + bool proofs_enabled, models_enabled, unsat_core_enabled; params_ref p; - m_params.init_solver_params(m(), *m_solver, p); - m_solver->init(m(), m_logic); + m_params.get_solver_params(m(), p, proofs_enabled, models_enabled, unsat_core_enabled); + m_solver = (*m_solver_factory)(m(), p, proofs_enabled, models_enabled, unsat_core_enabled, m_logic); } -void cmd_context::set_solver(solver * s) { +void cmd_context::set_solver_factory(solver_factory * f) { + m_solver_factory = f; m_check_sat_result = 0; - m_solver = s; - if (has_manager() && s != 0) { - init_solver_options(s); + if (has_manager() && f != 0) { + mk_solver(); // assert formulas and create scopes in the new solver. unsigned lim = 0; svector::iterator it = m_scopes.begin(); diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 2edc87ca6..63e5e7040 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -185,6 +185,7 @@ protected: }; svector m_scopes; + scoped_ptr m_solver_factory; ref m_solver; ref m_check_sat_result; @@ -243,7 +244,7 @@ protected: void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; } void print_unsupported_info(symbol const& s) { if (s != symbol::null) diagnostic_stream() << "; " << s << std::endl;} - void init_solver_options(solver * s); + void mk_solver(); public: cmd_context(bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null); @@ -289,8 +290,7 @@ public: pdecl_manager & pm() const { if (!m_pmanager) const_cast(this)->init_manager(); return *m_pmanager; } sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; } - void set_solver(solver * s); - solver * get_solver() const { return m_solver.get(); } + void set_solver_factory(solver_factory * s); void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; } check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); } check_sat_state cs_state() const; diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index 6d9222a37..2752967dd 100644 --- a/src/cmd_context/context_params.cpp +++ b/src/cmd_context/context_params.cpp @@ -131,11 +131,11 @@ params_ref context_params::merge_default_params(params_ref const & p) { } } -void context_params::init_solver_params(ast_manager & m, solver & s, params_ref const & p) { - s.set_produce_proofs(m.proofs_enabled() && m_proof); - s.set_produce_models(p.get_bool("model", m_model)); - s.set_produce_unsat_cores(p.get_bool("unsat_core", m_unsat_core)); - s.updt_params(merge_default_params(p)); +void context_params::get_solver_params(ast_manager const & m, params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled) { + proofs_enabled = m.proofs_enabled() && p.get_bool("proof", m_proof); + models_enabled = p.get_bool("model", m_model); + unsat_core_enabled = p.get_bool("unsat_core", m_unsat_core); + p = merge_default_params(p); } ast_manager * context_params::mk_ast_manager() { diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h index dd60b9616..526b4f517 100644 --- a/src/cmd_context/context_params.h +++ b/src/cmd_context/context_params.h @@ -22,7 +22,6 @@ Notes: #include"params.h" class ast_manager; -class solver; class context_params { void set_bool(bool & opt, char const * param, char const * value); @@ -50,13 +49,9 @@ public: */ /** - \brief Goodie for updating the solver params - based on the configuration of the context_params object. - - This method is used when creating solvers from the - cmd_context and API. + \brief Goodies for extracting parameters for creating a solver object. */ - void init_solver_params(ast_manager & m, solver & s, params_ref const & p); + void get_solver_params(ast_manager const & m, params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled); /** \brief Include in p parameters derived from this context_params. diff --git a/src/parsers/smt/smtlib_solver.cpp b/src/parsers/smt/smtlib_solver.cpp index ef28216bf..7c8572ad8 100644 --- a/src/parsers/smt/smtlib_solver.cpp +++ b/src/parsers/smt/smtlib_solver.cpp @@ -86,7 +86,7 @@ namespace smtlib { benchmark.add_formula(m_ast_manager.mk_true()); } m_ctx = alloc(cmd_context, true, &m_ast_manager, benchmark.get_logic()); - m_ctx->set_solver(mk_smt_strategic_solver(false)); + m_ctx->set_solver_factory(mk_smt_strategic_solver_factory()); 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 1551329c6..ef0b4ad6b 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/src/shell/smtlib_frontend.cpp @@ -30,9 +30,6 @@ Revision History: #include"subpaving_cmds.h" #include"smt_strategic_solver.h" -#include"tactic2solver.h" -#include"qfnra_nlsat_tactic.h" - extern bool g_display_statistics; extern void display_config(); static clock_t g_start_time; @@ -98,8 +95,7 @@ unsigned read_smtlib2_commands(char const * file_name) { signal(SIGINT, on_ctrl_c); cmd_context ctx; - solver * s = mk_smt_strategic_solver(false); - ctx.set_solver(s); + ctx.set_solver_factory(mk_smt_strategic_solver_factory()); install_dl_cmds(ctx); install_dbg_cmds(ctx); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index e8c1c6698..1fbb58847 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -25,166 +25,114 @@ namespace smt { class solver : public solver_na2as { smt_params m_params; - smt::kernel * m_context; + smt::kernel m_context; progress_callback * m_callback; + symbol m_logic; public: - solver():m_context(0), m_callback(0) {} - + solver(ast_manager & m, params_ref const & p, symbol const & l): + solver_na2as(m), + m_params(p), + m_context(m, m_params) { + m_logic = l; + if (m_logic != symbol::null) + m_context.set_logic(m_logic); + } + virtual ~solver() { - if (m_context != 0) - dealloc(m_context); } virtual void updt_params(params_ref const & p) { m_params.updt_params(p); - if (m_context == 0) - return; - m_context->updt_params(p); + m_context.updt_params(p); } virtual void collect_param_descrs(param_descrs & r) { - if (m_context == 0) { - ast_manager m; - reg_decl_plugins(m); - smt::kernel s(m, m_params); - s.collect_param_descrs(r); - } - else { - m_context->collect_param_descrs(r); - } - } - - virtual void init_core(ast_manager & m, symbol const & logic) { - reset(); - // We can throw exceptions when creating a smt::kernel object - // So, we should create the smt::kernel outside of the criticial section - // block. OMP does not allow exceptions to cross critical section boundaries. - smt::kernel * new_kernel = alloc(smt::kernel, m, m_params); - #pragma omp critical (solver) - { - m_context = new_kernel; - if (m_callback) - m_context->set_progress_callback(m_callback); - } - if (logic != symbol::null) - m_context->set_logic(logic); + m_context.collect_param_descrs(r); } virtual void collect_statistics(statistics & st) const { - if (m_context == 0) { - return; - } - else { - m_context->collect_statistics(st); - } - } - - virtual void reset_core() { - if (m_context != 0) { - #pragma omp critical (solver) - { - dealloc(m_context); - m_context = 0; - } - } - } - - // An exception may be thrown when creating a smt::kernel. - // So, there is no guarantee that m_context != 0 when - // using smt_solver from the SMT 2.0 command line frontend. - void check_context() const { - if (m_context == 0) - throw default_exception("Z3 failed to create solver, check previous error messages"); + m_context.collect_statistics(st); } virtual void assert_expr(expr * t) { - check_context(); - m_context->assert_expr(t); + m_context.assert_expr(t); } virtual void push_core() { - check_context(); - m_context->push(); + m_context.push(); } virtual void pop_core(unsigned n) { - check_context(); - m_context->pop(n); + m_context.pop(n); } virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) { - check_context(); TRACE("solver_na2as", tout << "smt_solver::check_sat_core: " << num_assumptions << "\n";); - return m_context->check(num_assumptions, assumptions); + return m_context.check(num_assumptions, assumptions); } virtual void get_unsat_core(ptr_vector & r) { - check_context(); - unsigned sz = m_context->get_unsat_core_size(); + 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)); + r.push_back(m_context.get_unsat_core_expr(i)); } virtual void get_model(model_ref & m) { - check_context(); - m_context->get_model(m); + m_context.get_model(m); } virtual proof * get_proof() { - check_context(); - return m_context->get_proof(); + return m_context.get_proof(); } virtual std::string reason_unknown() const { - check_context(); - return m_context->last_failure_as_string(); + return m_context.last_failure_as_string(); } virtual void get_labels(svector & r) { - check_context(); buffer tmp; - m_context->get_relevant_labels(0, 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); - } + 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); + m_context.set_progress_callback(callback); } virtual unsigned get_num_assertions() const { - if (m_context) - return m_context->size(); - else - return 0; + return m_context.size(); } virtual expr * get_assertion(unsigned idx) const { - SASSERT(m_context); SASSERT(idx < get_num_assertions()); - return m_context->get_formulas()[idx]; + return m_context.get_formulas()[idx]; } virtual void display(std::ostream & out) const { - if (m_context) - m_context->display(out); - else - out << "(solver)"; + m_context.display(out); } }; }; -solver * mk_smt_solver() { - return alloc(smt::solver); +solver * mk_smt_solver(ast_manager & m, params_ref const & p, symbol const & logic) { + return alloc(smt::solver, m, p, logic); } + +class smt_solver_factory : public solver_factory { +public: + virtual solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) { + return mk_smt_solver(m, p, logic); + } +}; + +solver_factory * mk_smt_solver_factory() { + return alloc(smt_solver_factory); +} + diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index e9af9aafa..81c9a1319 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -21,8 +21,13 @@ Notes: #ifndef _SMT_SOLVER_H_ #define _SMT_SOLVER_H_ -class solver; +#include"ast.h" +#include"params.h" -solver * mk_smt_solver(); +class solver; +class solver_factory; + +solver * mk_smt_solver(ast_manager & m, params_ref const & p, symbol const & logic); +solver_factory * mk_smt_solver_factory(); #endif diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp new file mode 100644 index 000000000..cd4191e76 --- /dev/null +++ b/src/solver/combined_solver.cpp @@ -0,0 +1,289 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + combined_solver.cpp + +Abstract: + + Implements the solver API by combining two solvers. + + This is a replacement for the strategic_solver class. + +Author: + + Leonardo (leonardo) 2012-12-11 + +Notes: + +--*/ +#include"solver.h" +#include"scoped_timer.h" +#include"combined_solver_params.hpp" +#define PS_VB_LVL 15 + +/** + \brief Implementation of the solver API that combines two given solvers. + + The combined solver has two modes: + - non-incremental + - incremental + In non-incremental mode, the first solver is used. + In incremental mode, the second one is used. + + A timeout for the second solver can be specified. + If the timeout is reached, then the first solver is executed. + + The object switches to incremental when: + - push is used + - assertions are peformed after a check_sat + - parameter ignore_solver1==false +*/ +class combined_solver : public solver { +public: + // Behavior when the incremental solver returns unknown. + enum inc_unknown_behavior { + IUB_RETURN_UNDEF, // just return unknown + IUB_USE_TACTIC_IF_QF, // invoke tactic if problem is quantifier free + IUB_USE_TACTIC // invoke tactic + }; + +private: + bool m_inc_mode; + bool m_check_sat_executed; + bool m_use_solver1_results; + ref m_solver1; + ref m_solver2; + + bool m_ignore_solver1; + inc_unknown_behavior m_inc_unknown_behavior; + unsigned m_inc_timeout; + + void switch_inc_mode() { + m_inc_mode = true; + } + + struct aux_timeout_eh : public event_handler { + solver * m_solver; + volatile bool m_canceled; + aux_timeout_eh(solver * s):m_solver(s), m_canceled(false) {} + virtual void operator()() { + m_solver->cancel(); + m_canceled = true; + } + }; + + void updt_local_params(params_ref const & _p) { + combined_solver_params p(_p); + m_inc_timeout = p.solver2_timeout(); + m_ignore_solver1 = p.ignore_solver1(); + m_inc_unknown_behavior = static_cast(p.solver2_unknown()); + } + + bool has_quantifiers() const { + unsigned sz = get_num_assertions(); + for (unsigned i = 0; i < sz; i++) { + if (::has_quantifiers(get_assertion(i))) + return true; + } + return false; + } + + bool use_solver1_when_undef() const { + switch (m_inc_unknown_behavior) { + case IUB_RETURN_UNDEF: return false; + case IUB_USE_TACTIC_IF_QF: return !has_quantifiers(); + case IUB_USE_TACTIC: return true; + default: + UNREACHABLE(); + return false; + } + } + +public: + combined_solver(solver * s1, solver * s2, params_ref const & p) { + m_solver1 = s1; + m_solver2 = s2; + updt_local_params(p); + m_inc_mode = false; + m_check_sat_executed = false; + m_use_solver1_results = true; + } + + virtual void updt_params(params_ref const & p) { + m_solver1->updt_params(p); + m_solver2->updt_params(p); + updt_local_params(p); + } + + virtual void collect_param_descrs(param_descrs & r) { + m_solver1->collect_param_descrs(r); + m_solver2->collect_param_descrs(r); + combined_solver_params::collect_param_descrs(r); + } + + virtual void set_produce_models(bool f) { + m_solver1->set_produce_models(f); + m_solver2->set_produce_models(f); + } + + virtual void assert_expr(expr * t) { + if (m_check_sat_executed) + switch_inc_mode(); + m_solver1->assert_expr(t); + m_solver2->assert_expr(t); + } + + virtual void assert_expr(expr * t, expr * a) { + if (m_check_sat_executed) + switch_inc_mode(); + m_solver1->assert_expr(t, a); + m_solver2->assert_expr(t, a); + } + + virtual void push() { + switch_inc_mode(); + m_solver1->push(); + m_solver2->push(); + } + + virtual void pop(unsigned n) { + switch_inc_mode(); + m_solver1->pop(n); + m_solver2->pop(n); + } + + virtual unsigned get_scope_level() const { + return m_solver1->get_scope_level(); + } + + virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) { + m_check_sat_executed = true; + + if (num_assumptions > 0 || // assumptions were provided + m_ignore_solver1) { + // must use incremental solver + switch_inc_mode(); + m_use_solver1_results = false; + return m_solver2->check_sat(num_assumptions, assumptions); + } + + if (m_inc_mode) { + if (m_inc_timeout == UINT_MAX) { + IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 2 (without a timeout)\")\n";); + lbool r = m_solver2->check_sat(0, 0); + if (r != l_undef || !use_solver1_when_undef()) { + m_use_solver1_results = false; + return r; + } + } + else { + IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 2 (with timeout)\")\n";); + aux_timeout_eh eh(m_solver2.get()); + lbool r; + { + scoped_timer timer(m_inc_timeout, &eh); + r = m_solver2->check_sat(0, 0); + } + if ((r != l_undef || !use_solver1_when_undef()) && !eh.m_canceled) { + m_use_solver1_results = false; + return r; + } + } + IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"solver 2 failed, trying solver1\")\n";); + } + + IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 1\")\n";); + m_use_solver1_results = true; + return m_solver1->check_sat(0, 0); + } + + virtual void set_cancel(bool f) { + m_solver1->set_cancel(f); + m_solver2->set_cancel(f); + } + + virtual void set_progress_callback(progress_callback * callback) { + m_solver1->set_progress_callback(callback); + m_solver2->set_progress_callback(callback); + } + + virtual unsigned get_num_assertions() const { + return m_solver1->get_num_assertions(); + } + + virtual expr * get_assertion(unsigned idx) const { + return m_solver1->get_assertion(idx); + } + + virtual void display(std::ostream & out) const { + m_solver1->display(out); + } + + virtual void collect_statistics(statistics & st) const { + if (m_use_solver1_results) + m_solver1->collect_statistics(st); + else + m_solver2->collect_statistics(st); + } + + virtual void get_unsat_core(ptr_vector & r) { + if (m_use_solver1_results) + m_solver1->get_unsat_core(r); + else + m_solver2->get_unsat_core(r); + } + + virtual void get_model(model_ref & m) { + if (m_use_solver1_results) + m_solver1->get_model(m); + else + m_solver2->get_model(m); + } + + virtual proof * get_proof() { + if (m_use_solver1_results) + return m_solver1->get_proof(); + else + return m_solver2->get_proof(); + } + + virtual std::string reason_unknown() const { + if (m_use_solver1_results) + return m_solver1->reason_unknown(); + else + return m_solver2->reason_unknown(); + } + + virtual void get_labels(svector & r) { + if (m_use_solver1_results) + return m_solver1->get_labels(r); + else + return m_solver2->get_labels(r); + } + +}; + + +solver * mk_combined_solver(solver * s1, solver * s2, params_ref const & p) { + return alloc(combined_solver, s1, s2, p); +} + +class combined_solver_factory : public solver_factory { + scoped_ptr m_f1; + scoped_ptr m_f2; +public: + combined_solver_factory(solver_factory * f1, solver_factory * f2):m_f1(f1), m_f2(f2) {} + virtual ~combined_solver_factory() {} + + virtual solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) { + return mk_combined_solver((*m_f1)(m, p, proofs_enabled, models_enabled, unsat_core_enabled, logic), + (*m_f2)(m, p, proofs_enabled, models_enabled, unsat_core_enabled, logic), + p); + } +}; + +solver_factory * mk_combined_solver_factory(solver_factory * f1, solver_factory * f2) { + return alloc(combined_solver_factory, f1, f2); +} diff --git a/src/solver/combined_solver.h b/src/solver/combined_solver.h new file mode 100644 index 000000000..2ccace7f0 --- /dev/null +++ b/src/solver/combined_solver.h @@ -0,0 +1,32 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + combined_solver.cpp + +Abstract: + + Implements the solver API by combining two solvers. + + This is a replacement for the strategic_solver class. + +Author: + + Leonardo (leonardo) 2012-12-11 + +Notes: + +--*/ +#ifndef _COMBINED_SOLVER_H_ +#define _COMBINED_SOLVER_H_ + +#include"params.h" + +class solver; +class solver_factory; + +solver * mk_combined_solver(solver * s1, solver * s2, params_ref const & p); +solver_factory * mk_combined_solver_factory(solver_factory * f1, solver_factory * f2); + +#endif diff --git a/src/solver/combined_solver_params.pyg b/src/solver/combined_solver_params.pyg new file mode 100644 index 000000000..7e1635c16 --- /dev/null +++ b/src/solver/combined_solver_params.pyg @@ -0,0 +1,9 @@ +def_module_params('combined_solver', + description='combines two solvers: non-incremental (solver1) and incremental (solver2)', + export=True, + params=(('solver2_timeout', UINT, UINT_MAX, "fallback to solver 1 after timeout even when in incremental model"), + ('ignore_solver1', BOOL, False, "if true, solver 2 is always used"), + ('solver2_unknown', UINT, 1, "what should be done when solver 2 returns unknown: 0 - just return unknown, 1 - execute solver 1 if quantifier free problem, 2 - execute solver 1") + )) + + diff --git a/src/solver/solver.h b/src/solver/solver.h index 5cd3da52b..e047bace1 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -23,6 +23,14 @@ Notes: #include"progress_callback.h" #include"params.h" +class solver; + +class solver_factory { +public: + virtual ~solver_factory() {} + virtual solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) = 0; +}; + /** \brief Abstract interface for making solvers available in the Z3 API and front-ends such as SMT 2.0 and (legacy) SMT 1.0. @@ -34,7 +42,6 @@ Notes: - statistics - results based on check_sat_result API - interruption (set_cancel) - - resets */ class solver : public check_sat_result { public: @@ -50,12 +57,6 @@ public: */ virtual void collect_param_descrs(param_descrs & r) {} - /** - \brief Enable/Disable proof production for this solver object. - - It is invoked before init(m, logic). - */ - virtual void set_produce_proofs(bool f) {} /** \brief Enable/Disable model generation for this solver object. @@ -63,23 +64,7 @@ public: The user may optionally invoke it after init(m, logic). */ virtual void set_produce_models(bool f) {} - /** - \brief Enable/Disable unsat core generation for this solver object. - - It is invoked before init(m, logic). - */ - virtual void set_produce_unsat_cores(bool f) {} - /** - \brief Initialize the solver object with the given ast_manager and logic. - */ - virtual void init(ast_manager & m, symbol const & logic) = 0; - - /** - \brief Reset the solver internal state. All assertions should be removed. - */ - virtual void reset() = 0; - /** \brief Add a new formula to the assertion stack. */ diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp index e71a9873b..9889b5872 100644 --- a/src/solver/solver_na2as.cpp +++ b/src/solver/solver_na2as.cpp @@ -22,8 +22,8 @@ Notes: #include"solver_na2as.h" #include"ast_smt2_pp.h" -solver_na2as::solver_na2as() { - m_manager = 0; +solver_na2as::solver_na2as(ast_manager & m): + m_manager(m) { } solver_na2as::~solver_na2as() { @@ -35,23 +35,16 @@ void solver_na2as::assert_expr(expr * t, expr * a) { assert_expr(t); } else { - 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); + 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); + 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; @@ -89,9 +82,9 @@ void solver_na2as::pop(unsigned n) { } void solver_na2as::restore_assumptions(unsigned old_sz) { - SASSERT(old_sz == 0 || m_manager != 0); + SASSERT(old_sz == 0); for (unsigned i = old_sz; i < m_assumptions.size(); i++) { - m_manager->dec_ref(m_assumptions[i]); + m_manager.dec_ref(m_assumptions[i]); } m_assumptions.shrink(old_sz); } @@ -100,7 +93,3 @@ 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 index eb12479fc..15750344a 100644 --- a/src/solver/solver_na2as.h +++ b/src/solver/solver_na2as.h @@ -25,30 +25,26 @@ Notes: #include"solver.h" class solver_na2as : public solver { - ast_manager * m_manager; + ast_manager & m_manager; ptr_vector m_assumptions; unsigned_vector m_scopes; void restore_assumptions(unsigned old_sz); public: - solver_na2as(); + solver_na2as(ast_manager & m); 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; }; diff --git a/src/solver/strategic_solver.cpp b/src/solver/strategic_solver.cpp index 40d77066e..fa7458ea3 100644 --- a/src/solver/strategic_solver.cpp +++ b/src/solver/strategic_solver.cpp @@ -16,6 +16,7 @@ Author: Notes: --*/ +#if 0 #include"strategic_solver.h" #include"scoped_timer.h" #include"ast_smt2_pp.h" @@ -526,6 +527,7 @@ void strategic_solver::display(std::ostream & out) const { } } +#endif diff --git a/src/solver/strategic_solver.h b/src/solver/strategic_solver.h index 1883a88cd..0bae8b254 100644 --- a/src/solver/strategic_solver.h +++ b/src/solver/strategic_solver.h @@ -61,7 +61,8 @@ private: bool m_force_tactic; // use tactics even when auto_config = false bool m_inc_mode; bool m_check_sat_executed; - scoped_ptr m_inc_solver; + scoped_ptr m_inc_solver_factory; + ref m_inc_solver; unsigned m_inc_solver_timeout; inc_unknown_behavior m_inc_unknown_behavior; scoped_ptr m_default_fct; @@ -107,12 +108,12 @@ private: bool use_tactic_when_undef() const; public: - strategic_solver(); + strategic_solver(ast_manager & m, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic); ~strategic_solver(); ast_manager & m() const { SASSERT(m_manager); return *m_manager; } - void set_inc_solver(solver * s); + void set_inc_solver_factory(solver_factory * s); void set_inc_solver_timeout(unsigned timeout); void set_default_tactic(tactic_factory * fct); void set_tactic_for(symbol const & logic, tactic_factory * fct); diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index e630f9c78..1268fbcea 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -19,96 +19,115 @@ Author: Notes: --*/ -#include"tactic2solver.h" +#include"solver_na2as.h" +#include"tactic.h" #include"ast_smt2_pp.h" -tactic2solver_core::ctx::ctx(ast_manager & m, symbol const & logic): - m_logic(logic), +/** + \brief Simulates the incremental solver interface using a tactic. + + Every query will be solved from scratch. So, this is not a good + option for applications trying to solve many easy queries that a + similar to each other. +*/ +class tactic2solver : public solver_na2as { + expr_ref_vector m_assertions; + unsigned_vector m_scopes; + ref m_result; + tactic_ref m_tactic; + symbol m_logic; + params_ref m_params; + bool m_produce_models; + bool m_produce_proofs; + bool m_produce_unsat_cores; +public: + tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic); + virtual ~tactic2solver(); + + virtual void updt_params(params_ref const & p); + virtual void collect_param_descrs(param_descrs & r); + + virtual void set_produce_models(bool f) { m_produce_models = f; } + + virtual void assert_expr(expr * t); + + 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); + + virtual void collect_statistics(statistics & st) const; + virtual void get_unsat_core(ptr_vector & r); + virtual void get_model(model_ref & m); + virtual proof * get_proof(); + virtual std::string reason_unknown() const; + virtual void get_labels(svector & r) {} + + virtual void set_progress_callback(progress_callback * callback) {} + + virtual unsigned get_num_assertions() const; + virtual expr * get_assertion(unsigned idx) const; + + virtual void display(std::ostream & out) const; +}; + +tactic2solver::tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic): + solver_na2as(m), m_assertions(m) { + + m_tactic = t; + m_logic = logic; + m_params = p; + + m_produce_models = produce_models; + m_produce_proofs = produce_proofs; + m_produce_unsat_cores = produce_unsat_cores; } -tactic2solver_core::~tactic2solver_core() { +tactic2solver::~tactic2solver() { } -void tactic2solver_core::init_core(ast_manager & m, symbol const & logic) { - m_ctx = alloc(ctx, m, logic); -} - -void tactic2solver_core::updt_params(params_ref const & p) { +void tactic2solver::updt_params(params_ref const & p) { m_params = p; } -void tactic2solver_core::collect_param_descrs(param_descrs & r) { - if (m_ctx) { - if (!m_ctx->m_tactic) { - #pragma omp critical (tactic2solver_core) - { - m_ctx->m_tactic = get_tactic(m_ctx->m(), m_params); - } - - if (m_ctx->m_tactic) { - m_ctx->m_tactic->collect_param_descrs(r); - } - - #pragma omp critical (tactic2solver_core) - { - m_ctx->m_tactic = 0; - } - } - else { - m_ctx->m_tactic->collect_param_descrs(r); - } - } +void tactic2solver::collect_param_descrs(param_descrs & r) { + if (m_tactic.get()) + m_tactic->collect_param_descrs(r); } -void tactic2solver_core::reset_core() { - SASSERT(m_ctx); - m_ctx->m_assertions.reset(); - m_ctx->m_scopes.reset(); - m_ctx->m_result = 0; +void tactic2solver::assert_expr(expr * t) { + m_assertions.push_back(t); + m_result = 0; } -void tactic2solver_core::assert_expr(expr * t) { - SASSERT(m_ctx); - m_ctx->m_assertions.push_back(t); - m_ctx->m_result = 0; +void tactic2solver::push_core() { + m_scopes.push_back(m_assertions.size()); + m_result = 0; } -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::pop_core(unsigned n) { + unsigned new_lvl = m_scopes.size() - n; + unsigned old_sz = m_scopes[new_lvl]; + m_assertions.shrink(old_sz); + m_scopes.shrink(new_lvl); + m_result = 0; } -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]; - m_ctx->m_assertions.shrink(old_sz); - m_ctx->m_scopes.shrink(new_lvl); - m_ctx->m_result = 0; -} - -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; - #pragma omp critical (tactic2solver_core) - { - m_ctx->m_tactic = get_tactic(m, p); - if (m_ctx->m_tactic) { - m_ctx->m_result = alloc(simple_check_sat_result, m); - } - } - if (!m_ctx->m_tactic) - return l_undef; - tactic & t = *(m_ctx->m_tactic); - simple_check_sat_result & result = *(m_ctx->m_result); +lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) { + if (m_tactic.get() == 0) + return l_false; + ast_manager & m = m_assertions.m(); + m_result = alloc(simple_check_sat_result, m); + m_tactic->cleanup(); + m_tactic->updt_params(m_params); + m_tactic->set_logic(m_logic); goal_ref g = alloc(goal, m, m_produce_proofs, m_produce_models, m_produce_unsat_cores); - t.set_logic(m_ctx->m_logic); - unsigned sz = m_ctx->m_assertions.size(); + + unsigned sz = m_assertions.size(); for (unsigned i = 0; i < sz; i++) { - g->assert_expr(m_ctx->m_assertions.get(i)); + g->assert_expr(m_assertions.get(i)); } for (unsigned i = 0; i < num_assumptions; i++) { g->assert_expr(assumptions[i], m.mk_asserted(assumptions[i]), m.mk_leaf(assumptions[i])); @@ -119,17 +138,17 @@ lbool tactic2solver_core::check_sat_core(unsigned num_assumptions, expr * const expr_dependency_ref core(m); std::string reason_unknown = "unknown"; try { - switch (::check_sat(t, g, md, pr, core, reason_unknown)) { + switch (::check_sat(*m_tactic, g, md, pr, core, reason_unknown)) { case l_true: - result.set_status(l_true); + m_result->set_status(l_true); break; case l_false: - result.set_status(l_false); + m_result->set_status(l_false); break; default: - result.set_status(l_undef); + m_result->set_status(l_undef); if (reason_unknown != "") - result.m_unknown = reason_unknown; + m_result->m_unknown = reason_unknown; break; } } @@ -137,112 +156,115 @@ lbool tactic2solver_core::check_sat_core(unsigned num_assumptions, expr * const throw ex; } catch (z3_exception & ex) { - TRACE("tactic2solver_core", tout << "exception: " << ex.msg() << "\n";); - result.set_status(l_undef); - result.m_unknown = ex.msg(); + TRACE("tactic2solver", tout << "exception: " << ex.msg() << "\n";); + m_result->set_status(l_undef); + m_result->m_unknown = ex.msg(); } - t.collect_statistics(result.m_stats); - result.m_model = md; - result.m_proof = pr; + m_tactic->collect_statistics(m_result->m_stats); + m_result->m_model = md; + m_result->m_proof = pr; if (m_produce_unsat_cores) { ptr_vector core_elems; m.linearize(core, core_elems); - result.m_core.append(core_elems.size(), core_elems.c_ptr()); + m_result->m_core.append(core_elems.size(), core_elems.c_ptr()); } - - #pragma omp critical (tactic2solver_core) - { - m_ctx->m_tactic = 0; - } - return result.status(); + m_tactic->cleanup(); + return m_result->status(); } -void tactic2solver_core::set_cancel(bool f) { - #pragma omp critical (tactic2solver_core) - { - if (m_ctx && m_ctx->m_tactic) - m_ctx->m_tactic->set_cancel(f); - } +void tactic2solver::set_cancel(bool f) { + if (m_tactic.get()) + m_tactic->set_cancel(f); } -void tactic2solver_core::collect_statistics(statistics & st) const { - if (m_ctx->m_result.get()) - m_ctx->m_result->collect_statistics(st); +void tactic2solver::collect_statistics(statistics & st) const { + if (m_result.get()) + m_result->collect_statistics(st); } -void tactic2solver_core::get_unsat_core(ptr_vector & r) { - if (m_ctx->m_result.get()) - m_ctx->m_result->get_unsat_core(r); +void tactic2solver::get_unsat_core(ptr_vector & r) { + if (m_result.get()) + m_result->get_unsat_core(r); } -void tactic2solver_core::get_model(model_ref & m) { - if (m_ctx->m_result.get()) - m_ctx->m_result->get_model(m); +void tactic2solver::get_model(model_ref & m) { + if (m_result.get()) + m_result->get_model(m); } -proof * tactic2solver_core::get_proof() { - if (m_ctx->m_result.get()) - return m_ctx->m_result->get_proof(); +proof * tactic2solver::get_proof() { + if (m_result.get()) + return m_result->get_proof(); else return 0; } -std::string tactic2solver_core::reason_unknown() const { - if (m_ctx->m_result.get()) - return m_ctx->m_result->reason_unknown(); +std::string tactic2solver::reason_unknown() const { + if (m_result.get()) + return m_result->reason_unknown(); else return std::string("unknown"); } -unsigned tactic2solver_core::get_num_assertions() const { - if (m_ctx) - return m_ctx->m_assertions.size(); - else - return 0; +unsigned tactic2solver::get_num_assertions() const { + return m_assertions.size(); } -expr * tactic2solver_core::get_assertion(unsigned idx) const { - SASSERT(m_ctx); - return m_ctx->m_assertions.get(idx); +expr * tactic2solver::get_assertion(unsigned idx) const { + return m_assertions.get(idx); } -void tactic2solver_core::display(std::ostream & out) const { - if (m_ctx) { - ast_manager & m = m_ctx->m_assertions.m(); - unsigned num = m_ctx->m_assertions.size(); - out << "(solver"; - for (unsigned i = 0; i < num; i++) { - out << "\n " << mk_ismt2_pp(m_ctx->m_assertions.get(i), m, 2); - } - out << ")"; +void tactic2solver::display(std::ostream & out) const { + ast_manager & m = m_assertions.m(); + unsigned num = m_assertions.size(); + out << "(solver"; + for (unsigned i = 0; i < num; i++) { + out << "\n " << mk_ismt2_pp(m_assertions.get(i), m, 2); } - else { - out << "(solver)"; + out << ")"; +} + +solver * mk_tactic2solver(ast_manager & m, + tactic * t, + params_ref const & p, + bool produce_proofs, + bool produce_models, + bool produce_unsat_cores, + symbol const & logic) { + return alloc(tactic2solver, m, t, p, produce_proofs, produce_models, produce_unsat_cores, logic); +} + +class tactic2solver_factory : public solver_factory { + ref m_tactic; +public: + tactic2solver_factory(tactic * t):m_tactic(t) { } + + virtual ~tactic2solver_factory() {} + + virtual solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) { + return mk_tactic2solver(m, m_tactic.get(), p, proofs_enabled, models_enabled, unsat_core_enabled, logic); + } +}; + +class tactic_factory2solver_factory : public solver_factory { + scoped_ptr m_factory; +public: + tactic_factory2solver_factory(tactic_factory * f):m_factory(f) { + } + + virtual ~tactic_factory2solver_factory() {} + + virtual solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) { + tactic * t = (*m_factory)(m, p); + return mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, logic); + } +}; + +solver_factory * mk_tactic2solver_factory(tactic * t) { + return alloc(tactic2solver_factory, t); } -tactic2solver::tactic2solver(tactic * t): - m_tactic(t) { -} - -tactic2solver::~tactic2solver() { -} - -tactic * tactic2solver::get_tactic(ast_manager & m, params_ref const & p) { - m_tactic->cleanup(); - m_tactic->updt_params(p); - return m_tactic.get(); -} - -tactic_factory2solver::~tactic_factory2solver() { -} - -void tactic_factory2solver::set_tactic(tactic_factory * f) { - m_tactic_factory = f; -} - -tactic * tactic_factory2solver::get_tactic(ast_manager & m, params_ref const & p) { - if (m_tactic_factory == 0) - return 0; - return (*m_tactic_factory)(m, p); +solver_factory * mk_tactic_factory2solver_factory(tactic_factory * f) { + return alloc(tactic_factory2solver_factory, f); } diff --git a/src/solver/tactic2solver.h b/src/solver/tactic2solver.h index 0a057b04b..f20b1c4dd 100644 --- a/src/solver/tactic2solver.h +++ b/src/solver/tactic2solver.h @@ -22,88 +22,22 @@ Notes: #ifndef _TACTIC2SOLVER_H_ #define _TACTIC2SOLVER_H_ -#include"solver_na2as.h" -#include"tactic.h" +#include"params.h" +class ast_manager; +class tactic; +class tactic_factory; +class solver; +class solver_factory; -/** - \brief Simulates the incremental solver interface using a tactic. - - Every query will be solved from scratch. So, this is not a good - option for applications trying to solve many easy queries that a - similar to each other. -*/ -class tactic2solver_core : public solver_na2as { - struct ctx { - symbol m_logic; - expr_ref_vector m_assertions; - unsigned_vector m_scopes; - ref m_result; - tactic_ref m_tactic; - ctx(ast_manager & m, symbol const & logic); - ast_manager & m() const { return m_assertions.m(); } - }; - scoped_ptr m_ctx; - params_ref m_params; - bool m_produce_models; - bool m_produce_proofs; - bool m_produce_unsat_cores; -public: - tactic2solver_core():m_ctx(0), m_produce_models(false), m_produce_proofs(false), m_produce_unsat_cores(false) {} - virtual ~tactic2solver_core(); - - virtual tactic * get_tactic(ast_manager & m, params_ref const & p) = 0; - - 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 assert_expr(expr * t); - - 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); - - virtual void collect_statistics(statistics & st) const; - virtual void get_unsat_core(ptr_vector & r); - virtual void get_model(model_ref & m); - virtual proof * get_proof(); - virtual std::string reason_unknown() const; - virtual void get_labels(svector & r) {} - - virtual void set_progress_callback(progress_callback * callback) {} - - virtual unsigned get_num_assertions() const; - virtual expr * get_assertion(unsigned idx) const; - - virtual void display(std::ostream & out) const; -}; - -class tactic2solver : public tactic2solver_core { - tactic_ref m_tactic; -public: - tactic2solver(tactic * t); - virtual ~tactic2solver(); - virtual tactic * get_tactic(ast_manager & m, params_ref const & p); -}; - - -class tactic_factory2solver : public tactic2solver_core { - scoped_ptr m_tactic_factory; -public: - virtual ~tactic_factory2solver(); - /** - \brief Set tactic that will be used to process the satisfiability queries. - */ - void set_tactic(tactic_factory * f); - virtual tactic * get_tactic(ast_manager & m, params_ref const & p); -}; +solver * mk_tactic2solver(ast_manager & m, + tactic * t = 0, + params_ref const & p = params_ref(), + bool produce_proofs = false, + bool produce_models = true, + bool produce_unsat_cores = false, + symbol const & logic = symbol::null); +solver_factory * mk_tactic2solver_factory(tactic * t); +solver_factory * mk_tactic_factory2solver_factory(tactic_factory * f); #endif diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 7a274a830..3d83d8815 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -18,7 +18,8 @@ Notes: --*/ #include"cmd_context.h" -#include"strategic_solver.h" +#include"combined_solver.h" +#include"tactic2solver.h" #include"qfbv_tactic.h" #include"qflia_tactic.h" #include"qfnia_tactic.h" @@ -36,57 +37,76 @@ Notes: #include"horn_tactic.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)); -MK_SIMPLE_TACTIC_FACTORY(qfauflia_fct, mk_qfauflia_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(auflia_fct, mk_auflia_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(auflira_fct, mk_auflira_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(aufnira_fct, mk_aufnira_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(ufnia_fct, mk_ufnia_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(uflra_fct, mk_uflra_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(lra_fct, mk_lra_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(qfbv_fct, mk_qfbv_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(default_fct, mk_default_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(qfaufbv_fct, mk_qfaufbv_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(qflra_fct, mk_qflra_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(qflia_fct, mk_qflia_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(qfufbv_fct, mk_qfufbv_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(qfnia_fct, mk_qfnia_tactic(m, p)); -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)); -MK_SIMPLE_TACTIC_FACTORY(horn_fct, mk_horn_tactic(m, p)); - -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)); - s->set_tactic_for(symbol("QF_IDL"), alloc(qfidl_fct)); - s->set_tactic_for(symbol("QF_LIA"), alloc(qflia_fct)); - s->set_tactic_for(symbol("QF_LRA"), alloc(qflra_fct)); - s->set_tactic_for(symbol("QF_NIA"), alloc(qfnia_fct)); - s->set_tactic_for(symbol("QF_NRA"), alloc(qfnra_fct)); - s->set_tactic_for(symbol("QF_AUFLIA"), alloc(qfauflia_fct)); - s->set_tactic_for(symbol("QF_AUFBV"), alloc(qfaufbv_fct)); - s->set_tactic_for(symbol("QF_ABV"), alloc(qfaufbv_fct)); - s->set_tactic_for(symbol("QF_UFBV"), alloc(qfufbv_fct)); - s->set_tactic_for(symbol("AUFLIA"), alloc(auflia_fct)); - s->set_tactic_for(symbol("AUFLIRA"), alloc(auflira_fct)); - s->set_tactic_for(symbol("AUFNIRA"), alloc(aufnira_fct)); - s->set_tactic_for(symbol("UFNIA"), alloc(ufnia_fct)); - s->set_tactic_for(symbol("UFLRA"), alloc(uflra_fct)); - s->set_tactic_for(symbol("LRA"), alloc(lra_fct)); - s->set_tactic_for(symbol("UFBV"), alloc(ufbv_fct)); - s->set_tactic_for(symbol("BV"), alloc(ufbv_fct)); - s->set_tactic_for(symbol("QF_FPA"), alloc(qffpa_fct)); - s->set_tactic_for(symbol("QF_FPABV"), alloc(qffpa_fct)); - s->set_tactic_for(symbol("HORN"), alloc(horn_fct)); +tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const & logic) { + if (logic=="QF_UF") + return mk_qfufbv_tactic(m, p); + else if (logic=="QF_BV") + return mk_qfbv_tactic(m, p); + else if (logic=="QF_IDL") + return mk_qfidl_tactic(m, p); + else if (logic=="QF_LIA") + return mk_qflia_tactic(m, p); + else if (logic=="QF_LRA") + return mk_qflra_tactic(m, p); + else if (logic=="QF_NIA") + return mk_qfnia_tactic(m, p); + else if (logic=="QF_NRA") + return mk_qfnra_tactic(m, p); + else if (logic=="QF_AUFLIA") + return mk_qfauflia_tactic(m, p); + else if (logic=="QF_AUFBV") + return mk_qfaufbv_tactic(m, p); + else if (logic=="QF_ABV") + return mk_qfaufbv_tactic(m, p); + else if (logic=="QF_UFBV") + return mk_qfufbv_tactic(m, p); + else if (logic=="AUFLIA") + return mk_auflia_tactic(m, p); + else if (logic=="AUFLIRA") + return mk_auflira_tactic(m, p); + else if (logic=="AUFNIRA") + return mk_aufnira_tactic(m, p); + else if (logic=="UFNIA") + return mk_ufnia_tactic(m, p); + else if (logic=="UFLRA") + return mk_uflra_tactic(m, p); + else if (logic=="LRA") + return mk_lra_tactic(m, p); + else if (logic=="UFBV") + return mk_ufbv_tactic(m, p); + else if (logic=="BV") + return mk_ufbv_tactic(m, p); + else if (logic=="QF_FPA") + return mk_qffpa_tactic(m, p); + else if (logic=="QF_FPABV") + return mk_qffpa_tactic(m, p); + else if (logic=="HORN") + return mk_horn_tactic(m, p); + else + return mk_default_tactic(m, p); } -solver * mk_smt_strategic_solver(bool force_tactic) { - strategic_solver * s = alloc(strategic_solver); - s->force_tactic(force_tactic); - s->set_inc_solver(mk_smt_solver()); - init(s); - return s; +class smt_strategic_solver_factory : public solver_factory { + symbol const & m_logic; +public: + smt_strategic_solver_factory(symbol const & logic):m_logic(logic) {} + + virtual ~smt_strategic_solver_factory() {} + + virtual solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) { + symbol l; + if (m_logic != symbol::null) + l = m_logic; + else + l = logic; + tactic * t = mk_tactic_for_logic(m, p, logic); + return mk_combined_solver(mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, l), + mk_smt_solver(m, p, l), + p); + } +}; + +solver_factory * mk_smt_strategic_solver_factory(symbol const & logic) { + return alloc(smt_strategic_solver_factory, logic); } + diff --git a/src/tactic/portfolio/smt_strategic_solver.h b/src/tactic/portfolio/smt_strategic_solver.h index 060721e09..1d132532a 100644 --- a/src/tactic/portfolio/smt_strategic_solver.h +++ b/src/tactic/portfolio/smt_strategic_solver.h @@ -20,8 +20,8 @@ Notes: #ifndef _SMT_STRATEGIC_SOLVER_H_ #define _SMT_STRATEGIC_SOLVER_H_ -class solver; -// Create a strategic solver for the Z3 API -solver * mk_smt_strategic_solver(bool force_tactic=false); +class solver_factory; + +solver_factory * mk_smt_strategic_solver_factory(symbol const & logic = symbol::null); #endif