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

remove debug out

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-12-13 19:36:55 -08:00
parent 9054e72920
commit dbb4bbe7dc
1 changed files with 0 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -147,7 +147,6 @@ namespace datalog {
void assign_data(const relation_fact & f) { void assign_data(const relation_fact & f) {
m_empty = false; m_empty = false;
verbose_stream() << "assign data " << f << "\n";
unsigned n = get_signature().size(); unsigned n = get_signature().size();
SASSERT(f.size()==n); SASSERT(f.size()==n);
m_data.reset(); m_data.reset();
@ -159,7 +158,6 @@ 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);
@ -186,7 +184,6 @@ 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 {
@ -340,7 +337,6 @@ 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;
@ -408,7 +404,6 @@ 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);