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

reach_fact --> rf

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-31 17:12:13 -07:00
parent 7a8563a34c
commit cfcc084688
2 changed files with 39 additions and 39 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -335,7 +335,7 @@ pob *derivation::create_next_child ()
mev.set_model (*model); mev.set_model (*model);
// find must summary used // find must summary used
reach_fact *rf = pt.get_used_reach_fact (mev, true); reach_fact *rf = pt.get_used_rf (mev, true);
// get an implicant of the summary // get an implicant of the summary
expr_ref_vector u(m), lits (m); expr_ref_vector u(m), lits (m);
@ -759,7 +759,7 @@ 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_rf (model_evaluator_util& mev,
bool all) { bool all) {
expr_ref v (m); expr_ref v (m);
@ -772,7 +772,7 @@ reach_fact* pred_transformer::get_used_reach_fact (model_evaluator_util& mev,
return nullptr; return nullptr;
} }
reach_fact *pred_transformer::get_used_origin_reach_fact (model_evaluator_util& mev, reach_fact *pred_transformer::get_used_origin_rf (model_evaluator_util& mev,
unsigned oidx) { unsigned oidx) {
expr_ref b(m), v(m); expr_ref b(m), v(m);
@ -830,10 +830,10 @@ const datalog::rule *pred_transformer::find_rule(model &model,
bool used = false; bool used = false;
func_decl* d = r->get_tail(i)->get_decl(); func_decl* d = r->get_tail(i)->get_decl();
const pred_transformer &pt = ctx.get_pred_transformer(d); const pred_transformer &pt = ctx.get_pred_transformer(d);
if (!pt.has_reach_facts()) {is_concrete = false;} if (!pt.has_rfs()) {is_concrete = false;}
else { else {
expr_ref v(m); expr_ref v(m);
pm.formula_n2o(pt.get_last_reach_tag (), v, i); pm.formula_n2o(pt.get_last_rf_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;
@ -971,7 +971,7 @@ void pred_transformer::add_lemma_from_child (pred_transformer& child,
} }
app_ref pred_transformer::mk_fresh_reach_tag () app_ref pred_transformer::mk_fresh_rf_tag ()
{ {
std::stringstream name; std::stringstream name;
func_decl_ref decl(m); func_decl_ref decl(m);
@ -982,19 +982,19 @@ app_ref pred_transformer::mk_fresh_reach_tag ()
return app_ref(m.mk_const (pm.get_n_pred (decl)), m); return app_ref(m.mk_const (pm.get_n_pred (decl)), m);
} }
void pred_transformer::add_reach_fact (reach_fact *rf) void pred_transformer::add_rf (reach_fact *rf)
{ {
timeit _timer (is_trace_enabled("spacer_timeit"), timeit _timer (is_trace_enabled("spacer_timeit"),
"spacer::pred_transformer::add_reach_fact", "spacer::pred_transformer::add_rf",
verbose_stream ()); verbose_stream ());
TRACE ("spacer", TRACE ("spacer",
tout << "add_reach_fact: " << head()->get_name() << " " tout << "add_rf: " << head()->get_name() << " "
<< (rf->is_init () ? "INIT " : "") << (rf->is_init () ? "INIT " : "")
<< mk_pp(rf->get (), m) << "\n";); << mk_pp(rf->get (), m) << "\n";);
// -- avoid duplicates // -- avoid duplicates
if (!rf || get_reach_fact(rf->get())) {return;} if (!rf || get_rf(rf->get())) {return;}
// all initial facts are grouped together // all initial facts are grouped together
SASSERT (!rf->is_init () || m_reach_facts.empty () || SASSERT (!rf->is_init () || m_reach_facts.empty () ||
@ -1007,7 +1007,7 @@ void pred_transformer::add_reach_fact (reach_fact *rf)
if (!m_reach_facts.empty()) {last_tag = m_reach_facts.back()->tag();} if (!m_reach_facts.empty()) {last_tag = m_reach_facts.back()->tag();}
if (rf->is_init ()) if (rf->is_init ())
new_tag = mk_fresh_reach_tag(); new_tag = mk_fresh_rf_tag();
else else
// side-effect: updates m_solver with rf // side-effect: updates m_solver with rf
new_tag = to_app(extend_initial(rf->get())->get_arg(0)); new_tag = to_app(extend_initial(rf->get())->get_arg(0));
@ -1070,7 +1070,7 @@ expr_ref pred_transformer::get_reachable()
return res; return res;
} }
expr* pred_transformer::get_last_reach_tag () const expr* pred_transformer::get_last_rf_tag () const
{return m_reach_facts.empty() ? nullptr : m_reach_facts.back()->tag();} {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)
@ -1134,7 +1134,7 @@ expr_ref pred_transformer::get_origin_summary (model_evaluator_util &mev,
// -- no auxiliary variables in lemmas // -- no auxiliary variables in lemmas
*aux = nullptr; *aux = nullptr;
} else { // find must summary to use } else { // find must summary to use
reach_fact *f = get_used_origin_reach_fact (mev, oidx); reach_fact *f = get_used_origin_rf (mev, oidx);
summary.push_back (f->get ()); summary.push_back (f->get ());
*aux = &f->aux_vars (); *aux = &f->aux_vars ();
} }
@ -1294,9 +1294,9 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core,
for (unsigned i = 0; i < m_predicates.size(); i++) { for (unsigned i = 0; i < m_predicates.size(); i++) {
const pred_transformer &pt = const pred_transformer &pt =
ctx.get_pred_transformer(m_predicates[i]); ctx.get_pred_transformer(m_predicates[i]);
if (pt.has_reach_facts()) { if (pt.has_rfs()) {
expr_ref a(m); expr_ref a(m);
pm.formula_n2o(pt.get_last_reach_tag(), a, i); pm.formula_n2o(pt.get_last_rf_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));
@ -1521,7 +1521,7 @@ void pred_transformer::initialize(decl2rel const& pts)
} }
void pred_transformer::init_reach_facts () void pred_transformer::init_rfs ()
{ {
expr_ref_vector v(m); expr_ref_vector v(m);
reach_fact_ref fact; reach_fact_ref fact;
@ -1531,7 +1531,7 @@ void pred_transformer::init_reach_facts ()
if (r->get_uninterpreted_tail_size() == 0) { if (r->get_uninterpreted_tail_size() == 0) {
fact = alloc (reach_fact, m, *r, m_rule2transition.find(r), fact = alloc (reach_fact, m, *r, m_rule2transition.find(r),
get_aux_vars(*r), true); get_aux_vars(*r), true);
add_reach_fact(fact.get ()); add_rf(fact.get ());
} }
} }
} }
@ -2164,7 +2164,7 @@ void context::init_rules(datalog::rule_set& rules, decl2rel& rels)
} }
// initialize reach facts // initialize reach facts
for (auto &entry : rels) {entry.m_value->init_reach_facts();} for (auto &entry : rels) {entry.m_value->init_rfs();}
} }
void context::inherit_lemmas(const decl2rel &rels) { void context::inherit_lemmas(const decl2rel &rels) {
@ -2505,7 +2505,7 @@ unsigned context::get_cex_depth()
pred_transformer* pt; pred_transformer* pt;
// get and discard query rule // get and discard query rule
fact = m_query->get_last_reach_fact (); fact = m_query->get_last_rf ();
r = &fact->get_rule (); r = &fact->get_rule ();
unsigned cex_depth = 0; unsigned cex_depth = 0;
@ -2580,7 +2580,7 @@ void context::get_rules_along_trace(datalog::rule_ref_vector& rules)
pred_transformer* pt; pred_transformer* pt;
// get query rule // get query rule
fact = m_query->get_last_reach_fact (); fact = m_query->get_last_rf ();
r = &fact->get_rule (); r = &fact->get_rule ();
rules.push_back (const_cast<datalog::rule *> (r)); rules.push_back (const_cast<datalog::rule *> (r));
TRACE ("spacer", TRACE ("spacer",
@ -2687,7 +2687,7 @@ expr_ref context::get_ground_sat_answer()
datalog::rule const* r; datalog::rule const* r;
// get and discard query rule // get and discard query rule
reach_fact = m_query->get_last_reach_fact (); reach_fact = m_query->get_last_rf ();
r = &reach_fact->get_rule (); r = &reach_fact->get_rule ();
// initialize queues // initialize queues
@ -3028,8 +3028,8 @@ bool context::is_reachable(pob &n)
mev.set_model(*model); mev.set_model(*model);
// -- update must summary // -- update must summary
if (r && r->get_uninterpreted_tail_size () > 0) { if (r && r->get_uninterpreted_tail_size () > 0) {
reach_fact_ref rf = n.pt().mk_reach_fact (n, mev, *r); reach_fact_ref rf = n.pt().mk_rf (n, mev, *r);
n.pt ().add_reach_fact (rf.get ()); n.pt ().add_rf (rf.get ());
} }
// if n has a derivation, create a new child and report l_undef // if n has a derivation, create a new child and report l_undef
@ -3168,9 +3168,9 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
if (is_concrete) { if (is_concrete) {
// -- update must summary // -- update must summary
if (r && r->get_uninterpreted_tail_size() > 0) { if (r && r->get_uninterpreted_tail_size() > 0) {
reach_fact_ref rf = n.pt().mk_reach_fact (n, mev, *r); reach_fact_ref rf = n.pt().mk_rf (n, mev, *r);
checkpoint (); checkpoint ();
n.pt ().add_reach_fact (rf.get ()); n.pt ().add_rf (rf.get ());
checkpoint (); checkpoint ();
} }
@ -3383,12 +3383,12 @@ bool context::propagate(unsigned min_prop_lvl,
return false; return false;
} }
reach_fact *pred_transformer::mk_reach_fact (pob& n, model_evaluator_util &mev, reach_fact *pred_transformer::mk_rf (pob& n, model_evaluator_util &mev,
const datalog::rule& r) const datalog::rule& r)
{ {
SASSERT(&n.pt() == this); SASSERT(&n.pt() == this);
timeit _timer1 (is_trace_enabled("spacer_timeit"), timeit _timer1 (is_trace_enabled("spacer_timeit"),
"mk_reach_fact", "mk_rf",
verbose_stream ()); verbose_stream ());
expr_ref res(m); expr_ref res(m);
reach_fact_ref_vector child_reach_facts; reach_fact_ref_vector child_reach_facts;
@ -3405,7 +3405,7 @@ reach_fact *pred_transformer::mk_reach_fact (pob& n, model_evaluator_util &mev,
pred_transformer& ch_pt = ctx.get_pred_transformer (pred); pred_transformer& ch_pt = ctx.get_pred_transformer (pred);
// get a reach fact of body preds used in the model // get a reach fact of body preds used in the model
expr_ref o_ch_reach (m); expr_ref o_ch_reach (m);
reach_fact *kid = ch_pt.get_used_origin_reach_fact (mev, i); reach_fact *kid = ch_pt.get_used_origin_rf (mev, i);
child_reach_facts.push_back (kid); child_reach_facts.push_back (kid);
pm.formula_n2o (kid->get (), o_ch_reach, i); pm.formula_n2o (kid->get (), o_ch_reach, i);
path_cons.push_back (o_ch_reach); path_cons.push_back (o_ch_reach);
@ -3444,7 +3444,7 @@ reach_fact *pred_transformer::mk_reach_fact (pob& n, model_evaluator_util &mev,
{ {
timeit _timer1 (is_trace_enabled("spacer_timeit"), timeit _timer1 (is_trace_enabled("spacer_timeit"),
"mk_reach_fact::qe_project", "mk_rf::qe_project",
verbose_stream ()); verbose_stream ());
mbp(vars, res, mev.get_model(), false /*, false */); mbp(vars, res, mev.get_model(), false /*, false */);
} }

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

@ -339,14 +339,14 @@ 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);
app_ref mk_fresh_reach_tag (); app_ref mk_fresh_rf_tag ();
public: public:
pred_transformer(context& ctx, manager& pm, func_decl* head); pred_transformer(context& ctx, manager& pm, func_decl* head);
~pred_transformer(); ~pred_transformer();
inline bool use_native_mbp (); inline bool use_native_mbp ();
reach_fact *get_reach_fact (expr *v) { reach_fact *get_rf (expr *v) {
for (auto *rf : m_reach_facts) { for (auto *rf : m_reach_facts) {
if (v == rf->get()) {return rf;} if (v == rf->get()) {return rf;}
} }
@ -379,9 +379,9 @@ public:
bool is_must_reachable(expr* state, model_ref* model = nullptr); bool is_must_reachable(expr* state, model_ref* model = nullptr);
/// \brief Returns reachability fact active in the given model /// \brief Returns reachability fact active in the given model
/// all determines whether initial reachability facts are included as well /// all determines whether initial reachability facts are included as well
reach_fact *get_used_reach_fact(model_evaluator_util& mev, bool all = true); reach_fact *get_used_rf(model_evaluator_util& mev, bool all = true);
/// \brief Returns reachability fact active in the origin of the given model /// \brief Returns reachability fact active in the origin of the given model
reach_fact* get_used_origin_reach_fact(model_evaluator_util &mev, unsigned oidx); reach_fact* get_used_origin_rf(model_evaluator_util &mev, unsigned oidx);
expr_ref get_origin_summary(model_evaluator_util &mev, expr_ref get_origin_summary(model_evaluator_util &mev,
unsigned level, unsigned oidx, bool must, unsigned level, unsigned oidx, bool must,
const ptr_vector<app> **aux); const ptr_vector<app> **aux);
@ -400,15 +400,15 @@ public:
bool add_lemma(expr * lemma, unsigned lvl); bool add_lemma(expr * lemma, unsigned lvl);
bool add_lemma(lemma* lem) {return m_frames.add_lemma(lem);} bool add_lemma(lemma* lem) {return m_frames.add_lemma(lem);}
expr* get_reach_case_var (unsigned idx) const; expr* get_reach_case_var (unsigned idx) const;
bool has_reach_facts () const { return !m_reach_facts.empty () ;} bool has_rfs () const { return !m_reach_facts.empty () ;}
/// initialize reachability facts using initial rules /// initialize reachability facts using initial rules
void init_reach_facts (); void init_rfs ();
reach_fact *mk_reach_fact(pob &n, model_evaluator_util &mev, reach_fact *mk_rf(pob &n, model_evaluator_util &mev,
const datalog::rule &r); const datalog::rule &r);
void add_reach_fact (reach_fact *fact); // add reachability fact void add_rf (reach_fact *fact); // add reachability fact
reach_fact* get_last_reach_fact () const { return m_reach_facts.back (); } reach_fact* get_last_rf () const { return m_reach_facts.back (); }
expr* get_last_reach_tag () const; expr* get_last_rf_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){