From b70687acc9948becaf6e46d807a4931a449eb279 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 Nov 2012 16:35:08 -0700 Subject: [PATCH] cleanning solver initialization, and fixing named assertion support Signed-off-by: Leonardo de Moura --- src/api/api_solver.cpp | 55 ++-- src/api/api_solver.h | 5 +- src/cmd_context/basic_cmds.cpp | 4 +- src/cmd_context/cmd_context.cpp | 30 ++- src/cmd_context/cmd_context.h | 4 +- src/smt/smt_solver.cpp | 1 + src/solver/solver.h | 7 +- src/solver/strategic_solver.cpp | 236 +++++++++++------- src/solver/strategic_solver.h | 68 ++--- src/tactic/core/propagate_values_tactic.cpp | 1 + src/tactic/goal.cpp | 4 + src/tactic/goal.h | 6 +- src/tactic/portfolio/smt_strategic_solver.cpp | 2 +- 13 files changed, 268 insertions(+), 155 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 8aecc0a3a..6d1becb4d 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -33,14 +33,29 @@ 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); + 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_smt_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); @@ -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/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 532affef7..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); } @@ -1258,9 +1280,6 @@ 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); @@ -1405,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 73e212da1..34a3375d7 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -270,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; } diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 081649971..888e1b34c 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -107,6 +107,7 @@ namespace smt { 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); } diff --git a/src/solver/solver.h b/src/solver/solver.h index 4d244f5ef..6f9887c1a 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -64,19 +64,20 @@ public: /** \brief Enable/Disable proof production for this solver object. - It is invoked after init(m, logic). + It is invoked before init(m, logic). */ virtual void set_produce_proofs(bool f) {} /** \brief Enable/Disable model generation for this solver object. - It is invoked after 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) {} /** \brief Enable/Disable unsat core generation for this solver object. - It is invoked after init(m, logic). + It is invoked before init(m, logic). */ virtual void set_produce_unsat_cores(bool f) {} diff --git a/src/solver/strategic_solver.cpp b/src/solver/strategic_solver.cpp index 94414bcb1..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_core(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_core() { +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_core() { 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_core() { +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_core(unsigned n) { +void strategic_solver::pop(unsigned n) { DEBUG_CODE({ SASSERT(n <= m_num_scopes); m_num_scopes -= n; @@ -214,6 +295,20 @@ void strategic_solver_core::pop_core(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::get_scope_level() const { + if (m_ctx == 0) + return 0; + return m_ctx->m_assertions.size(); } struct aux_timeout_eh : public event_handler { @@ -226,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); @@ -252,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; @@ -268,15 +363,16 @@ lbool strategic_solver_core::check_sat_with_assumptions(unsigned num_assumptions } init_inc_solver(); m_use_inc_solver_results = true; - TRACE("solver_na2as", tout << "invoking inc_solver with " << num_assumptions << " assumptions\n";); + 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_core(unsigned num_assumptions, expr * const * assumptions) { - TRACE("solver_na2as", tout << "assumptions at strategic_solver_core:\n"; +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 @@ -331,10 +427,18 @@ lbool strategic_solver_core::check_sat_core(unsigned num_assumptions, expr * con 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); @@ -346,10 +450,14 @@ lbool strategic_solver_core::check_sat_core(unsigned num_assumptions, expr * con 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) @@ -359,15 +467,18 @@ void strategic_solver_core::set_cancel(bool f) { } } -void strategic_solver_core::get_unsat_core(ptr_vector & r) { - TRACE("solver_na2as", tout << "get_unsat_core, m_use_inc_solver_results: " << m_use_inc_solver_results << "\n";); +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); @@ -377,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(); @@ -387,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(); @@ -395,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"; @@ -423,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_core(ast_manager & m, symbol const & logic) { - strategic_solver_core::init_core(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_core() { - SASSERT(m_ctx); - strategic_solver_core::push_core(); - m_ctx->m_scopes.push_back(m_ctx->m_assertions.size()); -} - -void strategic_solver::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); - strategic_solver_core::pop_core(n); -} - -void strategic_solver::reset_core() { - m_ctx = 0; - strategic_solver_core::reset_core(); -} + diff --git a/src/solver/strategic_solver.h b/src/solver/strategic_solver.h index de4a7ff92..e903e9bd0 100644 --- a/src/solver/strategic_solver.h +++ b/src/solver/strategic_solver.h @@ -19,7 +19,7 @@ Notes: #ifndef _STRATEGIC_SOLVER_H_ #define _STRATEGIC_SOLVER_H_ -#include"solver_na2as.h" +#include"solver.h" #include"tactic.h" class progress_callback; @@ -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_na2as { +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,22 +123,25 @@ 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_core(ast_manager & m, symbol const & logic); + virtual void init(ast_manager & m, symbol const & logic); virtual void collect_statistics(statistics & st) const; - virtual void reset_core(); + virtual void reset(); 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 assert_expr(expr * t, expr * a); + 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 get_unsat_core(ptr_vector & r); virtual void get_model(model_ref & m); virtual proof * get_proof(); @@ -139,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_core(ast_manager & m, symbol const & logic); - - virtual void assert_expr(expr * t); - virtual void push_core(); - virtual void pop_core(unsigned n); - virtual void reset_core(); - - virtual unsigned get_num_assertions() const; - virtual expr * get_assertion(unsigned idx) const; -}; - - - #endif 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 ad259f843..c6dad42b2 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -233,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++) { diff --git a/src/tactic/goal.h b/src/tactic/goal.h index 2b7162b85..294987699 100644 --- a/src/tactic/goal.h +++ b/src/tactic/goal.h @@ -105,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); } diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index b958c42b9..50d972a0d 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -55,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));