mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

Rotate first entry for refinement

Browse source
This commit is contained in:
Jakob Rath 2022-12-20 09:32:27 +01:00
parent 86a36a524a
commit e5b142b265
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -308,6 +308,10 @@ namespace polysat {
rational const& max_value = s.var2pdd(v).max_value(); rational const& max_value = s.var2pdd(v).max_value();
rational mod_value = max_value + 1; rational mod_value = max_value + 1;
// Rotate the 'first' entry, to prevent getting stuck in a refinement loop
// with an early entry when a later entry could give a better interval.
m_equal_lin[v] = m_equal_lin[v]->next();
auto delta_l = [&](rational const& coeff_val) { auto delta_l = [&](rational const& coeff_val) {
return floor((coeff_val - e->interval.lo_val()) / e->coeff); return floor((coeff_val - e->interval.lo_val()) / e->coeff);
}; };
@ -418,6 +422,10 @@ namespace polysat {
rational const& max_value = s.var2pdd(v).max_value(); rational const& max_value = s.var2pdd(v).max_value();
rational const mod_value = max_value + 1; rational const mod_value = max_value + 1;
// Rotate the 'first' entry, to prevent getting stuck in a refinement loop
// with an early entry when a later entry could give a better interval.
m_diseq_lin[v] = m_diseq_lin[v]->next();
do { do {
LOG("refine-disequal-lin for src: " << e->src); LOG("refine-disequal-lin for src: " << e->src);
// We compute an interval if the concrete value 'val' violates the constraint: // We compute an interval if the concrete value 'val' violates the constraint: