mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

fix #1897

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-23 10:00:57 -07:00
parent 540922766d
commit 184ae7211e
5 changed files with 82 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/smt/smt_context.cpp
View file

@ -494,7 +494,7 @@ namespace smt {
try { try {
TRACE("add_eq", tout << "assigning: #" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";); TRACE("add_eq", tout << "assigning: #" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";);
TRACE("add_eq_detail", tout << "assigning\n" << mk_pp(n1->get_owner(), m_manager) << "\n" << mk_pp(n2->get_owner(), m_manager) << "\n"; TRACE("add_eq_detail", tout << "assigning\n" << enode_pp(n1, *this) << "\n" << enode_pp(n2, *this) << "\n";
tout << "kind: " << js.get_kind() << "\n";); tout << "kind: " << js.get_kind() << "\n";);
m_stats.m_num_add_eq++; m_stats.m_num_add_eq++;
@ -1232,7 +1232,7 @@ namespace smt {
if (depth == 0) if (depth == 0)
return false; return false;
if (r1->get_num_parents() < SMALL_NUM_PARENTS) { if (r1->get_num_parents() < SMALL_NUM_PARENTS) {
TRACE("is_ext_diseq", tout << mk_bounded_pp(n1->get_owner(), m_manager) << " " << mk_bounded_pp(n2->get_owner(), m_manager) << " " << depth << "\n";); TRACE("is_ext_diseq", tout << enode_pp(n1, *this) << " " << enode_pp(n2, *this) << " " << depth << "\n";);
for (enode * p1 : enode::parents(r1)) { for (enode * p1 : enode::parents(r1)) {
if (!is_relevant(p1)) if (!is_relevant(p1))
continue; continue;
@ -1241,7 +1241,7 @@ namespace smt {
if (!p1->is_cgr()) if (!p1->is_cgr())
continue; continue;
func_decl * f = p1->get_decl(); func_decl * f = p1->get_decl();
TRACE("is_ext_diseq", tout << "p1: " << mk_bounded_pp(p1->get_owner(), m_manager) << "\n";); TRACE("is_ext_diseq", tout << "p1: " << enode_pp(p1, *this) << "\n";);
unsigned num_args = p1->get_num_args(); unsigned num_args = p1->get_num_args();
for (enode * p2 : enode::parents(r2)) { for (enode * p2 : enode::parents(r2)) {
if (!is_relevant(p2)) if (!is_relevant(p2))
@ -1250,7 +1250,7 @@ namespace smt {
continue; continue;
if (!p2->is_cgr()) if (!p2->is_cgr())
continue; continue;
TRACE("is_ext_diseq", tout << "p2: " << mk_bounded_pp(p2->get_owner(), m_manager) << "\n";); TRACE("is_ext_diseq", tout << "p2: " << enode_pp(p2, *this) << "\n";);
if (p1->get_root() != p2->get_root() && p2->get_decl() == f && p2->get_num_args() == num_args) { if (p1->get_root() != p2->get_root() && p2->get_decl() == f && p2->get_num_args() == num_args) {
unsigned j = 0; unsigned j = 0;
for (j = 0; j < num_args; j++) { for (j = 0; j < num_args; j++) {
@ -1264,7 +1264,7 @@ namespace smt {
break; break;
} }
if (j == num_args) { if (j == num_args) {
TRACE("is_ext_diseq", tout << "found parents: " << mk_bounded_pp(p1->get_owner(), m_manager) << " " << mk_bounded_pp(p2->get_owner(), m_manager) << "\n";); TRACE("is_ext_diseq", tout << "found parents: " << enode_pp(p1, *this) << " " << enode_pp(p2, *this) << "\n";);
if (is_ext_diseq(p1, p2, depth - 1)) if (is_ext_diseq(p1, p2, depth - 1))
return true; return true;
} }
@ -1770,7 +1770,7 @@ namespace smt {
void context::set_conflict(const b_justification & js, literal not_l) { void context::set_conflict(const b_justification & js, literal not_l) {
if (!inconsistent()) { if (!inconsistent()) {
TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout, js); ); TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout << " ", js); );
m_conflict = js; m_conflict = js;
m_not_l = not_l; m_not_l = not_l;
} }
@ -4290,7 +4290,7 @@ namespace smt {
for (enode * parent : enode::parents(n)) { for (enode * parent : enode::parents(n)) {
family_id fid = parent->get_owner()->get_family_id(); family_id fid = parent->get_owner()->get_family_id();
if (fid != th_id && fid != m_manager.get_basic_family_id()) { if (fid != th_id && fid != m_manager.get_basic_family_id()) {
TRACE("is_shared", tout << mk_pp(n->get_owner(), m_manager) << "\nis shared because of:\n" << mk_pp(parent->get_owner(), m_manager) << "\n";); TRACE("is_shared", tout << enode_pp(n, *this) << "\nis shared because of:\n" << enode_pp(parent, *this) << "\n";);
return true; return true;
} }
} }

16
src/smt/smt_context.h
View file

@ -1609,6 +1609,22 @@ namespace smt {
void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_asserted_formulas.insert_macro(f, m, pr, dep); } void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_asserted_formulas.insert_macro(f, m, pr, dep); }
}; };
struct enode_eq_pp {
context const& ctx;
enode_pair const& p;
enode_eq_pp(enode_pair const& p, context const& ctx): ctx(ctx), p(p) {}
};
std::ostream& operator<<(std::ostream& out, enode_eq_pp const& p);
struct enode_pp {
context const& ctx;
enode* n;
enode_pp(enode* n, context const& ctx): ctx(ctx), n(n) {}
};
std::ostream& operator<<(std::ostream& out, enode_pp const& p);
}; };
#endif /* SMT_CONTEXT_H_ */ #endif /* SMT_CONTEXT_H_ */

12
src/smt/smt_context_pp.cpp
View file

@ -603,5 +603,17 @@ namespace smt {
display(out, j); display(out, j);
} }
std::ostream& operator<<(std::ostream& out, enode_pp const& p) {
ast_manager& m = p.ctx.get_manager();
enode* n = p.n;
return out << "[#" << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), m) << "]";
}
std::ostream& operator<<(std::ostream& out, enode_eq_pp const& p) {
return out << enode_pp(p.p.first, p.ctx) << " = " << enode_pp(p.p.second, p.ctx) << "\n";
}
}; };

77
src/smt/theory_datatype.cpp
View file

@ -365,7 +365,7 @@ namespace smt {
if (!is_recognizer(n)) if (!is_recognizer(n))
return; return;
TRACE("datatype", tout << "assigning recognizer: #" << n->get_owner_id() << " is_true: " << is_true << "\n" TRACE("datatype", tout << "assigning recognizer: #" << n->get_owner_id() << " is_true: " << is_true << "\n"
<< mk_bounded_pp(n->get_owner(), get_manager()) << "\n";); << enode_pp(n, ctx) << "\n";);
SASSERT(n->get_num_args() == 1); SASSERT(n->get_num_args() == 1);
enode * arg = n->get_arg(0); enode * arg = n->get_arg(0);
theory_var tv = arg->get_th_var(get_id()); theory_var tv = arg->get_th_var(get_id());
@ -393,11 +393,10 @@ namespace smt {
} }
void theory_datatype::relevant_eh(app * n) { void theory_datatype::relevant_eh(app * n) {
TRACE("datatype", tout << "relevant_eh: " << mk_bounded_pp(n, get_manager()) << "\n";);
context & ctx = get_context(); context & ctx = get_context();
TRACE("datatype", tout << "relevant_eh: " << mk_pp(n, get_manager()) << "\n";);
SASSERT(ctx.relevancy()); SASSERT(ctx.relevancy());
if (is_recognizer(n)) { if (is_recognizer(n)) {
TRACE("datatype", tout << "relevant_eh: #" << n->get_id() << "\n" << mk_bounded_pp(n, get_manager()) << "\n";);
SASSERT(ctx.e_internalized(n)); SASSERT(ctx.e_internalized(n));
enode * e = ctx.get_enode(n); enode * e = ctx.get_enode(n);
theory_var v = e->get_arg(0)->get_th_var(get_id()); theory_var v = e->get_arg(0)->get_th_var(get_id());
@ -483,31 +482,41 @@ namespace smt {
SASSERT(app->get_root() == root->get_root()); SASSERT(app->get_root() == root->get_root());
if (app != root) if (app != root)
m_used_eqs.push_back(enode_pair(app, root)); m_used_eqs.push_back(enode_pair(app, root));
TRACE("datatype",
tout << "occurs_check\n";
for (enode_pair const& p : m_used_eqs) {
tout << enode_eq_pp(p, get_context());
});
} }
// start exploring subgraph below `app` // start exploring subgraph below `app`
bool theory_datatype::occurs_check_enter(enode * app) { bool theory_datatype::occurs_check_enter(enode * app) {
oc_mark_on_stack(app); app = app->get_root();
theory_var v = app->get_root()->get_th_var(get_id()); theory_var v = app->get_th_var(get_id());
if (v != null_theory_var) { if (v == null_theory_var) {
v = m_find.find(v); return false;
var_data * d = m_var_data[v]; }
if (d->m_constructor) { v = m_find.find(v);
for (enode * arg : enode::args(d->m_constructor)) { var_data * d = m_var_data[v];
if (oc_cycle_free(arg)) { if (!d->m_constructor) {
continue; return false;
} }
if (oc_on_stack(arg)) { enode * parent = d->m_constructor;
// arg was explored before app, and is still on the stack: cycle oc_mark_on_stack(parent);
occurs_check_explain(app, arg); for (enode * arg : enode::args(parent)) {
return true; if (oc_cycle_free(arg)) {
} continue;
// explore `arg` (with parent `app`) }
if (m_util.is_datatype(get_manager().get_sort(arg->get_owner()))) { if (oc_on_stack(arg)) {
m_parent.insert(arg->get_root(), app); // arg was explored before app, and is still on the stack: cycle
oc_push_stack(arg); occurs_check_explain(parent, arg);
} return true;
} }
// explore `arg` (with paren)
if (m_util.is_datatype(get_manager().get_sort(arg->get_owner()))) {
m_parent.insert(arg->get_root(), parent);
oc_push_stack(arg);
} }
} }
return false; return false;
@ -521,7 +530,7 @@ namespace smt {
a3 = cons(v3, a1) a3 = cons(v3, a1)
*/ */
bool theory_datatype::occurs_check(enode * n) { bool theory_datatype::occurs_check(enode * n) {
TRACE("datatype", tout << "occurs check: #" << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), get_manager()) << "\n";); TRACE("datatype", tout << "occurs check: " << enode_pp(n, get_context()) << "\n";);
m_stats.m_occurs_check++; m_stats.m_occurs_check++;
bool res = false; bool res = false;
@ -535,7 +544,7 @@ namespace smt {
if (oc_cycle_free(app)) continue; if (oc_cycle_free(app)) continue;
TRACE("datatype", tout << "occurs check loop: #" << app->get_owner_id() << " " << mk_bounded_pp(app->get_owner(), get_manager()) << (op==ENTER?" enter":" exit")<< "\n";); TRACE("datatype", tout << "occurs check loop: " << enode_pp(app, get_context()) << (op==ENTER?" enter":" exit")<< "\n";);
switch (op) { switch (op) {
case ENTER: case ENTER:
@ -553,12 +562,6 @@ namespace smt {
context & ctx = get_context(); context & ctx = get_context();
region & r = ctx.get_region(); region & r = ctx.get_region();
ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), r, 0, nullptr, m_used_eqs.size(), m_used_eqs.c_ptr()))); ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), r, 0, nullptr, m_used_eqs.size(), m_used_eqs.c_ptr())));
TRACE("datatype",
tout << "occurs_check: true\n";
for (enode_pair const& p : m_used_eqs) {
tout << "eq: #" << p.first->get_owner_id() << " #" << p.second->get_owner_id() << "\n";
tout << mk_bounded_pp(p.first->get_owner(), get_manager()) << " " << mk_bounded_pp(p.second->get_owner(), get_manager()) << "\n";
});
} }
return res; return res;
} }
@ -613,7 +616,7 @@ namespace smt {
var_data * d = m_var_data[v]; var_data * d = m_var_data[v];
out << "v" << v << " #" << get_enode(v)->get_owner_id() << " -> v" << m_find.find(v) << " "; out << "v" << v << " #" << get_enode(v)->get_owner_id() << " -> v" << m_find.find(v) << " ";
if (d->m_constructor) if (d->m_constructor)
out << mk_bounded_pp(d->m_constructor->get_owner(), get_manager()); out << enode_pp(d->m_constructor, get_context());
else else
out << "(null)"; out << "(null)";
out << "\n"; out << "\n";
@ -778,11 +781,11 @@ namespace smt {
SASSERT(!lits.empty()); SASSERT(!lits.empty());
region & reg = ctx.get_region(); region & reg = ctx.get_region();
TRACE("datatype_conflict", tout << mk_ismt2_pp(recognizer->get_owner(), get_manager()) << "\n"; TRACE("datatype_conflict", tout << mk_ismt2_pp(recognizer->get_owner(), get_manager()) << "\n";
for (unsigned i = 0; i < lits.size(); i++) { for (literal l : lits) {
ctx.display_detailed_literal(tout, lits[i]); tout << "\n"; ctx.display_detailed_literal(tout, l); tout << "\n";
} }
for (unsigned i = 0; i < eqs.size(); i++) { for (auto const& p : eqs) {
tout << mk_ismt2_pp(eqs[i].first->get_owner(), get_manager()) << " = " << mk_ismt2_pp(eqs[i].second->get_owner(), get_manager()) << "\n"; tout << enode_eq_pp(p, ctx);
}); });
ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), reg, lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr()))); ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), reg, lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr())));
} }

