From 3ee32c02d83c4f1d58e326f58b5764eb04e1d204 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 23 Nov 2015 11:26:15 -0800 Subject: [PATCH] feat(library/blast/congruence_closure): add freeze_partitions API for qcf procedure --- src/library/blast/congruence_closure.cpp | 69 +++++++++++++++++------- src/library/blast/congruence_closure.h | 21 ++++++-- 2 files changed, 69 insertions(+), 21 deletions(-) diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp index d26a19549..b9e02329e 100644 --- a/src/library/blast/congruence_closure.cpp +++ b/src/library/blast/congruence_closure.cpp @@ -105,11 +105,11 @@ scope_congruence_closure::~scope_congruence_closure() { } void congruence_closure::initialize() { - mk_entry_core(get_iff_name(), mk_true(), false); - mk_entry_core(get_iff_name(), mk_false(), false); + mk_entry_core(get_iff_name(), mk_true(), false, true); + mk_entry_core(get_iff_name(), mk_false(), false, true); } -void congruence_closure::mk_entry_core(name const & R, expr const & e, bool to_propagate) { +void congruence_closure::mk_entry_core(name const & R, expr const & e, bool to_propagate, bool interpreted) { lean_assert(!m_entries.find(eqc_key(R, e))); entry n; n.m_next = e; @@ -117,6 +117,7 @@ void congruence_closure::mk_entry_core(name const & R, expr const & e, bool to_p n.m_cg_root = e; n.m_size = 1; n.m_flipped = false; + n.m_interpreted = interpreted; n.m_to_propagate = to_propagate; m_entries.insert(eqc_key(R, e), n); if (R != get_eq_name()) { @@ -149,7 +150,8 @@ void congruence_closure::mk_entry(name const & R, expr const & e, bool to_propag } return; } - mk_entry_core(R, e, to_propagate); + bool interpreted = false; + mk_entry_core(R, e, to_propagate, interpreted); } static bool all_distinct(buffer const & es) { @@ -573,15 +575,15 @@ void congruence_closure::internalize_core(name const & R, expr const & e, bool t case expr_kind::Sort: return; case expr_kind::Constant: case expr_kind::Local: - mk_entry_core(R, e, to_propagate); + mk_entry_core(R, e, to_propagate, false); return; case expr_kind::Lambda: - mk_entry_core(R, e, false); + mk_entry_core(R, e, false, false); return; case expr_kind::Macro: for (unsigned i = 0; i < macro_num_args(e); i++) internalize_core(R, macro_arg(e, i), false, false); - mk_entry_core(R, e, to_propagate); + mk_entry_core(R, e, to_propagate, false); break; case expr_kind::Pi: // TODO(Leo): should we support congruence for arrows? @@ -591,12 +593,12 @@ void congruence_closure::internalize_core(name const & R, expr const & e, bool t internalize_core(R, binding_body(e), toplevel, to_propagate); } if (is_prop(e)) { - mk_entry_core(R, e, false); + mk_entry_core(R, e, false, false); } return; case expr_kind::App: { bool is_lapp = is_logical_app(e); - mk_entry_core(R, e, to_propagate && !is_lapp); + mk_entry_core(R, e, to_propagate && !is_lapp, false); buffer args; expr const & fn = get_app_args(e, args); if (toplevel) { @@ -698,7 +700,7 @@ void congruence_closure::reinsert_parents(name const & R, expr const & e) { }); } -static bool is_interpreted(expr const & e) { +static bool is_true_or_false(expr const & e) { return is_constant(e, get_true_name()) || is_constant(e, get_false_name()); } @@ -724,7 +726,7 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con // anyway. // 2- r1->m_size > r2->m_size // Reason: performance. Condition was has precedence - if ((r1->m_size > r2->m_size && !is_interpreted(n2->m_root)) || is_interpreted(n1->m_root)) { + if ((r1->m_size > r2->m_size && !r2->m_interpreted) || r1->m_interpreted) { std::swap(e1, e2); std::swap(n1, n2); std::swap(r1, r2); @@ -732,6 +734,9 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con flipped = true; } + if (r1->m_interpreted && r2->m_interpreted) + m_inconsistent = true; + expr e1_root = n1->m_root; expr e2_root = n2->m_root; entry new_n1 = *n1; @@ -751,7 +756,7 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con remove_parents(R, e1); // force all m_root fields in e1 equivalence class to point to e2_root - bool propagate = R == get_iff_name() && is_interpreted(e2_root); + bool propagate = R == get_iff_name() && is_true_or_false(e2_root); buffer to_propagate; expr it = e1; do { @@ -838,11 +843,22 @@ void congruence_closure::process_todo() { } } -void congruence_closure::add_eqv(name const & R, expr const & lhs, expr const & rhs, expr const & H) { +void congruence_closure::add_eqv_core(name const & R, expr const & lhs, expr const & rhs, expr const & H) { push_todo(R, lhs, rhs, H); process_todo(); } +void congruence_closure::add_eqv(name const & R, expr const & lhs, expr const & rhs, expr const & H) { + if (is_inconsistent()) + return; + flet set_cc(g_cc, this); + clear_todo(); + bool toplevel = false; bool to_propagate = false; + internalize_core(R, lhs, toplevel, to_propagate); + internalize_core(R, rhs, toplevel, to_propagate); + add_eqv_core(R, lhs, rhs, H); +} + void congruence_closure::add(hypothesis_idx hidx) { if (is_inconsistent()) return; @@ -862,20 +878,20 @@ void congruence_closure::add(hypothesis_idx hidx) { if (is_neg) { bool toplevel = true; bool to_propagate = false; internalize_core(get_iff_name(), p, toplevel, to_propagate); - add_eqv(get_iff_name(), p, mk_false(), b.mk_iff_false_intro(h.get_self())); + add_eqv_core(get_iff_name(), p, mk_false(), b.mk_iff_false_intro(h.get_self())); } else { bool toplevel = false; bool to_propagate = false; internalize_core(R, lhs, toplevel, to_propagate); internalize_core(R, rhs, toplevel, to_propagate); - add_eqv(R, lhs, rhs, h.get_self()); + add_eqv_core(R, lhs, rhs, h.get_self()); } } else if (is_prop(p)) { bool toplevel = true; bool to_propagate = false; internalize_core(get_iff_name(), p, toplevel, to_propagate); if (is_neg) { - add_eqv(get_iff_name(), p, mk_false(), b.mk_iff_false_intro(h.get_self())); + add_eqv_core(get_iff_name(), p, mk_false(), b.mk_iff_false_intro(h.get_self())); } else { - add_eqv(get_iff_name(), p, mk_true(), b.mk_iff_true_intro(h.get_self())); + add_eqv_core(get_iff_name(), p, mk_true(), b.mk_iff_true_intro(h.get_self())); } } } catch (app_builder_exception &) {} @@ -1127,10 +1143,14 @@ optional congruence_closure::get_uneqv_proof(name const & R, expr const & } bool congruence_closure::is_inconsistent() const { - return is_eqv(get_iff_name(), mk_true(), mk_false()); + // If the m_inconsistent flag is true and partitions have not been frozen, then + // true and false must be in the same equivalence class. + lean_assert(!m_inconsistent || m_froze_partitions || is_eqv(get_iff_name(), mk_true(), mk_false())); + return m_inconsistent; } optional congruence_closure::get_inconsistency_proof() const { + lean_assert(!m_froze_partitions); try { app_builder & b = get_app_builder(); if (auto p = get_eqv_proof(get_iff_name(), mk_true(), mk_false())) { @@ -1148,6 +1168,7 @@ bool congruence_closure::proved(expr const & e) const { } optional congruence_closure::get_proof(expr const & e) const { + lean_assert(!m_froze_partitions); try { app_builder & b = get_app_builder(); if (auto p = get_eqv_proof(get_iff_name(), e, mk_true())) { @@ -1165,6 +1186,7 @@ bool congruence_closure::disproved(expr const & e) const { } optional congruence_closure::get_disproof(expr const & e) const { + lean_assert(!m_froze_partitions); try { app_builder & b = get_app_builder(); if (auto p = get_eqv_proof(get_iff_name(), e, mk_false())) { @@ -1201,6 +1223,17 @@ expr congruence_closure::get_next(name const & R, expr const & e) const { } } +void congruence_closure::freeze_partitions() { + m_froze_partitions = true; + entries new_entries; + m_entries.for_each([&](eqc_key const & k, entry e) { + if (k.m_expr == e.m_root) + e.m_interpreted = true; + new_entries.insert(k, e); + }); + m_entries = new_entries; +} + void congruence_closure::display_eqc(name const & R, expr const & e) const { auto out = diagnostic(env(), ios()); bool first = true; diff --git a/src/library/blast/congruence_closure.h b/src/library/blast/congruence_closure.h index 1c0f74e59..3d46ca1d3 100644 --- a/src/library/blast/congruence_closure.h +++ b/src/library/blast/congruence_closure.h @@ -45,6 +45,7 @@ class congruence_closure { optional m_proof; unsigned m_flipped:1; // proof has been flipped unsigned m_to_propagate:1; // must be propagated back to state when in equivalence class containing true/false + unsigned m_interpreted:1; // true if the node should be viewed as an abstract value unsigned m_size; // number of elements in the equivalence class, it is meaningless if 'e' != m_root }; @@ -99,7 +100,12 @@ class congruence_closure { parents m_parents; congruences m_congruences; list m_non_eq_relations; - + /** The congruence closure module has a mode where the root of + each equivalence class is marked as an interpreted/abstract + value. Moreover, in this mode proof production is disabled. + This capability is useful for heuristic instantiation. */ + bool m_froze_partitions{false}; + bool m_inconsistent{false}; void update_non_eq_relations(name const & R); void register_to_propagate(expr const & e); @@ -112,7 +118,7 @@ class congruence_closure { congr_key mk_congr_key(ext_congr_lemma const & lemma, expr const & e) const; void check_iff_true(congr_key const & k); - void mk_entry_core(name const & R, expr const & e, bool to_propagate); + void mk_entry_core(name const & R, expr const & e, bool to_propagate, bool interpreted); void mk_entry(name const & R, expr const & e, bool to_propagate); void add_occurrence(name const & Rp, expr const & parent, name const & Rc, expr const & child); void add_congruence_table(ext_congr_lemma const & lemma, expr const & e); @@ -121,7 +127,7 @@ class congruence_closure { void remove_parents(name const & R, expr const & e); void reinsert_parents(name const & R, expr const & e); void add_eqv_step(name const & R, expr e1, expr e2, expr const & H); - void add_eqv(name const & R, expr const & lhs, expr const & rhs, expr const & H); + void add_eqv_core(name const & R, expr const & lhs, expr const & rhs, expr const & H); expr mk_congr_proof_core(name const & R, expr const & lhs, expr const & rhs) const; expr mk_congr_proof(name const & R, expr const & lhs, expr const & rhs) const; @@ -159,8 +165,12 @@ public: If H is none of the forms above, this method does nothing. */ void add(hypothesis_idx hidx); + /** \brief Assert the equivalence (R a b) with proof H. */ + void add_eqv(name const & R, expr const & a, expr const & b, expr const & H); + /** \brief Return true if an inconsistency has been detected, i.e., true and false are in the same equivalence class */ bool is_inconsistent() const; + /** \brief Return the proof of inconsistency */ optional get_inconsistency_proof() const; @@ -185,6 +195,11 @@ public: expr get_root(name const & R, expr const & e) const; expr get_next(name const & R, expr const & e) const; + /** \brief Mark the root of each equivalence class as an "abstract value" + After this method is invoked, proof production is disabled. Moreover, + merging two different partitions will trigger an inconsistency. */ + void freeze_partitions(); + /** \brief dump for debugging purposes. */ void display() const; void display_eqcs() const;