From f0ccffe96889f6262ebb0963ea88962da28bcd2b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 23 Nov 2015 15:03:46 -0800 Subject: [PATCH] feat(library/blast/congruence_closure): track mod-time --- src/library/blast/congruence_closure.cpp | 19 +++++++++++++++++++ src/library/blast/congruence_closure.h | 13 +++++++++++-- 2 files changed, 30 insertions(+), 2 deletions(-) diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp index 0e7bc2f196..75eb9162f8 100644 --- a/src/library/blast/congruence_closure.cpp +++ b/src/library/blast/congruence_closure.cpp @@ -120,6 +120,7 @@ void congruence_closure::mk_entry_core(name const & R, expr const & e, bool to_p n.m_flipped = false; n.m_interpreted = interpreted; n.m_to_propagate = to_propagate; + n.m_mt = m_gmt; m_entries.insert(eqc_key(R, e), n); if (R != get_eq_name()) { // lift equalities to R @@ -699,6 +700,22 @@ void congruence_closure::reinsert_parents(name const & R, expr const & e) { }); } +void congruence_closure::update_mt(name const & R, expr const & e) { + expr r = get_root(R, e); + auto ps = m_parents.find(child_key(R, r)); + if (!ps) return; + ps->for_each([&](parent_occ const & p) { + auto it = m_entries.find(p); + lean_assert(it); + if (it->m_mt < m_gmt) { + auto new_it = *it; + new_it.m_mt = m_gmt; + m_entries.insert(p, new_it); + update_mt(p.m_R, p.m_expr); + } + }); +} + static bool is_true_or_false(expr const & e) { return is_constant(e, get_true_name()) || is_constant(e, get_false_name()); } @@ -832,6 +849,8 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con } } + update_mt(R, e2_root); + if (get_config().m_trace_cc) { diagnostic(env(), ios()) << "added equivalence " << ppb(e1) << " [" << R << "] " << ppb(e2) << "\n"; display(); diff --git a/src/library/blast/congruence_closure.h b/src/library/blast/congruence_closure.h index 00ec0b79df..2c680fa2c0 100644 --- a/src/library/blast/congruence_closure.h +++ b/src/library/blast/congruence_closure.h @@ -47,6 +47,11 @@ class congruence_closure { 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 + unsigned m_mt; + // The field m_mt is used to implement the mod-time optimization introduce by the Simplify theorem prover. + // The basic idea is to introduce a counter gmt that records the number of heuristic instantiation that have + // occurred in the current branch. It is incremented after each round of heuristic instantiation. + // The field m_mt records the last time any proper descendant of of thie entry was involved in a merge. }; /* Key (R, e) for the mapping (R, e) -> entry */ @@ -104,8 +109,9 @@ class congruence_closure { 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}; + short m_froze_partitions{false}; + short m_inconsistent{false}; + unsigned m_gmt{0}; void update_non_eq_relations(name const & R); void register_to_propagate(expr const & e); @@ -126,6 +132,7 @@ class congruence_closure { void invert_trans(name const & R, expr const & e); void remove_parents(name const & R, expr const & e); void reinsert_parents(name const & R, expr const & e); + void update_mt(name const & R, expr const & e); void add_eqv_step(name const & R, expr e1, expr e2, expr const & H); void add_eqv_core(name const & R, expr const & lhs, expr const & rhs, expr const & H); @@ -200,6 +207,8 @@ public: merging two different partitions will trigger an inconsistency. */ void freeze_partitions(); + void inc_gmt() { m_gmt++; } + /** \brief dump for debugging purposes. */ void display() const; void display_eqcs() const;