mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

fix #3834

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-08 04:56:15 -07:00
parent dde0c9bd0d
commit 7595371721
5 changed files with 22 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/muz/base/dl_context.cpp
View file

@ -885,8 +885,8 @@ namespace datalog {
}
bool context::is_monotone() {
// only the spacer engine uses monotone semantics.
return get_engine() == SPACER_ENGINE;
// assumes flush_add_rules was called
return m_rule_properties.is_monotone();
}

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

@ -1000,19 +1000,18 @@ namespace datalog {
var_subst vs(m, false);
expr_ref new_head_e = vs(m_head, subst_vals.size(), subst_vals.c_ptr());
m.inc_ref(new_head_e);
app_ref new_head_a = rm.ensure_app(vs(m_head, subst_vals.size(), subst_vals.c_ptr()));
m.inc_ref(new_head_a);
m.dec_ref(m_head);
m_head = to_app(new_head_e);
m_head = new_head_a;
for (unsigned i = 0; i < m_tail_size; i++) {
app * old_tail = get_tail(i);
expr_ref new_tail_e = vs(old_tail, subst_vals.size(), subst_vals.c_ptr());
app_ref new_tail_a = rm.ensure_app(vs(old_tail, subst_vals.size(), subst_vals.c_ptr()));
bool sign = is_neg_tail(i);
m.inc_ref(new_tail_e);
m.inc_ref(new_tail_a);
m.dec_ref(old_tail);
m_tail[i] = TAG(app *, to_app(new_tail_e), sign);
m_tail[i] = TAG(app *, new_tail_a.get(), sign);
}
}

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

@ -151,8 +151,6 @@ namespace datalog {
void remove_labels(expr_ref& fml, proof_ref& pr);
app_ref ensure_app(expr* e);
void check_app(expr* e);
bool contains_predicate(expr* fml) const;
@ -274,6 +272,8 @@ namespace datalog {
rule_counter& get_counter() { return m_counter; }
app_ref ensure_app(expr* e);
void to_formula(rule const& r, expr_ref& result);
std::ostream& display_smt2(rule const& r, std::ostream & out);

18
src/muz/base/rule_properties.cpp
View file

@ -26,12 +26,15 @@ Notes:
using namespace datalog;
rule_properties::rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& p):
m(m), rm(rm), m_ctx(ctx), m_is_predicate(p), m_dt(m), m_dl(m), m_a(m), m_bv(m), m_ar(m), m_generate_proof(false) {}
m(m), rm(rm), m_ctx(ctx), m_is_predicate(p),
m_dt(m), m_dl(m), m_a(m), m_bv(m), m_ar(m),
m_generate_proof(false), m_collected(false) {}
rule_properties::~rule_properties() {}
void rule_properties::collect(rule_set const& rules) {
reset();
m_collected = true;
expr_sparse_mark visited;
for (rule* r : rules) {
m_rule = r;
@ -115,12 +118,11 @@ void rule_properties::check_nested_free() {
void rule_properties::check_existential_tail() {
ast_mark visited;
ptr_vector<expr> todo, tocheck;
for (unsigned i = 0; i < m_interp_pred.size(); ++i) {
rule& r = *m_interp_pred[i];
unsigned ut_size = r.get_uninterpreted_tail_size();
unsigned t_size = r.get_tail_size();
for (rule* r : m_interp_pred) {
unsigned ut_size = r->get_uninterpreted_tail_size();
unsigned t_size = r->get_tail_size();
for (unsigned i = ut_size; i < t_size; ++i) {
todo.push_back(r.get_tail(i));
todo.push_back(r->get_tail(i));
}
}
context::contains_pred contains_p(m_ctx);
@ -155,8 +157,7 @@ void rule_properties::check_existential_tail() {
tocheck.push_back(e);
}
}
for (unsigned i = 0; i < tocheck.size(); ++i) {
expr* e = tocheck[i];
for (expr* e : tocheck) {
if (check_pred(e)) {
std::ostringstream out;
out << "recursive predicate " << mk_ismt2_pp(e, m) << " occurs nested in the body of a rule";
@ -225,5 +226,6 @@ void rule_properties::reset() {
m_interp_pred.reset();
m_negative_rules.reset();
m_inf_sort.reset();
m_collected = false;
}

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

@ -46,6 +46,7 @@ namespace datalog {
ptr_vector<rule> m_interp_pred;
ptr_vector<rule> m_negative_rules;
ptr_vector<rule> m_inf_sort;
bool m_collected;
void insert(ptr_vector<rule>& rules, rule* r);
void check_sort(sort* s);
@ -61,6 +62,7 @@ namespace datalog {
void check_for_negated_predicates();
void check_nested_free();
void check_infinite_sorts();
bool is_monotone() { SASSERT(m_collected); return m_negative_rules.empty(); }
void operator()(var* n);
void operator()(quantifier* n);
void operator()(app* n);