mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
na
This commit is contained in:
parent
aced115b70
commit
7e68d546ba
|
@ -735,7 +735,7 @@ SASSERT(false);
|
|||
}
|
||||
|
||||
std::ostream& egraph::display(std::ostream& out, unsigned max_args, enode* n) const {
|
||||
out << n->get_expr_id() << " := ";
|
||||
out << "#" << n->get_expr_id() << " := ";
|
||||
expr* f = n->get_expr();
|
||||
if (is_app(f))
|
||||
out << mk_bounded_pp(f, m, 1) << " ";
|
||||
|
|
|
@ -149,6 +149,8 @@ namespace euf {
|
|||
}
|
||||
|
||||
bool solver::is_external(bool_var v) {
|
||||
if (s().is_external(v))
|
||||
return true;
|
||||
if (nullptr != m_bool_var2expr.get(v, nullptr))
|
||||
return true;
|
||||
for (auto* s : m_solvers)
|
||||
|
|
|
@ -105,24 +105,23 @@ namespace sat {
|
|||
m_core.push_back(lit2ext(lit));
|
||||
if (is_sat == l_true) {
|
||||
IF_VERBOSE(0, display(s, verbose_stream()));
|
||||
s.display(verbose_stream());
|
||||
UNREACHABLE();
|
||||
return false;
|
||||
}
|
||||
TRACE("dual", m_solver.display(tout << "is-sat: " << is_sat << " core: " << m_core << "\n"););
|
||||
m_solver.user_pop(1);
|
||||
return is_sat == l_false;
|
||||
}
|
||||
|
||||
|
||||
std::ostream& dual_solver::display(solver const& s, std::ostream& out) const {
|
||||
for (auto r : m_roots)
|
||||
out << r << " " << m_solver.value(r) << "\n";
|
||||
for (unsigned v = 0; v < m_solver.num_vars(); ++v) {
|
||||
bool_var w = m_var2ext.get(v, null_bool_var);
|
||||
if (w == null_bool_var)
|
||||
continue;
|
||||
lbool v1 = m_solver.value(v);
|
||||
lbool v2 = s.value(w);
|
||||
if (v1 == v2)
|
||||
if (v1 == v2 || v2 == l_undef)
|
||||
continue;
|
||||
out << w << " " << v1 << " " << v2 << "\n";
|
||||
}
|
||||
|
|
|
@ -278,12 +278,12 @@ struct goal2sat::imp : public sat::sat_internalizer {
|
|||
l = sign ? mk_true() : ~mk_true();
|
||||
}
|
||||
else {
|
||||
if (m_euf) {
|
||||
convert_euf(t, root, sign);
|
||||
return;
|
||||
}
|
||||
if (!is_uninterp_const(t)) {
|
||||
if (m_euf) {
|
||||
convert_euf(t, root, sign);
|
||||
return;
|
||||
}
|
||||
else if (!is_app(t)) {
|
||||
if (!is_app(t)) {
|
||||
std::ostringstream strm;
|
||||
strm << mk_ismt2_pp(t, m);
|
||||
throw_op_not_handled(strm.str());
|
||||
|
|
Loading…
Reference in a new issue