16
src/smt/theory_lra.cpp
View file

@ -1361,8 +1361,7 @@ public:
} }
enode* n2 = get_enode(other); enode* n2 = get_enode(other);
if (n1->get_root() != n2->get_root()) { if (n1->get_root() != n2->get_root()) {
TRACE("arith", tout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n"; TRACE("arith", tout << enode_eq_pp(enode_pair(n1, n2), ctx());
tout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n";
tout << "v" << v << " = " << "v" << other << "\n";); tout << "v" << v << " = " << "v" << other << "\n";);
m_assume_eq_candidates.push_back(std::make_pair(v, other)); m_assume_eq_candidates.push_back(std::make_pair(v, other));
result = true; result = true;
@ -2800,15 +2799,15 @@ public:
get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, nullptr)); get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, nullptr));
TRACE("arith", TRACE("arith",
for (unsigned i = 0; i < m_core.size(); ++i) { for (literal c : m_core) {
ctx().display_detailed_literal(tout, m_core[i]); ctx().display_detailed_literal(tout, c);
tout << "\n"; tout << "\n";
} }
for (unsigned i = 0; i < m_eqs.size(); ++i) { for (enode_pair const& p : m_eqs) {
tout << mk_pp(m_eqs[i].first->get_owner(), m) << " = " << mk_pp(m_eqs[i].second->get_owner(), m) << "\n"; tout << enode_eq_pp(p, ctx());
} }
tout << " ==> "; tout << " ==> ";
tout << mk_pp(x->get_owner(), m) << " = " << mk_pp(y->get_owner(), m) << "\n"; tout << enode_pp(x, ctx()) << " = " << enode_pp(y, ctx()) << "\n";
); );
// parameters are TBD. // parameters are TBD.
@ -3371,8 +3370,7 @@ public:
break; break;
} }
case equality_source: case equality_source:
out << mk_pp(m_equalities[idx].first->get_owner(), m) << " = " out << enode_eq_pp(m_equalities[idx], ctx());
<< mk_pp(m_equalities[idx].second->get_owner(), m) << "\n";
break; break;
case definition_source: { case definition_source: {
theory_var v = m_definitions[idx]; theory_var v = m_definitions[idx];