From 2889ec58704ce09038146ccbfc5ff7ba6dcd99fe Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Nov 2015 11:59:34 -0800 Subject: [PATCH] feat(library/blast/state): add methods for deleting hypotheses --- src/library/blast/hypothesis.h | 6 +- src/library/blast/state.cpp | 134 ++++++++++++++++++++++++++++++--- src/library/blast/state.h | 47 +++++++++--- 3 files changed, 162 insertions(+), 25 deletions(-) diff --git a/src/library/blast/hypothesis.h b/src/library/blast/hypothesis.h index 209215d89..f1b35b566 100644 --- a/src/library/blast/hypothesis.h +++ b/src/library/blast/hypothesis.h @@ -25,7 +25,7 @@ using hypothesis_idx_map = typename lean::rb_map; class hypothesis { friend class state; name m_name; // for pretty printing - unsigned m_active:1; + unsigned m_dead:1; unsigned m_dep_depth; // dependency depth unsigned m_proof_depth; // proof depth when the hypothesis was created hypothesis_idx_set m_deps; // hypotheses used by the type and/or value of this hypothesis. @@ -34,9 +34,9 @@ class hypothesis { optional m_value; // justification for this object. // Remark: if blast::is_local(m_value) is true, then the hypothesis is an assumption public: - hypothesis():m_active(false), m_dep_depth(0) {} + hypothesis():m_dead(false), m_dep_depth(0) {} name const & get_name() const { return m_name; } - bool is_active() const { return m_active; } + bool is_dead() const { return m_dead; } unsigned get_dep_depth() const { return m_dep_depth; } unsigned get_proof_depth() const { return m_proof_depth; } hypothesis_idx_set const & get_backward_deps() const { return m_deps; } diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index a30acf4c7..d438fd230 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -299,7 +299,9 @@ bool state::check_hypothesis(expr const & e, unsigned hidx, hypothesis const & h } bool state::check_hypothesis(unsigned hidx, hypothesis const & h) const { - lean_assert(check_hypothesis(h.get_type(), hidx, h)); + if (!h.is_dead()) { + lean_assert(check_hypothesis(h.get_type(), hidx, h)); + } return true; } @@ -337,8 +339,9 @@ struct hypothesis_dep_depth_lt { }; void state::get_sorted_hypotheses(hypothesis_idx_buffer & r) const { - m_branch.m_hyp_decls.for_each([&](unsigned hidx, hypothesis const &) { - r.push_back(hidx); + m_branch.m_hyp_decls.for_each([&](unsigned hidx, hypothesis const & h) { + if (!h.is_dead()) + r.push_back(hidx); }); std::sort(r.begin(), r.end(), hypothesis_dep_depth_lt(*this)); } @@ -357,7 +360,17 @@ void state::add_forward_dep(unsigned hidx_user, unsigned hidx_provider) { } } +void state::del_forward_dep(unsigned hidx_user, unsigned hidx_provider) { + auto s = m_branch.m_forward_deps.find(hidx_provider); + lean_assert(s); + lean_assert(s->contains(hidx_user)); + hypothesis_idx_set new_s(*s); + new_s.erase(hidx_user); + m_branch.m_forward_deps.insert(hidx_provider, new_s); +} + void state::add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user) { + lean_assert(!h_user.is_dead()); if (!has_href(e) && !has_mref(e)) return; // nothing to be done for_each(e, [&](expr const & l, unsigned) { @@ -424,6 +437,99 @@ expr state::mk_hypothesis(expr const & type) { return mk_hypothesis(hidx, name(*g_prefix, hidx), type, none_expr()); } +void state::del_hypotheses(buffer const & to_delete, hypothesis_idx_set const & to_delete_set) { + for (hypothesis_idx h : to_delete) { + hypothesis h_decl = *get_hypothesis_decl(h); + if (m_branch.m_active.contains(h)) { + m_branch.m_active.erase(h); + remove_from_indices(h_decl, h); + } + m_branch.m_assumption.erase(h); + m_branch.m_forward_deps.erase(h); + h_decl.m_deps.for_each([&](hypothesis_idx h_dep) { + if (to_delete_set.contains(h_dep)) { + // we don't need to update forward deps for h_dep since + // it will also be deleted. + return; + } + del_forward_dep(h, h_dep); + }); + h_decl.m_deps = hypothesis_idx_set(); + h_decl.m_dead = true; + m_branch.m_hyp_decls.insert(h, h_decl); + // Remark: we don't remove h from m_todo_queue. It is too expensive. + // So, the method activate_hypothesis MUST check whether the candidate + // hypothesis is dead or not. + } +} + +void state::collect_forward_deps(hypothesis_idx hidx, buffer & result, hypothesis_idx_set & already_found) { + unsigned qhead = result.size(); + while (true) { + hypothesis_idx_set s = get_forward_deps(hidx); + s.for_each([&](hypothesis_idx h_dep) { + if (already_found.contains(h_dep)) + return; + already_found.insert(h_dep); + result.push_back(h_dep); + }); + if (qhead == result.size()) + return; + hidx = result[qhead]; + qhead++; + } +} + +/* Return true iff the target type does not depend on any of the hypotheses in to_delete */ +bool state::safe_to_delete(buffer const & to_delete) { + for (hypothesis_idx h : to_delete) { + if (m_branch.m_target_deps.contains(h)) { + // h cannot be deleted since the target type + // depends on it. + return false; + } + } + return true; +} + +void state::collect_forward_deps(hypothesis_idx hidx, buffer & result) { + hypothesis_idx_set found; + collect_forward_deps(hidx, result, found); +} + +bool state::del_hypotheses(buffer const & hs) { + hypothesis_idx_set found; + buffer to_delete; + for (hypothesis_idx hidx : hs) { + to_delete.push_back(hidx); + found.insert(hidx); + collect_forward_deps(hidx, to_delete, found); + } + if (!safe_to_delete(to_delete)) + return false; + del_hypotheses(to_delete, found); + return true; +} + +bool state::del_hypothesis(hypothesis_idx hidx) { + hypothesis_idx_set found; + buffer to_delete; + to_delete.push_back(hidx); + found.insert(hidx); + collect_forward_deps(hidx, to_delete, found); + if (!safe_to_delete(to_delete)) + return false; + del_hypotheses(to_delete, found); + return true; +} + +hypothesis_idx_set state::get_forward_deps(hypothesis_idx hidx) const { + if (auto r = m_branch.m_forward_deps.find(hidx)) + return *r; + else + return hypothesis_idx_set(); +} + static optional to_head_index(expr type) { is_not(type, type); expr const & f = get_app_fn(type); @@ -470,14 +576,22 @@ void state::update_indices(hypothesis_idx hidx) { /* TODO(Leo): update congruence closure indices */ } +void state::remove_from_indices(hypothesis const & h, hypothesis_idx hidx) { + if (auto i = to_head_index(h)) + m_branch.m_head_to_hyps.erase(*i, hidx); +} + optional state::activate_hypothesis() { - if (m_branch.m_todo_queue.empty()) { - return optional(); - } else { - unsigned hidx = m_branch.m_todo_queue.erase_min(); - m_branch.m_active.insert(hidx); - update_indices(hidx); - return optional(hidx); + while (true) { + if (m_branch.m_todo_queue.empty()) + return optional(); + unsigned hidx = m_branch.m_todo_queue.erase_min(); + hypothesis const * h_decl = get_hypothesis_decl(hidx); + if (!h_decl->is_dead()) { + m_branch.m_active.insert(hidx); + update_indices(hidx); + return optional(hidx); + } } } diff --git a/src/library/blast/state.h b/src/library/blast/state.h index 4ae91ab3b..e58d2df7a 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -103,12 +103,13 @@ class branch { typedef rb_map todo_queue; // Hypothesis/facts in the current state hypothesis_decls m_hyp_decls; - // We break the set of hypotheses in m_context in 3 sets that are not necessarily disjoint: + // We break the set of hypotheses in m_hyp_decls in 4 sets that are not necessarily disjoint: // - assumption // - active // - todo + // - dead // - // The sets active and todo are disjoint. + // The sets active and todo are disjoint. The set dead is also disjoint from the other sets. // // A hypothesis is an "assumption" if it comes from the input goal, // "intros" proof step, or an assumption obtained when applying an elimination step. @@ -142,15 +143,7 @@ class state { void add_forward_dep(hypothesis_idx hidx_user, hypothesis_idx hidx_provider); void add_deps(expr const & e, hypothesis & h_user, hypothesis_idx hidx_user); void add_deps(hypothesis & h_user, hypothesis_idx hidx_user); - - /** \brief Compute the weight of a hypothesis with the given type - We use this weight to update the todo_queue. */ - double compute_weight(hypothesis_idx hidx, expr const & type); - - /** \brief This method is invoked when a hypothesis move from todo to active. - - We will update indices and data-structures (e.g., congruence closure). */ - void update_indices(hypothesis_idx hidx); + void del_forward_dep(unsigned hidx_user, unsigned hidx_provider); expr mk_hypothesis(hypothesis_idx new_hidx, name const & n, expr const & type, optional const & value); @@ -159,6 +152,21 @@ class state { expr mk_binding(bool is_lambda, unsigned num, expr const * hrefs, expr const & b) const; + /** \brief Compute the weight of a hypothesis with the given type + We use this weight to update the todo_queue. */ + double compute_weight(hypothesis_idx hidx, expr const & type); + + /** \brief This method is invoked when a hypothesis move from todo to active. + We will update indices and data-structures (e.g., congruence closure). */ + void update_indices(hypothesis_idx hidx); + + /** \brief Remove the given hypothesis from indexing data-structures */ + void remove_from_indices(hypothesis const & h, hypothesis_idx hidx); + + void del_hypotheses(buffer const & to_delete, hypothesis_idx_set const & to_delete_set); + void collect_forward_deps(hypothesis_idx hidx, buffer & result, hypothesis_idx_set & already_found); + bool safe_to_delete(buffer const & to_delete); + #ifdef LEAN_DEBUG bool check_hypothesis(expr const & e, hypothesis_idx hidx, hypothesis const & h) const; bool check_hypothesis(hypothesis_idx hidx, hypothesis const & h) const; @@ -191,12 +199,24 @@ public: /************************ Hypotheses *************************/ - expr mk_hypothesis(name const & n, expr const & type, expr const & value); expr mk_hypothesis(expr const & type, expr const & value); expr mk_hypothesis(name const & n, expr const & type); expr mk_hypothesis(expr const & type); + /** \brief Delete the given hypothesis and any other hypothesis that depends on it. + The procedure is only performed if the target does not depend on the given hypothesis. + Return true if success, and failure otherwise (target depends on hidx). + + The hypothesese objects are not really deleted, we keep them at m_hyp_decls, + but they are removed from all indexing data-structures. + */ + bool del_hypothesis(hypothesis_idx hidx); + bool del_hypotheses(buffer const & hs); + + /** \brief Collect all hypothesis in \c result that depend directly or indirectly on hidx */ + void collect_forward_deps(hypothesis_idx hidx, buffer & result); + /** \brief Return true iff the hypothesis with index \c hidx_user depends on the hypothesis with index \c hidx_provider. */ bool hidx_depends_on(hypothesis_idx hidx_user, hypothesis_idx hidx_provider) const; @@ -230,6 +250,9 @@ public: /** \brief Return (active) hypotheses whose head symbol is equal to target or it is the negation of */ list get_head_related() const; + /** \brief Return the set of hypotheses that (directly) depend on the given one */ + hypothesis_idx_set get_forward_deps(hypothesis_idx hidx) const; + /************************ Abstracting hypotheses *************************/