From 451d42319b80bf855c648813a7226356f9512243 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 31 May 2018 14:26:21 -0700 Subject: [PATCH] Rename m_reach_ctx into m_reach_solver --- src/muz/spacer/spacer_context.cpp | 18 +++++++++--------- src/muz/spacer/spacer_context.h | 2 +- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index ba7a2cb9b..0a5be7893 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -637,7 +637,7 @@ pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head): pm(pm), m(pm.get_manager()), ctx(ctx), m_head(head, m), m_sig(m), m_solver(pm, ctx.get_params(), head->get_name()), - m_reach_ctx (pm.mk_solver2()), + m_reach_solver (pm.mk_solver2()), m_pobs(*this), m_frames(*this), m_reach_facts(), m_rf_init_sz(0), @@ -739,12 +739,12 @@ bool pred_transformer::is_must_reachable(expr* state, model_ref* model) // reachable using the init rule of the current transformer if (m_reach_facts.empty()) { return false; } - m_reach_ctx->push (); - m_reach_ctx->assert_expr (state); - m_reach_ctx->assert_expr (m.mk_not (m_reach_case_vars.back ())); - lbool res = m_reach_ctx->check_sat (0, nullptr); - if (model) { m_reach_ctx->get_model(*model); } - m_reach_ctx->pop (1); + m_reach_solver->push (); + m_reach_solver->assert_expr (state); + m_reach_solver->assert_expr (m.mk_not (m_reach_case_vars.back ())); + lbool res = m_reach_solver->check_sat (0, nullptr); + if (model) { m_reach_solver->get_model(*model); } + m_reach_solver->pop (1); return (res == l_true); } @@ -1011,7 +1011,7 @@ void pred_transformer::add_reach_fact (reach_fact *fact) if (fact->is_init()) {m_rf_init_sz++;} - // update m_reach_ctx + // update m_reach_solver expr_ref last_var (m); expr_ref new_var (m); expr_ref fml (m); @@ -1029,7 +1029,7 @@ void pred_transformer::add_reach_fact (reach_fact *fact) if (last_var) {fml = m.mk_or(m.mk_not(last_var), fact->get(), new_var);} else {fml = m.mk_or(fact->get(), new_var);} - m_reach_ctx->assert_expr (fml); + m_reach_solver->assert_expr (fml); TRACE ("spacer", tout << "updating reach ctx: " << mk_pp(fml, m) << "\n";); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 4ece95489..77836a389 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -291,7 +291,7 @@ class pred_transformer { ptr_vector m_use; // places where 'this' is referenced. ptr_vector m_rules; // rules used to derive transformer prop_solver m_solver; // solver context - solver* m_reach_ctx; // context for reachability facts + ref m_reach_solver; // context for reachability facts pobs m_pobs; // proof obligations created so far frames m_frames; // frames with lemmas reach_fact_ref_vector m_reach_facts; // reach facts