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; };