From 48eb6cb138c5d6b545296d99e598564782b224a3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 10 Nov 2015 17:27:39 -0800 Subject: [PATCH] refactor(library/blast/state): simplify state --- src/library/blast/state.cpp | 32 -------------------------------- src/library/blast/state.h | 14 -------------- 2 files changed, 46 deletions(-) diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index a70308f32..5a24853fa 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -29,34 +29,8 @@ bool metavar_decl::restrict_context_using(metavar_decl const & other) { state::state() {} -/** \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_set const & c, expr const & type) { unsigned midx = mk_mref_idx(); - for_each(type, [&](expr const & e, unsigned) { - if (!has_href(e)) - return false; - if (is_href(e)) { - lean_assert(c.contains(href_index(e))); - add_fixed_by(href_index(e), midx); - return false; - } - return true; // continue search - }); m_metavar_decls.insert(midx, metavar_decl(c, type)); return blast::mk_mref(midx); } @@ -406,9 +380,6 @@ void state::add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user) { add_forward_dep(hidx_user, hidx_provider); } return false; - } else if (is_mref(l)) { - m_branch.m_mvar_idxs.insert(mref_index(l)); - return false; } else { return true; } @@ -496,9 +467,6 @@ void state::set_target(expr const & t) { } else if (is_href(e)) { m_branch.m_target_deps.insert(href_index(e)); return false; - } else if (is_mref(e)) { - m_branch.m_mvar_idxs.insert(mref_index(e)); - return false; } else { return true; } diff --git a/src/library/blast/state.h b/src/library/blast/state.h index 31f328148..bb9b37304 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -103,7 +103,6 @@ class branch { 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; - metavar_idx_set m_mvar_idxs; }; /** \brief Proof state for the blast tactic */ @@ -111,20 +110,10 @@ class state { typedef metavar_idx_map metavar_decls; typedef metavar_idx_map eassignment; typedef metavar_idx_map uassignment; - typedef hypothesis_idx_map fixed_by; typedef list proof_steps; uassignment m_uassignment; metavar_decls m_metavar_decls; eassignment m_eassignment; - // 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; unsigned m_proof_depth{0}; proof_steps m_proof_steps; branch m_branch; @@ -144,7 +133,6 @@ class state { expr mk_hypothesis(unsigned new_hidx, name const & n, expr const & type, optional const & value); - void add_fixed_by(unsigned hidx, unsigned midx); unsigned add_metavar_decl(metavar_decl const & decl); goal to_goal(branch const &) const; @@ -173,8 +161,6 @@ public: metavar_decl const * get_metavar_decl(unsigned idx) const { return m_metavar_decls.find(idx); } metavar_decl const * get_metavar_decl(expr const & e) const { return get_metavar_decl(mref_index(e)); } - bool has_mvar(expr const & e) const { return m_branch.m_mvar_idxs.contains(mref_index(e)); } - /************************ Save/Restore branch *************************/