mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

Cleanup

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-22 09:34:01 -07:00
parent 68b7966254
commit 95d820196b
2 changed files with 118 additions and 154 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -658,16 +658,8 @@ pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head):
m_extend_lit = m.mk_not (m.mk_const (pm.get_n_pred (v->get_decl ()))); m_extend_lit = m.mk_not (m.mk_const (pm.get_n_pred (v->get_decl ())));
} }
pred_transformer::~pred_transformer() pred_transformer::~pred_transformer() {
{ for (auto &entry : m_rule2transition) {m.dec_ref(entry.m_value);}
rule2inst::iterator it2 = m_rule2inst.begin(), end2 = m_rule2inst.end();
for (; it2 != end2; ++it2) {
dealloc(it2->m_value);
}
rule2expr::iterator it3 = m_rule2transition.begin(), end3 = m_rule2transition.end();
for (; it3 != end3; ++it3) {
m.dec_ref(it3->m_value);
}
} }
std::ostream& pred_transformer::display(std::ostream& out) const std::ostream& pred_transformer::display(std::ostream& out) const
@ -1556,20 +1548,19 @@ void pred_transformer::init_rule(decl2rel const& pts, datalog::rule const& rule,
// Predicates that are variable representatives. Other predicates at // Predicates that are variable representatives. Other predicates at
// positions the variables occur are made equivalent with these. // positions the variables occur are made equivalent with these.
expr_ref_vector side(m); expr_ref_vector side(m);
app_ref_vector* var_reprs = alloc(app_ref_vector, m); app_ref_vector var_reprs(m);
SASSERT(var_reprs);
ptr_vector<app> aux_vars; ptr_vector<app> aux_vars;
unsigned ut_size = rule.get_uninterpreted_tail_size(); unsigned ut_size = rule.get_uninterpreted_tail_size();
unsigned t_size = rule.get_tail_size(); unsigned t_size = rule.get_tail_size();
SASSERT(ut_size <= t_size); SASSERT(ut_size <= t_size);
init_atom(pts, rule.get_head(), *var_reprs, side, UINT_MAX); init_atom(pts, rule.get_head(), var_reprs, side, UINT_MAX);
for (unsigned i = 0; i < ut_size; ++i) { for (unsigned i = 0; i < ut_size; ++i) {
if (rule.is_neg_tail(i)) { if (rule.is_neg_tail(i)) {
throw default_exception("SPACER does not support " throw default_exception("SPACER does not support "
"negated predicates in rule tails"); "negated predicates in rule tails");
} }
init_atom(pts, rule.get_tail(i), *var_reprs, side, i); init_atom(pts, rule.get_tail(i), var_reprs, side, i);
} }
// -- substitute free variables // -- substitute free variables
expr_ref fml(m); expr_ref fml(m);
@ -1579,12 +1570,12 @@ void pred_transformer::init_rule(decl2rel const& pts, datalog::rule const& rule,
{tail.push_back(rule.get_tail(i));} {tail.push_back(rule.get_tail(i));}
fml = mk_and (tail); fml = mk_and (tail);
ground_free_vars(fml, *var_reprs, aux_vars, ut_size == 0); ground_free_vars(fml, var_reprs, aux_vars, ut_size == 0);
SASSERT(is_all_non_null(*var_reprs)); SASSERT(is_all_non_null(var_reprs));
expr_ref tmp(m); expr_ref tmp(m);
var_subst (m, false)(fml, var_reprs->size (), var_subst(m, false)(fml, var_reprs.size (),
(expr*const*)var_reprs->c_ptr(), tmp); (expr*const*)var_reprs.c_ptr(), tmp);
flatten_and (tmp, side); flatten_and (tmp, side);
fml = mk_and(side); fml = mk_and(side);
side.reset (); side.reset ();
@ -1607,12 +1598,11 @@ void pred_transformer::init_rule(decl2rel const& pts, datalog::rule const& rule,
m_rule2transition.insert(&rule, fml); m_rule2transition.insert(&rule, fml);
} }
// AG: shouldn't this be under the if-statement above? // AG: shouldn't this be under the if-statement above?
m_rule2inst.insert(&rule, var_reprs);
m_rule2vars.insert(&rule, aux_vars); m_rule2vars.insert(&rule, aux_vars);
TRACE("spacer", TRACE("spacer",
tout << rule.get_decl()->get_name() << "\n"; tout << rule.get_decl()->get_name() << "\n";
tout << *var_reprs << "\n";); tout << var_reprs << "\n";);
} }

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

