mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

#5223

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-05-05 16:11:21 -07:00
parent 2b1b10be69
commit 87c0a8136f
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/sat/smt/dt_solver.cpp
View file

@ -249,7 +249,7 @@ namespace dt {
SASSERT(!d->m_constructor);
SASSERT(!recognizer || ctx.value(recognizer) == l_false || !is_final);
TRACE("dt", tout << "non_rec_c: " << non_rec_c->get_name() << " #rec: " << d->m_recognizers.size() << "\n";);
TRACE("dt", tout << ctx.bpp(n) << " non_rec_c: " << non_rec_c->get_name() << " #rec: " << d->m_recognizers.size() << "\n";);
if (!recognizer && non_rec_c->get_arity() == 0) {
sat::literal eq = eq_internalize(n->get_expr(), m.mk_const(non_rec_c));
@ -474,7 +474,7 @@ namespace dt {
var_data* d2 = m_var_data[v2];
auto* con1 = d1->m_constructor;
auto* con2 = d2->m_constructor;
TRACE("dt", tout << "merging v" << v1 << " v" << v2 << "\n" << ctx.bpp(con1) << " " << ctx.bpp(con2) << "\n";);
TRACE("dt", tout << "merging v" << v1 << " v" << v2 << "\n" << ctx.bpp(var2enode(v1)) << " == " << ctx.bpp(var2enode(v2)) << " " << ctx.bpp(con1) << " " << ctx.bpp(con2) << "\n";);
if (con1 && con2 && con1->get_decl() != con2->get_decl())
ctx.set_conflict(euf::th_explain::conflict(*this, con1, con2));
else if (con2 && !con1) {
@ -782,7 +782,6 @@ namespace dt {
}
}
mk_var(n);
}
else if (is_recognizer(term)) {
mk_var(n);
@ -794,6 +793,8 @@ namespace dt {
SASSERT(is_accessor(term));
SASSERT(n->num_args() == 1);
mk_var(n->get_arg(0));
if (is_datatype(n))
mk_var(n);
}
return true;