diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index 184a5fa02..017bac724 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -978,13 +978,14 @@ namespace datalog { } } - void rule::get_vars(ptr_vector& sorts) const { + void rule::get_vars(ast_manager& m, ptr_vector& 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()); } } diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 1c31dc6b4..7104bae1f 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -304,7 +304,7 @@ namespace datalog { void norm_vars(rule_manager & rm); - void get_vars(ptr_vector& sorts) const; + void get_vars(ast_manager& m, ptr_vector& sorts) const; void to_formula(expr_ref& result) const; diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp index 0dcbf4644..51b1a5295 100644 --- a/src/muz/bmc/dl_bmc_engine.cpp +++ b/src/muz/bmc/dl_bmc_engine.cpp @@ -148,7 +148,7 @@ namespace datalog { void mk_qrule_vars(datalog::rule const& r, unsigned rule_id, expr_ref_vector& sub) { ptr_vector 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 rule_vars; expr_ref_vector args(m), conjs(m); - r.get_vars(rule_vars); + r.get_vars(m, rule_vars); obj_hashtable 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 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 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 sorts; - r.get_vars(sorts); + r.get_vars(m, sorts); // populate substitution of bound variables. sub.reset(); sub.resize(sorts.size()); diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp index 9303181b6..641d40779 100644 --- a/src/muz/transforms/dl_mk_array_blast.cpp +++ b/src/muz/transforms/dl_mk_array_blast.cpp @@ -87,7 +87,7 @@ namespace datalog { else { if (m_next_var == 0) { ptr_vector 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)); diff --git a/src/muz/transforms/dl_mk_coalesce.cpp b/src/muz/transforms/dl_mk_coalesce.cpp index 8c7f1d5b4..ac7a58d8d 100644 --- a/src/muz/transforms/dl_mk_coalesce.cpp +++ b/src/muz/transforms/dl_mk_coalesce.cpp @@ -62,7 +62,7 @@ namespace datalog { rule_ref r(const_cast(&rl), rm); ptr_vector sorts; expr_ref_vector revsub(m), conjs(m); - rl.get_vars(sorts); + rl.get_vars(m, sorts); revsub.resize(sorts.size()); svector 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 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) { diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp index 9c55ca658..fcb8d7b85 100644 --- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp +++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp @@ -199,7 +199,7 @@ namespace datalog { expr_ref fml(m), cnst(m); var_ref var(m); ptr_vector 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); diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index 712c82feb..522bd2e86 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -143,11 +143,8 @@ namespace datalog { expr_ref_vector result(m); ptr_vector 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); diff --git a/src/muz/transforms/dl_mk_scale.cpp b/src/muz/transforms/dl_mk_scale.cpp index 9ada7be20..271bf5f62 100644 --- a/src/muz/transforms/dl_mk_scale.cpp +++ b/src/muz/transforms/dl_mk_scale.cpp @@ -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)));