feat(library/blast/state): add methods for deleting hypotheses
This commit is contained in:
parent
0a25652885
commit
2889ec5870
3 changed files with 162 additions and 25 deletions
|
@ -25,7 +25,7 @@ using hypothesis_idx_map = typename lean::rb_map<unsigned, T, unsigned_cmp>;
|
||||||
class hypothesis {
|
class hypothesis {
|
||||||
friend class state;
|
friend class state;
|
||||||
name m_name; // for pretty printing
|
name m_name; // for pretty printing
|
||||||
unsigned m_active:1;
|
unsigned m_dead:1;
|
||||||
unsigned m_dep_depth; // dependency depth
|
unsigned m_dep_depth; // dependency depth
|
||||||
unsigned m_proof_depth; // proof depth when the hypothesis was created
|
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.
|
hypothesis_idx_set m_deps; // hypotheses used by the type and/or value of this hypothesis.
|
||||||
|
@ -34,9 +34,9 @@ class hypothesis {
|
||||||
optional<expr> m_value; // justification for this object.
|
optional<expr> m_value; // justification for this object.
|
||||||
// Remark: if blast::is_local(m_value) is true, then the hypothesis is an assumption
|
// Remark: if blast::is_local(m_value) is true, then the hypothesis is an assumption
|
||||||
public:
|
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; }
|
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_dep_depth() const { return m_dep_depth; }
|
||||||
unsigned get_proof_depth() const { return m_proof_depth; }
|
unsigned get_proof_depth() const { return m_proof_depth; }
|
||||||
hypothesis_idx_set const & get_backward_deps() const { return m_deps; }
|
hypothesis_idx_set const & get_backward_deps() const { return m_deps; }
|
||||||
|
|
|
@ -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 {
|
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;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -337,8 +339,9 @@ struct hypothesis_dep_depth_lt {
|
||||||
};
|
};
|
||||||
|
|
||||||
void state::get_sorted_hypotheses(hypothesis_idx_buffer & r) const {
|
void state::get_sorted_hypotheses(hypothesis_idx_buffer & r) const {
|
||||||
m_branch.m_hyp_decls.for_each([&](unsigned hidx, hypothesis const &) {
|
m_branch.m_hyp_decls.for_each([&](unsigned hidx, hypothesis const & h) {
|
||||||
r.push_back(hidx);
|
if (!h.is_dead())
|
||||||
|
r.push_back(hidx);
|
||||||
});
|
});
|
||||||
std::sort(r.begin(), r.end(), hypothesis_dep_depth_lt(*this));
|
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) {
|
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))
|
if (!has_href(e) && !has_mref(e))
|
||||||
return; // nothing to be done
|
return; // nothing to be done
|
||||||
for_each(e, [&](expr const & l, unsigned) {
|
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());
|
return mk_hypothesis(hidx, name(*g_prefix, hidx), type, none_expr());
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void state::del_hypotheses(buffer<hypothesis_idx> 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<hypothesis_idx> & 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<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;
|
||||||
|
}
|
||||||
|
|
||||||
|
void state::collect_forward_deps(hypothesis_idx hidx, buffer<hypothesis_idx> & result) {
|
||||||
|
hypothesis_idx_set found;
|
||||||
|
collect_forward_deps(hidx, result, found);
|
||||||
|
}
|
||||||
|
|
||||||
|
bool state::del_hypotheses(buffer<hypothesis_idx> const & hs) {
|
||||||
|
hypothesis_idx_set found;
|
||||||
|
buffer<hypothesis_idx> 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<hypothesis_idx> 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<head_index> to_head_index(expr type) {
|
static optional<head_index> to_head_index(expr type) {
|
||||||
is_not(type, type);
|
is_not(type, type);
|
||||||
expr const & f = get_app_fn(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 */
|
/* 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<unsigned> state::activate_hypothesis() {
|
optional<unsigned> state::activate_hypothesis() {
|
||||||
if (m_branch.m_todo_queue.empty()) {
|
while (true) {
|
||||||
return optional<unsigned>();
|
if (m_branch.m_todo_queue.empty())
|
||||||
} else {
|
return optional<unsigned>();
|
||||||
unsigned hidx = m_branch.m_todo_queue.erase_min();
|
unsigned hidx = m_branch.m_todo_queue.erase_min();
|
||||||
m_branch.m_active.insert(hidx);
|
hypothesis const * h_decl = get_hypothesis_decl(hidx);
|
||||||
update_indices(hidx);
|
if (!h_decl->is_dead()) {
|
||||||
return optional<unsigned>(hidx);
|
m_branch.m_active.insert(hidx);
|
||||||
|
update_indices(hidx);
|
||||||
|
return optional<unsigned>(hidx);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -103,12 +103,13 @@ class branch {
|
||||||
typedef rb_map<double, hypothesis_idx, double_cmp> todo_queue;
|
typedef rb_map<double, hypothesis_idx, double_cmp> todo_queue;
|
||||||
// Hypothesis/facts in the current state
|
// Hypothesis/facts in the current state
|
||||||
hypothesis_decls m_hyp_decls;
|
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
|
// - assumption
|
||||||
// - active
|
// - active
|
||||||
// - todo
|
// - 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,
|
// A hypothesis is an "assumption" if it comes from the input goal,
|
||||||
// "intros" proof step, or an assumption obtained when applying an elimination step.
|
// "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_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(expr const & e, hypothesis & h_user, hypothesis_idx hidx_user);
|
||||||
void add_deps(hypothesis & h_user, hypothesis_idx hidx_user);
|
void add_deps(hypothesis & h_user, hypothesis_idx hidx_user);
|
||||||
|
void del_forward_dep(unsigned hidx_user, unsigned hidx_provider);
|
||||||
/** \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);
|
|
||||||
|
|
||||||
expr mk_hypothesis(hypothesis_idx new_hidx, name const & n, expr const & type, optional<expr> const & value);
|
expr mk_hypothesis(hypothesis_idx new_hidx, name const & n, expr const & type, optional<expr> const & value);
|
||||||
|
|
||||||
|
@ -159,6 +152,21 @@ class state {
|
||||||
|
|
||||||
expr mk_binding(bool is_lambda, unsigned num, expr const * hrefs, expr const & b) const;
|
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<hypothesis_idx> const & to_delete, hypothesis_idx_set const & to_delete_set);
|
||||||
|
void collect_forward_deps(hypothesis_idx hidx, buffer<hypothesis_idx> & result, hypothesis_idx_set & already_found);
|
||||||
|
bool safe_to_delete(buffer<hypothesis_idx> const & to_delete);
|
||||||
|
|
||||||
#ifdef LEAN_DEBUG
|
#ifdef LEAN_DEBUG
|
||||||
bool check_hypothesis(expr const & e, hypothesis_idx hidx, hypothesis const & h) const;
|
bool check_hypothesis(expr const & e, hypothesis_idx hidx, hypothesis const & h) const;
|
||||||
bool check_hypothesis(hypothesis_idx hidx, hypothesis const & h) const;
|
bool check_hypothesis(hypothesis_idx hidx, hypothesis const & h) const;
|
||||||
|
@ -191,12 +199,24 @@ public:
|
||||||
/************************
|
/************************
|
||||||
Hypotheses
|
Hypotheses
|
||||||
*************************/
|
*************************/
|
||||||
|
|
||||||
expr mk_hypothesis(name const & n, expr const & type, expr const & value);
|
expr mk_hypothesis(name const & n, expr const & type, expr const & value);
|
||||||
expr mk_hypothesis(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(name const & n, expr const & type);
|
||||||
expr mk_hypothesis(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<hypothesis_idx> const & hs);
|
||||||
|
|
||||||
|
/** \brief Collect all hypothesis in \c result that depend directly or indirectly on hidx */
|
||||||
|
void collect_forward_deps(hypothesis_idx hidx, buffer<hypothesis_idx> & result);
|
||||||
|
|
||||||
/** \brief Return true iff the hypothesis with index \c hidx_user depends on the hypothesis with index
|
/** \brief Return true iff the hypothesis with index \c hidx_user depends on the hypothesis with index
|
||||||
\c hidx_provider. */
|
\c hidx_provider. */
|
||||||
bool hidx_depends_on(hypothesis_idx hidx_user, hypothesis_idx hidx_provider) const;
|
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 */
|
/** \brief Return (active) hypotheses whose head symbol is equal to target or it is the negation of */
|
||||||
list<hypothesis_idx> get_head_related() const;
|
list<hypothesis_idx> 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
|
Abstracting hypotheses
|
||||||
*************************/
|
*************************/
|
||||||
|
|
Loading…
Reference in a new issue