mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

Fix interval check

Browse source
This commit is contained in:
Jakob Rath 2022-10-03 15:22:00 +02:00
parent e09cf4faa5
commit 811843cf45
1 changed files with 12 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -644,7 +644,6 @@ namespace polysat {
// using the equivalence: t \in [l;h[ <=> t-l < h-l // using the equivalence: t \in [l;h[ <=> t-l < h-l
entry* n = e->next(); entry* n = e->next();
#if 0
// Choose the next interval which furthest extends the covered region. // Choose the next interval which furthest extends the covered region.
// Example: // Example:
// covered: [-------] // covered: [-------]
@ -668,11 +667,21 @@ namespace polysat {
// The interval 'first' is always part of the lemma. If we reach first again here, we have covered the complete domain. // The interval 'first' is always part of the lemma. If we reach first again here, we have covered the complete domain.
while (n != first) { while (n != first) {
entry* n1 = n->next(); entry* n1 = n->next();
if (!e->interval.currently_contains(n1->interval.lo_val())) // Check if n1 is eligible; if yes, then n1 is better than n.
//
// Case 1, n1 overlaps e (unless n1 == e):
// e: [------[
// n1: [----[
// Case 2, n1 connects to e:
// e: [------[
// n1: [----[
if (n1 == e)
break; break;
if (!e->interval.currently_contains(n1->interval.lo_val()))
if (e->interval.hi_val() != n1->interval.lo_val())
break;
n = n1; n = n1;
} }
#endif
if (!e->interval.is_full()) { if (!e->interval.is_full()) {
auto const& hi = e->interval.hi(); auto const& hi = e->interval.hi();