From 2e32cf51f95ed00634f03b9f1afe9ec5dca4e7b0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Nov 2015 10:38:25 -0800 Subject: [PATCH] feat(library/blast/state): do not track dependecies to values --- src/library/blast/simple_strategy.cpp | 1 + src/library/blast/state.cpp | 4 ---- 2 files changed, 1 insertion(+), 4 deletions(-) diff --git a/src/library/blast/simple_strategy.cpp b/src/library/blast/simple_strategy.cpp index 4a75b6dbe..efc510800 100644 --- a/src/library/blast/simple_strategy.cpp +++ b/src/library/blast/simple_strategy.cpp @@ -70,6 +70,7 @@ class simple_strategy { optional search_upto(unsigned depth) { action_result r = next_action(); while (true) { + lean_assert(curr_state().check_invariant()); if (curr_state().get_proof_depth() > depth) r = action_result::failed(); switch (r.get_kind()) { diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index 0e731acd8..a30acf4c7 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -300,7 +300,6 @@ bool state::check_hypothesis(expr const & e, unsigned hidx, hypothesis const & h bool state::check_hypothesis(unsigned hidx, hypothesis const & h) const { lean_assert(check_hypothesis(h.get_type(), hidx, h)); - lean_assert(h.is_assumption() || check_hypothesis(*h.get_value(), hidx, h)); return true; } @@ -383,9 +382,6 @@ void state::add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user) { void state::add_deps(hypothesis & h_user, unsigned hidx_user) { add_deps(h_user.m_type, h_user, hidx_user); - if (!h_user.is_assumption()) { - add_deps(*h_user.m_value, h_user, hidx_user); - } } double state::compute_weight(unsigned hidx, expr const & /* type */) {