mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

spacer: cleaner management of rf tags

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-31 17:06:01 -07:00
parent ada548b5ae
commit 7a8563a34c
2 changed files with 70 additions and 78 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -641,18 +641,24 @@ pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head):
m_pobs(*this), m_pobs(*this),
m_frames(*this), m_frames(*this),
m_reach_facts(), m_rf_init_sz(0), m_reach_facts(), m_rf_init_sz(0),
m_transition_clause(m), m_transition(m), m_init(m), m_extend_lit(m), m_transition_clause(m), m_transition(m), m_init(m),
m_all_init(false), m_extend_lit0(m), m_extend_lit(m),
m_reach_case_vars(m) m_all_init(false)
{ {
m_solver = alloc(prop_solver, m, ctx.mk_solver0(), ctx.mk_solver1(), m_solver = alloc(prop_solver, m, ctx.mk_solver0(), ctx.mk_solver1(),
ctx.get_params(), head->get_name()); ctx.get_params(), head->get_name());
init_sig (); init_sig ();
m_extend_lit = mk_extend_lit();
m_extend_lit0 = m_extend_lit;
}
app_ref pred_transformer::mk_extend_lit() {
app_ref v(m); app_ref v(m);
std::stringstream name; std::stringstream name;
name << m_head->get_name () << "_ext0"; name << m_head->get_name () << "_ext0";
v = m.mk_const (symbol(name.str().c_str()), m.mk_bool_sort()); v = m.mk_const (symbol(name.str().c_str()), m.mk_bool_sort());
m_extend_lit = m.mk_not (m.mk_const (pm.get_n_pred (v->get_decl ()))); return app_ref(m.mk_not (m.mk_const (pm.get_n_pred (v->get_decl ()))), m);
} }
pred_transformer::~pred_transformer() { pred_transformer::~pred_transformer() {
@ -743,7 +749,7 @@ bool pred_transformer::is_must_reachable(expr* state, model_ref* model)
m_reach_solver->push (); m_reach_solver->push ();
m_reach_solver->assert_expr (state); m_reach_solver->assert_expr (state);
m_reach_solver->assert_expr (m.mk_not (m_reach_case_vars.back ())); m_reach_solver->assert_expr (m.mk_not (m_reach_facts.back()->tag()));
lbool res = m_reach_solver->check_sat (0, nullptr); lbool res = m_reach_solver->check_sat (0, nullptr);
if (model) { m_reach_solver->get_model(*model); } if (model) { m_reach_solver->get_model(*model); }
m_reach_solver->pop (1); m_reach_solver->pop (1);
@ -754,39 +760,29 @@ bool pred_transformer::is_must_reachable(expr* state, model_ref* model)
reach_fact* pred_transformer::get_used_reach_fact (model_evaluator_util& mev, reach_fact* pred_transformer::get_used_reach_fact (model_evaluator_util& mev,
bool all) bool all) {
{
expr_ref v (m); expr_ref v (m);
for (unsigned i = all ? 0 : m_rf_init_sz, sz = m_reach_case_vars.size (); for (auto *rf : m_reach_facts) {
i < sz; i++) { if (!all && rf->is_init()) continue;
VERIFY (mev.eval (m_reach_case_vars.get (i), v, false)); VERIFY(mev.eval (rf->tag(), v, false));
if (m.is_false (v)) { if (m.is_false(v)) return rf;
return m_reach_facts.get (i);
} }
} UNREACHABLE();
UNREACHABLE ();
return nullptr; return nullptr;
} }
reach_fact *pred_transformer::get_used_origin_reach_fact (model_evaluator_util& mev, reach_fact *pred_transformer::get_used_origin_reach_fact (model_evaluator_util& mev,
unsigned oidx) unsigned oidx) {
{
expr_ref b(m), v(m); expr_ref b(m), v(m);
reach_fact *res = nullptr;
for (unsigned i = 0, sz = m_reach_case_vars.size (); i < sz; i++) { for (auto *rf : m_reach_facts) {
pm.formula_n2o (m_reach_case_vars.get (i), v, oidx); pm.formula_n2o (rf->tag(), v, oidx);
VERIFY(mev.eval (v, b, false)); VERIFY(mev.eval (v, b, false));
if (m.is_false (b)) return rf;
if (m.is_false (b)) {
res = m_reach_facts.get (i);
break;
} }
} UNREACHABLE();
SASSERT (res); return nullptr;
return res;
} }
const datalog::rule *pred_transformer::find_rule(model &model) { const datalog::rule *pred_transformer::find_rule(model &model) {
@ -837,7 +833,7 @@ const datalog::rule *pred_transformer::find_rule(model &model,
if (!pt.has_reach_facts()) {is_concrete = false;} if (!pt.has_reach_facts()) {is_concrete = false;}
else { else {
expr_ref v(m); expr_ref v(m);
pm.formula_n2o(pt.get_last_reach_case_var (), v, i); pm.formula_n2o(pt.get_last_reach_tag (), v, i);
model.eval(to_app (v.get ())->get_decl (), vl); model.eval(to_app (v.get ())->get_decl (), vl);
used = m.is_false (vl); used = m.is_false (vl);
is_concrete = is_concrete && used; is_concrete = is_concrete && used;
@ -975,23 +971,18 @@ void pred_transformer::add_lemma_from_child (pred_transformer& child,
} }
expr* pred_transformer::mk_fresh_reach_case_var () app_ref pred_transformer::mk_fresh_reach_tag ()
{ {
std::stringstream name; std::stringstream name;
func_decl_ref decl(m); func_decl_ref decl(m);
name << head ()->get_name () << "#reach_case_" << m_reach_case_vars.size (); name << head ()->get_name () << "#reach_tag_" << m_reach_facts.size ();
decl = m.mk_func_decl (symbol (name.str ().c_str ()), 0, decl = m.mk_func_decl (symbol (name.str ().c_str ()), 0,
(sort*const*)nullptr, m.mk_bool_sort ()); (sort*const*)nullptr, m.mk_bool_sort ());
m_reach_case_vars.push_back (m.mk_const (pm.get_n_pred (decl))); return app_ref(m.mk_const (pm.get_n_pred (decl)), m);
return m_reach_case_vars.back ();
} }
expr* pred_transformer::get_reach_case_var (unsigned idx) const void pred_transformer::add_reach_fact (reach_fact *rf)
{return m_reach_case_vars.get (idx);}
void pred_transformer::add_reach_fact (reach_fact *fact)
{ {
timeit _timer (is_trace_enabled("spacer_timeit"), timeit _timer (is_trace_enabled("spacer_timeit"),
"spacer::pred_transformer::add_reach_fact", "spacer::pred_transformer::add_reach_fact",
@ -999,46 +990,45 @@ void pred_transformer::add_reach_fact (reach_fact *fact)
TRACE ("spacer", TRACE ("spacer",
tout << "add_reach_fact: " << head()->get_name() << " " tout << "add_reach_fact: " << head()->get_name() << " "
<< (fact->is_init () ? "INIT " : "") << (rf->is_init () ? "INIT " : "")
<< mk_pp(fact->get (), m) << "\n";); << mk_pp(rf->get (), m) << "\n";);
// -- avoid duplicates // -- avoid duplicates
if (fact == nullptr || get_reach_fact(fact->get())) {return;} if (!rf || get_reach_fact(rf->get())) {return;}
// all initial facts are grouped together // all initial facts are grouped together
SASSERT (!fact->is_init () || m_reach_facts.empty () || SASSERT (!rf->is_init () || m_reach_facts.empty () ||
m_reach_facts.back ()->is_init ()); m_reach_facts.back ()->is_init ());
m_reach_facts.push_back (fact); // create tags
if (fact->is_init()) {m_rf_init_sz++;} app_ref last_tag(m);
app_ref new_tag(m);
expr_ref fml(m);
if (!m_reach_facts.empty()) {last_tag = m_reach_facts.back()->tag();}
if (rf->is_init ())
new_tag = mk_fresh_reach_tag();
else
// side-effect: updates m_solver with rf
new_tag = to_app(extend_initial(rf->get())->get_arg(0));
rf->set_tag(new_tag);
// add to m_reach_facts
m_reach_facts.push_back (rf);
if (rf->is_init()) {m_rf_init_sz++;}
// update m_reach_solver // update m_reach_solver
expr_ref last_var (m); if (last_tag) {fml = m.mk_or(m.mk_not(last_tag), rf->get(), rf->tag());}
expr_ref new_var (m); else {fml = m.mk_or(rf->get(), rf->tag());}
expr_ref fml (m);
if (!m_reach_case_vars.empty()) {last_var = m_reach_case_vars.back();}
if (fact->is_init ())
{new_var = mk_fresh_reach_case_var();}
else {
new_var = extend_initial (fact->get ())->get_arg (0);
m_reach_case_vars.push_back (new_var);
}
SASSERT (m_reach_facts.size () == m_reach_case_vars.size ());
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_solver->assert_expr (fml); m_reach_solver->assert_expr (fml);
TRACE ("spacer", TRACE ("spacer", tout << "updating reach ctx: " << fml << "\n";);
tout << "updating reach ctx: " << mk_pp(fml, m) << "\n";);
lemma lem(m, fml, infty_level()); // update solvers of other pred_transformers
// XXX wrap rf into a lemma to fit the API
lemma fake_lemma(m, fml, infty_level());
// update users; reach facts are independent of levels // update users; reach facts are independent of levels
for (auto use : m_use) for (auto use : m_use)
{use->add_lemma_from_child (*this, &lem, infty_level());} use->add_lemma_from_child (*this, &fake_lemma, infty_level());
} }
expr_ref pred_transformer::get_reachable() expr_ref pred_transformer::get_reachable()
@ -1080,8 +1070,8 @@ expr_ref pred_transformer::get_reachable()
return res; return res;
} }
expr* pred_transformer::get_last_reach_case_var () const expr* pred_transformer::get_last_reach_tag () const
{return m_reach_case_vars.empty () ? nullptr : m_reach_case_vars.back ();} {return m_reach_facts.empty() ? nullptr : m_reach_facts.back()->tag();}
expr_ref pred_transformer::get_cover_delta(func_decl* p_orig, int level) expr_ref pred_transformer::get_cover_delta(func_decl* p_orig, int level)
{ {
@ -1306,7 +1296,7 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core,
ctx.get_pred_transformer(m_predicates[i]); ctx.get_pred_transformer(m_predicates[i]);
if (pt.has_reach_facts()) { if (pt.has_reach_facts()) {
expr_ref a(m); expr_ref a(m);
pm.formula_n2o(pt.get_last_reach_case_var (), a, i); pm.formula_n2o(pt.get_last_reach_tag(), a, i);
reach_assumps.push_back(m.mk_not (a)); reach_assumps.push_back(m.mk_not (a));
} else { } else {
reach_assumps.push_back(m.mk_not (entry.m_key)); reach_assumps.push_back(m.mk_not (entry.m_key));

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

@ -68,6 +68,9 @@ class reach_fact {
const datalog::rule &m_rule; const datalog::rule &m_rule;
reach_fact_ref_vector m_justification; reach_fact_ref_vector m_justification;
// variable used to tag this reach fact in an incremental disjunction
app_ref m_tag;
bool m_init; bool m_init;
public: public:
@ -75,10 +78,10 @@ public:
expr* fact, const ptr_vector<app> &aux_vars, expr* fact, const ptr_vector<app> &aux_vars,
bool init = false) : bool init = false) :
m_ref_count (0), m_fact (fact, m), m_aux_vars (aux_vars), m_ref_count (0), m_fact (fact, m), m_aux_vars (aux_vars),
m_rule(rule), m_init (init) {} m_rule(rule), m_tag(m), m_init (init) {}
reach_fact (ast_manager &m, const datalog::rule &rule, reach_fact (ast_manager &m, const datalog::rule &rule,
expr* fact, bool init = false) : expr* fact, bool init = false) :
m_ref_count (0), m_fact (fact, m), m_rule(rule), m_init (init) {} m_ref_count (0), m_fact (fact, m), m_rule(rule), m_tag(m), m_init (init) {}
bool is_init () {return m_init;} bool is_init () {return m_init;}
const datalog::rule& get_rule () {return m_rule;} const datalog::rule& get_rule () {return m_rule;}
@ -89,6 +92,9 @@ public:
expr *get () {return m_fact.get ();} expr *get () {return m_fact.get ();}
const ptr_vector<app> &aux_vars () {return m_aux_vars;} const ptr_vector<app> &aux_vars () {return m_aux_vars;}
app* tag() const {SASSERT(m_tag); return m_tag;}
void set_tag(app* tag) {m_tag = tag;}
void inc_ref () {++m_ref_count;} void inc_ref () {++m_ref_count;}
void dec_ref () void dec_ref ()
{ {
@ -303,7 +309,8 @@ class pred_transformer {
expr_ref_vector m_transition_clause; // extra clause for trans expr_ref_vector m_transition_clause; // extra clause for trans
expr_ref m_transition; // transition relation expr_ref m_transition; // transition relation
expr_ref m_init; // initial condition expr_ref m_init; // initial condition
app_ref m_extend_lit; // literal to extend initial state app_ref m_extend_lit0; // first literal used to extend initial state
app_ref m_extend_lit; // current literal to extend initial state
bool m_all_init; // true if the pt has no uninterpreted body in any rule bool m_all_init; // true if the pt has no uninterpreted body in any rule
ptr_vector<func_decl> m_predicates; // temp vector used with find_predecessors() ptr_vector<func_decl> m_predicates; // temp vector used with find_predecessors()
stats m_stats; stats m_stats;
@ -312,13 +319,8 @@ class pred_transformer {
stopwatch m_ctp_watch; stopwatch m_ctp_watch;
stopwatch m_mbp_watch; stopwatch m_mbp_watch;
/// Auxiliary variables to represent different disjunctive
/// cases of must summaries. Stored over 'n' (a.k.a. new)
/// versions of the variables
expr_ref_vector m_reach_case_vars;
void init_sig(); void init_sig();
app_ref mk_extend_lit();
void ensure_level(unsigned level); void ensure_level(unsigned level);
void add_lemma_core (lemma *lemma, bool ground_only = false); void add_lemma_core (lemma *lemma, bool ground_only = false);
void add_lemma_from_child (pred_transformer &child, lemma *lemma, void add_lemma_from_child (pred_transformer &child, lemma *lemma,
@ -337,7 +339,7 @@ class pred_transformer {
void add_premises(decl2rel const& pts, unsigned lvl, datalog::rule& rule, expr_ref_vector& r); void add_premises(decl2rel const& pts, unsigned lvl, datalog::rule& rule, expr_ref_vector& r);
expr* mk_fresh_reach_case_var (); app_ref mk_fresh_reach_tag ();
public: public:
pred_transformer(context& ctx, manager& pm, func_decl* head); pred_transformer(context& ctx, manager& pm, func_decl* head);
@ -406,7 +408,7 @@ public:
const datalog::rule &r); const datalog::rule &r);
void add_reach_fact (reach_fact *fact); // add reachability fact void add_reach_fact (reach_fact *fact); // add reachability fact
reach_fact* get_last_reach_fact () const { return m_reach_facts.back (); } reach_fact* get_last_reach_fact () const { return m_reach_facts.back (); }
expr* get_last_reach_case_var () const; expr* get_last_reach_tag () const;
pob* mk_pob(pob *parent, unsigned level, unsigned depth, pob* mk_pob(pob *parent, unsigned level, unsigned depth,
expr *post, app_ref_vector const &b){ expr *post, app_ref_vector const &b){