From 2549e49e72b70a81851289cbfa4e3ed4b4eca051 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 15 Nov 2015 13:32:43 -0800 Subject: [PATCH] feat(library/blast): add priority_queue for hypotheses we want to eliminate (apply recursion over) --- src/library/blast/state.cpp | 16 ++++++++++++++++ src/library/blast/state.h | 9 ++++++++- 2 files changed, 24 insertions(+), 1 deletion(-) diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index 8700c1d5c..231c47acc 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -425,6 +425,7 @@ void state::add_deps(hypothesis & h_user, unsigned hidx_user) { double state::compute_weight(unsigned hidx, expr const & /* type */) { // TODO(Leo): use heuristics and machine learning for computing the weight of a new hypothesis + // This method should not be here. return 1.0 / (static_cast(hidx) + 1.0); } @@ -608,6 +609,21 @@ optional state::activate_hypothesis() { } } +optional state::select_rec_hypothesis() { + while (true) { + if (m_branch.m_rec_queue.empty()) + return optional(); + unsigned hidx = m_branch.m_rec_queue.erase_min(); + hypothesis const * h_decl = get_hypothesis_decl(hidx); + if (!h_decl->is_dead()) + return optional(hidx); + } +} + +void state::add_to_rec_queue(hypothesis_idx hidx, double w) { + m_branch.m_rec_queue.insert(w, hidx); +} + bool state::hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const { if (auto s = m_branch.m_forward_deps.find(hidx_provider)) { return s->contains(hidx_user); diff --git a/src/library/blast/state.h b/src/library/blast/state.h index 019bbd112..de67a0eba 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -105,7 +105,9 @@ class branch { struct inv_double_cmp { int operator()(double const & d1, double const & d2) const { return d1 > d2 ? -1 : (d1 < d2 ? 1 : 0); } }; - typedef rb_map todo_queue; + typedef rb_map priority_queue; + typedef priority_queue todo_queue; + typedef priority_queue rec_queue; // Hypothesis/facts in the current state hypothesis_decls m_hyp_decls; // We break the set of hypotheses in m_hyp_decls in 4 sets that are not necessarily disjoint: @@ -126,6 +128,7 @@ class branch { hypothesis_idx_set m_assumption; hypothesis_idx_set m_active; todo_queue m_todo_queue; + rec_queue m_rec_queue; // priority queue for hypothesis we want to eliminate/recurse head_map m_head_to_hyps; forward_deps m_forward_deps; // given an entry (h -> {h_1, ..., h_n}), we have that each h_i uses h. expr m_target; @@ -260,6 +263,10 @@ public: /** \brief Activate the next hypothesis in the TODO queue, return none if the TODO queue is empty. */ optional activate_hypothesis(); + /** \brief Pick next hypothesis from the rec queue */ + optional select_rec_hypothesis(); + void add_to_rec_queue(hypothesis_idx hidx, double w); + /** \brief Store in \c r the hypotheses in this branch sorted by dependency depth */ void get_sorted_hypotheses(hypothesis_idx_buffer & r) const; /** \brief Sort hypotheses in r */