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

simplify theory case split handling

Browse source
This commit is contained in:
Murphy Berzish 2017-05-01 18:22:49 -04:00
parent 3bce61e0d4
commit b86d472eaf
1 changed files with 2 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/smt/smt_context.cpp
View file

@ -3057,19 +3057,8 @@ namespace smt {
literal l2 = *set_it; literal l2 = *set_it;
if (l2 != l) { if (l2 != l) {
b_justification js(l); b_justification js(l);
switch (get_assignment(l2)) { TRACE("theory_case_split", tout << "case split literal "; l2.display(tout, m_manager, m_bool_var2expr.c_ptr()););
case l_false: assign(~l2, js);
TRACE("theory_case_split", tout << "case split literal " << l2.index() << " is already assigned False" << std::endl;);
break;
case l_undef:
TRACE("theory_case_split", tout << "case split literal " << l2.index() << " is not assigned" << std::endl;);
assign(~l2, js);
break;
case l_true:
TRACE("theory_case_split", tout << "case split literal " << l2.index() << " is already assigned True" << std::endl;);
assign(~l2, js);
break;
}
if (inconsistent()) { if (inconsistent()) {
TRACE("theory_case_split", tout << "conflict detected!" << std::endl;); TRACE("theory_case_split", tout << "conflict detected!" << std::endl;);
return false; return false;