From 9921228dd5fa8cbf79d028d4704dbf7f75b5e7c1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 14 Nov 2015 13:16:00 -0800 Subject: [PATCH] feat(library/blast): add simp_rule_sets to branch --- src/library/blast/simple_strategy.cpp | 1 + src/library/blast/state.h | 12 ++++++++++++ 2 files changed, 13 insertions(+) diff --git a/src/library/blast/simple_strategy.cpp b/src/library/blast/simple_strategy.cpp index 9a63fedc4..bfcd240a1 100644 --- a/src/library/blast/simple_strategy.cpp +++ b/src/library/blast/simple_strategy.cpp @@ -155,6 +155,7 @@ class simple_strategy { } optional search() { + curr_state().set_simp_rule_sets(get_simp_rule_sets(env())); state s = curr_state(); unsigned d = m_config.m_init_depth; while (true) { diff --git a/src/library/blast/state.h b/src/library/blast/state.h index 8123b0c2a..e42f348ee 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "kernel/expr.h" #include "library/head_map.h" #include "library/tactic/goal.h" +#include "library/simplifier/simp_rule_set.h" #include "library/blast/action_result.h" #include "library/blast/hypothesis.h" @@ -129,6 +130,7 @@ 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; + simp_rule_sets m_simp_rule_sets; }; /** \brief Proof state for the blast tactic */ @@ -400,6 +402,16 @@ public: assignment_snapshot save_assignment(); void restore_assignment(assignment_snapshot const & s); + /************************ + Simplification rules + *************************/ + void set_simp_rule_sets(simp_rule_sets const & s) { + m_branch.m_simp_rule_sets = s; + } + simp_rule_sets get_simp_rule_sets() const { + return m_branch.m_simp_rule_sets; + } + /************************ Debugging support *************************/