From 16fefe850a51de6d4007cc504a95fc05c5f7e353 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 31 May 2018 11:16:05 -0700 Subject: [PATCH] Factored mbp into pred_transformer and added stats --- src/muz/spacer/spacer_context.cpp | 27 +++++++++++++++------------ src/muz/spacer/spacer_context.h | 6 ++++++ 2 files changed, 21 insertions(+), 12 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 9d8e3d6af..ba7a2cb9b 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -227,8 +227,6 @@ pob *derivation::create_next_child (model_evaluator_util &mev) expr_ref_vector summaries (m); app_ref_vector vars (m); - bool use_native_mbp = get_context ().use_native_mbp (); - bool ground = get_context ().use_ground_cti (); // -- find first may premise while (m_active < m_premises.size() && m_premises[m_active].is_must()) { summaries.push_back (m_premises[m_active].get_summary ()); @@ -246,7 +244,7 @@ pob *derivation::create_next_child (model_evaluator_util &mev) timeit _timer1 (is_trace_enabled("spacer_timeit"), "create_next_child::qproject1", verbose_stream ()); - qe_project (m, vars, m_trans, mev.get_model (), true, use_native_mbp, !ground); + pt().mbp(vars, m_trans, mev.get_model()); //qe::reduce_array_selects (*mev.get_model (), m_trans); // remember variables that need to be existentially quantified m_evars.append (vars); @@ -274,7 +272,7 @@ pob *derivation::create_next_child (model_evaluator_util &mev) timeit _timer2 (is_trace_enabled("spacer_timeit"), "create_next_child::qproject2", verbose_stream ()); - qe_project (m, vars, post, mev.get_model (), true, use_native_mbp, !ground); + pt().mbp(vars, post, mev.get_model()); //qe::reduce_array_selects (*mev.get_model (), post); // remember variables that need to be existentially quantified @@ -309,9 +307,6 @@ pob *derivation::create_next_child () { if (m_active + 1 >= m_premises.size()) { return nullptr; } - bool use_native_mbp = get_context ().use_native_mbp (); - bool ground = get_context ().use_ground_cti (); - // update the summary of the active node to some must summary // construct a new model consistent with the must summary of m_active premise @@ -375,8 +370,7 @@ pob *derivation::create_next_child () { vars.push_back(m.mk_const(pm.o2n(pt.sig(i), 0))); } if (!vars.empty ()) { - qe_project (m, vars, m_trans, mev.get_model (), true, use_native_mbp, - !ground); + this->pt().mbp(vars, m_trans, mev.get_model()); // keep track of implicitly quantified variables m_evars.append (vars); } @@ -701,6 +695,7 @@ void pred_transformer::collect_statistics(statistics& st) const st.update ("time.spacer.solve.pt.must_reachable", m_must_reachable_watch.get_seconds ()); st.update("time.spacer.ctp", m_ctp_watch.get_seconds()); + st.update("time.spacer.mbp", m_mbp_watch.get_seconds()); } void pred_transformer::reset_statistics() @@ -711,6 +706,7 @@ void pred_transformer::reset_statistics() m_initialize_watch.reset (); m_must_reachable_watch.reset (); m_ctp_watch.reset(); + m_mbp_watch.reset(); } void pred_transformer::init_sig() @@ -1255,6 +1251,14 @@ bool pred_transformer::is_qblocked (pob &n) { return res == l_false; } + +void pred_transformer::mbp(app_ref_vector &vars, expr_ref &fml, + const model_ref &mdl, bool reduce_all_selects) { + scoped_watch _t_(m_mbp_watch); + qe_project(m, vars, fml, mdl, reduce_all_selects, + use_native_mbp(), !ctx.use_ground_cti()); +} + // // check if predicate transformer has a satisfiable predecessor state. // returns either a satisfiable predecessor state or @@ -3439,7 +3443,7 @@ reach_fact *pred_transformer::mk_reach_fact (pob& n, model_evaluator_util &mev, timeit _timer1 (is_trace_enabled("spacer_timeit"), "mk_reach_fact::qe_project", verbose_stream ()); - qe_project (m, vars, res, mev.get_model (), false, ctx.use_native_mbp()); + mbp(vars, res, mev.get_model(), false /*, false */); } @@ -3517,8 +3521,7 @@ bool context::create_children(pob& n, datalog::rule const& r, n.get_skolems(vars); expr_ref phi1 = mk_and (Phi); - qe_project (m, vars, phi1, mev.get_model (), true, - m_use_native_mbp, !m_ground_cti); + n.pt().mbp(vars, phi1, mev.get_model ()); //qe::reduce_array_selects (*mev.get_model (), phi1); SASSERT (!m_ground_cti || vars.empty ()); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 9675fad09..4ece95489 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -310,6 +310,7 @@ class pred_transformer { stopwatch m_initialize_watch; stopwatch m_must_reachable_watch; stopwatch m_ctp_watch; + stopwatch m_mbp_watch; /// Auxiliary variables to represent different disjunctive @@ -458,6 +459,10 @@ public: /// \brief Returns true if the obligation is already blocked by current quantified lemmas bool is_qblocked (pob &n); + /// \brief interface to Model Based Projection + void mbp(app_ref_vector &vars, expr_ref &fml, const model_ref &mdl, + bool reduce_all_selects = true); + }; @@ -679,6 +684,7 @@ public: ast_manager &get_ast_manager () const {return m_parent.get_ast_manager ();} manager &get_manager () const {return m_parent.get_manager ();} context &get_context() const {return m_parent.get_context();} + pred_transformer &pt() const {return m_parent.pt();} };