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

refactor(library/blast/state): simplify blast state

Browse source
This commit is contained in:
Leonardo de Moura 2016-03-01 14:27:58 -08:00
parent 16dc021736
commit 2a4b3b75bd
2 changed files with 30 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -99,7 +99,6 @@ branch::branch(branch const & b):
m_todo_queue(b.m_todo_queue),
m_forward_deps(b.m_forward_deps),
m_target(b.m_target),
m_target_deps(b.m_target_deps),
m_hyp_index(b.m_hyp_index) {
unsigned n = get_extension_manager().get_num_extensions();
m_extensions = new branch_extension*[n];
@ -117,7 +116,6 @@ branch::branch(branch && b):
m_todo_queue(std::move(b.m_todo_queue)),
m_forward_deps(std::move(b.m_forward_deps)),
m_target(std::move(b.m_target)),
m_target_deps(std::move(b.m_target_deps)),
m_hyp_index(std::move(b.m_hyp_index)) {
unsigned n = get_extension_manager().get_num_extensions();
m_extensions = new branch_extension*[n];
@ -135,7 +133,6 @@ void branch::swap(branch & b) {
std::swap(m_hyp_index, b.m_hyp_index);
std::swap(m_forward_deps, b.m_forward_deps);
std::swap(m_target, b.m_target);
std::swap(m_target_deps, b.m_target_deps);
std::swap(m_extensions, b.m_extensions);
}
@ -623,6 +620,10 @@ void state::add_deps(hypothesis & h_user, unsigned hidx_user) {
add_deps(h_user.m_type, h_user, hidx_user);
}
bool state::has_target_forward_deps(hypothesis_idx hidx) const {
return has_forward_deps(hidx) || target_depends_on(hidx);
}
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.
@ -707,25 +708,13 @@ void state::collect_forward_deps(hypothesis_idx hidx, hypothesis_idx_buffer_set
}
}
/* Return true iff the target type does not depend on any of the hypotheses in to_delete */
bool state::safe_to_delete(buffer<hypothesis_idx> 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;
}
bool state::del_hypotheses(buffer<hypothesis_idx> const & hs) {
hypothesis_idx_buffer_set to_delete;
for (hypothesis_idx hidx : hs) {
to_delete.insert(hidx);
collect_forward_deps(hidx, to_delete);
}
if (!safe_to_delete(to_delete.as_buffer()))
if (target_depends_on(to_delete.as_buffer()))
return false;
del_hypotheses(to_delete.as_buffer(), to_delete.as_set());
return true;
@ -735,7 +724,7 @@ bool state::del_hypothesis(hypothesis_idx hidx) {
hypothesis_idx_buffer_set to_delete;
to_delete.insert(hidx);
collect_forward_deps(hidx, to_delete);
if (!safe_to_delete(to_delete.as_buffer()))
if (target_depends_on(to_delete.as_buffer()))
return false;
del_hypotheses(to_delete.as_buffer(), to_delete.as_set());
return true;
@ -902,19 +891,6 @@ bool state::hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const {
void state::set_target(expr const & t) {
m_branch.m_target = t;
m_branch.m_target_deps.clear();
if (has_href(t) || has_mref(t)) {
for_each(t, [&](expr const & e, unsigned) {
if (!has_href(e) && !has_mref(e)) {
return false;
} else if (is_href(e)) {
m_branch.m_target_deps.insert(href_index(e));
return false;
} else {
return true;
}
});
}
unsigned n = get_extension_manager().get_num_extensions();
for (unsigned i = 0; i < n; i++) {
branch_extension * ext = get_extension_core(i);
@ -922,6 +898,27 @@ void state::set_target(expr const & t) {
}
}
bool state::target_depends_on(buffer<hypothesis_idx> const & hidxs) const {
bool found_href = false;
for_each(m_branch.m_target, [&](expr const & e, unsigned) {
if (found_href) return false;
if (!has_local(e)) return false;
if (is_href(e)) {
if (std::find(hidxs.begin(), hidxs.end(), href_index(e)) != hidxs.end())
found_href = true;
return false;
}
return true; // continue;
});
return found_href;
}
bool state::target_depends_on(hypothesis_idx hidx) const {
buffer<hypothesis_idx> hidxs;
hidxs.push_back(hidx);
return target_depends_on(hidxs);
}
bool state::target_depends_on(expr const & h) const {
return target_depends_on(href_index(h));
}

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

@ -154,7 +154,6 @@ class branch {
todo_queue m_todo_queue;
forward_deps m_forward_deps; // given an entry (h -> {h_1, ..., h_n}), we have that each h_i uses h.
expr m_target;
hypothesis_idx_set m_target_deps;
discr_tree m_hyp_index;
branch_extension ** m_extensions;
public:
@ -205,7 +204,6 @@ class state {
void remove_from_indices(hypothesis const & h, hypothesis_idx hidx);
void del_hypotheses(buffer<hypothesis_idx> const & to_delete, hypothesis_idx_set const & to_delete_set);
bool safe_to_delete(buffer<hypothesis_idx> const & to_delete);
void display_active(std::ostream & out) const;
@ -264,9 +262,7 @@ public:
hypothesis_idx_set get_direct_forward_deps(hypothesis_idx hidx) const;
bool has_forward_deps(hypothesis_idx hidx) const { return !get_direct_forward_deps(hidx).empty(); }
/** \brief Return true iff other hypotheses or the target type depends on hidx. */
bool has_target_forward_deps(hypothesis_idx hidx) const {
return has_forward_deps(hidx) || m_branch.m_target_deps.contains(hidx);
}
bool has_target_forward_deps(hypothesis_idx hidx) const;
/** \brief Collect in \c result the hypotheses that (directly) depend on \c hidx and satisfy \c pred. */
template<typename P>
void collect_direct_forward_deps(hypothesis_idx hidx, hypothesis_idx_buffer_set & result, P && pred) {
@ -354,7 +350,8 @@ public:
void set_target(expr const & t);
expr const & get_target() const { return m_branch.m_target; }
/** \brief Return true iff the target depends on the given hypothesis */
bool target_depends_on(hypothesis_idx hidx) const { return m_branch.m_target_deps.contains(hidx); }
bool target_depends_on(buffer<hypothesis_idx> const & hidxs) const;
bool target_depends_on(hypothesis_idx hidx) const;
bool target_depends_on(expr const & h) const;
/************************