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