From 4ef480e2a59f682426017ac985309d1a415c3050 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jun 2020 12:52:42 -0700 Subject: [PATCH] add op cache Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 26 +++++++++++++++++++++++ src/ast/rewriter/seq_rewriter.h | 35 +++++++++++++++++++++++++++++++ src/qe/qsat.cpp | 13 ++++++++---- src/smt/smt_case_split_queue.cpp | 4 ++-- src/smt/smt_context.cpp | 5 ++++- 5 files changed, 76 insertions(+), 7 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 955d6f34b..ea0cb3156 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3849,3 +3849,29 @@ bool seq_rewriter::reduce_subsequence(expr_ref_vector& ls, expr_ref_vector& rs, } return true; } + +seq_rewriter::op_cache::op_cache(ast_manager& m): + m(m), + m_trail(m) +{} + +expr* seq_rewriter::op_cache::find(decl_kind op, expr* a, expr* b) { + op_entry e(op, a, b, nullptr); + m_table.find(e); + return e.r; +} + +void seq_rewriter::op_cache::insert(decl_kind op, expr* a, expr* b, expr* r) { + cleanup(); + if (a) m_trail.push_back(a); + if (b) m_trail.push_back(b); + if (r) m_trail.push_back(r); + m_table.insert(op_entry(op, a, b, r)); +} + +void seq_rewriter::op_cache::cleanup() { + if (m_table.size() >= m_max_cache_size) { + m_trail.reset(); + m_table.reset(); + } +} diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 5519ee0fc..74f06f5f8 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -127,6 +127,41 @@ class seq_rewriter { unknown_c }; + + class op_cache { + struct op_entry { + decl_kind k; + expr* a, *b, *r; + op_entry(decl_kind k, expr* a, expr* b, expr* r): k(k), a(a), b(b), r(r) {} + op_entry():k(0), a(nullptr), b(nullptr), r(nullptr) {} + }; + + struct hash_entry { + unsigned operator()(op_entry const& e) const { + return mk_mix(e.k, e.a ? e.a->get_id() : 0, e.b ? e.b->get_id() : 0); + } + }; + + struct eq_entry { + bool operator()(op_entry const& a, op_entry const& b) const { + return a.k == b.k && a.a == b.a && a.b == b.b; + } + }; + + typedef hashtable op_table; + + ast_manager& m; + unsigned m_max_cache_size { 10000 }; + expr_ref_vector m_trail; + op_table m_table; + void cleanup(); + + public: + op_cache(ast_manager& m); + expr* find(decl_kind op, expr* a, expr* b); + void insert(decl_kind op, expr* a, expr* b, expr* r); + }; + length_comparison compare_lengths(expr_ref_vector const& as, expr_ref_vector const& bs) { return compare_lengths(as.size(), as.c_ptr(), bs.size(), bs.c_ptr()); } diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 351363f0b..248344c21 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -563,7 +563,11 @@ namespace qe { m_solver->collect_statistics(st); } void reset_statistics() { - init(); + clear(); + } + void collect_statistics(statistics& st) { + if (m_solver) + m_solver->collect_statistics(st); } void clear() { @@ -735,6 +739,7 @@ namespace qe { m_fa.init(); m_ex.init(); } + /** \brief create a quantifier prefix formula. @@ -1334,8 +1339,8 @@ namespace qe { void collect_statistics(statistics & st) const override { st.copy(m_st); - m_fa.s().collect_statistics(st); - m_ex.s().collect_statistics(st); + m_fa.collect_statistics(st); + m_ex.collect_statistics(st); m_pred_abs.collect_statistics(st); st.update("qsat num rounds", m_stats.m_num_rounds); m_pred_abs.collect_statistics(st); @@ -1348,7 +1353,7 @@ namespace qe { } void cleanup() override { - reset(); + clear(); } void set_logic(symbol const & l) override { diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp index ddb66ec33..d31f09d06 100644 --- a/src/smt/smt_case_split_queue.cpp +++ b/src/smt/smt_case_split_queue.cpp @@ -1252,12 +1252,12 @@ namespace { namespace smt { case_split_queue * mk_case_split_queue(context & ctx, smt_params & p) { if (ctx.relevancy_lvl() < 2 && (p.m_case_split_strategy == CS_RELEVANCY || p.m_case_split_strategy == CS_RELEVANCY_ACTIVITY || - p.m_case_split_strategy == CS_RELEVANCY_GOAL)) { + p.m_case_split_strategy == CS_RELEVANCY_GOAL)) { warning_msg("relevancy must be enabled to use option CASE_SPLIT=3, 4 or 5"); p.m_case_split_strategy = CS_ACTIVITY; } if (p.m_auto_config && (p.m_case_split_strategy == CS_RELEVANCY || p.m_case_split_strategy == CS_RELEVANCY_ACTIVITY || - p.m_case_split_strategy == CS_RELEVANCY_GOAL)) { + p.m_case_split_strategy == CS_RELEVANCY_GOAL)) { warning_msg("auto configuration (option AUTO_CONFIG) must be disabled to use option CASE_SPLIT=3, 4 or 5"); p.m_case_split_strategy = CS_ACTIVITY; } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 4f90bbcef..10b904c35 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -47,7 +47,7 @@ namespace smt { m_fparams(p), m_params(_p), m_setup(*this, p), - m_relevancy_lvl(p.m_relevancy_lvl), + m_relevancy_lvl(m_fparams.m_relevancy_lvl), m_asserted_formulas(m, p, _p), m_rewriter(m), m_qmanager(alloc(quantifier_manager, *this, p, _p)), @@ -95,6 +95,9 @@ namespace smt { m_last_search_failure(UNKNOWN), m_searching(false) { + std::cout << "create: " << m_fparams.m_relevancy_lvl << "\n"; + SASSERT(m_fparams.m_relevancy_lvl != 0); + SASSERT(m_scope_lvl == 0); SASSERT(m_base_lvl == 0); SASSERT(m_search_lvl == 0);