michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/blast): add priority_queue for hypotheses we want to eliminate (apply recursion over)

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-15 13:32:43 -08:00
parent 4cd5e18bd0
commit 2549e49e72
2 changed files with 24 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/library/blast/state.cpp
View file

@ -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<double>(hidx) + 1.0);
}
@ -608,6 +609,21 @@ optional<unsigned> state::activate_hypothesis() {
}
}
optional<unsigned> state::select_rec_hypothesis() {
while (true) {
if (m_branch.m_rec_queue.empty())
return optional<unsigned>();
unsigned hidx = m_branch.m_rec_queue.erase_min();
hypothesis const * h_decl = get_hypothesis_decl(hidx);
if (!h_decl->is_dead())
return optional<unsigned>(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);

9
src/library/blast/state.h
View file

@ -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<double, hypothesis_idx, inv_double_cmp> todo_queue;
typedef rb_map<double, hypothesis_idx, inv_double_cmp> 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<hypothesis_idx> 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<hypothesis_idx> activate_hypothesis();
/** \brief Pick next hypothesis from the rec queue */
optional<hypothesis_idx> 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 */