From 9054e729203931be474a9cdb15d6bc16e000cf01 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Dec 2022 19:35:20 -0800 Subject: [PATCH] fix #6467 --- src/muz/base/dl_rule.cpp | 25 ++++++++------- src/muz/base/dl_rule.h | 2 +- src/muz/base/dl_util.h | 23 +++++++------- src/muz/rel/dl_base.h | 2 +- src/muz/rel/dl_finite_product_relation.cpp | 2 +- src/muz/rel/dl_mk_explanations.cpp | 37 ++++++++++++---------- src/muz/rel/dl_relation_manager.cpp | 2 +- src/muz/rel/dl_sieve_relation.cpp | 4 +-- 8 files changed, 51 insertions(+), 46 deletions(-) diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index a1864d3b9..4ef02c03c 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -1013,28 +1013,31 @@ namespace datalog { } } - void rule::display(context & ctx, std::ostream & out) const { + void rule::display(context & ctx, std::ostream & out, bool compact) const { ast_manager & m = ctx.get_manager(); - out << m_name.str () << ":\n"; + if (!compact) + out << m_name.str () << ":\n"; output_predicate(ctx, m_head, out); if (m_tail_size == 0) { - out << ".\n"; + out << "."; + if (!compact) + out << "\n"; return; } out << " :- "; for (unsigned i = 0; i < m_tail_size; i++) { if (i > 0) out << ","; - out << "\n "; + if (!compact) + out << "\n"; + out << " "; if (is_neg_tail(i)) out << "not "; app * t = get_tail(i); - if (ctx.is_predicate(t)) { + if (ctx.is_predicate(t)) output_predicate(ctx, t, out); - } - else { + else out << mk_pp(t, m); - } } out << '.'; if (ctx.output_profile()) { @@ -1042,10 +1045,10 @@ namespace datalog { output_profile(out); out << '}'; } - out << '\n'; - if (m_proof) { + if (!compact) + out << '\n'; + if (m_proof) out << mk_pp(m_proof, m) << '\n'; - } } diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 6a21a2621..60b2bbe8f 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -365,7 +365,7 @@ namespace datalog { void get_vars(ast_manager& m, ptr_vector& sorts) const; - void display(context & ctx, std::ostream & out) const; + void display(context & ctx, std::ostream & out, bool compact = false) const; /** \brief Return the name(s) associated with this rule. Plural for preprocessed (e.g. obtained by inlining) rules. diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h index 4688a67fd..623f287f7 100644 --- a/src/muz/base/dl_util.h +++ b/src/muz/base/dl_util.h @@ -320,32 +320,31 @@ namespace datalog { unsigned_vector & res, bool & identity); template - void permutate_by_cycle(T & container, unsigned cycle_len, const unsigned * permutation_cycle) { - if (cycle_len<2) { + void permute_by_cycle(T& container, unsigned cycle_len, const unsigned * permutation_cycle) { + if (cycle_len < 2) return; - } auto aux = container[permutation_cycle[0]]; - for (unsigned i=1; i - void permutate_by_cycle(ref_vector & container, unsigned cycle_len, const unsigned * permutation_cycle) { + void permute_by_cycle(ref_vector & container, unsigned cycle_len, const unsigned * permutation_cycle) { if (cycle_len<2) { return; } + verbose_stream() << "ptr\n"; T * aux = container.get(permutation_cycle[0]); - for (unsigned i=1; i - void permutate_by_cycle(T & container, const unsigned_vector & permutation_cycle) { - permutate_by_cycle(container, permutation_cycle.size(), permutation_cycle.data()); + void permute_by_cycle(T & container, const unsigned_vector & permutation_cycle) { + permute_by_cycle(container, permutation_cycle.size(), permutation_cycle.data()); } diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index ea317ca45..f6d031624 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -160,7 +160,7 @@ namespace datalog { SASSERT(cycle_len>=2); result=src; - permutate_by_cycle(result, cycle_len, permutation_cycle); + permute_by_cycle(result, cycle_len, permutation_cycle); } /** diff --git a/src/muz/rel/dl_finite_product_relation.cpp b/src/muz/rel/dl_finite_product_relation.cpp index a991c9e6c..b1cdf0553 100644 --- a/src/muz/rel/dl_finite_product_relation.cpp +++ b/src/muz/rel/dl_finite_product_relation.cpp @@ -674,7 +674,7 @@ namespace datalog { unsigned sig_sz = r.get_signature().size(); unsigned_vector permutation; add_sequence(0, sig_sz, permutation); - permutate_by_cycle(permutation, cycle_len, permutation_cycle); + permute_by_cycle(permutation, cycle_len, permutation_cycle); unsigned_vector table_permutation; diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp index 7c5691c0a..37c67e0c8 100644 --- a/src/muz/rel/dl_mk_explanations.cpp +++ b/src/muz/rel/dl_mk_explanations.cpp @@ -70,20 +70,16 @@ namespace datalog { m_union_decl(mk_explanations::get_union_decl(get_context()), get_ast_manager()) {} ~explanation_relation_plugin() override { - for (unsigned i = 0; i < m_pool.size(); ++i) { - for (unsigned j = 0; j < m_pool[i].size(); ++j) { + for (unsigned i = 0; i < m_pool.size(); ++i) + for (unsigned j = 0; j < m_pool[i].size(); ++j) dealloc(m_pool[i][j]); - } - } } bool can_handle_signature(const relation_signature & s) override { unsigned n=s.size(); - for (unsigned i=0; iget_sort()), m_data[0]); + verbose_stream() << "FORMULA " << fml << "\n"; } bool is_undefined(unsigned col_idx) const { @@ -339,6 +340,7 @@ namespace datalog { if (!r.empty()) { relation_fact proj_data = r.m_data; project_out_vector_columns(proj_data, m_removed_cols); + verbose_stream() << "project\n"; res->assign_data(proj_data); } return res; @@ -365,9 +367,9 @@ namespace datalog { explanation_relation * res = static_cast(plugin.mk_empty(get_result_signature())); if (!r.empty()) { - relation_fact permutated_data = r.m_data; - permutate_by_cycle(permutated_data, m_cycle); - res->assign_data(permutated_data); + relation_fact permuted_data = r.m_data; + permute_by_cycle(dynamic_cast(permuted_data), m_cycle); + res->assign_data(permuted_data); } return res; } @@ -406,6 +408,7 @@ namespace datalog { } else { if (tgt.empty()) { + verbose_stream() << "union\n"; tgt.assign_data(src.m_data); if (delta && delta->empty()) { delta->assign_data(src.m_data); @@ -704,7 +707,7 @@ namespace datalog { symbol mk_explanations::get_rule_symbol(rule * r) { if (r->name() == symbol::null) { std::stringstream sstm; - r->display(m_context, sstm); + r->display(m_context, sstm, true); std::string res = sstm.str(); res = res.substr(0, res.find_last_not_of('\n')+1); return symbol(res.c_str()); diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index 9410e2ab0..8de25c8f3 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -1149,7 +1149,7 @@ namespace datalog { } void modify_fact(table_fact & f) const override { - permutate_by_cycle(f, m_cycle); + permute_by_cycle(f, m_cycle); } table_base * operator()(const table_base & t) override { diff --git a/src/muz/rel/dl_sieve_relation.cpp b/src/muz/rel/dl_sieve_relation.cpp index c7eab9549..801108999 100644 --- a/src/muz/rel/dl_sieve_relation.cpp +++ b/src/muz/rel/dl_sieve_relation.cpp @@ -413,14 +413,14 @@ namespace datalog { unsigned sig_sz = r.get_signature().size(); unsigned_vector permutation; add_sequence(0, sig_sz, permutation); - permutate_by_cycle(permutation, cycle_len, permutation_cycle); + permute_by_cycle(permutation, cycle_len, permutation_cycle); bool inner_identity; unsigned_vector inner_permutation; collect_sub_permutation(permutation, r.m_sig2inner, inner_permutation, inner_identity); bool_vector result_inner_cols = r.m_inner_cols; - permutate_by_cycle(result_inner_cols, cycle_len, permutation_cycle); + permute_by_cycle(result_inner_cols, cycle_len, permutation_cycle); relation_signature result_sig; relation_signature::from_rename(r.get_signature(), cycle_len, permutation_cycle, result_sig);