From 75953717218b55425198aa6c103171ccc5768fdd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Apr 2020 04:56:15 -0700 Subject: [PATCH] fix #3834 Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_context.cpp | 4 ++-- src/muz/base/dl_rule.cpp | 13 ++++++------- src/muz/base/dl_rule.h | 4 ++-- src/muz/base/rule_properties.cpp | 18 ++++++++++-------- src/muz/base/rule_properties.h | 2 ++ 5 files changed, 22 insertions(+), 19 deletions(-) diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index dfe5b8fc4..3bec0738b 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -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(); } diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index 5b8e1c733..ddb84c77e 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -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); } } diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 55e482bb7..8371d4871 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -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); diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index 3696ae1de..28c2f7dfe 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -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 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; } diff --git a/src/muz/base/rule_properties.h b/src/muz/base/rule_properties.h index 364af65b9..fbc2466fb 100644 --- a/src/muz/base/rule_properties.h +++ b/src/muz/base/rule_properties.h @@ -46,6 +46,7 @@ namespace datalog { ptr_vector m_interp_pred; ptr_vector m_negative_rules; ptr_vector m_inf_sort; + bool m_collected; void insert(ptr_vector& 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);