mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

fix #4054 (#4277)

Browse source 
* flag when quantified lemmas are added to smt_context

* When solver returns unknown but cannot create child, return unknown

* handle unknowns when qlemmas and weak_abs are turned on
This commit is contained in:
Hari Govind V K 2020-05-21 12:58:09 -04:00 • committed by GitHub
parent bfd2407e0f
commit ed92b8437c
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
4 changed files with 160 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -702,7 +702,7 @@ pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head):
m_reach_facts(), m_rf_init_sz(0),
m_transition_clause(m), m_transition(m), m_init(m),
m_extend_lit0(m), m_extend_lit(m),
m_all_init(false)
m_all_init(false), m_has_quantified_frame(false)
{
m_solver = alloc(prop_solver, m, ctx.mk_solver0(), ctx.mk_solver1(),
ctx.get_params(), head->get_name());
@ -840,6 +840,29 @@ reach_fact *pred_transformer::get_used_origin_rf(model& mdl, unsigned oidx) {
return nullptr;
}
// get all reachable facts used in the model.
void pred_transformer::get_all_used_rf(model &mdl, unsigned oidx,
reach_fact_ref_vector &res) {
expr_ref b(m);
res.reset();
model::scoped_model_completion _sc_(mdl, false);
for (auto *rf : m_reach_facts) {
pm.formula_n2o(rf->tag(), b, oidx);
if (mdl.is_false(b))
res.push_back(rf);
}
}
// get all reachable facts in the post state
void pred_transformer::get_all_used_rf(model &mdl, reach_fact_ref_vector &res) {
res.reset();
model::scoped_model_completion _sc_(mdl, false);
for (auto *rf : m_reach_facts) {
if (mdl.is_false(rf->tag()))
res.push_back(rf);
}
}
const datalog::rule *pred_transformer::find_rule(model &model) {
expr_ref val(m);
@ -978,6 +1001,7 @@ void pred_transformer::add_lemma_from_child (pred_transformer& child,
inst.set(j, m.mk_implies(a, inst.get(j)));
}
if (lemma->is_ground() || (get_context().use_qlemmas() && !ground_only)) {
m_has_quantified_frame = true;
inst.push_back(fmls.get(i));
}
SASSERT (!inst.empty ());
@ -1849,8 +1873,10 @@ void pred_transformer::updt_solver(prop_solver *solver) {
}
// (quantified) lemma
if (u->is_ground() || get_context().use_qlemmas())
if (u->is_ground() || get_context().use_qlemmas()) {
m_has_quantified_frame = true;
fmls.push_back(u->get_expr());
}
// send to solver
if (is_infty_level(u->level()))
@ -3321,6 +3347,96 @@ void context::predecessor_eh()
}
}
// Update a partial model to be consistent over reachable facts in pt
// Conceptually, a reachable fact is asserted as tag == > fact,
// where tag is a Boolean literal and fact a formula. When the model is partial,
// it is possible that tag is true, but model.eval(fact) is unknown
// This function fixes the model by flipping the value of tag in
// this case.
bool pred_transformer::mk_mdl_rf_consistent(const datalog::rule *r,
model &model) {
expr_ref rf(m);
reach_fact_ref_vector child_reach_facts;
SASSERT(r != nullptr);
ptr_vector<func_decl> preds;
find_predecessors(*r, preds);
for (unsigned i = 0; i < preds.size(); i++) {
func_decl *pred = preds[i];
bool atleast_one_true = false;
pred_transformer &ch_pt = ctx.get_pred_transformer(pred);
// get all reach facts of pred used in the model
expr_ref o_ch_reach(m);
reach_fact_ref_vector used_rfs;
ch_pt.get_all_used_rf(model, i, used_rfs);
for (auto *rf : used_rfs) {
pm.formula_n2o(rf->get(), o_ch_reach, i);
if (!model.is_true(o_ch_reach)) {
func_decl *tag = to_app(rf->tag())->get_decl();
set_true_in_mdl(model, tag);
} else
atleast_one_true = true;
}
if (used_rfs.size() > 0 && !atleast_one_true) {
TRACE("spacer_detail",
tout << "model does not satisfy any reachable fact\n";);
return false;
}
}
return true;
}
// Update a partial model to be consistent over reachable facts.
// Conceptually, a reachable fact is asserted as tag == > fact,
// where tag is a Boolean literal and fact a formula. When the model is partial,
// it is possible that tag is true, but model.eval(fact) is unknown
// This function fixes the model by flipping the value of tag in
// this case.
bool context::mk_mdl_rf_consistent(model &mdl) {
reach_fact_ref_vector used_rfs;
expr_ref exp(m);
for (auto &rel : m_rels) {
bool atleast_one_true = false;
pred_transformer &pt = *rel.m_value;
used_rfs.reset();
pt.get_all_used_rf(mdl, used_rfs);
for (auto *rf : used_rfs) {
if (!mdl.is_true(rf->get())) {
func_decl *tag = to_app(rf->tag())->get_decl();
set_true_in_mdl(mdl, tag);
} else
atleast_one_true = true;
}
if (used_rfs.size() > 0 && !atleast_one_true) {
TRACE("spacer_detail",
tout << "model does not satisfy any reachable fact\n";);
return false;
}
}
return true;
}
// Handle cases where solver returns unknown but returns a good enough model
// model is good enough if it satisfies
// 1. all the reachable states whose tag is set in the model
// 2. Tr && pob
lbool context::handle_unknown(pob &n, const datalog::rule *r, model &model) {
if (r == nullptr) {
if (model.is_true(n.post()) && mk_mdl_rf_consistent(model))
return l_true;
else
return l_undef;
}
// model \models reach_fact && Tr && pob
if (model.is_true(n.pt().get_transition(*r)) && model.is_true(n.post()) &&
n.pt().mk_mdl_rf_consistent(r, model)) {
return l_true;
}
return l_undef;
}
/// Checks whether the given pob is reachable
/// returns l_true if reachable, l_false if unreachable
/// returns l_undef if reachability cannot be decided
@ -3375,6 +3491,8 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
lbool res = n.pt ().is_reachable (n, &cube, &model, uses_level, is_concrete, r,
reach_pred_used, num_reuse_reach);
if (model) model->set_model_completion(false);
if (res == l_undef) res = handle_unknown(n, r, *model);
checkpoint ();
IF_VERBOSE (1, verbose_stream () << "." << std::flush;);
switch (res) {
@ -3427,15 +3545,27 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
return next ? l_undef : l_true;
}
// create a child of n
out.push_back(&n);
VERIFY(create_children (n, *r, *model, reach_pred_used, out));
IF_VERBOSE(1, verbose_stream () << " U "
<< std::fixed << std::setprecision(2)
<< watch.get_seconds () << "\n";);
return l_undef;
// Try to create child with model
// create_children() might return false if solver is incomplete (e.g.,
// due to weak_abs)
if (create_children(n, *r, *model, reach_pred_used, out)) {
out.push_back(&n);
IF_VERBOSE(1, verbose_stream()
<< " U " << std::fixed << std::setprecision(2)
<< watch.get_seconds() << "\n";);
return l_undef;
} else if (n.weakness() < 10) {
// Cannot create child. Increase weakness and try again.
SASSERT(out.empty());
n.bump_weakness();
IF_VERBOSE(1, verbose_stream()
<< " UNDEF " << std::fixed << std::setprecision(2)
<< watch.get_seconds() << "\n";);
// Recursion bounded by weakness (atmost 10 right now)
return expand_pob(n, out);
}
TRACE("spacer", tout << "unknown state: " << mk_and(cube) << "\n";);
throw unknown_exception();
}
case l_false: {
// n is unreachable, create new summary facts

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

@ -409,6 +409,7 @@ class pred_transformer {
stopwatch m_must_reachable_watch;
stopwatch m_ctp_watch;
stopwatch m_mbp_watch;
bool m_has_quantified_frame; // True when a quantified lemma is in the frame
void init_sig();
app_ref mk_extend_lit();
@ -441,6 +442,7 @@ public:
~pred_transformer() {}
inline bool use_native_mbp ();
bool mk_mdl_rf_consistent(const datalog::rule *r, model &mdl);
reach_fact *get_rf (expr *v) {
for (auto *rf : m_reach_facts) {
if (v == rf->get()) {return rf;}
@ -480,6 +482,9 @@ public:
reach_fact *get_used_rf(model& mdl, bool all = true);
/// \brief Returns reachability fact active in the origin of the given model
reach_fact* get_used_origin_rf(model &mdl, unsigned oidx);
/// \brief Collects all the reachable facts used in mdl
void get_all_used_rf(model &mdl, unsigned oidx, reach_fact_ref_vector& res);
void get_all_used_rf(model &mdl, reach_fact_ref_vector &res);
expr_ref get_origin_summary(model &mdl,
unsigned level, unsigned oidx, bool must,
const ptr_vector<app> **aux);
@ -1051,6 +1056,9 @@ class context {
void predecessor_eh();
void updt_params();
lbool handle_unknown(pob &n, const datalog::rule *r, model &model);
bool mk_mdl_rf_consistent(model &mdl);
public:
/**
Initial values of predicates are stored in corresponding relations in dctx.

10
src/muz/spacer/spacer_util.cpp
View file

@ -980,7 +980,13 @@ namespace {
for_each_expr(cd, fml);
}
}
// set the value of a boolean function to true in model
void set_true_in_mdl(model &model, func_decl *f) {
SASSERT(f->get_arity() == 0);
model.unregister_decl(f);
model.register_decl(f, model.get_manager().mk_true());
model.reset_eval_cache();
}
} // namespace spacer
template class rewriter_tpl<spacer::adhoc_rewriter_cfg>;
template class rewriter_tpl<spacer::adhoc_rewriter_rpp>;

3
src/muz/spacer/spacer_util.h
View file

@ -140,6 +140,9 @@ namespace spacer {
bool is_clause(ast_manager &m, expr *n);
bool is_literal(ast_manager &m, expr *n);
bool is_atom(ast_manager &m, expr *n);
// set f to true in model
void set_true_in_mdl(model &model, func_decl *f);
}
#endif