mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

propagate weakness from pob down to all related checks

Browse source 
If a pob was discharged with a weak solver, propagate the level of
weakness to inductive generalization and to lemma propagation.
This commit is contained in:
Arie Gurfinkel 2017-08-17 22:37:45 -04:00
parent b8b3703511
commit 68518b0e32
4 changed files with 53 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

36
src/muz/spacer/spacer_context.cpp
View file

@ -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<bool> _arith_ignore_int_(fparams.m_arith_ignore_int,
m_weak_abs && n.weakness() < 1);
flet<bool> _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 ();

13
src/muz/spacer/spacer_context.h
View file

@ -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<bool>& 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; }

13
src/muz/spacer/spacer_generalizers.cpp
View file

@ -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<expr> 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);

15
src/muz/spacer/spacer_prop_solver.h
View file

@ -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;
}
};
};
}