mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

Moved quick-check out of the refinement loop

Browse source
This commit is contained in:
Clemens Eisenhofer 2023-02-16 07:21:17 +01:00
parent 5ddc727f91
commit 5fbfa0be8f
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1107,6 +1107,8 @@ namespace {
template <query_t mode>
lbool viable::query(pvar v, typename query_result<mode>::result_t& result) {
if (!quick_bit_check(v))
return l_false;
// max number of interval refinements before falling back to the univariate solver
unsigned const refinement_budget = 1000;
unsigned refinements = refinement_budget;
@ -1145,9 +1147,6 @@ namespace {
lo = 0;
hi = max_value;
if (!quick_bit_check(v))
return l_false;
auto* e = m_units[v];
if (!e && !refine_viable(v, lo))
return refined;