mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-05 19:00:25 +00:00
Code Activity

simplify side conditions on reduced intervals

Browse source
This commit is contained in:
Jakob Rath 2024-04-03 11:34:18 +02:00
parent d19de4b1d3
commit c5b02f8360
1 changed files with 14 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/sat/smt/polysat/viable.cpp
View file

@ -1001,9 +1001,11 @@ namespace polysat {
// //
// new_lo = lo[w-1:k] if lo[k-1:0] = 0 // new_lo = lo[w-1:k] if lo[k-1:0] = 0
// lo[w-1:k] + 1 otherwise // lo[w-1:k] + 1 otherwise
// = ceil( lo / 2^k )
// //
// new_hi = hi[w-1:k] if hi[k-1:0] = 0 // new_hi = hi[w-1:k] if hi[k-1:0] = 0
// hi[w-1:k] + 1 otherwise // hi[w-1:k] + 1 otherwise
// = ceil( hi / 2^k )
// //
// Reference: Fig. 1 (dtrim) in BitvectorsMCSAT // Reference: Fig. 1 (dtrim) in BitvectorsMCSAT
@ -1052,33 +1054,22 @@ namespace polysat {
// 0 < hi < lo: full // 0 < hi < lo: full
// 0 == hi < lo: empty // 0 == hi < lo: empty
// //
if (new_lo == new_hi) { if (new_lo == new_hi) {
bool is_empty_ivl; bool is_empty = true;
if (lo < hi) { if (lo.is_zero()) {
ne->side_cond.push_back(cs.ult(pdd_lo, pdd_hi)); SASSERT(!hi.is_zero());
if (lo == 0) { // 0 == lo < hi
ne->side_cond.push_back(cs.eq(pdd_lo)); ne->side_cond.push_back(cs.eq(pdd_lo));
is_empty_ivl = false; ne->side_cond.push_back(~cs.eq(pdd_hi));
} is_empty = false;
else {
ne->side_cond.push_back(~cs.eq(pdd_lo));
is_empty_ivl = true;
}
} }
else { else if (!hi.is_zero() && hi < lo) {
SASSERT(hi < lo); // 0 < hi < lo
ne->side_cond.push_back(~cs.eq(pdd_hi));
ne->side_cond.push_back(cs.ult(pdd_hi, pdd_lo)); ne->side_cond.push_back(cs.ult(pdd_hi, pdd_lo));
if (hi == 0) { is_empty = false;
ne->side_cond.push_back(cs.eq(pdd_hi));
is_empty_ivl = true;
}
else {
ne->side_cond.push_back(~cs.eq(pdd_hi));
is_empty_ivl = false;
}
} }
if (is_empty_ivl) { if (is_empty) {
m_alloc.push_back(ne); m_alloc.push_back(ne);
return find_t::multiple; return find_t::multiple;
} }