From f1c9c9b7cd441effa16313b61f4b07bf0fe52b49 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 Nov 2012 12:15:45 -0700 Subject: [PATCH 01/17] resurrecting assertion_stack Signed-off-by: Leonardo de Moura --- src/ast/{macros => }/macro_substitution.cpp | 0 src/ast/{macros => }/macro_substitution.h | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename src/ast/{macros => }/macro_substitution.cpp (100%) rename src/ast/{macros => }/macro_substitution.h (100%) 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 From c9722a1313489bd355102ec242b39b904435946f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 Nov 2012 12:21:14 -0700 Subject: [PATCH 02/17] removing dead code Signed-off-by: Leonardo de Moura --- src/smt/asserted_formulas.cpp | 5 --- src/smt/asserted_formulas.h | 5 --- src/smt/smt_context.h | 6 ---- src/smt/user_rewriter.cpp | 24 --------------- src/smt/user_rewriter.h | 58 ----------------------------------- 5 files changed, 98 deletions(-) delete mode 100644 src/smt/user_rewriter.cpp delete mode 100644 src/smt/user_rewriter.h 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/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/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 From 26ffee95fc2b5b1c824bccca809370095bb1a872 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 Nov 2012 12:37:24 -0700 Subject: [PATCH 03/17] resurrecting assertion stack Signed-off-by: Leonardo de Moura --- src/ast/rewriter/expr_replacer.cpp | 9 + src/ast/rewriter/expr_replacer.h | 4 +- src/tactic/assertion_stack.cpp | 328 +++++++++++++++++++++++++++++ src/tactic/assertion_stack.h | 138 ++++++++++++ 4 files changed, 477 insertions(+), 2 deletions(-) create mode 100644 src/tactic/assertion_stack.cpp create mode 100644 src/tactic/assertion_stack.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/tactic/assertion_stack.cpp b/src/tactic/assertion_stack.cpp new file mode 100644 index 000000000..ac2fd31df --- /dev/null +++ b/src/tactic/assertion_stack.cpp @@ -0,0 +1,328 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + assertion_stack.cpp + +Abstract: + + Assertion stacks + +Author: + + Leonardo de Moura (leonardo) 2012-02-17 + +Revision History: + +--*/ +#include"assertion_stack.h" +#include"well_sorted.h" +#include"ast_smt2_pp.h" +#include"ref_util.h" +#include"expr_replacer.h" + +assertion_stack::assertion_stack(ast_manager & m, bool models_enabled, bool core_enabled): + m_manager(m), + m_forbidden(m), + m_csubst(m, core_enabled) { + init(m.proofs_enabled(), models_enabled, core_enabled); +} + +assertion_stack::assertion_stack(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled): + m_manager(m), + m_forbidden(m), + m_csubst(m, core_enabled, proofs_enabled) { + init(proofs_enabled, models_enabled, core_enabled); +} + +void assertion_stack::init(bool proofs_enabled, bool models_enabled, bool core_enabled) { + m_ref_count = 0; + m_models_enabled = models_enabled; + m_proofs_enabled = proofs_enabled; + m_core_enabled = core_enabled; + m_inconsistent = false; + m_form_qhead = 0; +} + +assertion_stack::~assertion_stack() { + reset(); +} + +void assertion_stack::reset() { + m_inconsistent = false; + m_form_qhead = 0; + m_mc_qhead = 0; + dec_ref_collection_values(m_manager, m_forms); + dec_ref_collection_values(m_manager, m_proofs); + dec_ref_collection_values(m_manager, m_deps); + dec_ref_collection_values(m_manager, m_forbidden); + m_forbidden_set.reset(); + dec_ref_collection_values(m_manager, m_mc); + m_mc_tag.reset(); + m_csubst.reset(); + m_scopes.reset(); +} + +void assertion_stack::expand(expr * f, proof * pr, expr_dependency * dep, expr_ref & new_f, proof_ref & new_pr, expr_dependency_ref & new_dep) { + scoped_ptr r = mk_default_expr_replacer(m()); + (*r)(f, new_f, new_pr, new_dep); + // new_pr is a proof for f == new_f + // new_dep are the dependencies for showing f == new_f + if (proofs_enabled()) { + new_pr = m_manager.mk_modus_ponens(pr, new_pr); + } + if (unsat_core_enabled()) { + new_dep = m().mk_join(dep, new_dep); + } +} + +void assertion_stack::push_back(expr * f, proof * pr, expr_dependency * d) { + if (m().is_true(f)) + return; + if (m().is_false(f)) { + m_inconsistent = true; + } + else { + SASSERT(!m_inconsistent); + } + m().inc_ref(f); + m_forms.push_back(f); + if (proofs_enabled()) { + m().inc_ref(pr); + m_proofs.push_back(pr); + } + if (unsat_core_enabled()) { + m().inc_ref(d); + m_deps.push_back(d); + } +} + +void assertion_stack::quick_process(bool save_first, expr * & f, expr_dependency * d) { + if (!m().is_and(f) && !(m().is_not(f) && m().is_or(to_app(f)->get_arg(0)))) { + if (!save_first) { + push_back(f, 0, d); + } + return; + } + typedef std::pair expr_pol; + sbuffer todo; + todo.push_back(expr_pol(f, true)); + while (!todo.empty()) { + if (m_inconsistent) + return; + expr_pol p = todo.back(); + expr * curr = p.first; + bool pol = p.second; + todo.pop_back(); + if (pol && m().is_and(curr)) { + app * t = to_app(curr); + unsigned i = t->get_num_args(); + while (i > 0) { + --i; + todo.push_back(expr_pol(t->get_arg(i), true)); + } + } + else if (!pol && m().is_or(curr)) { + app * t = to_app(curr); + unsigned i = t->get_num_args(); + while (i > 0) { + --i; + todo.push_back(expr_pol(t->get_arg(i), false)); + } + } + else if (m().is_not(curr)) { + todo.push_back(expr_pol(to_app(curr)->get_arg(0), !pol)); + } + else { + if (!pol) + curr = m().mk_not(curr); + if (save_first) { + f = curr; + save_first = false; + } + else { + push_back(curr, 0, d); + } + } + } +} + +void assertion_stack::process_and(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) { + unsigned num = f->get_num_args(); + for (unsigned i = 0; i < num; i++) { + if (m_inconsistent) + return; + slow_process(save_first && i == 0, f->get_arg(i), m().mk_and_elim(pr, i), d, out_f, out_pr); + } +} + +void assertion_stack::process_not_or(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) { + unsigned num = f->get_num_args(); + for (unsigned i = 0; i < num; i++) { + if (m_inconsistent) + return; + expr * child = f->get_arg(i); + if (m().is_not(child)) { + expr * not_child = to_app(child)->get_arg(0); + slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), d, out_f, out_pr); + } + else { + expr_ref not_child(m()); + not_child = m().mk_not(child); + slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), d, out_f, out_pr); + } + } +} + +void assertion_stack::slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) { + if (m().is_and(f)) + process_and(save_first, to_app(f), pr, d, out_f, out_pr); + else if (m().is_not(f) && m().is_or(to_app(f)->get_arg(0))) + process_not_or(save_first, to_app(to_app(f)->get_arg(0)), pr, d, out_f, out_pr); + else if (save_first) { + out_f = f; + out_pr = pr; + } + else { + push_back(f, pr, d); + } +} + +void assertion_stack::slow_process(expr * f, proof * pr, expr_dependency * d) { + expr_ref out_f(m()); + proof_ref out_pr(m()); + slow_process(false, f, pr, d, out_f, out_pr); +} + +void assertion_stack::assert_expr(expr * f, proof * pr, expr_dependency * d) { + SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr))); + if (m_inconsistent) + return; + expr_ref new_f(m()); proof_ref new_pr(m()); expr_dependency_ref new_d(m()); + expand(f, pr, d, new_f, new_pr, new_d); + if (proofs_enabled()) + slow_process(f, pr, d); + else + quick_process(false, f, d); +} + +#ifdef Z3DEBUG +// bool assertion_stack::is_expanded(expr * f) { +// } +#endif + +void assertion_stack::update(unsigned i, expr * f, proof * pr, expr_dependency * d) { + SASSERT(i >= m_form_qhead); + SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr))); + if (m_inconsistent) + return; + if (proofs_enabled()) { + expr_ref out_f(m()); + proof_ref out_pr(m()); + slow_process(true, f, pr, d, out_f, out_pr); + if (!m_inconsistent) { + if (m().is_false(out_f)) { + push_back(out_f, out_pr, d); + } + else { + m().inc_ref(out_f); + m().dec_ref(m_forms[i]); + m_forms[i] = out_f; + + m().inc_ref(out_pr); + m().dec_ref(m_proofs[i]); + m_proofs[i] = out_pr; + + if (unsat_core_enabled()) { + m().inc_ref(d); + m().dec_ref(m_deps[i]); + m_deps[i] = d; + } + } + } + } + else { + quick_process(true, f, d); + if (!m_inconsistent) { + if (m().is_false(f)) { + push_back(f, 0, d); + } + else { + m().inc_ref(f); + m().dec_ref(m_forms[i]); + m_forms[i] = f; + + if (unsat_core_enabled()) { + m().inc_ref(d); + m().dec_ref(m_deps[i]); + m_deps[i] = d; + } + } + } + } +} + +void assertion_stack::expand_and_update(unsigned i, expr * f, proof * pr, expr_dependency * d) { + SASSERT(i >= m_form_qhead); + SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr))); + if (m_inconsistent) + return; + expr_ref new_f(m()); proof_ref new_pr(m()); expr_dependency_ref new_d(m()); + expand(f, pr, d, new_f, new_pr, new_d); + update(i, new_f, new_pr, new_d); +} + +void assertion_stack::push() { + commit(); + m_scopes.push_back(scope()); + scope & s = m_scopes.back(); + s.m_forms_lim = m_forms.size(); + s.m_forbidden_lim = m_forbidden.size(); + s.m_mc_lim = m_mc.size(); + s.m_inconsistent_old = m_inconsistent; +} + +void assertion_stack::pop(unsigned num_scopes) { +} + +void assertion_stack::commit() { +} + +#define MC_TAG_EXTENSION 0 +#define MC_TAG_FILTER 1 + +void assertion_stack::add_filter(func_decl * f) { + m().inc_ref(f); + m_mc.push_back(f); + m_mc_tag.push_back(MC_TAG_FILTER); +} + +void assertion_stack::add_definition(app * c, expr * def, proof * pr, expr_dependency * dep) { + +} + +void assertion_stack::convert(model_ref & m) { +} + +void assertion_stack::display(std::ostream & out) const { + out << "(assertion-stack"; + unsigned sz = size(); + for (unsigned i = 0; i < sz; i++) { + out << "\n "; + if (i == m_form_qhead) + out << "==>\n"; + out << mk_ismt2_pp(form(i), m(), 2); + } + out << ")" << std::endl; +} + +bool assertion_stack::is_well_sorted() const { + unsigned sz = size(); + for (unsigned i = 0; i < sz; i++) { + expr * t = form(i); + if (!::is_well_sorted(m(), t)) + return false; + } + return true; +} diff --git a/src/tactic/assertion_stack.h b/src/tactic/assertion_stack.h new file mode 100644 index 000000000..e416c5743 --- /dev/null +++ b/src/tactic/assertion_stack.h @@ -0,0 +1,138 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + assertion_stack.h + +Abstract: + + It should be viewed as the "goal" object for incremental solvers. + The main difference is the support of push/pop operations. Like a + goal, an assertion_stack contains expressions, their proofs (if + proof generation is enabled), and dependencies (if unsat core + generation is enabled). + + The assertions on the stack are grouped by scope levels. Scoped + levels are created using push, and removed using pop. + + Assertions may be "committed". Whenever a push is executed, all + "uncommitted" assertions are automatically committed. + Only uncommitted assertions can be simplified/reduced. + + An assertion set has a limited model converter that only supports + definitions (for constant elimination) and filters (for fresh + symbols introduced by tactics). + + Some tactics support assertion_stacks and can be applied to them. + However, a tactic can only access the assertions on the top level. + The assertion stack also informs the tactic which declarations + can't be eliminated since they occur in the already committed part. + +Author: + + Leonardo de Moura (leonardo) 2012-02-17 + +Revision History: + +--*/ +#ifndef _ASSERTION_STACK_H_ +#define _ASSERTION_STACK_H_ + +#include"ast.h" +#include"model.h" +#include"expr_substitution.h" + +class assertion_stack { + ast_manager & m_manager; + unsigned m_ref_count; + bool m_models_enabled; // model generation is enabled. + bool m_proofs_enabled; // proof production is enabled. m_manager.proofs_enabled() must be true if m_proofs_enabled == true + bool m_core_enabled; // unsat core extraction is enabled. + bool m_inconsistent; + ptr_vector m_forms; + ptr_vector m_proofs; + ptr_vector m_deps; + unsigned m_form_qhead; // position of first uncommitted assertion + unsigned m_mc_qhead; + + // Set of declarations that can't be eliminated + obj_hashtable m_forbidden_set; + func_decl_ref_vector m_forbidden; + + // Limited model converter support, it supports only extensions and filters. + // It should be viewed as combination of extension_model_converter and + // filter_model_converter for goals. + expr_substitution m_csubst; // substitution for eliminated constants + + // Model converter is just two sequences: func_decl and tag. + // Tag 0 (extension) func_decl was eliminated, and its definition is in m_vsubst or m_fsubst. + // Tag 1 (filter) func_decl was introduced by tactic, and must be removed from model. + ptr_vector m_mc; + char_vector m_mc_tag; + + struct scope { + unsigned m_forms_lim; + unsigned m_forbidden_lim; + unsigned m_mc_lim; + bool m_inconsistent_old; + }; + + svector m_scopes; + + void init(bool proofs_enabled, bool models_enabled, bool core_enabled); + void expand(expr * f, proof * pr, expr_dependency * dep, expr_ref & new_f, proof_ref & new_pr, expr_dependency_ref & new_dep); + void push_back(expr * f, proof * pr, expr_dependency * d); + void quick_process(bool save_first, expr * & f, expr_dependency * d); + void process_and(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr); + void process_not_or(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr); + void slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr); + void slow_process(expr * f, proof * pr, expr_dependency * d); + +public: + assertion_stack(ast_manager & m, bool models_enabled = true, bool core_enabled = true); + assertion_stack(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled); + ~assertion_stack(); + + void reset(); + + void inc_ref() { ++m_ref_count; } + void dec_ref() { --m_ref_count; if (m_ref_count == 0) dealloc(this); } + + ast_manager & m() const { return m_manager; } + + bool models_enabled() const { return m_models_enabled; } + bool proofs_enabled() const { return m_proofs_enabled; } + bool unsat_core_enabled() const { return m_core_enabled; } + bool inconsistent() const { return m_inconsistent; } + + unsigned size() const { return m_forms.size(); } + unsigned qhead() const { return m_form_qhead; } + expr * form(unsigned i) const { return m_forms[i]; } + proof * pr(unsigned i) const { return proofs_enabled() ? static_cast(m_proofs[i]) : 0; } + expr_dependency * dep(unsigned i) const { return unsat_core_enabled() ? m_deps[i] : 0; } + + 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 update(unsigned i, expr * f, proof * pr = 0, expr_dependency * dep = 0); + void expand_and_update(unsigned i, expr * f, proof * pr = 0, expr_dependency * d = 0); + + void commit(); + void push(); + void pop(unsigned num_scopes); + unsigned scope_lvl() const { return m_scopes.size(); } + + bool is_well_sorted() const; + + bool is_forbidden(func_decl * f) const { return m_forbidden_set.contains(f); } + void add_filter(func_decl * f); + void add_definition(app * c, expr * def, proof * pr, expr_dependency * dep); + + void convert(model_ref & m); + + void display(std::ostream & out) const; +}; + +#endif From ef0ee9a0c4e9578475c18165c5ee5d93153b9751 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 Nov 2012 12:47:24 -0700 Subject: [PATCH 04/17] code reorg Signed-off-by: Leonardo de Moura --- src/tactic/goal.cpp | 80 ++++++++++++++++++++++++++++++++++++++++++ src/tactic/goal.h | 84 ++++++--------------------------------------- 2 files changed, 91 insertions(+), 73 deletions(-) diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index 6897097be..ad259f843 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) @@ -570,6 +629,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..2b7162b85 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); } @@ -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; From c096fb534b222e7f7c9addb2376168d3fa4b4262 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 Nov 2012 13:28:10 -0700 Subject: [PATCH 05/17] checkpoint Signed-off-by: Leonardo de Moura --- src/ast/expr_substitution.cpp | 4 + src/ast/expr_substitution.h | 1 + src/tactic/assertion_stack.cpp | 700 +++++++++++++++++++++------------ src/tactic/assertion_stack.h | 80 +--- 4 files changed, 465 insertions(+), 320 deletions(-) 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/tactic/assertion_stack.cpp b/src/tactic/assertion_stack.cpp index ac2fd31df..03631f0d4 100644 --- a/src/tactic/assertion_stack.cpp +++ b/src/tactic/assertion_stack.cpp @@ -21,308 +21,498 @@ Revision History: #include"ast_smt2_pp.h" #include"ref_util.h" #include"expr_replacer.h" +#include"model.h" +#include"expr_substitution.h" -assertion_stack::assertion_stack(ast_manager & m, bool models_enabled, bool core_enabled): - m_manager(m), - m_forbidden(m), - m_csubst(m, core_enabled) { - init(m.proofs_enabled(), models_enabled, core_enabled); +struct assertion_stack::imp { + ast_manager & m_manager; + bool m_models_enabled; // model generation is enabled. + bool m_proofs_enabled; // proof production is enabled. m_manager.proofs_enabled() must be true if m_proofs_enabled == true + bool m_core_enabled; // unsat core extraction is enabled. + bool m_inconsistent; + ptr_vector m_forms; + ptr_vector m_proofs; + ptr_vector m_deps; + unsigned m_form_qhead; // position of first uncommitted assertion + unsigned m_mc_qhead; + + // Set of declarations that can't be eliminated + obj_hashtable m_forbidden_set; + func_decl_ref_vector m_forbidden; + + // Limited model converter support, it supports only extensions and filters. + // It should be viewed as combination of extension_model_converter and + // filter_model_converter for goals. + expr_substitution m_csubst; // substitution for eliminated constants + + // Model converter is just two sequences: func_decl and tag. + // Tag 0 (extension) func_decl was eliminated, and its definition is in m_vsubst or m_fsubst. + // Tag 1 (filter) func_decl was introduced by tactic, and must be removed from model. + ptr_vector m_mc; + char_vector m_mc_tag; + + struct scope { + unsigned m_forms_lim; + unsigned m_forbidden_lim; + unsigned m_mc_lim; + bool m_inconsistent_old; + }; + + svector m_scopes; + + imp(ast_manager & m, bool models_enabled, bool core_enabled): + m_manager(m), + m_forbidden(m), + m_csubst(m, core_enabled) { + init(m.proofs_enabled(), models_enabled, core_enabled); + } + + imp(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled): + m_manager(m), + m_forbidden(m), + m_csubst(m, core_enabled, proofs_enabled) { + init(proofs_enabled, models_enabled, core_enabled); + } + + void init(bool proofs_enabled, bool models_enabled, bool core_enabled) { + m_models_enabled = models_enabled; + m_proofs_enabled = proofs_enabled; + m_core_enabled = core_enabled; + m_inconsistent = false; + m_form_qhead = 0; + } + + ~imp() { + reset(); + } + + ast_manager & m() const { return m_manager; } + + bool models_enabled() const { return m_models_enabled; } + + bool proofs_enabled() const { return m_proofs_enabled; } + + bool unsat_core_enabled() const { return m_core_enabled; } + + bool inconsistent() const { return m_inconsistent; } + + unsigned size() const { return m_forms.size(); } + + unsigned qhead() const { return m_form_qhead; } + + expr * form(unsigned i) const { return m_forms[i]; } + + proof * pr(unsigned i) const { + if (proofs_enabled()) + return m_proofs[i]; + else + return 0; + } + + expr_dependency * dep(unsigned i) const { + if (unsat_core_enabled()) + return m_deps[i]; + else + return 0; + } + + void reset() { + m_inconsistent = false; + m_form_qhead = 0; + m_mc_qhead = 0; + dec_ref_collection_values(m_manager, m_forms); + dec_ref_collection_values(m_manager, m_proofs); + dec_ref_collection_values(m_manager, m_deps); + dec_ref_collection_values(m_manager, m_forbidden); + m_forbidden_set.reset(); + dec_ref_collection_values(m_manager, m_mc); + m_mc_tag.reset(); + m_csubst.reset(); + m_scopes.reset(); + } + + void expand(expr * f, proof * pr, expr_dependency * dep, expr_ref & new_f, proof_ref & new_pr, expr_dependency_ref & new_dep) { + scoped_ptr r = mk_default_expr_replacer(m()); + (*r)(f, new_f, new_pr, new_dep); + // new_pr is a proof for f == new_f + // new_dep are the dependencies for showing f == new_f + if (proofs_enabled()) { + new_pr = m_manager.mk_modus_ponens(pr, new_pr); + } + if (unsat_core_enabled()) { + new_dep = m().mk_join(dep, new_dep); + } + } + + void push_back(expr * f, proof * pr, expr_dependency * d) { + if (m().is_true(f)) + return; + if (m().is_false(f)) { + m_inconsistent = true; + } + else { + SASSERT(!m_inconsistent); + } + m().inc_ref(f); + m_forms.push_back(f); + if (proofs_enabled()) { + m().inc_ref(pr); + m_proofs.push_back(pr); + } + if (unsat_core_enabled()) { + m().inc_ref(d); + m_deps.push_back(d); + } + } + + void quick_process(bool save_first, expr * & f, expr_dependency * d) { + if (!m().is_and(f) && !(m().is_not(f) && m().is_or(to_app(f)->get_arg(0)))) { + if (!save_first) { + push_back(f, 0, d); + } + return; + } + typedef std::pair expr_pol; + sbuffer todo; + todo.push_back(expr_pol(f, true)); + while (!todo.empty()) { + if (m_inconsistent) + return; + expr_pol p = todo.back(); + expr * curr = p.first; + bool pol = p.second; + todo.pop_back(); + if (pol && m().is_and(curr)) { + app * t = to_app(curr); + unsigned i = t->get_num_args(); + while (i > 0) { + --i; + todo.push_back(expr_pol(t->get_arg(i), true)); + } + } + else if (!pol && m().is_or(curr)) { + app * t = to_app(curr); + unsigned i = t->get_num_args(); + while (i > 0) { + --i; + todo.push_back(expr_pol(t->get_arg(i), false)); + } + } + else if (m().is_not(curr)) { + todo.push_back(expr_pol(to_app(curr)->get_arg(0), !pol)); + } + else { + if (!pol) + curr = m().mk_not(curr); + if (save_first) { + f = curr; + save_first = false; + } + else { + push_back(curr, 0, d); + } + } + } + } + + void process_and(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) { + unsigned num = f->get_num_args(); + for (unsigned i = 0; i < num; i++) { + if (m_inconsistent) + return; + slow_process(save_first && i == 0, f->get_arg(i), m().mk_and_elim(pr, i), d, out_f, out_pr); + } + } + + void process_not_or(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) { + unsigned num = f->get_num_args(); + for (unsigned i = 0; i < num; i++) { + if (m_inconsistent) + return; + expr * child = f->get_arg(i); + if (m().is_not(child)) { + expr * not_child = to_app(child)->get_arg(0); + slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), d, out_f, out_pr); + } + else { + expr_ref not_child(m()); + not_child = m().mk_not(child); + slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), d, out_f, out_pr); + } + } + } + + void slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) { + if (m().is_and(f)) + process_and(save_first, to_app(f), pr, d, out_f, out_pr); + else if (m().is_not(f) && m().is_or(to_app(f)->get_arg(0))) + process_not_or(save_first, to_app(to_app(f)->get_arg(0)), pr, d, out_f, out_pr); + else if (save_first) { + out_f = f; + out_pr = pr; + } + else { + push_back(f, pr, d); + } + } + + void slow_process(expr * f, proof * pr, expr_dependency * d) { + expr_ref out_f(m()); + proof_ref out_pr(m()); + slow_process(false, f, pr, d, out_f, out_pr); + } + + void assert_expr(expr * f, proof * pr, expr_dependency * d) { + SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr))); + if (m_inconsistent) + return; + expr_ref new_f(m()); proof_ref new_pr(m()); expr_dependency_ref new_d(m()); + expand(f, pr, d, new_f, new_pr, new_d); + if (proofs_enabled()) + slow_process(f, pr, d); + else + quick_process(false, f, d); + } + + void update(unsigned i, expr * f, proof * pr, expr_dependency * d) { + SASSERT(i >= m_form_qhead); + SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr))); + if (m_inconsistent) + return; + if (proofs_enabled()) { + expr_ref out_f(m()); + proof_ref out_pr(m()); + slow_process(true, f, pr, d, out_f, out_pr); + if (!m_inconsistent) { + if (m().is_false(out_f)) { + push_back(out_f, out_pr, d); + } + else { + m().inc_ref(out_f); + m().dec_ref(m_forms[i]); + m_forms[i] = out_f; + + m().inc_ref(out_pr); + m().dec_ref(m_proofs[i]); + m_proofs[i] = out_pr; + + if (unsat_core_enabled()) { + m().inc_ref(d); + m().dec_ref(m_deps[i]); + m_deps[i] = d; + } + } + } + } + else { + quick_process(true, f, d); + if (!m_inconsistent) { + if (m().is_false(f)) { + push_back(f, 0, d); + } + else { + m().inc_ref(f); + m().dec_ref(m_forms[i]); + m_forms[i] = f; + + if (unsat_core_enabled()) { + m().inc_ref(d); + m().dec_ref(m_deps[i]); + m_deps[i] = d; + } + } + } + } + } + + void expand_and_update(unsigned i, expr * f, proof * pr, expr_dependency * d) { + SASSERT(i >= m_form_qhead); + SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr))); + if (m_inconsistent) + return; + expr_ref new_f(m()); proof_ref new_pr(m()); expr_dependency_ref new_d(m()); + expand(f, pr, d, new_f, new_pr, new_d); + update(i, new_f, new_pr, new_d); + } + + void push() { + commit(); + m_scopes.push_back(scope()); + scope & s = m_scopes.back(); + s.m_forms_lim = m_forms.size(); + s.m_forbidden_lim = m_forbidden.size(); + s.m_mc_lim = m_mc.size(); + s.m_inconsistent_old = m_inconsistent; + } + + void pop(unsigned num_scopes) { + } + + void commit() { + } + + unsigned scope_lvl() const { + return m_scopes.size(); + } + + bool is_forbidden(func_decl * f) const { + return m_forbidden_set.contains(f); + } + +#define MC_TAG_EXTENSION 0 +#define MC_TAG_FILTER 1 + + void add_filter(func_decl * f) { + m().inc_ref(f); + m_mc.push_back(f); + m_mc_tag.push_back(MC_TAG_FILTER); + } + + void add_definition(app * c, expr * def, proof * pr, expr_dependency * dep) { + SASSERT(c->get_num_args() == 0); + SASSERT(!m_csubst.contains(c)); + m_csubst.insert(c, def, pr, dep); + func_decl * d = c->get_decl(); + m().inc_ref(d); + m_mc.push_back(d); + m_mc_tag.push_back(MC_TAG_EXTENSION); + } + + void convert(model_ref & m) { + } + + void display(std::ostream & out) const { + out << "(assertion-stack"; + unsigned sz = size(); + for (unsigned i = 0; i < sz; i++) { + out << "\n "; + if (i == m_form_qhead) + out << "==>\n"; + out << mk_ismt2_pp(form(i), m(), 2); + } + out << ")" << std::endl; + } + + bool is_well_sorted() const { + unsigned sz = size(); + for (unsigned i = 0; i < sz; i++) { + expr * t = form(i); + if (!::is_well_sorted(m(), t)) + return false; + } + return true; + } +}; + +assertion_stack::assertion_stack(ast_manager & m, bool models_enabled, bool core_enabled) { + m_imp = alloc(imp, m, models_enabled, core_enabled); } -assertion_stack::assertion_stack(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled): - m_manager(m), - m_forbidden(m), - m_csubst(m, core_enabled, proofs_enabled) { - init(proofs_enabled, models_enabled, core_enabled); -} - -void assertion_stack::init(bool proofs_enabled, bool models_enabled, bool core_enabled) { - m_ref_count = 0; - m_models_enabled = models_enabled; - m_proofs_enabled = proofs_enabled; - m_core_enabled = core_enabled; - m_inconsistent = false; - m_form_qhead = 0; +assertion_stack::assertion_stack(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled) { + m_imp = alloc(imp, m, proofs_enabled, models_enabled, core_enabled); } assertion_stack::~assertion_stack() { - reset(); + dealloc(m_imp); } void assertion_stack::reset() { - m_inconsistent = false; - m_form_qhead = 0; - m_mc_qhead = 0; - dec_ref_collection_values(m_manager, m_forms); - dec_ref_collection_values(m_manager, m_proofs); - dec_ref_collection_values(m_manager, m_deps); - dec_ref_collection_values(m_manager, m_forbidden); - m_forbidden_set.reset(); - dec_ref_collection_values(m_manager, m_mc); - m_mc_tag.reset(); - m_csubst.reset(); - m_scopes.reset(); + m_imp->reset(); } -void assertion_stack::expand(expr * f, proof * pr, expr_dependency * dep, expr_ref & new_f, proof_ref & new_pr, expr_dependency_ref & new_dep) { - scoped_ptr r = mk_default_expr_replacer(m()); - (*r)(f, new_f, new_pr, new_dep); - // new_pr is a proof for f == new_f - // new_dep are the dependencies for showing f == new_f - if (proofs_enabled()) { - new_pr = m_manager.mk_modus_ponens(pr, new_pr); - } - if (unsat_core_enabled()) { - new_dep = m().mk_join(dep, new_dep); - } +ast_manager & assertion_stack::m() const { + return m_imp->m(); } -void assertion_stack::push_back(expr * f, proof * pr, expr_dependency * d) { - if (m().is_true(f)) - return; - if (m().is_false(f)) { - m_inconsistent = true; - } - else { - SASSERT(!m_inconsistent); - } - m().inc_ref(f); - m_forms.push_back(f); - if (proofs_enabled()) { - m().inc_ref(pr); - m_proofs.push_back(pr); - } - if (unsat_core_enabled()) { - m().inc_ref(d); - m_deps.push_back(d); - } +bool assertion_stack::models_enabled() const { + return m_imp->models_enabled(); } -void assertion_stack::quick_process(bool save_first, expr * & f, expr_dependency * d) { - if (!m().is_and(f) && !(m().is_not(f) && m().is_or(to_app(f)->get_arg(0)))) { - if (!save_first) { - push_back(f, 0, d); - } - return; - } - typedef std::pair expr_pol; - sbuffer todo; - todo.push_back(expr_pol(f, true)); - while (!todo.empty()) { - if (m_inconsistent) - return; - expr_pol p = todo.back(); - expr * curr = p.first; - bool pol = p.second; - todo.pop_back(); - if (pol && m().is_and(curr)) { - app * t = to_app(curr); - unsigned i = t->get_num_args(); - while (i > 0) { - --i; - todo.push_back(expr_pol(t->get_arg(i), true)); - } - } - else if (!pol && m().is_or(curr)) { - app * t = to_app(curr); - unsigned i = t->get_num_args(); - while (i > 0) { - --i; - todo.push_back(expr_pol(t->get_arg(i), false)); - } - } - else if (m().is_not(curr)) { - todo.push_back(expr_pol(to_app(curr)->get_arg(0), !pol)); - } - else { - if (!pol) - curr = m().mk_not(curr); - if (save_first) { - f = curr; - save_first = false; - } - else { - push_back(curr, 0, d); - } - } - } +bool assertion_stack::proofs_enabled() const { + return m_imp->proofs_enabled(); } -void assertion_stack::process_and(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) { - unsigned num = f->get_num_args(); - for (unsigned i = 0; i < num; i++) { - if (m_inconsistent) - return; - slow_process(save_first && i == 0, f->get_arg(i), m().mk_and_elim(pr, i), d, out_f, out_pr); - } +bool assertion_stack::unsat_core_enabled() const { + return m_imp->unsat_core_enabled(); } -void assertion_stack::process_not_or(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) { - unsigned num = f->get_num_args(); - for (unsigned i = 0; i < num; i++) { - if (m_inconsistent) - return; - expr * child = f->get_arg(i); - if (m().is_not(child)) { - expr * not_child = to_app(child)->get_arg(0); - slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), d, out_f, out_pr); - } - else { - expr_ref not_child(m()); - not_child = m().mk_not(child); - slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), d, out_f, out_pr); - } - } +bool assertion_stack::inconsistent() const { + return m_imp->inconsistent(); } -void assertion_stack::slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) { - if (m().is_and(f)) - process_and(save_first, to_app(f), pr, d, out_f, out_pr); - else if (m().is_not(f) && m().is_or(to_app(f)->get_arg(0))) - process_not_or(save_first, to_app(to_app(f)->get_arg(0)), pr, d, out_f, out_pr); - else if (save_first) { - out_f = f; - out_pr = pr; - } - else { - push_back(f, pr, d); - } +unsigned assertion_stack::size() const { + return m_imp->size(); } -void assertion_stack::slow_process(expr * f, proof * pr, expr_dependency * d) { - expr_ref out_f(m()); - proof_ref out_pr(m()); - slow_process(false, f, pr, d, out_f, out_pr); +unsigned assertion_stack::qhead() const { + return m_imp->qhead(); +} + +expr * assertion_stack::form(unsigned i) const { + return m_imp->form(i); +} + +proof * assertion_stack::pr(unsigned i) const { + return m_imp->pr(i); +} + +expr_dependency * assertion_stack::dep(unsigned i) const { + return m_imp->dep(i); } void assertion_stack::assert_expr(expr * f, proof * pr, expr_dependency * d) { - SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr))); - if (m_inconsistent) - return; - expr_ref new_f(m()); proof_ref new_pr(m()); expr_dependency_ref new_d(m()); - expand(f, pr, d, new_f, new_pr, new_d); - if (proofs_enabled()) - slow_process(f, pr, d); - else - quick_process(false, f, d); + return m_imp->assert_expr(f, pr, d); } -#ifdef Z3DEBUG -// bool assertion_stack::is_expanded(expr * f) { -// } -#endif +void assertion_stack::assert_expr(expr * f) { + assert_expr(f, proofs_enabled() ? m().mk_asserted(f) : 0, 0); +} void assertion_stack::update(unsigned i, expr * f, proof * pr, expr_dependency * d) { - SASSERT(i >= m_form_qhead); - SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr))); - if (m_inconsistent) - return; - if (proofs_enabled()) { - expr_ref out_f(m()); - proof_ref out_pr(m()); - slow_process(true, f, pr, d, out_f, out_pr); - if (!m_inconsistent) { - if (m().is_false(out_f)) { - push_back(out_f, out_pr, d); - } - else { - m().inc_ref(out_f); - m().dec_ref(m_forms[i]); - m_forms[i] = out_f; - - m().inc_ref(out_pr); - m().dec_ref(m_proofs[i]); - m_proofs[i] = out_pr; - - if (unsat_core_enabled()) { - m().inc_ref(d); - m().dec_ref(m_deps[i]); - m_deps[i] = d; - } - } - } - } - else { - quick_process(true, f, d); - if (!m_inconsistent) { - if (m().is_false(f)) { - push_back(f, 0, d); - } - else { - m().inc_ref(f); - m().dec_ref(m_forms[i]); - m_forms[i] = f; - - if (unsat_core_enabled()) { - m().inc_ref(d); - m().dec_ref(m_deps[i]); - m_deps[i] = d; - } - } - } - } + m_imp->update(i, f, pr, d); } void assertion_stack::expand_and_update(unsigned i, expr * f, proof * pr, expr_dependency * d) { - SASSERT(i >= m_form_qhead); - SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr))); - if (m_inconsistent) - return; - expr_ref new_f(m()); proof_ref new_pr(m()); expr_dependency_ref new_d(m()); - expand(f, pr, d, new_f, new_pr, new_d); - update(i, new_f, new_pr, new_d); -} - -void assertion_stack::push() { - commit(); - m_scopes.push_back(scope()); - scope & s = m_scopes.back(); - s.m_forms_lim = m_forms.size(); - s.m_forbidden_lim = m_forbidden.size(); - s.m_mc_lim = m_mc.size(); - s.m_inconsistent_old = m_inconsistent; -} - -void assertion_stack::pop(unsigned num_scopes) { + m_imp->expand_and_update(i, f, pr, d); } void assertion_stack::commit() { + m_imp->commit(); } -#define MC_TAG_EXTENSION 0 -#define MC_TAG_FILTER 1 +void assertion_stack::push() { + m_imp->push(); +} + +void assertion_stack::pop(unsigned num_scopes) { + m_imp->pop(num_scopes); +} + +unsigned assertion_stack::scope_lvl() const { + return m_imp->scope_lvl(); +} + +bool assertion_stack::is_well_sorted() const { + return m_imp->is_well_sorted(); +} + + +bool assertion_stack::is_forbidden(func_decl * f) const { + return m_imp->is_forbidden(f); +} void assertion_stack::add_filter(func_decl * f) { - m().inc_ref(f); - m_mc.push_back(f); - m_mc_tag.push_back(MC_TAG_FILTER); + m_imp->add_filter(f); } void assertion_stack::add_definition(app * c, expr * def, proof * pr, expr_dependency * dep) { - + m_imp->add_definition(c, def, pr, dep); } void assertion_stack::convert(model_ref & m) { + m_imp->convert(m); } void assertion_stack::display(std::ostream & out) const { - out << "(assertion-stack"; - unsigned sz = size(); - for (unsigned i = 0; i < sz; i++) { - out << "\n "; - if (i == m_form_qhead) - out << "==>\n"; - out << mk_ismt2_pp(form(i), m(), 2); - } - out << ")" << std::endl; -} - -bool assertion_stack::is_well_sorted() const { - unsigned sz = size(); - for (unsigned i = 0; i < sz; i++) { - expr * t = form(i); - if (!::is_well_sorted(m(), t)) - return false; - } - return true; + m_imp->display(out); } diff --git a/src/tactic/assertion_stack.h b/src/tactic/assertion_stack.h index e416c5743..d6bb195e9 100644 --- a/src/tactic/assertion_stack.h +++ b/src/tactic/assertion_stack.h @@ -41,97 +41,47 @@ Revision History: #include"ast.h" #include"model.h" -#include"expr_substitution.h" class assertion_stack { - ast_manager & m_manager; - unsigned m_ref_count; - bool m_models_enabled; // model generation is enabled. - bool m_proofs_enabled; // proof production is enabled. m_manager.proofs_enabled() must be true if m_proofs_enabled == true - bool m_core_enabled; // unsat core extraction is enabled. - bool m_inconsistent; - ptr_vector m_forms; - ptr_vector m_proofs; - ptr_vector m_deps; - unsigned m_form_qhead; // position of first uncommitted assertion - unsigned m_mc_qhead; - - // Set of declarations that can't be eliminated - obj_hashtable m_forbidden_set; - func_decl_ref_vector m_forbidden; - - // Limited model converter support, it supports only extensions and filters. - // It should be viewed as combination of extension_model_converter and - // filter_model_converter for goals. - expr_substitution m_csubst; // substitution for eliminated constants - - // Model converter is just two sequences: func_decl and tag. - // Tag 0 (extension) func_decl was eliminated, and its definition is in m_vsubst or m_fsubst. - // Tag 1 (filter) func_decl was introduced by tactic, and must be removed from model. - ptr_vector m_mc; - char_vector m_mc_tag; - - struct scope { - unsigned m_forms_lim; - unsigned m_forbidden_lim; - unsigned m_mc_lim; - bool m_inconsistent_old; - }; - - svector m_scopes; - - void init(bool proofs_enabled, bool models_enabled, bool core_enabled); - void expand(expr * f, proof * pr, expr_dependency * dep, expr_ref & new_f, proof_ref & new_pr, expr_dependency_ref & new_dep); - void push_back(expr * f, proof * pr, expr_dependency * d); - void quick_process(bool save_first, expr * & f, expr_dependency * d); - void process_and(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr); - void process_not_or(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr); - void slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr); - void slow_process(expr * f, proof * pr, expr_dependency * d); - + struct imp; + imp * m_imp; public: assertion_stack(ast_manager & m, bool models_enabled = true, bool core_enabled = true); assertion_stack(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled); ~assertion_stack(); void reset(); - - void inc_ref() { ++m_ref_count; } - void dec_ref() { --m_ref_count; if (m_ref_count == 0) dealloc(this); } - ast_manager & m() const { return m_manager; } + ast_manager & m() const; - bool models_enabled() const { return m_models_enabled; } - bool proofs_enabled() const { return m_proofs_enabled; } - bool unsat_core_enabled() const { return m_core_enabled; } - bool inconsistent() const { return m_inconsistent; } + bool models_enabled() const; + bool proofs_enabled() const; + bool unsat_core_enabled() const; + bool inconsistent() const; - unsigned size() const { return m_forms.size(); } - unsigned qhead() const { return m_form_qhead; } - expr * form(unsigned i) const { return m_forms[i]; } - proof * pr(unsigned i) const { return proofs_enabled() ? static_cast(m_proofs[i]) : 0; } - expr_dependency * dep(unsigned i) const { return unsat_core_enabled() ? m_deps[i] : 0; } + unsigned size() const; + unsigned qhead() const; + expr * form(unsigned i) const; + proof * pr(unsigned i) const; + expr_dependency * dep(unsigned i) const; 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); void update(unsigned i, expr * f, proof * pr = 0, expr_dependency * dep = 0); void expand_and_update(unsigned i, expr * f, proof * pr = 0, expr_dependency * d = 0); void commit(); void push(); void pop(unsigned num_scopes); - unsigned scope_lvl() const { return m_scopes.size(); } + unsigned scope_lvl() const; bool is_well_sorted() const; - bool is_forbidden(func_decl * f) const { return m_forbidden_set.contains(f); } + bool is_forbidden(func_decl * f) const; void add_filter(func_decl * f); void add_definition(app * c, expr * def, proof * pr, expr_dependency * dep); void convert(model_ref & m); - void display(std::ostream & out) const; }; From 398f1b1de1003d11574560b7715da72f835f1e9b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 Nov 2012 13:29:09 -0700 Subject: [PATCH 06/17] moving assertion_stack to mcsat branch Signed-off-by: Leonardo de Moura --- src/tactic/assertion_stack.cpp | 518 --------------------------------- src/tactic/assertion_stack.h | 88 ------ 2 files changed, 606 deletions(-) delete mode 100644 src/tactic/assertion_stack.cpp delete mode 100644 src/tactic/assertion_stack.h diff --git a/src/tactic/assertion_stack.cpp b/src/tactic/assertion_stack.cpp deleted file mode 100644 index 03631f0d4..000000000 --- a/src/tactic/assertion_stack.cpp +++ /dev/null @@ -1,518 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - assertion_stack.cpp - -Abstract: - - Assertion stacks - -Author: - - Leonardo de Moura (leonardo) 2012-02-17 - -Revision History: - ---*/ -#include"assertion_stack.h" -#include"well_sorted.h" -#include"ast_smt2_pp.h" -#include"ref_util.h" -#include"expr_replacer.h" -#include"model.h" -#include"expr_substitution.h" - -struct assertion_stack::imp { - ast_manager & m_manager; - bool m_models_enabled; // model generation is enabled. - bool m_proofs_enabled; // proof production is enabled. m_manager.proofs_enabled() must be true if m_proofs_enabled == true - bool m_core_enabled; // unsat core extraction is enabled. - bool m_inconsistent; - ptr_vector m_forms; - ptr_vector m_proofs; - ptr_vector m_deps; - unsigned m_form_qhead; // position of first uncommitted assertion - unsigned m_mc_qhead; - - // Set of declarations that can't be eliminated - obj_hashtable m_forbidden_set; - func_decl_ref_vector m_forbidden; - - // Limited model converter support, it supports only extensions and filters. - // It should be viewed as combination of extension_model_converter and - // filter_model_converter for goals. - expr_substitution m_csubst; // substitution for eliminated constants - - // Model converter is just two sequences: func_decl and tag. - // Tag 0 (extension) func_decl was eliminated, and its definition is in m_vsubst or m_fsubst. - // Tag 1 (filter) func_decl was introduced by tactic, and must be removed from model. - ptr_vector m_mc; - char_vector m_mc_tag; - - struct scope { - unsigned m_forms_lim; - unsigned m_forbidden_lim; - unsigned m_mc_lim; - bool m_inconsistent_old; - }; - - svector m_scopes; - - imp(ast_manager & m, bool models_enabled, bool core_enabled): - m_manager(m), - m_forbidden(m), - m_csubst(m, core_enabled) { - init(m.proofs_enabled(), models_enabled, core_enabled); - } - - imp(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled): - m_manager(m), - m_forbidden(m), - m_csubst(m, core_enabled, proofs_enabled) { - init(proofs_enabled, models_enabled, core_enabled); - } - - void init(bool proofs_enabled, bool models_enabled, bool core_enabled) { - m_models_enabled = models_enabled; - m_proofs_enabled = proofs_enabled; - m_core_enabled = core_enabled; - m_inconsistent = false; - m_form_qhead = 0; - } - - ~imp() { - reset(); - } - - ast_manager & m() const { return m_manager; } - - bool models_enabled() const { return m_models_enabled; } - - bool proofs_enabled() const { return m_proofs_enabled; } - - bool unsat_core_enabled() const { return m_core_enabled; } - - bool inconsistent() const { return m_inconsistent; } - - unsigned size() const { return m_forms.size(); } - - unsigned qhead() const { return m_form_qhead; } - - expr * form(unsigned i) const { return m_forms[i]; } - - proof * pr(unsigned i) const { - if (proofs_enabled()) - return m_proofs[i]; - else - return 0; - } - - expr_dependency * dep(unsigned i) const { - if (unsat_core_enabled()) - return m_deps[i]; - else - return 0; - } - - void reset() { - m_inconsistent = false; - m_form_qhead = 0; - m_mc_qhead = 0; - dec_ref_collection_values(m_manager, m_forms); - dec_ref_collection_values(m_manager, m_proofs); - dec_ref_collection_values(m_manager, m_deps); - dec_ref_collection_values(m_manager, m_forbidden); - m_forbidden_set.reset(); - dec_ref_collection_values(m_manager, m_mc); - m_mc_tag.reset(); - m_csubst.reset(); - m_scopes.reset(); - } - - void expand(expr * f, proof * pr, expr_dependency * dep, expr_ref & new_f, proof_ref & new_pr, expr_dependency_ref & new_dep) { - scoped_ptr r = mk_default_expr_replacer(m()); - (*r)(f, new_f, new_pr, new_dep); - // new_pr is a proof for f == new_f - // new_dep are the dependencies for showing f == new_f - if (proofs_enabled()) { - new_pr = m_manager.mk_modus_ponens(pr, new_pr); - } - if (unsat_core_enabled()) { - new_dep = m().mk_join(dep, new_dep); - } - } - - void push_back(expr * f, proof * pr, expr_dependency * d) { - if (m().is_true(f)) - return; - if (m().is_false(f)) { - m_inconsistent = true; - } - else { - SASSERT(!m_inconsistent); - } - m().inc_ref(f); - m_forms.push_back(f); - if (proofs_enabled()) { - m().inc_ref(pr); - m_proofs.push_back(pr); - } - if (unsat_core_enabled()) { - m().inc_ref(d); - m_deps.push_back(d); - } - } - - void quick_process(bool save_first, expr * & f, expr_dependency * d) { - if (!m().is_and(f) && !(m().is_not(f) && m().is_or(to_app(f)->get_arg(0)))) { - if (!save_first) { - push_back(f, 0, d); - } - return; - } - typedef std::pair expr_pol; - sbuffer todo; - todo.push_back(expr_pol(f, true)); - while (!todo.empty()) { - if (m_inconsistent) - return; - expr_pol p = todo.back(); - expr * curr = p.first; - bool pol = p.second; - todo.pop_back(); - if (pol && m().is_and(curr)) { - app * t = to_app(curr); - unsigned i = t->get_num_args(); - while (i > 0) { - --i; - todo.push_back(expr_pol(t->get_arg(i), true)); - } - } - else if (!pol && m().is_or(curr)) { - app * t = to_app(curr); - unsigned i = t->get_num_args(); - while (i > 0) { - --i; - todo.push_back(expr_pol(t->get_arg(i), false)); - } - } - else if (m().is_not(curr)) { - todo.push_back(expr_pol(to_app(curr)->get_arg(0), !pol)); - } - else { - if (!pol) - curr = m().mk_not(curr); - if (save_first) { - f = curr; - save_first = false; - } - else { - push_back(curr, 0, d); - } - } - } - } - - void process_and(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) { - unsigned num = f->get_num_args(); - for (unsigned i = 0; i < num; i++) { - if (m_inconsistent) - return; - slow_process(save_first && i == 0, f->get_arg(i), m().mk_and_elim(pr, i), d, out_f, out_pr); - } - } - - void process_not_or(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) { - unsigned num = f->get_num_args(); - for (unsigned i = 0; i < num; i++) { - if (m_inconsistent) - return; - expr * child = f->get_arg(i); - if (m().is_not(child)) { - expr * not_child = to_app(child)->get_arg(0); - slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), d, out_f, out_pr); - } - else { - expr_ref not_child(m()); - not_child = m().mk_not(child); - slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), d, out_f, out_pr); - } - } - } - - void slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) { - if (m().is_and(f)) - process_and(save_first, to_app(f), pr, d, out_f, out_pr); - else if (m().is_not(f) && m().is_or(to_app(f)->get_arg(0))) - process_not_or(save_first, to_app(to_app(f)->get_arg(0)), pr, d, out_f, out_pr); - else if (save_first) { - out_f = f; - out_pr = pr; - } - else { - push_back(f, pr, d); - } - } - - void slow_process(expr * f, proof * pr, expr_dependency * d) { - expr_ref out_f(m()); - proof_ref out_pr(m()); - slow_process(false, f, pr, d, out_f, out_pr); - } - - void assert_expr(expr * f, proof * pr, expr_dependency * d) { - SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr))); - if (m_inconsistent) - return; - expr_ref new_f(m()); proof_ref new_pr(m()); expr_dependency_ref new_d(m()); - expand(f, pr, d, new_f, new_pr, new_d); - if (proofs_enabled()) - slow_process(f, pr, d); - else - quick_process(false, f, d); - } - - void update(unsigned i, expr * f, proof * pr, expr_dependency * d) { - SASSERT(i >= m_form_qhead); - SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr))); - if (m_inconsistent) - return; - if (proofs_enabled()) { - expr_ref out_f(m()); - proof_ref out_pr(m()); - slow_process(true, f, pr, d, out_f, out_pr); - if (!m_inconsistent) { - if (m().is_false(out_f)) { - push_back(out_f, out_pr, d); - } - else { - m().inc_ref(out_f); - m().dec_ref(m_forms[i]); - m_forms[i] = out_f; - - m().inc_ref(out_pr); - m().dec_ref(m_proofs[i]); - m_proofs[i] = out_pr; - - if (unsat_core_enabled()) { - m().inc_ref(d); - m().dec_ref(m_deps[i]); - m_deps[i] = d; - } - } - } - } - else { - quick_process(true, f, d); - if (!m_inconsistent) { - if (m().is_false(f)) { - push_back(f, 0, d); - } - else { - m().inc_ref(f); - m().dec_ref(m_forms[i]); - m_forms[i] = f; - - if (unsat_core_enabled()) { - m().inc_ref(d); - m().dec_ref(m_deps[i]); - m_deps[i] = d; - } - } - } - } - } - - void expand_and_update(unsigned i, expr * f, proof * pr, expr_dependency * d) { - SASSERT(i >= m_form_qhead); - SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr))); - if (m_inconsistent) - return; - expr_ref new_f(m()); proof_ref new_pr(m()); expr_dependency_ref new_d(m()); - expand(f, pr, d, new_f, new_pr, new_d); - update(i, new_f, new_pr, new_d); - } - - void push() { - commit(); - m_scopes.push_back(scope()); - scope & s = m_scopes.back(); - s.m_forms_lim = m_forms.size(); - s.m_forbidden_lim = m_forbidden.size(); - s.m_mc_lim = m_mc.size(); - s.m_inconsistent_old = m_inconsistent; - } - - void pop(unsigned num_scopes) { - } - - void commit() { - } - - unsigned scope_lvl() const { - return m_scopes.size(); - } - - bool is_forbidden(func_decl * f) const { - return m_forbidden_set.contains(f); - } - -#define MC_TAG_EXTENSION 0 -#define MC_TAG_FILTER 1 - - void add_filter(func_decl * f) { - m().inc_ref(f); - m_mc.push_back(f); - m_mc_tag.push_back(MC_TAG_FILTER); - } - - void add_definition(app * c, expr * def, proof * pr, expr_dependency * dep) { - SASSERT(c->get_num_args() == 0); - SASSERT(!m_csubst.contains(c)); - m_csubst.insert(c, def, pr, dep); - func_decl * d = c->get_decl(); - m().inc_ref(d); - m_mc.push_back(d); - m_mc_tag.push_back(MC_TAG_EXTENSION); - } - - void convert(model_ref & m) { - } - - void display(std::ostream & out) const { - out << "(assertion-stack"; - unsigned sz = size(); - for (unsigned i = 0; i < sz; i++) { - out << "\n "; - if (i == m_form_qhead) - out << "==>\n"; - out << mk_ismt2_pp(form(i), m(), 2); - } - out << ")" << std::endl; - } - - bool is_well_sorted() const { - unsigned sz = size(); - for (unsigned i = 0; i < sz; i++) { - expr * t = form(i); - if (!::is_well_sorted(m(), t)) - return false; - } - return true; - } -}; - -assertion_stack::assertion_stack(ast_manager & m, bool models_enabled, bool core_enabled) { - m_imp = alloc(imp, m, models_enabled, core_enabled); -} - -assertion_stack::assertion_stack(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled) { - m_imp = alloc(imp, m, proofs_enabled, models_enabled, core_enabled); -} - -assertion_stack::~assertion_stack() { - dealloc(m_imp); -} - -void assertion_stack::reset() { - m_imp->reset(); -} - -ast_manager & assertion_stack::m() const { - return m_imp->m(); -} - -bool assertion_stack::models_enabled() const { - return m_imp->models_enabled(); -} - -bool assertion_stack::proofs_enabled() const { - return m_imp->proofs_enabled(); -} - -bool assertion_stack::unsat_core_enabled() const { - return m_imp->unsat_core_enabled(); -} - -bool assertion_stack::inconsistent() const { - return m_imp->inconsistent(); -} - -unsigned assertion_stack::size() const { - return m_imp->size(); -} - -unsigned assertion_stack::qhead() const { - return m_imp->qhead(); -} - -expr * assertion_stack::form(unsigned i) const { - return m_imp->form(i); -} - -proof * assertion_stack::pr(unsigned i) const { - return m_imp->pr(i); -} - -expr_dependency * assertion_stack::dep(unsigned i) const { - return m_imp->dep(i); -} - -void assertion_stack::assert_expr(expr * f, proof * pr, expr_dependency * d) { - return m_imp->assert_expr(f, pr, d); -} - -void assertion_stack::assert_expr(expr * f) { - assert_expr(f, proofs_enabled() ? m().mk_asserted(f) : 0, 0); -} - -void assertion_stack::update(unsigned i, expr * f, proof * pr, expr_dependency * d) { - m_imp->update(i, f, pr, d); -} - -void assertion_stack::expand_and_update(unsigned i, expr * f, proof * pr, expr_dependency * d) { - m_imp->expand_and_update(i, f, pr, d); -} - -void assertion_stack::commit() { - m_imp->commit(); -} - -void assertion_stack::push() { - m_imp->push(); -} - -void assertion_stack::pop(unsigned num_scopes) { - m_imp->pop(num_scopes); -} - -unsigned assertion_stack::scope_lvl() const { - return m_imp->scope_lvl(); -} - -bool assertion_stack::is_well_sorted() const { - return m_imp->is_well_sorted(); -} - - -bool assertion_stack::is_forbidden(func_decl * f) const { - return m_imp->is_forbidden(f); -} - -void assertion_stack::add_filter(func_decl * f) { - m_imp->add_filter(f); -} - -void assertion_stack::add_definition(app * c, expr * def, proof * pr, expr_dependency * dep) { - m_imp->add_definition(c, def, pr, dep); -} - -void assertion_stack::convert(model_ref & m) { - m_imp->convert(m); -} - -void assertion_stack::display(std::ostream & out) const { - m_imp->display(out); -} diff --git a/src/tactic/assertion_stack.h b/src/tactic/assertion_stack.h deleted file mode 100644 index d6bb195e9..000000000 --- a/src/tactic/assertion_stack.h +++ /dev/null @@ -1,88 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - assertion_stack.h - -Abstract: - - It should be viewed as the "goal" object for incremental solvers. - The main difference is the support of push/pop operations. Like a - goal, an assertion_stack contains expressions, their proofs (if - proof generation is enabled), and dependencies (if unsat core - generation is enabled). - - The assertions on the stack are grouped by scope levels. Scoped - levels are created using push, and removed using pop. - - Assertions may be "committed". Whenever a push is executed, all - "uncommitted" assertions are automatically committed. - Only uncommitted assertions can be simplified/reduced. - - An assertion set has a limited model converter that only supports - definitions (for constant elimination) and filters (for fresh - symbols introduced by tactics). - - Some tactics support assertion_stacks and can be applied to them. - However, a tactic can only access the assertions on the top level. - The assertion stack also informs the tactic which declarations - can't be eliminated since they occur in the already committed part. - -Author: - - Leonardo de Moura (leonardo) 2012-02-17 - -Revision History: - ---*/ -#ifndef _ASSERTION_STACK_H_ -#define _ASSERTION_STACK_H_ - -#include"ast.h" -#include"model.h" - -class assertion_stack { - struct imp; - imp * m_imp; -public: - assertion_stack(ast_manager & m, bool models_enabled = true, bool core_enabled = true); - assertion_stack(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled); - ~assertion_stack(); - - void reset(); - - ast_manager & m() const; - - bool models_enabled() const; - bool proofs_enabled() const; - bool unsat_core_enabled() const; - bool inconsistent() const; - - unsigned size() const; - unsigned qhead() const; - expr * form(unsigned i) const; - proof * pr(unsigned i) const; - expr_dependency * dep(unsigned i) const; - - void assert_expr(expr * f, proof * pr, expr_dependency * d); - void assert_expr(expr * f); - void update(unsigned i, expr * f, proof * pr = 0, expr_dependency * dep = 0); - void expand_and_update(unsigned i, expr * f, proof * pr = 0, expr_dependency * d = 0); - - void commit(); - void push(); - void pop(unsigned num_scopes); - unsigned scope_lvl() const; - - bool is_well_sorted() const; - - bool is_forbidden(func_decl * f) const; - void add_filter(func_decl * f); - void add_definition(app * c, expr * def, proof * pr, expr_dependency * dep); - - void convert(model_ref & m); - void display(std::ostream & out) const; -}; - -#endif From adb6d0580521c682aafa71c20f418c5aeaea7974 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 Nov 2012 14:43:02 -0700 Subject: [PATCH 07/17] fixed typo Signed-off-by: Leonardo de Moura --- src/solver/solver.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solver/solver.h b/src/solver/solver.h index e8823df4f..1cbc681c0 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -64,19 +64,19 @@ public: /** \brief Enable/Disable proof production for this solver object. - It is invoked before init(m, logic). + It is invoked after init(m, logic). */ virtual void set_produce_proofs(bool f) {} /** \brief Enable/Disable model generation for this solver object. - It is invoked before init(m, logic). + It is invoked 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). + It is invoked after init(m, logic). */ virtual void set_produce_unsat_cores(bool f) {} From cadd35bf7a76abf5afd62399c56d0a35d1aa0325 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 Nov 2012 21:44:35 -0700 Subject: [PATCH 08/17] checkpoint Signed-off-by: Leonardo de Moura --- src/api/api_context.cpp | 16 +-- src/api/api_context.h | 6 +- src/api/api_datalog.h | 2 +- src/api/api_parsers.cpp | 2 +- src/api/api_solver_old.cpp | 38 +++---- src/api/api_user_theory.cpp | 4 +- src/muz_qe/dl_bmc_engine.cpp | 2 +- src/muz_qe/dl_bmc_engine.h | 4 +- src/muz_qe/dl_smt_relation.cpp | 8 +- src/muz_qe/pdr_context.cpp | 2 +- src/muz_qe/pdr_farkas_learner.cpp | 4 +- src/muz_qe/pdr_farkas_learner.h | 4 +- src/muz_qe/pdr_generalizers.cpp | 2 +- src/muz_qe/pdr_manager.cpp | 2 +- src/muz_qe/pdr_manager.h | 2 +- src/muz_qe/pdr_prop_solver.h | 2 +- src/muz_qe/pdr_quantifiers.cpp | 4 +- src/muz_qe/pdr_smt_context_manager.cpp | 10 +- src/muz_qe/pdr_smt_context_manager.h | 10 +- src/muz_qe/qe.cpp | 4 +- src/muz_qe/qe_sat_tactic.cpp | 22 ++--- src/smt/default_solver.cpp | 10 +- src/smt/default_solver.h | 2 +- src/smt/expr_context_simplifier.cpp | 2 +- src/smt/expr_context_simplifier.h | 4 +- src/smt/ni_solver.cpp | 10 +- src/smt/smt_implied_equalities.cpp | 6 +- src/smt/smt_implied_equalities.h | 4 +- src/smt/{smt_solver.cpp => smt_kernel.cpp} | 98 +++++++++---------- src/smt/{smt_solver.h => smt_kernel.h} | 42 ++++---- src/smt/smt_model_checker.cpp | 2 +- src/smt/smt_quantifier.cpp | 4 +- src/smt/smt_quantifier.h | 2 +- src/smt/tactic/ctx_solver_simplify_tactic.cpp | 4 +- src/smt/tactic/smt_tactic.cpp | 8 +- src/smt/user_plugin/user_smt_theory.cpp | 4 +- src/smt/user_plugin/user_smt_theory.h | 4 +- src/test/quant_solve.cpp | 6 +- 38 files changed, 185 insertions(+), 177 deletions(-) rename src/smt/{smt_solver.cpp => smt_kernel.cpp} (74%) rename src/smt/{smt_solver.h => smt_kernel.h} (82%) 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..2d5c3d0c4 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -253,7 +253,7 @@ extern "C" { class z3_context_solver : public solver { 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) {} 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/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 c544d9edf..1280810e3 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -1866,7 +1866,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_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/smt/default_solver.cpp b/src/smt/default_solver.cpp index 73ce084f3..1a895d212 100644 --- a/src/smt/default_solver.cpp +++ b/src/smt/default_solver.cpp @@ -7,7 +7,7 @@ Module Name: Abstract: - Wrapps smt::solver as a solver for cmd_context + Wrapps smt::kernel as a solver for cmd_context Author: @@ -17,13 +17,13 @@ Notes: --*/ #include"solver.h" -#include"smt_solver.h" +#include"smt_kernel.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; + smt::kernel * m_context; public: default_solver():m_params(0), m_context(0) {} @@ -47,7 +47,7 @@ public: ast_manager m; reg_decl_plugins(m); front_end_params p; - smt::solver s(m, p); + smt::kernel s(m, p); s.collect_param_descrs(r); } else { @@ -60,7 +60,7 @@ public: reset(); #pragma omp critical (solver) { - m_context = alloc(smt::solver, m, *m_params); + m_context = alloc(smt::kernel, m, *m_params); } if (logic != symbol::null) m_context->set_logic(logic); diff --git a/src/smt/default_solver.h b/src/smt/default_solver.h index 170a55e56..adffac1c3 100644 --- a/src/smt/default_solver.h +++ b/src/smt/default_solver.h @@ -7,7 +7,7 @@ Module Name: Abstract: - Wrapps smt::solver as a solver for cmd_context + Wrapps smt::kernel as a solver for cmd_context and external API Author: 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 index a0341cb32..cd0cd503a 100644 --- a/src/smt/ni_solver.cpp +++ b/src/smt/ni_solver.cpp @@ -6,7 +6,7 @@ Module Name: ni_solver.cpp Abstract: - Wrappers for smt::solver that are non-incremental & (quasi-incremental). + Wrappers for smt::kernel that are non-incremental & (quasi-incremental). Author: @@ -16,13 +16,13 @@ Notes: --*/ #include"ni_solver.h" -#include"smt_solver.h" +#include"smt_kernel.h" #include"cmd_context.h" class ni_smt_solver : public solver { protected: cmd_context & m_cmd_ctx; - smt::solver * m_context; + smt::kernel * m_context; progress_callback * m_callback; public: ni_smt_solver(cmd_context & ctx):m_cmd_ctx(ctx), m_context(0), m_callback(0) {} @@ -83,7 +83,7 @@ public: reset(); #pragma omp critical (ni_solver) { - m_context = alloc(smt::solver, m_cmd_ctx.m(), m_cmd_ctx.params()); + m_context = alloc(smt::kernel, m_cmd_ctx.m(), m_cmd_ctx.params()); } if (m_cmd_ctx.has_logic()) m_context->set_logic(m_cmd_ctx.get_logic()); @@ -149,7 +149,7 @@ public: virtual void collect_param_descrs(param_descrs & r) { - smt::solver::collect_param_descrs(r); + smt::kernel::collect_param_descrs(r); } }; 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_solver.cpp b/src/smt/smt_kernel.cpp similarity index 74% rename from src/smt/smt_solver.cpp rename to src/smt/smt_kernel.cpp index 6bdfd0524..9d87b1363 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_kernel.cpp @@ -3,11 +3,11 @@ Copyright (c) 2012 Microsoft Corporation Module Name: - smt_solver.h + smt_kernel.cpp Abstract: - New frontend for the incremental solver. + New frontend for smt::context. Author: @@ -16,14 +16,14 @@ Author: Revision History: --*/ -#include"smt_solver.h" +#include"smt_kernel.h" #include"smt_context.h" #include"ast_smt2_pp.h" #include"params2front_end_params.h" namespace smt { - struct solver::imp { + struct kernel::imp { smt::context m_kernel; params_ref m_params; @@ -53,7 +53,7 @@ namespace smt { } void assert_expr(expr * e) { - TRACE("smt_solver", tout << "assert:\n" << mk_ismt2_pp(e, m()) << "\n";); + TRACE("smt_kernel", tout << "assert:\n" << mk_ismt2_pp(e, m()) << "\n";); m_kernel.assert_expr(e); } @@ -74,12 +74,12 @@ namespace smt { } void push() { - TRACE("smt_solver", tout << "push()\n";); + TRACE("smt_kernel", tout << "push()\n";); m_kernel.push(); } void pop(unsigned num_scopes) { - TRACE("smt_solver", tout << "pop()\n";); + TRACE("smt_kernel", tout << "pop()\n";); m_kernel.pop(num_scopes); } @@ -148,7 +148,7 @@ namespace smt { // 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"; + out << "(kernel"; for (unsigned i = 0; i < num; i++) { out << "\n " << mk_ismt2_pp(fms[i], m(), 2); } @@ -183,170 +183,170 @@ namespace smt { } }; - solver::solver(ast_manager & m, front_end_params & fp, params_ref const & p) { + kernel::kernel(ast_manager & m, front_end_params & fp, params_ref const & p) { m_imp = alloc(imp, m, fp, p); } - solver::~solver() { + kernel::~kernel() { dealloc(m_imp); } - ast_manager & solver::m() const { + ast_manager & kernel::m() const { return m_imp->m(); } - bool solver::set_logic(symbol logic) { + bool kernel::set_logic(symbol logic) { return m_imp->set_logic(logic); } - void solver::set_progress_callback(progress_callback * callback) { + void kernel::set_progress_callback(progress_callback * callback) { m_imp->set_progress_callback(callback); } - void solver::assert_expr(expr * e) { + void kernel::assert_expr(expr * e) { m_imp->assert_expr(e); } - void solver::assert_expr(expr * e, proof * pr) { + void kernel::assert_expr(expr * e, proof * pr) { m_imp->assert_expr(e, pr); } - unsigned solver::size() const { + unsigned kernel::size() const { return m_imp->size(); } - expr * const * solver::get_formulas() const { + expr * const * kernel::get_formulas() const { return m_imp->get_formulas(); } - bool solver::reduce() { + bool kernel::reduce() { return m_imp->reduce(); } - void solver::push() { + void kernel::push() { m_imp->push(); } - void solver::pop(unsigned num_scopes) { + void kernel::pop(unsigned num_scopes) { m_imp->pop(num_scopes); } - unsigned solver::get_scope_level() const { + unsigned kernel::get_scope_level() const { return m_imp->get_scope_level(); } - void solver::reset() { + void kernel::reset() { ast_manager & _m = m(); front_end_params & fps = m_imp->fparams(); params_ref ps = m_imp->params(); - #pragma omp critical (smt_solver) + #pragma omp critical (smt_kernel) { dealloc(m_imp); m_imp = alloc(imp, _m, fps, ps); } } - bool solver::inconsistent() { + bool kernel::inconsistent() { return m_imp->inconsistent(); } - lbool solver::setup_and_check() { + lbool kernel::setup_and_check() { set_cancel(false); return m_imp->setup_and_check(); } - lbool solver::check(unsigned num_assumptions, expr * const * assumptions) { + lbool kernel::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";); + TRACE("smt_kernel", tout << "check result: " << r << "\n";); return r; } - void solver::get_model(model_ref & m) const { + void kernel::get_model(model_ref & m) const { m_imp->get_model(m); } - proof * solver::get_proof() { + proof * kernel::get_proof() { return m_imp->get_proof(); } - unsigned solver::get_unsat_core_size() const { + unsigned kernel::get_unsat_core_size() const { return m_imp->get_unsat_core_size(); } - expr * solver::get_unsat_core_expr(unsigned idx) const { + expr * kernel::get_unsat_core_expr(unsigned idx) const { return m_imp->get_unsat_core_expr(idx); } - failure solver::last_failure() const { + failure kernel::last_failure() const { return m_imp->last_failure(); } - std::string solver::last_failure_as_string() const { + std::string kernel::last_failure_as_string() const { return m_imp->last_failure_as_string(); } - void solver::get_assignments(expr_ref_vector & result) { + void kernel::get_assignments(expr_ref_vector & result) { m_imp->get_assignments(result); } - void solver::get_relevant_labels(expr * cnstr, buffer & result) { + void kernel::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) { + void kernel::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) { + void kernel::get_relevant_literals(expr_ref_vector & result) { m_imp->get_relevant_literals(result); } - void solver::get_guessed_literals(expr_ref_vector & result) { + void kernel::get_guessed_literals(expr_ref_vector & result) { m_imp->get_guessed_literals(result); } - void solver::display(std::ostream & out) const { + void kernel::display(std::ostream & out) const { m_imp->display(out); } - void solver::collect_statistics(::statistics & st) const { + void kernel::collect_statistics(::statistics & st) const { m_imp->collect_statistics(st); } - void solver::reset_statistics() { + void kernel::reset_statistics() { m_imp->reset_statistics(); } - void solver::display_statistics(std::ostream & out) const { + void kernel::display_statistics(std::ostream & out) const { m_imp->display_statistics(out); } - void solver::display_istatistics(std::ostream & out) const { + void kernel::display_istatistics(std::ostream & out) const { m_imp->display_istatistics(out); } - void solver::set_cancel(bool f) { - #pragma omp critical (smt_solver) + void kernel::set_cancel(bool f) { + #pragma omp critical (smt_kernel) { if (m_imp) m_imp->set_cancel(f); } } - bool solver::canceled() const { + bool kernel::canceled() const { return m_imp->canceled(); } - void solver::updt_params(params_ref const & p) { + void kernel::updt_params(params_ref const & p) { return m_imp->updt_params(p); } - void solver::collect_param_descrs(param_descrs & d) { + void kernel::collect_param_descrs(param_descrs & d) { solver_front_end_params_descrs(d); } - context & solver::kernel() { + context & kernel::get_context() { return m_imp->m_kernel; } diff --git a/src/smt/smt_solver.h b/src/smt/smt_kernel.h similarity index 82% rename from src/smt/smt_solver.h rename to src/smt/smt_kernel.h index 1d04df9ed..4c381e113 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_kernel.h @@ -3,11 +3,13 @@ Copyright (c) 2012 Microsoft Corporation Module Name: - smt_solver.h + smt_kernel.h Abstract: - New frontend for the incremental solver. + 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: @@ -15,9 +17,15 @@ Author: 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_SOLVER_H_ -#define _SMT_SOLVER_H_ +#ifndef _SMT_KERNEL_H_ +#define _SMT_KERNEL_H_ #include"ast.h" #include"params.h" @@ -34,13 +42,13 @@ namespace smt { class enode; class context; - class solver { + class kernel { struct imp; imp * m_imp; public: - solver(ast_manager & m, front_end_params & fp, params_ref const & p = params_ref()); + kernel(ast_manager & m, front_end_params & fp, params_ref const & p = params_ref()); - ~solver(); + ~kernel(); ast_manager & m() const; @@ -51,7 +59,7 @@ namespace smt { bool set_logic(symbol logic); /** - brief Set progress meter. Solver will invoke the callback from time to time. + brief Set progress meter. Kernel will invoke the callback from time to time. */ void set_progress_callback(progress_callback * callback); @@ -67,7 +75,7 @@ namespace smt { void assert_expr(expr * e, proof * pr); /** - \brief Return the number of asserted formulas in the solver. + \brief Return the number of asserted formulas in the kernel. */ unsigned size() const; @@ -101,7 +109,7 @@ namespace smt { unsigned get_scope_level() const; /** - \brief Reset the solver. + \brief Reset the kernel. All assertions are erased. */ void reset(); @@ -155,7 +163,7 @@ namespace smt { std::string last_failure_as_string() const; /** - \brief Return the set of formulas assigned by the solver. + \brief Return the set of formulas assigned by the kernel. */ void get_assignments(expr_ref_vector & result); @@ -180,7 +188,7 @@ namespace smt { void get_guessed_literals(expr_ref_vector & result); /** - \brief (For debubbing purposes) Prints the state of the solver + \brief (For debubbing purposes) Prints the state of the kernel */ void display(std::ostream & out) const; @@ -190,7 +198,7 @@ namespace smt { void collect_statistics(::statistics & st) const; /** - \brief Reset solver statistics. + \brief Reset kernel statistics. */ void reset_statistics(); @@ -205,7 +213,7 @@ namespace smt { void display_istatistics(std::ostream & out) const; /** - \brief Interrupt the solver. + \brief Interrupt the kernel. */ void set_cancel(bool f = true); void cancel() { set_cancel(true); } @@ -216,7 +224,7 @@ namespace smt { void reset_cancel() { set_cancel(false); } /** - \brief Return true if the solver was interrupted. + \brief Return true if the kernel was interrupted. */ bool canceled() const; @@ -231,7 +239,7 @@ namespace smt { static void collect_param_descrs(param_descrs & d); /** - \brief Return a reference to the kernel. + \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. @@ -240,7 +248,7 @@ namespace smt { \warning We should not use this method */ - context & kernel(); + context & get_context(); }; }; 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/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/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/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"; From 230382d4c993b2447526dfa33c77d42df93ac443 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 Nov 2012 21:52:27 -0700 Subject: [PATCH 09/17] default_solver --> smt_solver Signed-off-by: Leonardo de Moura --- src/api/api_solver.cpp | 4 +- src/smt/default_solver.cpp | 181 ----------------- src/smt/default_solver.h | 26 --- src/smt/smt_solver.cpp | 185 ++++++++++++++++++ src/smt/smt_solver.h | 28 +++ src/tactic/portfolio/smt_strategic_solver.cpp | 4 +- 6 files changed, 217 insertions(+), 211 deletions(-) delete mode 100644 src/smt/default_solver.cpp delete mode 100644 src/smt/default_solver.h create mode 100644 src/smt/smt_solver.cpp create mode 100644 src/smt/smt_solver.h diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 9b3619a6e..8aecc0a3a 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -29,7 +29,7 @@ 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" { @@ -38,7 +38,7 @@ extern "C" { 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 = 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); diff --git a/src/smt/default_solver.cpp b/src/smt/default_solver.cpp deleted file mode 100644 index 1a895d212..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::kernel as a solver for cmd_context - -Author: - - Leonardo (leonardo) 2012-10-21 - -Notes: - ---*/ -#include"solver.h" -#include"smt_kernel.h" -#include"reg_decl_plugins.h" -#include"front_end_params.h" - -class default_solver : public solver { - front_end_params * m_params; - smt::kernel * 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::kernel 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::kernel, 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 adffac1c3..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::kernel as a solver for cmd_context and external API - -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/smt_solver.cpp b/src/smt/smt_solver.cpp new file mode 100644 index 000000000..516a6321e --- /dev/null +++ b/src/smt/smt_solver.cpp @@ -0,0 +1,185 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + smt_solver.cpp + +Abstract: + + Wraps smt::kernel as a solver for the external API and cmd_context. + +Author: + + Leonardo (leonardo) 2012-10-21 + +Notes: + +--*/ +#include"solver.h" +#include"smt_kernel.h" +#include"reg_decl_plugins.h" +#include"front_end_params.h" + +namespace smt { + + class solver : public ::solver { + front_end_params * m_params; + smt::kernel * m_context; + public: + solver():m_params(0), m_context(0) {} + + virtual ~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::kernel 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::kernel, 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_smt_solver() { + return alloc(smt::solver); +} diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h new file mode 100644 index 000000000..e9af9aafa --- /dev/null +++ b/src/smt/smt_solver.h @@ -0,0 +1,28 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + smt_solver.h + +Abstract: + + Wraps smt::kernel as a solver for the external API and cmd_context. + +Author: + + Leonardo (leonardo) 2012-10-21 + +Notes: + + This file was called default_solver.h. It was a bad name. + +--*/ +#ifndef _SMT_SOLVER_H_ +#define _SMT_SOLVER_H_ + +class solver; + +solver * mk_smt_solver(); + +#endif diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 52762edc4..00c0afaa5 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -34,7 +34,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)); @@ -90,7 +90,7 @@ solver * mk_smt_strategic_solver(cmd_context & ctx) { 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; } From d545f187f81b29e8532bf4a5227a1a97fc79a4a6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 Nov 2012 08:28:34 -0700 Subject: [PATCH 10/17] working on named assertions support Signed-off-by: Leonardo de Moura --- src/api/api_parsers.cpp | 14 ++--- src/smt/ni_solver.cpp | 39 +++++--------- src/smt/smt_solver.cpp | 21 +++----- src/solver/solver.h | 7 +++ src/solver/solver_na2as.cpp | 96 +++++++++++++++++++++++++++++++++ src/solver/solver_na2as.h | 55 +++++++++++++++++++ src/solver/strategic_solver.cpp | 33 +++++------- src/solver/strategic_solver.h | 23 ++++---- src/solver/tactic2solver.cpp | 15 ++---- src/solver/tactic2solver.h | 16 +++--- 10 files changed, 223 insertions(+), 96 deletions(-) create mode 100644 src/solver/solver_na2as.cpp create mode 100644 src/solver/solver_na2as.h diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index 2d5c3d0c4..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::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/smt/ni_solver.cpp b/src/smt/ni_solver.cpp index cd0cd503a..eab8d80cd 100644 --- a/src/smt/ni_solver.cpp +++ b/src/smt/ni_solver.cpp @@ -18,8 +18,9 @@ Notes: #include"ni_solver.h" #include"smt_kernel.h" #include"cmd_context.h" +#include"solver_na2as.h" -class ni_smt_solver : public solver { +class ni_smt_solver : public solver_na2as { protected: cmd_context & m_cmd_ctx; smt::kernel * m_context; @@ -32,7 +33,7 @@ public: dealloc(m_context); } - virtual void init(ast_manager & m, symbol const & logic) { + virtual void init_core(ast_manager & m, symbol const & logic) { // do nothing } @@ -45,7 +46,7 @@ public: } } - virtual void reset() { + virtual void reset_core() { if (m_context != 0) { #pragma omp critical (ni_solver) { @@ -59,18 +60,14 @@ public: // do nothing } - virtual void push() { + virtual void push_core() { // do nothing } - virtual void pop(unsigned n) { + virtual void pop_core(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(); @@ -92,7 +89,7 @@ public: assert_exprs(); } - virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) { + virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) { // erase current solver, and create a new one. init_solver(); @@ -165,15 +162,15 @@ public: virtual ~qi_smt_solver() {} - virtual void init(ast_manager & m, symbol const & logic) { + virtual void init_core(ast_manager & m, symbol const & logic) { if (m_inc_mode) { init_solver(); m_inc_mode = true; } } - virtual void reset() { - ni_smt_solver::reset(); + virtual void reset_core() { + ni_smt_solver::reset_core(); m_inc_mode = false; } @@ -196,31 +193,23 @@ public: } } - virtual void push() { + virtual void push_core() { switch_to_inc(); SASSERT(m_context); m_context->push(); SASSERT(m_inc_mode); } - virtual void pop(unsigned n) { + virtual void pop_core(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) { + virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) { if (!m_inc_mode) { - lbool r = ni_smt_solver::check_sat(num_assumptions, assumptions); + lbool r = ni_smt_solver::check_sat_core(num_assumptions, assumptions); SASSERT(!m_inc_mode); return r; } diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 516a6321e..5ca7d2dad 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -16,14 +16,14 @@ Author: Notes: --*/ -#include"solver.h" +#include"solver_na2as.h" #include"smt_kernel.h" #include"reg_decl_plugins.h" #include"front_end_params.h" namespace smt { - class solver : public ::solver { + class solver : public solver_na2as { front_end_params * m_params; smt::kernel * m_context; public: @@ -57,7 +57,7 @@ namespace smt { } } - virtual void init(ast_manager & m, symbol const & logic) { + virtual void init_core(ast_manager & m, symbol const & logic) { SASSERT(m_params); reset(); #pragma omp critical (solver) @@ -77,7 +77,7 @@ namespace smt { } } - virtual void reset() { + virtual void reset_core() { if (m_context != 0) { #pragma omp critical (solver) { @@ -92,24 +92,17 @@ namespace smt { m_context->assert_expr(t); } - virtual void push() { + virtual void push_core() { SASSERT(m_context); m_context->push(); } - virtual void pop(unsigned n) { + virtual void pop_core(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) { + virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) { SASSERT(m_context); return m_context->check(num_assumptions, assumptions); } diff --git a/src/solver/solver.h b/src/solver/solver.h index 1cbc681c0..4d244f5ef 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -95,6 +95,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..81f313857 --- /dev/null +++ b/src/solver/solver_na2as.cpp @@ -0,0 +1,96 @@ +/*++ +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" + +solver_na2as::solver_na2as() { + m_manager = 0; +} + +solver_na2as::~solver_na2as() { + reset(); +} + +void solver_na2as::assert_expr(expr * t, expr * a) { + SASSERT(m_manager != 0); + expr * new_t = m_manager->mk_implies(a, t); + m_manager->inc_ref(a); + m_assumptions.push_back(a); + 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(num_assumptions, assumptions); +} + +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(m_manager); + 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() { + if (m_manager) + 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..84de62820 100644 --- a/src/solver/strategic_solver.cpp +++ b/src/solver/strategic_solver.cpp @@ -128,7 +128,7 @@ 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_core::init_core(ast_manager & m, symbol const & logic) { m_manager = &m; m_logic = logic; if (m_inc_mode) { @@ -165,7 +165,7 @@ void strategic_solver_core::collect_statistics(statistics & st) const { } } -void strategic_solver_core::reset() { +void strategic_solver_core::reset_core() { m_logic = symbol::null; m_inc_mode = false; m_check_sat_executed = false; @@ -199,14 +199,14 @@ void strategic_solver_core::assert_expr(expr * t) { } } -void strategic_solver_core::push() { +void strategic_solver_core::push_core() { DEBUG_CODE(m_num_scopes++;); init_inc_solver(); if (m_inc_solver) m_inc_solver->push(); } -void strategic_solver_core::pop(unsigned n) { +void strategic_solver_core::pop_core(unsigned n) { DEBUG_CODE({ SASSERT(n <= m_num_scopes); m_num_scopes -= n; @@ -216,13 +216,6 @@ void strategic_solver_core::pop(unsigned n) { m_inc_solver->pop(n); } -unsigned strategic_solver_core::get_scope_level() const { - if (m_inc_solver) - return m_inc_solver->get_scope_level(); - else - return 0; -} - struct aux_timeout_eh : public event_handler { solver * m_solver; volatile bool m_canceled; @@ -278,7 +271,7 @@ lbool strategic_solver_core::check_sat_with_assumptions(unsigned num_assumptions return m_inc_solver->check_sat(num_assumptions, assumptions); } -lbool strategic_solver_core::check_sat(unsigned num_assumptions, expr * const * assumptions) { +lbool strategic_solver_core::check_sat_core(unsigned num_assumptions, expr * const * assumptions) { reset_results(); m_check_sat_executed = true; if (num_assumptions > 0 || // assumptions were provided @@ -427,8 +420,8 @@ 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); +void strategic_solver::init_core(ast_manager & m, symbol const & logic) { + strategic_solver_core::init_core(m, logic); m_ctx = alloc(ctx, m); } @@ -449,24 +442,24 @@ void strategic_solver::assert_expr(expr * t) { m_ctx->m_assertions.push_back(t); } -void strategic_solver::push() { +void strategic_solver::push_core() { SASSERT(m_ctx); - strategic_solver_core::push(); + strategic_solver_core::push_core(); m_ctx->m_scopes.push_back(m_ctx->m_assertions.size()); } -void strategic_solver::pop(unsigned n) { +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(n); + strategic_solver_core::pop_core(n); } -void strategic_solver::reset() { +void strategic_solver::reset_core() { m_ctx = 0; - strategic_solver_core::reset(); + strategic_solver_core::reset_core(); } diff --git a/src/solver/strategic_solver.h b/src/solver/strategic_solver.h index 4d4a47388..de4a7ff92 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.h" +#include"solver_na2as.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 { +class strategic_solver_core : public solver_na2as { public: // Behavior when the incremental solver returns unknown. enum inc_unknown_behavior { @@ -123,14 +123,13 @@ public: virtual void display(std::ostream & out) const; - 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(); + virtual void reset_core(); 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 push_core(); + virtual void pop_core(unsigned n); + virtual lbool check_sat_core(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(); @@ -153,12 +152,12 @@ class strategic_solver : public strategic_solver_core { public: strategic_solver() {} - virtual void init(ast_manager & m, symbol const & logic); + virtual void init_core(ast_manager & m, symbol const & logic); virtual void assert_expr(expr * t); - virtual void push(); - virtual void pop(unsigned n); - virtual void reset(); + 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; 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); From 33c165490c329d4d77f9d06d283ab7d22fd63e2a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 Nov 2012 09:43:07 -0700 Subject: [PATCH 11/17] fixed solver_na2as Signed-off-by: Leonardo de Moura --- src/solver/solver_na2as.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp index 81f313857..48980fa7c 100644 --- a/src/solver/solver_na2as.cpp +++ b/src/solver/solver_na2as.cpp @@ -26,7 +26,8 @@ solver_na2as::solver_na2as() { } solver_na2as::~solver_na2as() { - reset(); + if (m_manager) + restore_assumptions(0); } void solver_na2as::assert_expr(expr * t, expr * a) { @@ -91,6 +92,7 @@ unsigned solver_na2as::get_scope_level() const { } void solver_na2as::reset() { + reset_core(); if (m_manager) restore_assumptions(0); } From e1eb3ee8ee9de37a0b8f97f42795764e52228788 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 Nov 2012 11:36:59 -0700 Subject: [PATCH 12/17] fixed bug in solver_na2as Signed-off-by: Leonardo de Moura --- src/smt/ni_solver.cpp | 2 +- src/solver/solver_na2as.cpp | 13 ++++++------- 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/src/smt/ni_solver.cpp b/src/smt/ni_solver.cpp index eab8d80cd..692e1b042 100644 --- a/src/smt/ni_solver.cpp +++ b/src/smt/ni_solver.cpp @@ -77,7 +77,7 @@ public: } void init_solver() { - reset(); + reset_core(); #pragma omp critical (ni_solver) { m_context = alloc(smt::kernel, m_cmd_ctx.m(), m_cmd_ctx.params()); diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp index 48980fa7c..e9d5eba3e 100644 --- a/src/solver/solver_na2as.cpp +++ b/src/solver/solver_na2as.cpp @@ -26,15 +26,15 @@ solver_na2as::solver_na2as() { } solver_na2as::~solver_na2as() { - if (m_manager) - restore_assumptions(0); + restore_assumptions(0); } void solver_na2as::assert_expr(expr * t, expr * a) { SASSERT(m_manager != 0); - expr * new_t = m_manager->mk_implies(a, t); 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); } @@ -62,7 +62,7 @@ struct append_assumptions { lbool solver_na2as::check_sat(unsigned num_assumptions, expr * const * assumptions) { append_assumptions app(m_assumptions, num_assumptions, assumptions); - return check_sat_core(num_assumptions, assumptions); + return check_sat_core(m_assumptions.size(), m_assumptions.c_ptr()); } void solver_na2as::push() { @@ -80,7 +80,7 @@ void solver_na2as::pop(unsigned n) { } void solver_na2as::restore_assumptions(unsigned old_sz) { - SASSERT(m_manager); + SASSERT(old_sz == 0 || m_manager != 0); for (unsigned i = old_sz; i < m_assumptions.size(); i++) { m_manager->dec_ref(m_assumptions[i]); } @@ -93,6 +93,5 @@ unsigned solver_na2as::get_scope_level() const { void solver_na2as::reset() { reset_core(); - if (m_manager) - restore_assumptions(0); + restore_assumptions(0); } From e08c569d8dc0aab6b686191f9ba772555389d64e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 Nov 2012 12:04:02 -0700 Subject: [PATCH 13/17] new qe example Signed-off-by: Leonardo de Moura --- examples/c++/example.cpp | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) 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"; } From e2f6a65aa22dc9b45ef303e5027e4a785b897149 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 Nov 2012 14:00:15 -0700 Subject: [PATCH 14/17] added support for named assertions --- src/cmd_context/cmd_context.cpp | 51 ++-- src/cmd_context/cmd_context.h | 11 +- src/cmd_context/cmd_context_to_goal.cpp | 24 +- src/parsers/smt/smtlib_solver.cpp | 2 +- src/shell/smtlib_frontend.cpp | 2 +- src/smt/ni_solver.cpp | 225 ------------------ src/smt/ni_solver.h | 30 --- src/smt/smt_solver.cpp | 14 +- src/solver/solver_na2as.cpp | 4 + src/solver/strategic_solver.cpp | 6 + src/tactic/portfolio/smt_strategic_solver.cpp | 8 - src/tactic/portfolio/smt_strategic_solver.h | 4 +- 12 files changed, 62 insertions(+), 319 deletions(-) delete mode 100644 src/smt/ni_solver.cpp delete mode 100644 src/smt/ni_solver.h diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index c56066827..532affef7 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1076,7 +1076,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 +1107,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 +1120,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 +1141,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 +1203,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 +1239,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); } @@ -1266,11 +1264,9 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions 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 +1274,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); diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 9296f0735..73e212da1 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); @@ -369,8 +367,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 +378,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/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/ni_solver.cpp b/src/smt/ni_solver.cpp deleted file mode 100644 index 692e1b042..000000000 --- a/src/smt/ni_solver.cpp +++ /dev/null @@ -1,225 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - ni_solver.cpp - -Abstract: - Wrappers for smt::kernel that are non-incremental & (quasi-incremental). - -Author: - - Leonardo (leonardo) 2011-03-30 - -Notes: - ---*/ -#include"ni_solver.h" -#include"smt_kernel.h" -#include"cmd_context.h" -#include"solver_na2as.h" - -class ni_smt_solver : public solver_na2as { -protected: - cmd_context & m_cmd_ctx; - smt::kernel * 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_core(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_core() { - 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_core() { - // do nothing - } - - virtual void pop_core(unsigned n) { - // do nothing - } - - 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_core(); - #pragma omp critical (ni_solver) - { - m_context = alloc(smt::kernel, 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_core(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::kernel::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_core(ast_manager & m, symbol const & logic) { - if (m_inc_mode) { - init_solver(); - m_inc_mode = true; - } - } - - virtual void reset_core() { - ni_smt_solver::reset_core(); - 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_core() { - switch_to_inc(); - SASSERT(m_context); - m_context->push(); - SASSERT(m_inc_mode); - } - - virtual void pop_core(unsigned n) { - switch_to_inc(); - SASSERT(m_context); - m_context->pop(n); - SASSERT(m_inc_mode); - } - - virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) { - if (!m_inc_mode) { - lbool r = ni_smt_solver::check_sat_core(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_solver.cpp b/src/smt/smt_solver.cpp index 5ca7d2dad..081649971 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -24,10 +24,11 @@ Notes: namespace smt { class solver : public solver_na2as { - front_end_params * m_params; - smt::kernel * m_context; + front_end_params * m_params; + smt::kernel * m_context; + progress_callback * m_callback; public: - solver():m_params(0), m_context(0) {} + solver():m_params(0), m_context(0), m_callback(0) {} virtual ~solver() { if (m_context != 0) @@ -63,6 +64,8 @@ namespace smt { #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); @@ -145,8 +148,9 @@ namespace smt { } virtual void set_progress_callback(progress_callback * callback) { - SASSERT(m_context); - m_context->set_progress_callback(callback); + m_callback = callback; + if (m_context) + m_context->set_progress_callback(callback); } virtual unsigned get_num_assertions() const { diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp index e9d5eba3e..f6d7414a5 100644 --- a/src/solver/solver_na2as.cpp +++ b/src/solver/solver_na2as.cpp @@ -20,6 +20,7 @@ Notes: --*/ #include"solver_na2as.h" +#include"ast_smt2_pp.h" solver_na2as::solver_na2as() { m_manager = 0; @@ -31,6 +32,9 @@ solver_na2as::~solver_na2as() { 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); diff --git a/src/solver/strategic_solver.cpp b/src/solver/strategic_solver.cpp index 84de62820..94414bcb1 100644 --- a/src/solver/strategic_solver.cpp +++ b/src/solver/strategic_solver.cpp @@ -268,10 +268,15 @@ 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";); 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"; + for (unsigned i = 0; i < num_assumptions; i++) { + tout << mk_ismt2_pp(assumptions[i], m()) << "\n"; + }); reset_results(); m_check_sat_executed = true; if (num_assumptions > 0 || // assumptions were provided @@ -355,6 +360,7 @@ 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";); if (m_use_inc_solver_results) { SASSERT(m_inc_solver); m_inc_solver->get_unsat_core(r); diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 00c0afaa5..1cf43a45c 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -18,7 +18,6 @@ Notes: --*/ #include"cmd_context.h" -#include"ni_solver.h" #include"strategic_solver_cmd.h" #include"qfbv_tactic.h" #include"qflia_tactic.h" @@ -80,13 +79,6 @@ 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); 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); From 181bdb681529b9457652acee5612788e3f11547a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 Nov 2012 14:18:12 -0700 Subject: [PATCH 15/17] removed dead files Signed-off-by: Leonardo de Moura --- src/cmd_context/strategic_solver_cmd.cpp | 34 ---------------- src/cmd_context/strategic_solver_cmd.h | 40 ------------------- src/tactic/portfolio/smt_strategic_solver.cpp | 2 +- 3 files changed, 1 insertion(+), 75 deletions(-) delete mode 100644 src/cmd_context/strategic_solver_cmd.cpp delete mode 100644 src/cmd_context/strategic_solver_cmd.h 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/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 1cf43a45c..b958c42b9 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -18,7 +18,7 @@ Notes: --*/ #include"cmd_context.h" -#include"strategic_solver_cmd.h" +#include"strategic_solver.h" #include"qfbv_tactic.h" #include"qflia_tactic.h" #include"qfnia_tactic.h" From b70687acc9948becaf6e46d807a4931a449eb279 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 Nov 2012 16:35:08 -0700 Subject: [PATCH 16/17] 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)); From c1587dc37d55aa168fbf5b6fd7f29a88882d9e52 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 Nov 2012 17:28:27 -0700 Subject: [PATCH 17/17] fixed some warnings reported by clang++ Signed-off-by: Leonardo de Moura --- src/ast/simplifier/poly_simplifier_plugin.h | 4 ++++ src/cmd_context/pdecl.h | 2 ++ src/muz_qe/pdr_context.h | 2 +- src/smt/theory_diff_logic.cpp | 2 ++ 4 files changed, 9 insertions(+), 1 deletion(-) 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/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/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h index 71b59ac26..1a6a3f9c6 100644 --- a/src/muz_qe/pdr_context.h +++ b/src/muz_qe/pdr_context.h @@ -270,7 +270,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/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; +};