@ -266,10 +266,10 @@ class pred_transformer {
typedef obj_map<datalog::rule const, expr*> rule2expr; typedef obj_map<datalog::rule const, expr*> rule2expr;
typedef obj_map<datalog::rule const, ptr_vector<app> > rule2apps; typedef obj_map<datalog::rule const, ptr_vector<app> > rule2apps;
typedef obj_map<expr, datalog::rule const*> expr2rule;
manager& pm; // spacer-manager manager& pm; // spacer::manager
ast_manager& m; // manager ast_manager& m; // ast_manager
context& ctx; context& ctx; // spacer::context
func_decl_ref m_head; // predicate func_decl_ref m_head; // predicate
func_decl_ref_vector m_sig; // signature func_decl_ref_vector m_sig; // signature
@ -277,21 +277,19 @@ class pred_transformer {
ptr_vector<datalog::rule> m_rules; // rules used to derive transformer ptr_vector<datalog::rule> m_rules; // rules used to derive transformer
prop_solver m_solver; // solver context prop_solver m_solver; // solver context
solver* m_reach_ctx; // context for reachability facts solver* m_reach_ctx; // context for reachability facts
pobs m_pobs; pobs m_pobs; // proof obligations created so far
frames m_frames; frames m_frames; // frames with lemmas
reach_fact_ref_vector m_reach_facts; // reach facts reach_fact_ref_vector m_reach_facts; // reach facts
/// Number of initial reachability facts unsigned m_rf_init_sz; // number of reach fact from INIT
unsigned m_rf_init_sz; expr2rule m_tag2rule; // map tag predicate to rule.
obj_map<expr, datalog::rule const*> m_tag2rule; // map tag predicate to rule.
rule2expr m_rule2tag; // map rule to predicate tag. rule2expr m_rule2tag; // map rule to predicate tag.
rule2inst m_rule2inst; // map rules to instantiations of indices
rule2expr m_rule2transition; // map rules to transition rule2expr m_rule2transition; // map rules to transition
rule2apps m_rule2vars; // map rule to auxiliary variables rule2apps m_rule2vars; // map rule to auxiliary variables
expr_ref m_transition; // transition relation. expr_ref m_transition; // transition relation.
expr_ref m_initial_state; // initial state. expr_ref m_initial_state; // initial state.
app_ref m_extend_lit; // literal to extend initial state app_ref m_extend_lit; // 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; ptr_vector<func_decl> m_predicates; // temp vector used with find_predecessors()
stats m_stats; stats m_stats;
stopwatch m_initialize_watch; stopwatch m_initialize_watch;
stopwatch m_must_reachable_watch; stopwatch m_must_reachable_watch;
@ -320,7 +318,6 @@ class pred_transformer {
void simplify_formulas(tactic& tac, expr_ref_vector& fmls); void simplify_formulas(tactic& tac, expr_ref_vector& fmls);
// Debugging
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 (); expr* mk_fresh_reach_case_var ();
@ -330,12 +327,13 @@ public:
~pred_transformer(); ~pred_transformer();
inline bool use_native_mbp (); inline bool use_native_mbp ();
reach_fact *get_reach_fact (expr *v) reach_fact *get_reach_fact (expr *v) {
{ for (auto *rf : m_reach_facts) {
for (unsigned i = 0, sz = m_reach_facts.size (); i < sz; ++i) if (v == rf->get()) {return rf;}
if(v == m_reach_facts [i]->get()) { return m_reach_facts[i]; } }
return nullptr; return nullptr;
} }
void find_predecessors(datalog::rule const& r, ptr_vector<func_decl>& predicates) const;
void add_rule(datalog::rule* r) {m_rules.push_back(r);} void add_rule(datalog::rule* r) {m_rules.push_back(r);}
void add_use(pred_transformer* pt) {if(!m_use.contains(pt)) {m_use.insert(pt);}} void add_use(pred_transformer* pt) {if(!m_use.contains(pt)) {m_use.insert(pt);}}
@ -369,7 +367,6 @@ public:
unsigned level, unsigned oidx, bool must, unsigned level, unsigned oidx, bool must,
const ptr_vector<app> **aux); const ptr_vector<app> **aux);
void find_predecessors(datalog::rule const& r, ptr_vector<func_decl>& predicates) const;
datalog::rule const* find_rule(model &mev, bool& is_concrete, datalog::rule const* find_rule(model &mev, bool& is_concrete,
vector<bool>& reach_pred_used, vector<bool>& reach_pred_used,
unsigned& num_reuse_reach); unsigned& num_reuse_reach);
@ -409,8 +406,10 @@ public:
unsigned& solver_level, expr_ref_vector* core = nullptr); unsigned& solver_level, expr_ref_vector* core = nullptr);
bool is_invariant(unsigned level, expr* lem, bool is_invariant(unsigned level, expr* lem,
unsigned& solver_level, expr_ref_vector* core = nullptr) unsigned& solver_level, expr_ref_vector* core = nullptr) {
{ UNREACHABLE(); return false; } // XXX only needed for legacy_frames to compile
UNREACHABLE(); return false;
}
bool check_inductive(unsigned level, expr_ref_vector& state, bool check_inductive(unsigned level, expr_ref_vector& state,
unsigned& assumes_level, unsigned weakness = UINT_MAX); unsigned& assumes_level, unsigned weakness = UINT_MAX);
@ -546,8 +545,7 @@ public:
double get_expand_time(unsigned depth) { return m_expand_watches[depth].get_seconds();} double get_expand_time(unsigned depth) { return m_expand_watches[depth].get_seconds();}
void inc_ref () {++m_ref_count;} void inc_ref () {++m_ref_count;}
void dec_ref () void dec_ref () {
{
--m_ref_count; --m_ref_count;
if(m_ref_count == 0) {dealloc(this);} if(m_ref_count == 0) {dealloc(this);}
} }
@ -630,6 +628,8 @@ class derivation {
/// -- create next child using given model as the guide /// -- create next child using given model as the guide
/// -- returns NULL if there is no next child /// -- returns NULL if there is no next child
pob* create_next_child (model_evaluator_util &mev); pob* create_next_child (model_evaluator_util &mev);
/// existentially quantify vars and skolemize the result
void exist_skolemize(expr *fml, app_ref_vector &vars, expr_ref &res);
public: public:
derivation (pob& parent, datalog::rule const& rule, derivation (pob& parent, datalog::rule const& rule,
expr *trans, app_ref_vector const &evars); expr *trans, app_ref_vector const &evars);
@ -645,8 +645,6 @@ public:
/// premise must be consistent with the transition relation /// premise must be consistent with the transition relation
pob *create_next_child (); pob *create_next_child ();
/// existentially quantify vars and skolemize the result
void exist_skolemize(expr *fml, app_ref_vector &vars, expr_ref &res);
datalog::rule const& get_rule () const { return m_rule; } datalog::rule const& get_rule () const { return m_rule; }
pob& get_parent () const { return m_parent; } pob& get_parent () const { return m_parent; }
ast_manager &get_ast_manager () const {return m_parent.get_ast_manager ();} ast_manager &get_ast_manager () const {return m_parent.get_ast_manager ();}
@ -672,8 +670,7 @@ public:
void pop () {m_obligations.pop ();} void pop () {m_obligations.pop ();}
void push (pob &n); void push (pob &n);
void inc_level () void inc_level () {
{
SASSERT (!m_obligations.empty () || m_root); SASSERT (!m_obligations.empty () || m_root);
m_max_level++; m_max_level++;
m_min_depth++; m_min_depth++;
@ -687,7 +684,6 @@ public:
unsigned max_level() {return m_max_level;} unsigned max_level() {return m_max_level;}
unsigned min_depth() {return m_min_depth;} unsigned min_depth() {return m_min_depth;}
size_t size() {return m_obligations.size();} size_t size() {return m_obligations.size();}
}; };
@ -797,12 +793,14 @@ class context {
lbool expand_pob(pob &n, pob_ref_buffer &out); lbool expand_pob(pob &n, pob_ref_buffer &out);
reach_fact *mk_reach_fact(pob& n, model_evaluator_util &mev, reach_fact *mk_reach_fact(pob& n, model_evaluator_util &mev,
datalog::rule const& r); datalog::rule const& r);
bool create_children(pob& n, datalog::rule const& r, bool create_children(pob& n, const datalog::rule &r,
model_evaluator_util &model, model_evaluator_util &mdl,
const vector<bool>& reach_pred_used, const vector<bool>& reach_pred_used,
pob_ref_buffer &out); pob_ref_buffer &out);
expr_ref mk_sat_answer(); expr_ref mk_sat_answer();
expr_ref mk_unsat_answer() const; expr_ref mk_unsat_answer() const;
unsigned get_cex_depth ();
// Generate inductive property // Generate inductive property
void get_level_property(unsigned lvl, expr_ref_vector& res, void get_level_property(unsigned lvl, expr_ref_vector& res,
@ -811,27 +809,21 @@ class context {
// Initialization // Initialization
void init_lemma_generalizers(); void init_lemma_generalizers();
void reset_lemma_generalizers();
void inherit_lemmas(const decl2rel& rels); void inherit_lemmas(const decl2rel& rels);
void init_global_smt_params(); void init_global_smt_params();
void init_rules(datalog::rule_set& rules, decl2rel& transformers);
// (re)initialize context with new relations
void init(const decl2rel &rels);
bool validate();
bool check_invariant(unsigned lvl); bool check_invariant(unsigned lvl);
bool check_invariant(unsigned lvl, func_decl* fn); bool check_invariant(unsigned lvl, func_decl* fn);
void checkpoint(); void checkpoint();
void init_rules(datalog::rule_set& rules, decl2rel& transformers);
// (re)initialize context with new relations
void init(const decl2rel &rels);
void simplify_formulas(); void simplify_formulas();
void reset_lemma_generalizers();
bool validate();
unsigned get_cex_depth ();
void dump_json(); void dump_json();
void predecessor_eh(); void predecessor_eh();
@ -839,16 +831,12 @@ class context {
public: public:
/** /**
Initial values of predicates are stored in corresponding relations in dctx. Initial values of predicates are stored in corresponding relations in dctx.
We check whether there is some reachable state of the relation checked_relation. We check whether there is some reachable state of the relation checked_relation.
*/ */
context( context(fixedpoint_params const& params, ast_manager& m);
fixedpoint_params const& params,
ast_manager& m);
~context(); ~context();
fixedpoint_params const& get_params() const { return m_params; } const fixedpoint_params &get_params() const { return m_params; }
bool use_native_mbp () {return m_use_native_mbp;} bool use_native_mbp () {return m_use_native_mbp;}
bool use_ground_cti () {return m_ground_cti;} bool use_ground_cti () {return m_ground_cti;}
bool use_instantiate () {return m_instantiate;} bool use_instantiate () {return m_instantiate;}
@ -858,67 +846,53 @@ public:
ast_manager& get_ast_manager() const {return m;} ast_manager& get_ast_manager() const {return m;}
manager& get_manager() {return m_pm;} manager& get_manager() {return m_pm;}
decl2rel const& get_pred_transformers() const {return m_rels;} decl2rel const& get_pred_transformers() const {return m_rels;}
pred_transformer& get_pred_transformer(func_decl* p) const pred_transformer& get_pred_transformer(func_decl* p) const {return *m_rels.find(p);}
{ return *m_rels.find(p); }
datalog::context& get_datalog_context() const datalog::context& get_datalog_context() const {
{ SASSERT(m_context); return *m_context; } SASSERT(m_context); return *m_context;
}
void update_rules(datalog::rule_set& rules);
lbool solve(unsigned from_lvl = 0);
lbool solve_from_lvl (unsigned from_lvl);
expr_ref get_answer(); expr_ref get_answer();
/** /**
* get bottom-up (from query) sequence of ground predicate instances * get bottom-up (from query) sequence of ground predicate instances
* (for e.g. P(0,1,0,0,3)) that together form a ground derivation to query * (for e.g. P(0,1,0,0,3)) that together form a ground derivation to query
*/ */
expr_ref get_ground_sat_answer (); expr_ref get_ground_sat_answer ();
void get_rules_along_trace (datalog::rule_ref_vector& rules);
void collect_statistics(statistics& st) const; void collect_statistics(statistics& st) const;
void reset_statistics(); void reset_statistics();
std::ostream& display(std::ostream& strm) const;
void display_certificate(std::ostream& strm) const {}
lbool solve(unsigned from_lvl = 0);
lbool solve_from_lvl (unsigned from_lvl);
void reset(); void reset();
std::ostream& display(std::ostream& out) const;
void display_certificate(std::ostream& out) const {NOT_IMPLEMENTED_YET();}
pob& get_root() const {return m_pob_queue.get_root();}
void set_query(func_decl* q) {m_query_pred = q;} void set_query(func_decl* q) {m_query_pred = q;}
void set_unsat() {m_last_result = l_false;} void set_unsat() {m_last_result = l_false;}
void set_model_converter(model_converter_ref& mc) {m_mc = mc;} void set_model_converter(model_converter_ref& mc) {m_mc = mc;}
void get_rules_along_trace (datalog::rule_ref_vector& rules);
model_converter_ref get_model_converter() { return m_mc; } model_converter_ref get_model_converter() { return m_mc; }
void set_proof_converter(proof_converter_ref& pc) { m_pc = pc; } void set_proof_converter(proof_converter_ref& pc) { m_pc = pc; }
scoped_ptr_vector<spacer_callback> &callbacks() {return m_callbacks;}
void update_rules(datalog::rule_set& rules);
unsigned get_num_levels(func_decl* p); unsigned get_num_levels(func_decl* p);
expr_ref get_cover_delta(int level, func_decl* p_orig, func_decl* p); expr_ref get_cover_delta(int level, func_decl* p_orig, func_decl* p);
void add_cover(int level, func_decl* pred, expr* property); void add_cover(int level, func_decl* pred, expr* property);
expr_ref get_reachable (func_decl* p); expr_ref get_reachable (func_decl* p);
void add_invariant (func_decl *pred, expr* property); void add_invariant (func_decl *pred, expr* property);
model_ref get_model(); model_ref get_model();
proof_ref get_proof() const; proof_ref get_proof() const;
pob& get_root() const { return m_pob_queue.get_root(); }
expr_ref get_constraints (unsigned lvl); expr_ref get_constraints (unsigned lvl);
void add_constraint (expr *c, unsigned lvl); void add_constraint (expr *c, unsigned lvl);
void new_lemma_eh(pred_transformer &pt, lemma *lem); void new_lemma_eh(pred_transformer &pt, lemma *lem);
scoped_ptr_vector<spacer_callback> &callbacks() {return m_callbacks;}
void new_pob_eh(pob *p); void new_pob_eh(pob *p);
bool is_inductive(); bool is_inductive();