mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

convert to loop

Browse source
This commit is contained in:
Jakob Rath 2022-12-16 13:11:20 +01:00
parent e23774a746
commit c54c564019
1 changed files with 19 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

51
src/math/polysat/viable.cpp
View file

@ -580,41 +580,28 @@ namespace polysat {
unsigned const refinement_budget = 1000;
unsigned refinements = refinement_budget;
refined:
while (refinements--) {
lbool res = l_undef;
if (!refinements) {
LOG("Refinement budget exhausted! Fall back to univariate solver.");
return query_fallback<mode>(v, result);
if constexpr (mode == query_t::find_viable)
res = query_find(v, result.first, result.second);
else if constexpr (mode == query_t::min_viable)
res = query_min(v, result) ? l_true : l_undef;
else if constexpr (mode == query_t::max_viable)
res = query_max(v, result) ? l_true : l_undef;
else if constexpr (mode == query_t::has_viable) {
NOT_IMPLEMENTED_YET();
}
else {
UNREACHABLE();
}
if (res != l_undef)
return res;
}
refinements--;
if constexpr (mode == query_t::find_viable) {
lbool res = query_find(v, result.first, result.second);
if (res == l_undef)
goto refined;
return res;
}
if constexpr (mode == query_t::min_viable) {
if (!query_min(v, result))
goto refined;
return l_true;
}
if constexpr (mode == query_t::max_viable) {
if (!query_max(v, result))
goto refined;
return l_true;
}
if constexpr (mode == query_t::has_viable) {
NOT_IMPLEMENTED_YET();
return l_undef;
}
UNREACHABLE();
return l_undef;
LOG("Refinement budget exhausted! Fall back to univariate solver.");
return query_fallback<mode>(v, result);
}
lbool viable::query_find(pvar v, rational& lo, rational& hi) {