mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

make get_vars populate all indices with sorts even if variable does not occur in rule. This makes the use of get_vars less prone to callers having to double check for null pointers

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-07-21 17:12:39 +02:00
parent 72fe197bda
commit 4957e71408
8 changed files with 16 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/muz/base/dl_rule.cpp
View file

@ -978,13 +978,14 @@ namespace datalog {
}
}
void rule::get_vars(ptr_vector<sort>& sorts) const {
void rule::get_vars(ast_manager& m, ptr_vector<sort>& sorts) const {
sorts.reset();
used_vars used;
get_used_vars(used);
unsigned sz = used.get_max_found_var_idx_plus_1();
for (unsigned i = 0; i < sz; ++i) {
sorts.push_back(used.get(i));
sort* s = used.get(i);
sorts.push_back(s?s:m.mk_bool_sort());
}
}

2
src/muz/base/dl_rule.h
View file

@ -304,7 +304,7 @@ namespace datalog {
void norm_vars(rule_manager & rm);
void get_vars(ptr_vector<sort>& sorts) const;
void get_vars(ast_manager& m, ptr_vector<sort>& sorts) const;
void to_formula(expr_ref& result) const;

10
src/muz/bmc/dl_bmc_engine.cpp
View file

@ -148,7 +148,7 @@ namespace datalog {
void mk_qrule_vars(datalog::rule const& r, unsigned rule_id, expr_ref_vector& sub) {
ptr_vector<sort> sorts;
r.get_vars(sorts);
r.get_vars(m, sorts);
// populate substitution of bound variables.
sub.reset();
sub.resize(sorts.size());
@ -421,7 +421,7 @@ namespace datalog {
ptr_vector<sort> rule_vars;
expr_ref_vector args(m), conjs(m);
r.get_vars(rule_vars);
r.get_vars(m, rule_vars);
obj_hashtable<expr> used_vars;
unsigned num_vars = 0;
for (unsigned i = 0; i < r.get_decl()->get_arity(); ++i) {
@ -514,7 +514,7 @@ namespace datalog {
unsigned sz = r->get_uninterpreted_tail_size();
ptr_vector<sort> rule_vars;
r->get_vars(rule_vars);
r->get_vars(m, rule_vars);
args.append(prop->get_num_args(), prop->get_args());
expr_ref_vector sub = mk_skolem_binding(*r, rule_vars, args);
if (sub.empty() && sz == 0) {
@ -803,7 +803,7 @@ namespace datalog {
func_decl* p = r.get_decl();
ptr_vector<func_decl> const& succs = *dtu.get_datatype_constructors(m.get_sort(path));
// populate substitution of bound variables.
r.get_vars(sorts);
r.get_vars(m, sorts);
sub.reset();
sub.resize(sorts.size());
for (unsigned k = 0; k < r.get_decl()->get_arity(); ++k) {
@ -1327,7 +1327,7 @@ namespace datalog {
void mk_rule_vars(rule& r, unsigned level, unsigned rule_id, expr_ref_vector& sub) {
ptr_vector<sort> sorts;
r.get_vars(sorts);
r.get_vars(m, sorts);
// populate substitution of bound variables.
sub.reset();
sub.resize(sorts.size());

2
src/muz/transforms/dl_mk_array_blast.cpp
View file

@ -87,7 +87,7 @@ namespace datalog {
else {
if (m_next_var == 0) {
ptr_vector<sort> vars;
r.get_vars(vars);
r.get_vars(m, vars);
m_next_var = vars.size() + 1;
}
v = m.mk_var(m_next_var, m.get_sort(e));

6
src/muz/transforms/dl_mk_coalesce.cpp
View file

@ -62,7 +62,7 @@ namespace datalog {
rule_ref r(const_cast<rule*>(&rl), rm);
ptr_vector<sort> sorts;
expr_ref_vector revsub(m), conjs(m);
rl.get_vars(sorts);
rl.get_vars(m, sorts);
revsub.resize(sorts.size());
svector<bool> valid(sorts.size(), true);
for (unsigned i = 0; i < sub.size(); ++i) {
@ -117,8 +117,8 @@ namespace datalog {
rule_ref res(rm);
bool_rewriter bwr(m);
svector<bool> is_neg;
tgt->get_vars(sorts1);
src.get_vars(sorts2);
tgt->get_vars(m, sorts1);
src.get_vars(m, sorts2);
mk_pred(head, src.get_head(), tgt->get_head());
for (unsigned i = 0; i < src.get_uninterpreted_tail_size(); ++i) {

5
src/muz/transforms/dl_mk_quantifier_instantiation.cpp
View file

@ -199,7 +199,7 @@ namespace datalog {
expr_ref fml(m), cnst(m);
var_ref var(m);
ptr_vector<sort> sorts;
r.get_vars(sorts);
r.get_vars(m, sorts);
m_uf.reset();
m_terms.reset();
m_var2cnst.reset();
@ -207,9 +207,6 @@ namespace datalog {
fml = m.mk_and(conjs.size(), conjs.c_ptr());
for (unsigned i = 0; i < sorts.size(); ++i) {
if (!sorts[i]) {
sorts[i] = m.mk_bool_sort();
}
var = m.mk_var(i, sorts[i]);
cnst = m.mk_fresh_const("C", sorts[i]);
m_var2cnst.insert(var, cnst);

5
src/muz/transforms/dl_mk_rule_inliner.cpp
View file

@ -143,11 +143,8 @@ namespace datalog {
expr_ref_vector result(m);
ptr_vector<sort> sorts;
expr_ref v(m), w(m);
r.get_vars(sorts);
r.get_vars(m, sorts);
for (unsigned i = 0; i < sorts.size(); ++i) {
if (!sorts[i]) {
sorts[i] = m.mk_bool_sort();
}
v = m.mk_var(i, sorts[i]);
m_subst.apply(2, m_deltas, expr_offset(v, is_tgt?0:1), w);
result.push_back(w);

2
src/muz/transforms/dl_mk_scale.cpp
View file

@ -141,7 +141,7 @@ namespace datalog {
m_cache.reset();
m_trail.reset();
m_eqs.reset();
r.get_vars(vars);
r.get_vars(m, vars);
unsigned num_vars = vars.size();
for (unsigned j = 0; j < utsz; ++j) {
tail.push_back(mk_pred(num_vars, r.get_tail(j)));