mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

#5349 #5338

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-16 16:01:14 -05:00
parent fbc3aa93a5
commit f95d0b7216
2 changed files with 20 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/smt/smt_model_finder.cpp
View file

@ -808,7 +808,6 @@ namespace smt {
if (t_val && !m.is_unique_value(t_val)) if (t_val && !m.is_unique_value(t_val))
for (expr* v : values) for (expr* v : values)
found |= m.are_equal(v, t_val); found |= m.are_equal(v, t_val);
if (t_val && !found && !already_found.contains(t_val)) { if (t_val && !found && !already_found.contains(t_val)) {
values.push_back(t_val); values.push_back(t_val);
already_found.insert(t_val); already_found.insert(t_val);
@ -1113,9 +1112,14 @@ namespace smt {
mk_inverses(); mk_inverses();
complete_partial_funcs(partial_funcs); complete_partial_funcs(partial_funcs);
TRACE("model_finder", tout << "after auf_solver fixing the model\n"; TRACE("model_finder", tout << "after auf_solver fixing the model\n";
display_nodes(tout); display_nodes(tout);
tout << "NEW MODEL:\n"; tout << "NEW MODEL:\n";
model_pp(tout, *m_model);); model_pp(tout, *m_model););
}
bool is_default_representative(expr* t) {
app* tt = nullptr;
return t && m_sort2k.find(t->get_sort(), tt) && (tt == t);
} }
}; };
@ -1185,15 +1189,15 @@ namespace smt {
node* n1 = s.get_A_f_i(m_f, m_arg_i); node* n1 = s.get_A_f_i(m_f, m_arg_i);
node* n2 = s.get_uvar(q, m_var_j); node* n2 = s.get_uvar(q, m_var_j);
CTRACE("model_finder", n1->get_sort() != n2->get_sort(), CTRACE("model_finder", n1->get_sort() != n2->get_sort(),
tout << "sort bug:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" << mk_ismt2_pp(q, m) << "\n"; tout << "sort bug:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" << mk_ismt2_pp(q, m) << "\n";
tout << "decl(0): " << q->get_decl_name(0) << "\n"; tout << "decl(0): " << q->get_decl_name(0) << "\n";
tout << "f: " << m_f->get_name() << " i: " << m_arg_i << "\n"; tout << "f: " << m_f->get_name() << " i: " << m_arg_i << "\n";
tout << "v: " << m_var_j << "\n"; tout << "v: " << m_var_j << "\n";
n1->get_root()->display(tout, m); n1->get_root()->display(tout, m);
n2->get_root()->display(tout, m); n2->get_root()->display(tout, m);
tout << "f signature: "; tout << "f signature: ";
for (unsigned i = 0; i < m_f->get_arity(); i++) tout << mk_pp(m_f->get_domain(i), m) << " "; for (unsigned i = 0; i < m_f->get_arity(); i++) tout << mk_pp(m_f->get_domain(i), m) << " ";
tout << "-> " << mk_pp(m_f->get_range(), m) << "\n"; tout << "-> " << mk_pp(m_f->get_range(), m) << "\n";
); );
n1->merge(n2); n1->merge(n2);
@ -2511,6 +2515,8 @@ namespace smt {
if (s == nullptr) if (s == nullptr)
return nullptr; return nullptr;
expr* t = s->get_inv(val); expr* t = s->get_inv(val);
if (m_auf_solver->is_default_representative(t))
return val;
if (t != nullptr) { if (t != nullptr) {
generation = s->get_generation(t); generation = s->get_generation(t);
} }

1
src/tactic/arith/probe_arith.cpp
View file

@ -496,6 +496,7 @@ struct is_non_nira_functor {
throw_found(n); throw_found(n);
if (m_linear && u.is_numeral(n->get_arg(1), r) && r.is_zero()) if (m_linear && u.is_numeral(n->get_arg(1), r) && r.is_zero())
throw_found(n); throw_found(n);
if (m_linear && u.is_numeral(n->get_arg(1), r) && !r.is_zero())
if (!is_ground(n->get_arg(0)) || !is_ground(n->get_arg(1))) if (!is_ground(n->get_arg(0)) || !is_ground(n->get_arg(1)))
throw_found(n); throw_found(n);
return; return;