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

cleanup pdecide

Browse source
This commit is contained in:
Jakob Rath 2023-02-02 13:28:28 +01:00
parent 5589d3389d
commit 2dc93116e5
1 changed files with 6 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/math/polysat/solver.cpp
View file

@ -666,33 +666,24 @@ namespace polysat {
justification j; justification j;
switch (m_viable.find_viable(v, val)) { switch (m_viable.find_viable(v, val)) {
case find_t::empty: case find_t::empty:
// NOTE: all such cases should be discovered elsewhere (e.g., during propagation/narrowing) UNREACHABLE(); // should have been discovered earlier in viable::intersect
// (fail here in debug mode so we notice if we miss some)
UNREACHABLE();
m_free_pvars.unassign_var_eh(v);
VERIFY(is_conflict());
return; return;
case find_t::singleton: case find_t::singleton:
// NOTE: this case may happen legitimately if all other possibilities were excluded by brute force search UNREACHABLE(); // should have been discovered earlier in viable::intersect
// NOTE 2: probably not true anymore; viable::intersect should trigger all propagations now return;
UNREACHABLE();
j = justification::propagation(m_level);
break;
case find_t::multiple: case find_t::multiple:
j = justification::decision(m_level + 1); j = justification::decision(m_level + 1);
break; break;
case find_t::resource_out: case find_t::resource_out:
// the value is not viable, so assign_verify will call the univariate solver.
j = justification::decision(m_level + 1);
verbose_stream() << "TODO: solver::pdecide got resource_out\n"; verbose_stream() << "TODO: solver::pdecide got resource_out\n";
m_lim.cancel(); m_lim.cancel();
return; return;
default: default:
UNREACHABLE(); UNREACHABLE();
break; return;
} }
if (j.is_decision()) SASSERT(j.is_decision());
push_level(); push_level();
assign_core(v, val, j); assign_core(v, val, j);
} }