mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
This commit is contained in:
parent
79296d8dfc
commit
16413b4f9a
|
@ -1261,7 +1261,8 @@ namespace opt {
|
|||
m_var2value[x] = eval(result);
|
||||
TRACE("opt1", tout << "updated eval " << x << " := " << eval(x) << "\n";);
|
||||
}
|
||||
retire_row(row_id1);
|
||||
else
|
||||
retire_row(row_id1);
|
||||
return result;
|
||||
}
|
||||
|
||||
|
|
|
@ -23,9 +23,9 @@ namespace q {
|
|||
std::ostream& lit::display(std::ostream& out) const {
|
||||
ast_manager& m = lhs.m();
|
||||
if (m.is_true(rhs) && !sign)
|
||||
return out << mk_bounded_pp(lhs, m, 2);
|
||||
return out << lhs;
|
||||
if (m.is_false(rhs) && !sign)
|
||||
return out << "(not " << mk_bounded_pp(lhs, m, 2) << ")";
|
||||
return out << "(not " << lhs << ")";
|
||||
return
|
||||
out << mk_bounded_pp(lhs, m, 2)
|
||||
<< (sign ? " != " : " == ")
|
||||
|
@ -43,13 +43,13 @@ namespace q {
|
|||
for (auto const& lit : m_lits)
|
||||
lit.display(out) << "\n";
|
||||
binding* b = m_bindings;
|
||||
if (b) {
|
||||
do {
|
||||
b->display(ctx, num_decls(), out) << "\n";
|
||||
b = b->next();
|
||||
}
|
||||
while (b != m_bindings);
|
||||
}
|
||||
if (!b)
|
||||
return out;
|
||||
do {
|
||||
b->display(ctx, num_decls(), out) << "\n";
|
||||
b = b->next();
|
||||
}
|
||||
while (b != m_bindings);
|
||||
return out;
|
||||
}
|
||||
|
||||
|
|
|
@ -162,7 +162,6 @@ namespace q {
|
|||
return r;
|
||||
if (r == l_true) {
|
||||
model_ref mdl;
|
||||
expr_ref proj(m);
|
||||
m_solver->get_model(mdl);
|
||||
if (check_forall_subst(q, *qb, *mdl))
|
||||
return l_false;
|
||||
|
|
Loading…
Reference in a new issue