mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

make explicit that we compare the concrete values

Browse source
This commit is contained in:
Jakob Rath 2022-08-22 14:17:47 +02:00
parent 3a759c1a28
commit c1e2ea80f5
2 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/interval.h
View file

@ -96,7 +96,7 @@ namespace polysat {
else
return val < hi_val() || val >= lo_val();
}
bool contains(eval_interval const& other) const {
bool currently_contains(eval_interval const& other) const {
if (is_full())
return true;
// lo <= lo' <= hi' <= hi'

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

@ -211,11 +211,11 @@ namespace polysat {
else {
entry* first = e;
do {
if (e->interval.contains(ne->interval)) {
if (e->interval.currently_contains(ne->interval)) {
m_alloc.push_back(ne);
return false;
}
while (ne->interval.contains(e->interval)) {
while (ne->interval.currently_contains(e->interval)) {
entry* n = e->next();
remove_entry(e);
if (!m_units[v]) {
@ -228,7 +228,7 @@ namespace polysat {
}
SASSERT(e->interval.lo_val() != ne->interval.lo_val());
if (e->interval.lo_val() > ne->interval.lo_val()) {
if (first->prev()->interval.contains(ne->interval)) {
if (first->prev()->interval.currently_contains(ne->interval)) {
m_alloc.push_back(ne);
return false;
}
@ -729,7 +729,7 @@ namespace polysat {
return false;
auto* n = e->next();
if (n != e && e->interval.contains(n->interval))
if (n != e && e->interval.currently_contains(n->interval))
return false;
if (n == first)