From 63c896681664caef293aa45121d187322ba92dd5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 29 Sep 2015 14:08:14 -0700 Subject: [PATCH] refactor(library/blast): change how we mark fixed/frozen hypothesis --- src/library/blast/branch.cpp | 8 -------- src/library/blast/branch.h | 8 -------- src/library/blast/hypothesis.h | 4 +--- src/library/blast/state.cpp | 24 ++++++++++++++++++++---- src/library/blast/state.h | 15 +++++++++++++-- 5 files changed, 34 insertions(+), 25 deletions(-) diff --git a/src/library/blast/branch.cpp b/src/library/blast/branch.cpp index df6f3c717..486c46ec2 100644 --- a/src/library/blast/branch.cpp +++ b/src/library/blast/branch.cpp @@ -10,14 +10,6 @@ Author: Leonardo de Moura namespace lean { namespace blast { -void branch::fix_hypothesis(unsigned idx) { - auto h = m_context.find(idx); - lean_assert(h); - hypothesis new_h(*h); - new_h.mark_fixed(); - m_context.insert(idx, new_h); -} - struct hypothesis_depth_lt { branch const & m_branch; hypothesis_depth_lt(branch const & b): m_branch(b) {} diff --git a/src/library/blast/branch.h b/src/library/blast/branch.h index 1b70a014d..8c6bc8f60 100644 --- a/src/library/blast/branch.h +++ b/src/library/blast/branch.h @@ -26,14 +26,6 @@ class branch { hypothesis_idx_set m_target_deps; metavar_idx_set m_mvar_idxs; - /** \brief Mark a hypothesis as fixed. The type/value of a fixed hypothesis cannot be - modified. A hypothesis is fixed when it occurs in the type of some metavariable. */ - void fix_hypothesis(unsigned idx); - void fix_hypothesis(expr const & e) { - lean_assert(is_href(e)); - fix_hypothesis(href_index(e)); - } - void add_forward_dep(unsigned hidx_user, unsigned hidx_provider); void add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user); void add_deps(hypothesis & h_user, unsigned hidx_user); diff --git a/src/library/blast/hypothesis.h b/src/library/blast/hypothesis.h index 9a87d44ac..faac20feb 100644 --- a/src/library/blast/hypothesis.h +++ b/src/library/blast/hypothesis.h @@ -25,14 +25,13 @@ class hypothesis { friend class branch; name m_name; // for pretty printing unsigned m_active:1; - unsigned m_fixed:1; // occurs in the type of a metavariable, so we should not update its type. unsigned m_depth; hypothesis_idx_set m_deps; // hypotheses used by the type and/or value of this hypothesis. expr m_type; optional m_value; optional m_justification; public: - hypothesis():m_active(true), m_fixed(false), m_depth(0) {} + hypothesis():m_active(true), m_depth(0) {} name const & get_name() const { return m_name; } bool is_active() const { return m_active; } unsigned get_depth() const { return m_depth; } @@ -40,7 +39,6 @@ public: expr const & get_type() const { return m_type; } optional const & get_value() const { return m_value; } optional const & get_justification() const { return m_justification; } - void mark_fixed() { m_fixed = true; } /** \brief Return true iff this hypothesis depends on \c h. */ bool depends_on(expr const & h) const { return m_deps.contains(href_index(h)); } }; diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index 08444f053..753f441ff 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -13,24 +13,40 @@ namespace lean { namespace blast { state::state():m_next_mref_index(0) {} +/** \brief Mark that hypothesis h with index hidx is fixed by the meta-variable midx. + That is, `h` occurs in the type of `midx`. */ +void state::add_fixed_by(unsigned hidx, unsigned midx) { + if (auto s = m_fixed_by.find(hidx)) { + if (!s->contains(midx)) { + metavar_idx_set new_s(*s); + new_s.insert(midx); + m_fixed_by.insert(hidx, new_s); + } + } else { + metavar_idx_set new_s; + new_s.insert(midx); + m_fixed_by.insert(hidx, new_s); + } +} + expr state::mk_metavar(hypothesis_idx_buffer const & ctx, expr const & type) { hypothesis_idx_set ctx_as_set; for (unsigned const & hidx : ctx) ctx_as_set.insert(hidx); + unsigned midx = m_next_mref_index; for_each(type, [&](expr const & e, unsigned) { if (!has_href(e)) return false; if (is_href(e)) { lean_assert(ctx_as_set.contains(href_index(e))); - m_main.fix_hypothesis(e); + add_fixed_by(href_index(e), midx); return false; } return true; // continue search }); - unsigned idx = m_next_mref_index; m_next_mref_index++; - m_metavar_decls.insert(idx, metavar_decl(to_list(ctx), ctx_as_set, type)); - return blast::mk_mref(idx); + m_metavar_decls.insert(midx, metavar_decl(to_list(ctx), ctx_as_set, type)); + return blast::mk_mref(midx); } expr state::mk_metavar(expr const & type) { diff --git a/src/library/blast/state.h b/src/library/blast/state.h index 1e2eef519..0a47f0827 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -27,13 +27,24 @@ public: class state { friend class context; - typedef metavar_idx_map metavar_decls; - typedef metavar_idx_map assignment; + typedef metavar_idx_map metavar_decls; + typedef metavar_idx_map assignment; + typedef hypothesis_idx_map fixed_by; unsigned m_next_mref_index; metavar_decls m_metavar_decls; assignment m_assignment; branch m_main; + // In the following mapping, each entry (h -> {m_1 ... m_n}) means that hypothesis `h` cannot be cleared + // in any branch where the metavariables m_1 ... m_n have not been replaced with the values assigned to them. + // That is, to be able to clear `h` in a branch `B`, we first need to check whether it + // is contained in this mapping or not. If it is, we should check whether any of the + // metavariables `m_1` ... `m_n` occur in `B` (this is a relatively quick check since + // `B` contains an over-approximation of all meta-variables occuring in it (i.e., m_mvar_idxs). + // If this check fails, then we should replace any assigned `m_i` with its value, if the intersection is still + // non-empty, then we cannot clear `h`. + fixed_by m_fixed_by; + void add_fixed_by(unsigned hidx, unsigned midx); unsigned add_metavar_decl(metavar_decl const & decl); goal to_goal(branch const &) const;