From 68518b0e320b01f6bf22375675980a790fad65f0 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 17 Aug 2017 22:37:45 -0400 Subject: [PATCH] propagate weakness from pob down to all related checks If a pob was discharged with a weak solver, propagate the level of weakness to inductive generalization and to lemma propagation. --- src/muz/spacer/spacer_context.cpp | 36 ++++++++++++++------------ src/muz/spacer/spacer_context.h | 13 +++++++--- src/muz/spacer/spacer_generalizers.cpp | 13 +++++++--- src/muz/spacer/spacer_prop_solver.h | 15 +++++++++++ 4 files changed, 53 insertions(+), 24 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 12ab70351..772eca1e1 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -715,6 +715,8 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core, // prepare the solver prop_solver::scoped_level _sl(m_solver, n.level()); prop_solver::scoped_subset_core _sc (m_solver, !n.use_farkas_generalizer ()); + prop_solver::scoped_weakness _sw(m_solver, 0, + ctx.weak_abs() ? n.weakness() : UINT_MAX); m_solver.set_core(core); m_solver.set_model(model); @@ -806,17 +808,20 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core, return l_undef; } -bool pred_transformer::is_invariant(unsigned level, expr* lemma, +bool pred_transformer::is_invariant(unsigned level, lemma* lem, unsigned& solver_level, expr_ref_vector* core) { - expr_ref_vector conj(m), aux(m); - expr_ref glemma(m); + expr_ref lemma(m); + lemma = lem->get_expr(); - if (!get_context().use_qlemmas() && is_quantifier(lemma)) { - SASSERT(is_forall(lemma)); + expr_ref_vector conj(m), aux(m); + expr_ref gnd_lemma(m); + + + if (!get_context().use_qlemmas() && !lem->is_ground()) { app_ref_vector tmp(m); - ground_expr(to_quantifier(lemma)->get_expr (), glemma, tmp); - lemma = glemma.get(); + ground_expr(to_quantifier(lemma)->get_expr (), gnd_lemma, tmp); + lemma = gnd_lemma.get(); } conj.push_back(mk_not(m, lemma)); @@ -824,6 +829,8 @@ bool pred_transformer::is_invariant(unsigned level, expr* lemma, prop_solver::scoped_level _sl(m_solver, level); prop_solver::scoped_subset_core _sc (m_solver, true); + prop_solver::scoped_weakness _sw (m_solver, 1, + ctx.weak_abs() ? lem->weakness() : UINT_MAX); m_solver.set_core(core); m_solver.set_model(nullptr); expr * bg = m_extend_lit.get (); @@ -839,7 +846,7 @@ bool pred_transformer::is_invariant(unsigned level, expr* lemma, } bool pred_transformer::check_inductive(unsigned level, expr_ref_vector& state, - unsigned& uses_level) + unsigned& uses_level, unsigned weakness) { manager& pm = get_manager(); expr_ref_vector conj(m), core(m); @@ -848,6 +855,8 @@ bool pred_transformer::check_inductive(unsigned level, expr_ref_vector& state, mk_assumptions(head(), states, conj); prop_solver::scoped_level _sl(m_solver, level); prop_solver::scoped_subset_core _sc (m_solver, true); + prop_solver::scoped_weakness _sw (m_solver, 1, + ctx.weak_abs() ? weakness : UINT_MAX); m_solver.set_core(&core); m_solver.set_model (nullptr); expr_ref_vector aux (m); @@ -1412,10 +1421,9 @@ bool pred_transformer::frames::propagate_to_next_level (unsigned level) unsigned solver_level; - expr * curr = m_lemmas [i]->get_expr (); - if (m_pt.is_invariant(tgt_level, curr, solver_level)) { + if (m_pt.is_invariant(tgt_level, m_lemmas.get(i), solver_level)) { m_lemmas [i]->set_level (solver_level); - m_pt.add_lemma_core (m_lemmas [i]); + m_pt.add_lemma_core (m_lemmas.get(i)); // percolate the lemma up to its new place for (unsigned j = i; (j+1) < sz && m_lt (m_lemmas[j+1], m_lemmas[j]); ++j) { @@ -2969,12 +2977,6 @@ lbool context::expand_node(pob& n) tout << "This pob can be blocked by instantiation\n";); } - smt_params &fparams = m_pm.fparams(); - flet _arith_ignore_int_(fparams.m_arith_ignore_int, - m_weak_abs && n.weakness() < 1); - flet _array_weak_(fparams.m_array_weak, - m_weak_abs && n.weakness() < 2); - lbool res = n.pt ().is_reachable (n, &cube, &model, uses_level, is_concrete, r, reach_pred_used, num_reuse_reach); checkpoint (); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index a18855afe..61317e93b 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -131,6 +131,7 @@ public: bool has_pob() {return m_pob;} pob_ref &get_pob() {return m_pob;} + inline unsigned weakness(); unsigned level () const {return m_lvl;} void set_level (unsigned lvl) {m_lvl = lvl;} @@ -399,10 +400,15 @@ public: datalog::rule const*& r, vector& reach_pred_used, unsigned& num_reuse_reach); - bool is_invariant(unsigned level, expr* lemma, + bool is_invariant(unsigned level, lemma* lem, unsigned& solver_level, expr_ref_vector* core = nullptr); + + bool is_invariant(unsigned level, expr* lem, + unsigned& solver_level, expr_ref_vector* core = nullptr) + { UNREACHABLE();} + bool check_inductive(unsigned level, expr_ref_vector& state, - unsigned& assumes_level); + unsigned& assumes_level, unsigned weakness = UINT_MAX); expr_ref get_formulas(unsigned level, bool add_axioms); @@ -549,7 +555,7 @@ struct pob_ref_gt : {return gt (n1.get (), n2.get ());} }; - +inline unsigned lemma::weakness() {return m_pob ? m_pob->weakness() : UINT_MAX;} /** */ class derivation { @@ -774,6 +780,7 @@ public: bool use_native_mbp () {return m_use_native_mbp;} bool use_ground_cti () {return m_ground_cti;} bool use_instantiate () { return m_instantiate; } + bool weak_abs() {return m_weak_abs;} bool use_qlemmas () {return m_use_qlemmas; } ast_manager& get_ast_manager() const { return m; } diff --git a/src/muz/spacer/spacer_generalizers.cpp b/src/muz/spacer/spacer_generalizers.cpp index 19989e440..e2058e93f 100644 --- a/src/muz/spacer/spacer_generalizers.cpp +++ b/src/muz/spacer/spacer_generalizers.cpp @@ -33,7 +33,8 @@ void lemma_sanity_checker::operator()(lemma_ref &lemma) { expr_ref_vector cube(lemma->get_ast_manager()); cube.append(lemma->get_cube()); ENSURE(lemma->get_pob()->pt().check_inductive(lemma->level(), - cube, uses_level)); + cube, uses_level, + lemma->weakness())); } @@ -58,6 +59,8 @@ void lemma_bool_inductive_generalizer::operator()(lemma_ref &lemma) { ptr_vector processed; expr_ref_vector extra_lits(m); + unsigned weakness = lemma->weakness(); + unsigned i = 0, num_failures = 0; while (i < cube.size() && (!m_failure_limit || num_failures < m_failure_limit)) { @@ -65,7 +68,7 @@ void lemma_bool_inductive_generalizer::operator()(lemma_ref &lemma) { lit = cube.get(i); cube[i] = true_expr; if (cube.size() > 1 && - pt.check_inductive(lemma->level(), cube, uses_level)) { + pt.check_inductive(lemma->level(), cube, uses_level, weakness)) { num_failures = 0; dirty = true; for (i = 0; i < cube.size() && @@ -82,7 +85,7 @@ void lemma_bool_inductive_generalizer::operator()(lemma_ref &lemma) { SASSERT(extra_lits.size() > 1); for (unsigned j = 0, sz = extra_lits.size(); !found && j < sz; ++j) { cube[i] = extra_lits.get(j); - if (pt.check_inductive(lemma->level(), cube, uses_level)) { + if (pt.check_inductive(lemma->level(), cube, uses_level, weakness)) { num_failures = 0; dirty = true; found = true; @@ -185,6 +188,8 @@ void lemma_array_eq_generalizer::operator() (lemma_ref &lemma) manager &pm = m_ctx.get_manager(); (void)pm; + unsigned weakness = lemma->weakness(); + expr_ref_vector core(m); expr_ref v(m); func_decl_set symb; @@ -264,7 +269,7 @@ void lemma_array_eq_generalizer::operator() (lemma_ref &lemma) pred_transformer &pt = lemma->get_pob()->pt(); // -- check if it is consistent with the transition relation unsigned uses_level1; - if (pt.check_inductive(lemma->level(), lits, uses_level1)) { + if (pt.check_inductive(lemma->level(), lits, uses_level1, weakness)) { TRACE("core_array_eq", tout << "Inductive!\n";); lemma->update_cube(lemma->get_pob(),lits); lemma->set_level(uses_level1); diff --git a/src/muz/spacer/spacer_prop_solver.h b/src/muz/spacer/spacer_prop_solver.h index 0cbcecfbf..c46063137 100644 --- a/src/muz/spacer/spacer_prop_solver.h +++ b/src/muz/spacer/spacer_prop_solver.h @@ -136,7 +136,22 @@ public: ~scoped_delta_level() {m_delta = false;} }; + class scoped_weakness { + smt_params &m_params; + bool m_arith_ignore_int; + bool m_array_weak; + public: + scoped_weakness(prop_solver &ps, unsigned solver_id, unsigned weakness) : + m_params(*ps.m_fparams[solver_id == 0 ? 0 : 0 /*1*/]) { + m_params.m_arith_ignore_int = weakness < 1; + m_params.m_array_weak = weakness < 2; + } + ~scoped_weakness() { + m_params.m_arith_ignore_int = m_arith_ignore_int; + m_params.m_array_weak = m_array_weak; + } + }; }; }