mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

fix #6467

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-12-13 19:35:20 -08:00
parent cd3d38caf7
commit 9054e72920
8 changed files with 51 additions and 46 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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(); ast_manager & m = ctx.get_manager();
out << m_name.str () << ":\n"; if (!compact)
out << m_name.str () << ":\n";
output_predicate(ctx, m_head, out); output_predicate(ctx, m_head, out);
if (m_tail_size == 0) { if (m_tail_size == 0) {
out << ".\n"; out << ".";
if (!compact)
out << "\n";
return; return;
} }
out << " :- "; out << " :- ";
for (unsigned i = 0; i < m_tail_size; i++) { for (unsigned i = 0; i < m_tail_size; i++) {
if (i > 0) if (i > 0)
out << ","; out << ",";
out << "\n "; if (!compact)
out << "\n";
out << " ";
if (is_neg_tail(i)) if (is_neg_tail(i))
out << "not "; out << "not ";
app * t = get_tail(i); app * t = get_tail(i);
if (ctx.is_predicate(t)) { if (ctx.is_predicate(t))
output_predicate(ctx, t, out); output_predicate(ctx, t, out);
} else
else {
out << mk_pp(t, m); out << mk_pp(t, m);
}
} }
out << '.'; out << '.';
if (ctx.output_profile()) { if (ctx.output_profile()) {
@ -1042,10 +1045,10 @@ namespace datalog {
output_profile(out); output_profile(out);
out << '}'; out << '}';
} }
out << '\n'; if (!compact)
if (m_proof) { out << '\n';
if (m_proof)
out << mk_pp(m_proof, m) << '\n'; out << mk_pp(m_proof, m) << '\n';
}
} }

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

