3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
better proof generation for the case when the query is reachable from initial
states. This case needs to be handled better so that spacer can assume
the problem is non-trivial.
This commit is contained in:
Arie Gurfinkel 2020-04-10 15:19:57 -04:00
parent d14ce97b76
commit a261bd94ed
3 changed files with 25 additions and 21 deletions

View file

@ -1004,19 +1004,19 @@ app_ref pred_transformer::mk_fresh_rf_tag ()
return app_ref(m.mk_const (pm.get_n_pred (decl)), m);
}
void pred_transformer::add_rf (reach_fact *rf)
void pred_transformer::add_rf (reach_fact *rf, bool force)
{
timeit _timer (is_trace_enabled("spacer_timeit"),
"spacer::pred_transformer::add_rf",
verbose_stream ());
TRACE ("spacer",
tout << "add_rf: " << head()->get_name() << " "
<< (rf->is_init () ? "INIT " : "")
<< mk_pp(rf->get (), m) << "\n";);
if (!rf) return;
TRACE("spacer", tout << "add_rf: " << head()->get_name() << " "
<< (rf->is_init() ? "INIT " : "")
<< mk_pp(rf->get(), m) << "\n";);
// -- avoid duplicates
if (!rf || get_rf(rf->get())) {return;}
// -- avoid duplicates unless forced
if (!force && get_rf(rf->get())) {return;}
// all initial facts are grouped together
SASSERT (!rf->is_init () || m_reach_facts.empty () ||
@ -1384,7 +1384,11 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core,
if (model && model->get()) {
r = find_rule(**model, is_concrete, reach_pred_used, num_reuse_reach);
TRACE("spacer",
tout << "reachable " << r << " is_concrete " << is_concrete << " rused: " << reach_pred_used << "\n";);
tout << "reachable is_sat: " << is_sat << " "
<< r << " is_concrete " << is_concrete << " rused: " << reach_pred_used << "\n";
ctx.get_datalog_context().get_rule_manager().display_smt2(*r, tout) << "\n";
);
TRACE("spacer_sat", tout << "model is:\n" << **model << "\n";);
}
return is_sat;
@ -1392,13 +1396,7 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core,
if (is_sat == l_false) {
SASSERT (reach_assumps.empty ());
TRACE ("spacer", tout << "unreachable with lemmas\n";
if (core) {
tout << "Core:\n";
for (unsigned i = 0; i < core->size (); i++) {
tout << mk_pp (core->get(i), m) << "\n";
}
}
);
if (core) tout << "Core:\n" << *core << "\n";);
uses_level = m_solver->uses_level();
return l_false;
}
@ -3378,10 +3376,15 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
// must-reachable
if (is_concrete) {
// -- update must summary
if (r && r->get_uninterpreted_tail_size() > 0) {
reach_fact_ref rf = n.pt().mk_rf (n, *model, *r);
CTRACE("spacer_sat", r,
tout << "Concrete reachable with a rule:\n";
get_datalog_context().get_rule_manager().display_smt2(*r, tout) << "\n";
);
bool is_root = m_pob_queue.is_root(n);
if (r && (r->get_uninterpreted_tail_size() > 0 || is_root )) {
reach_fact_ref rf = n.pt().mk_rf(n, *model, *r);
checkpoint ();
n.pt ().add_rf (rf.get ());
n.pt ().add_rf(rf.get (), is_root);
checkpoint ();
}

View file

@ -510,7 +510,7 @@ public:
/// initialize reachability facts using initial rules
void init_rfs ();
reach_fact *mk_rf(pob &n, model &mdl, const datalog::rule &r);
void add_rf (reach_fact *fact); // add reachability fact
void add_rf (reach_fact *fact, bool force = false); // add reachability fact
reach_fact* get_last_rf () const { return m_reach_facts.back (); }
expr* get_last_rf_tag () const;

View file

@ -64,8 +64,9 @@ proof_ref ground_sat_answer_op::operator()(pred_transformer &query) {
solver::scoped_push _s_(*m_solver);
m_solver->assert_expr(query.get_last_rf()->get());
lbool res = m_solver->check_sat(0, nullptr);
(void)res;
SASSERT(res == l_true);
CTRACE("spacer_sat", res != l_true, tout << "solver at check:\n";
m_solver->display(tout) << "res: " << res << "\n";);
VERIFY(res == l_true);
model_ref mdl;
m_solver->get_model(mdl);
mdl->compress();