mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

flatten if-then-else

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-30 23:28:30 -07:00
parent bcf0f671b8
commit 77cd82a5ca
1 changed files with 14 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/sat/tactic/goal2sat.cpp
View file

@ -300,24 +300,24 @@ struct goal2sat::imp : public sat::sat_internalizer {
add_dual_root(1, &tt);
l = sign ? tt : ~tt;
}
else {
if (m_euf) {
convert_euf(t, root, sign);
return;
}
if (!is_uninterp_const(t)) {
if (!is_app(t)) {
std::ostringstream strm;
strm << mk_ismt2_pp(t, m);
throw_op_not_handled(strm.str());
}
else
m_unhandled_funs.push_back(to_app(t)->get_decl());
else if (m_euf) {
convert_euf(t, root, sign);
return;
}
else if (!is_uninterp_const(t)) {
if (!is_app(t)) {
std::ostringstream strm;
strm << mk_ismt2_pp(t, m);
throw_op_not_handled(strm.str());
}
else
m_unhandled_funs.push_back(to_app(t)->get_decl());
}
else {
v = mk_bool_var(t);
l = sat::literal(v, sign);
bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t);
if (ext)
if (ext)
m_solver.set_external(v);
TRACE("sat", tout << "new_var: " << v << ": " << mk_bounded_pp(t, m, 2) << " " << is_uninterp_const(t) << "\n";);
}