@ -365,7 +365,7 @@ namespace datalog {
void get_vars(ast_manager& m, ptr_vector<sort>& sorts) const; void get_vars(ast_manager& m, ptr_vector<sort>& 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. \brief Return the name(s) associated with this rule. Plural for preprocessed (e.g. obtained by inlining) rules.

23
src/muz/base/dl_util.h
View file

@ -320,32 +320,31 @@ namespace datalog {
unsigned_vector & res, bool & identity); unsigned_vector & res, bool & identity);
template<class T> template<class T>
void permutate_by_cycle(T & container, unsigned cycle_len, const unsigned * permutation_cycle) { void permute_by_cycle(T& container, unsigned cycle_len, const unsigned * permutation_cycle) {
if (cycle_len<2) { if (cycle_len < 2)
return; return;
}
auto aux = container[permutation_cycle[0]]; auto aux = container[permutation_cycle[0]];
for (unsigned i=1; i<cycle_len; i++) { verbose_stream() << "xx " << cycle_len << "\n";
container[permutation_cycle[i-1]]=container[permutation_cycle[i]]; for (unsigned i = 1; i < cycle_len; i++)
} container[permutation_cycle[i-1]] = container[permutation_cycle[i]];
container[permutation_cycle[cycle_len-1]]=aux; container[permutation_cycle[cycle_len-1]] = aux;
} }
template<class T, class M> template<class T, class M>
void permutate_by_cycle(ref_vector<T,M> & container, unsigned cycle_len, const unsigned * permutation_cycle) { void permute_by_cycle(ref_vector<T,M> & container, unsigned cycle_len, const unsigned * permutation_cycle) {
if (cycle_len<2) { if (cycle_len<2) {
return; return;
} }
verbose_stream() << "ptr\n";
T * aux = container.get(permutation_cycle[0]); T * aux = container.get(permutation_cycle[0]);
for (unsigned i=1; i<cycle_len; i++) { for (unsigned i=1; i < cycle_len; i++) {
container.set(permutation_cycle[i-1], container.get(permutation_cycle[i])); container.set(permutation_cycle[i-1], container.get(permutation_cycle[i]));
} }
container.set(permutation_cycle[cycle_len-1], aux); container.set(permutation_cycle[cycle_len-1], aux);
} }
template<class T> template<class T>
void permutate_by_cycle(T & container, const unsigned_vector & permutation_cycle) { void permute_by_cycle(T & container, const unsigned_vector & permutation_cycle) {
permutate_by_cycle(container, permutation_cycle.size(), permutation_cycle.data()); permute_by_cycle(container, permutation_cycle.size(), permutation_cycle.data());
} }

2
src/muz/rel/dl_base.h
View file

@ -160,7 +160,7 @@ namespace datalog {
SASSERT(cycle_len>=2); SASSERT(cycle_len>=2);
result=src; result=src;
permutate_by_cycle(result, cycle_len, permutation_cycle); permute_by_cycle(result, cycle_len, permutation_cycle);
} }
/** /**

2
src/muz/rel/dl_finite_product_relation.cpp
View file

@ -674,7 +674,7 @@ namespace datalog {
unsigned sig_sz = r.get_signature().size(); unsigned sig_sz = r.get_signature().size();
unsigned_vector permutation; unsigned_vector permutation;
add_sequence(0, sig_sz, 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; unsigned_vector table_permutation;

37
src/muz/rel/dl_mk_explanations.cpp
View file

@ -70,20 +70,16 @@ namespace datalog {
m_union_decl(mk_explanations::get_union_decl(get_context()), get_ast_manager()) {} m_union_decl(mk_explanations::get_union_decl(get_context()), get_ast_manager()) {}
~explanation_relation_plugin() override { ~explanation_relation_plugin() override {
for (unsigned i = 0; i < m_pool.size(); ++i) { for (unsigned i = 0; i < m_pool.size(); ++i)
for (unsigned j = 0; j < m_pool[i].size(); ++j) { for (unsigned j = 0; j < m_pool[i].size(); ++j)
dealloc(m_pool[i][j]); dealloc(m_pool[i][j]);
}
}
} }
bool can_handle_signature(const relation_signature & s) override { bool can_handle_signature(const relation_signature & s) override {
unsigned n=s.size(); unsigned n=s.size();
for (unsigned i=0; i<n; i++) { for (unsigned i=0; i<n; i++)
if (!get_context().get_decl_util().is_rule_sort(s[i])) { if (!get_context().get_decl_util().is_rule_sort(s[i]))
return false; return false;
}
}
return true; return true;
} }
@ -105,9 +101,10 @@ namespace datalog {
relation_intersection_filter_fn * mk_filter_by_negation_fn(const relation_base & t, relation_intersection_filter_fn * mk_filter_by_negation_fn(const relation_base & t,
const relation_base & negated_obj, unsigned joined_col_cnt, const relation_base & negated_obj, unsigned joined_col_cnt,
const unsigned * t_cols, const unsigned * negated_cols) override; const unsigned * t_cols, const unsigned * negated_cols) override;
relation_intersection_filter_fn * mk_filter_by_intersection_fn(const relation_base & t, relation_intersection_filter_fn * mk_filter_by_intersection_fn(
const relation_base & src, unsigned joined_col_cnt, const relation_base & t,
const unsigned * t_cols, const unsigned * src_cols) override; const relation_base & src, unsigned joined_col_cnt,
const unsigned * t_cols, const unsigned * src_cols) override;
}; };
@ -150,7 +147,8 @@ namespace datalog {
void assign_data(const relation_fact & f) { void assign_data(const relation_fact & f) {
m_empty = false; m_empty = false;
unsigned n=get_signature().size(); verbose_stream() << "assign data " << f << "\n";
unsigned n = get_signature().size();
SASSERT(f.size()==n); SASSERT(f.size()==n);
m_data.reset(); m_data.reset();
m_data.append(n, f.data()); m_data.append(n, f.data());
@ -161,11 +159,13 @@ namespace datalog {
m_data.resize(get_signature().size()); m_data.resize(get_signature().size());
} }
void unite_with_data(const relation_fact & f) { void unite_with_data(const relation_fact & f) {
verbose_stream() << "unite data " << f << "\n";
if (empty()) { if (empty()) {
assign_data(f); assign_data(f);
return; return;
} }
unsigned n=get_signature().size(); unsigned n = get_signature().size();
SASSERT(f.size()==n); SASSERT(f.size()==n);
for (unsigned i=0; i<n; i++) { for (unsigned i=0; i<n; i++) {
SASSERT(!is_undefined(i)); SASSERT(!is_undefined(i));
@ -186,6 +186,7 @@ namespace datalog {
void to_formula(expr_ref& fml) const override { void to_formula(expr_ref& fml) const override {
ast_manager& m = fml.get_manager(); ast_manager& m = fml.get_manager();
fml = m.mk_eq(m.mk_var(0, m_data[0]->get_sort()), m_data[0]); fml = m.mk_eq(m.mk_var(0, m_data[0]->get_sort()), m_data[0]);
verbose_stream() << "FORMULA " << fml << "\n";
} }
bool is_undefined(unsigned col_idx) const { bool is_undefined(unsigned col_idx) const {
@ -339,6 +340,7 @@ namespace datalog {
if (!r.empty()) { if (!r.empty()) {
relation_fact proj_data = r.m_data; relation_fact proj_data = r.m_data;
project_out_vector_columns(proj_data, m_removed_cols); project_out_vector_columns(proj_data, m_removed_cols);
verbose_stream() << "project\n";
res->assign_data(proj_data); res->assign_data(proj_data);
} }
return res; return res;
@ -365,9 +367,9 @@ namespace datalog {
explanation_relation * res = static_cast<explanation_relation *>(plugin.mk_empty(get_result_signature())); explanation_relation * res = static_cast<explanation_relation *>(plugin.mk_empty(get_result_signature()));
if (!r.empty()) { if (!r.empty()) {
relation_fact permutated_data = r.m_data; relation_fact permuted_data = r.m_data;
permutate_by_cycle(permutated_data, m_cycle); permute_by_cycle(dynamic_cast<app_ref_vector&>(permuted_data), m_cycle);
res->assign_data(permutated_data); res->assign_data(permuted_data);
} }
return res; return res;
} }
@ -406,6 +408,7 @@ namespace datalog {
} }
else { else {
if (tgt.empty()) { if (tgt.empty()) {
verbose_stream() << "union\n";
tgt.assign_data(src.m_data); tgt.assign_data(src.m_data);
if (delta && delta->empty()) { if (delta && delta->empty()) {
delta->assign_data(src.m_data); delta->assign_data(src.m_data);
@ -704,7 +707,7 @@ namespace datalog {
symbol mk_explanations::get_rule_symbol(rule * r) { symbol mk_explanations::get_rule_symbol(rule * r) {
if (r->name() == symbol::null) { if (r->name() == symbol::null) {
std::stringstream sstm; std::stringstream sstm;
r->display(m_context, sstm); r->display(m_context, sstm, true);
std::string res = sstm.str(); std::string res = sstm.str();
res = res.substr(0, res.find_last_not_of('\n')+1); res = res.substr(0, res.find_last_not_of('\n')+1);
return symbol(res.c_str()); return symbol(res.c_str());

2
src/muz/rel/dl_relation_manager.cpp
View file

@ -1149,7 +1149,7 @@ namespace datalog {
} }
void modify_fact(table_fact & f) const override { 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 { table_base * operator()(const table_base & t) override {

4
src/muz/rel/dl_sieve_relation.cpp
View file

@ -413,14 +413,14 @@ namespace datalog {
unsigned sig_sz = r.get_signature().size(); unsigned sig_sz = r.get_signature().size();
unsigned_vector permutation; unsigned_vector permutation;
add_sequence(0, sig_sz, 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; bool inner_identity;
unsigned_vector inner_permutation; unsigned_vector inner_permutation;
collect_sub_permutation(permutation, r.m_sig2inner, inner_permutation, inner_identity); collect_sub_permutation(permutation, r.m_sig2inner, inner_permutation, inner_identity);
bool_vector result_inner_cols = r.m_inner_cols; 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 result_sig;
relation_signature::from_rename(r.get_signature(), cycle_len, permutation_cycle, result_sig); relation_signature::from_rename(r.get_signature(), cycle_len, permutation_cycle, result_sig);