From 9bdf3a0d33d83f21460d7a1ed0ae38d425379730 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 9 Nov 2015 12:41:52 -0800 Subject: [PATCH] refactor(library/blast): we should reuse uref/mref/href in idxs Motivation: avoid nasty bugs when caching results --- src/library/blast/blast.cpp | 5 +++-- src/library/blast/branch.cpp | 11 +++++++---- src/library/blast/branch.h | 3 ++- src/library/blast/expr.cpp | 28 ++++++++++++++++++++++++++++ src/library/blast/expr.h | 10 ++++++++++ src/library/blast/state.cpp | 11 ++--------- src/library/blast/state.h | 4 ---- 7 files changed, 52 insertions(+), 20 deletions(-) diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index d57825b07..fc306403f 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -191,7 +191,7 @@ class blastenv { } virtual level mk_uvar() { - return m_benv.m_curr_state.mk_uref(); + return mk_fresh_uref(); } virtual expr mk_mvar(expr const & type) { @@ -238,7 +238,7 @@ class blastenv { if (auto r = m_uvar2uref.find(meta_id(l))) { return *r; } else { - level uref = m_state.mk_uref(); + level uref = mk_fresh_uref(); m_uvar2uref.insert(meta_id(l), uref); return uref; } @@ -547,6 +547,7 @@ public: m_fun_info_manager(*m_tmp_ctx), m_congr_lemma_manager(m_app_builder, m_fun_info_manager), m_tctx(*this) { + init_uref_mref_href_idxs(); set_options(m_ios.get_options()); } diff --git a/src/library/blast/branch.cpp b/src/library/blast/branch.cpp index 3744da2c2..df7aed162 100644 --- a/src/library/blast/branch.cpp +++ b/src/library/blast/branch.cpp @@ -80,13 +80,11 @@ double branch::compute_weight(unsigned hidx, expr const & /* type */) { return 1.0 / (static_cast(hidx) + 1.0); } -expr branch::add_hypothesis(name const & n, expr const & type, expr const & value) { +expr branch::add_hypothesis(unsigned new_hidx, name const & n, expr const & type, expr const & value) { hypothesis new_h; new_h.m_name = n; new_h.m_type = type; new_h.m_value = value; - unsigned new_hidx = m_next; - m_next++; add_deps(new_h, new_hidx); m_context.insert(new_hidx, new_h); if (new_h.is_assumption()) @@ -98,8 +96,13 @@ expr branch::add_hypothesis(name const & n, expr const & type, expr const & valu static name * g_prefix = nullptr; +expr branch::add_hypothesis(name const & n, expr const & type, expr const & value) { + return add_hypothesis(mk_href_idx(), n, type, value); +} + expr branch::add_hypothesis(expr const & type, expr const & value) { - return add_hypothesis(name(*g_prefix, m_next), type, value); + unsigned hidx = mk_href_idx(); + return add_hypothesis(hidx, name(*g_prefix, hidx), type, value); } void branch::update_indices(unsigned /* hidx */) { diff --git a/src/library/blast/branch.h b/src/library/blast/branch.h index 71bf10926..efe96b160 100644 --- a/src/library/blast/branch.h +++ b/src/library/blast/branch.h @@ -21,7 +21,6 @@ class branch { typedef hypothesis_idx_map forward_deps; typedef rb_map todo_queue; friend class state; - unsigned m_next{0}; context m_context; // We break the set of hypotheses in m_context in 3 sets that are not necessarily disjoint: // - assumption @@ -59,6 +58,8 @@ class branch { We will update indices and data-structures (e.g., congruence closure). */ void update_indices(unsigned hidx); + expr add_hypothesis(unsigned new_hidx, name const & n, expr const & type, expr const & value); + public: branch() {} diff --git a/src/library/blast/expr.cpp b/src/library/blast/expr.cpp index 17660aa34..0abeebfc7 100644 --- a/src/library/blast/expr.cpp +++ b/src/library/blast/expr.cpp @@ -65,6 +65,34 @@ bool has_mref(expr const & e) { return lean::has_expr_metavar(e); } +LEAN_THREAD_VALUE(unsigned, m_next_uref_idx, 0); +LEAN_THREAD_VALUE(unsigned, m_next_mref_idx, 0); +LEAN_THREAD_VALUE(unsigned, m_next_href_idx, 0); + +unsigned mk_uref_idx() { + unsigned r = m_next_uref_idx; + m_next_uref_idx++; + return r; +} + +unsigned mk_mref_idx() { + unsigned r = m_next_mref_idx; + m_next_mref_idx++; + return r; +} + +unsigned mk_href_idx() { + unsigned r = m_next_href_idx; + m_next_href_idx++; + return r; +} + +void init_uref_mref_href_idxs() { + m_next_uref_idx = 0; + m_next_mref_idx = 0; + m_next_href_idx = 0; +} + void initialize_expr() { g_prefix = new name(name::mk_internal_unique_name()); g_dummy_type = new expr(mk_constant(*g_prefix)); diff --git a/src/library/blast/expr.h b/src/library/blast/expr.h index 0fb60541d..fe20321f3 100644 --- a/src/library/blast/expr.h +++ b/src/library/blast/expr.h @@ -31,6 +31,16 @@ bool has_mref(expr const & e); inline bool is_local_non_href(expr const & e) { return is_local(e) && !is_href(e); } +/** \brief Return the a fresh index for uref/mref/href. + \remark It is implemented using thread local storage. */ +unsigned mk_uref_idx(); +unsigned mk_mref_idx(); +unsigned mk_href_idx(); +/** \brief Reset thread local counters */ +void init_uref_mref_href_idxs(); + +inline level mk_fresh_uref() { return mk_uref(mk_uref_idx()); } + void initialize_expr(); void finalize_expr(); } diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index c2da366c4..40196edfa 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -24,7 +24,7 @@ bool metavar_decl::restrict_context_using(metavar_decl const & other) { return !to_erase.empty(); } -state::state():m_next_uref_index(0), m_next_mref_index(0) {} +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`. */ @@ -42,14 +42,8 @@ void state::add_fixed_by(unsigned hidx, unsigned midx) { } } -level state::mk_uref() { - unsigned idx = m_next_mref_index; - m_next_mref_index++; - return blast::mk_uref(idx); -} - expr state::mk_metavar(hypothesis_idx_set const & c, expr const & type) { - unsigned midx = m_next_mref_index; + unsigned midx = mk_mref_idx(); for_each(type, [&](expr const & e, unsigned) { if (!has_href(e)) return false; @@ -60,7 +54,6 @@ expr state::mk_metavar(hypothesis_idx_set const & c, expr const & type) { } return true; // continue search }); - m_next_mref_index++; m_metavar_decls.insert(midx, metavar_decl(c, type)); return blast::mk_mref(midx); } diff --git a/src/library/blast/state.h b/src/library/blast/state.h index d20a4188b..87f27d30e 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -68,9 +68,7 @@ class state { typedef metavar_idx_map uassignment; typedef hypothesis_idx_map fixed_by; typedef list proof_steps; - unsigned m_next_uref_index; // index of the next universe metavariable uassignment m_uassignment; - unsigned m_next_mref_index; // index of the next metavariable metavar_decls m_metavar_decls; eassignment m_eassignment; branch m_main; @@ -99,8 +97,6 @@ class state { public: state(); - level mk_uref(); - bool is_uref_assigned(level const & l) const { lean_assert(is_uref(l)); return m_uassignment.contains(uref_index(l));