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

disable assertions for now

Browse source
This commit is contained in:
Jakob Rath 2024-05-03 10:03:03 +02:00
parent f8c593edf9
commit 7a3349eeae
1 changed files with 27 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -837,6 +837,7 @@ namespace polysat {
* - y[abw] \not\in [ ceil(lo'/2^k'), ceil(hi'/2^k') [
* - ceil(lo/2^k) != ceil(hi/2^k) ... ensured by side conditions from interval reduction
* - ceil(lo'/2^k') != ceil(hi'/2^k') ... ensured by side conditions from interval reduction
* - ceil(lo/2^k) = lo[w-1:k] or ceil(lo/2^k) = lo[w-1:k] + 1 ... which case is ensured by side conditions
*
* Case ebw = abw:
* - Regular intervals that link up
@ -1040,6 +1041,8 @@ namespace polysat {
* where '?' is a placeholder for terms we don't care about.
*
*
* TODO: maybe here: after.lo[eew] \in [e.lo+1, e.hi+1] ???? (+1 on value level, so needs proper 2^k adjustment)
*
* before x[bew] \not\in [?,ceil(hi/2^k)[
* after y[aew] \not\in [ceil(lo/2^k'),?[
* e z[eew] \not\in [?,ceil(t/2^k'')[
@ -1060,7 +1063,7 @@ namespace polysat {
//
// e is the last entry of the hole.
// we need the constraint:
// e.hi in [ after.lo[ebw] ; before.hi[ebw] [
// e.hi in [ after.lo[eew] ; before.hi[eew] [
pdd t = e.e->interval.hi();
pdd lo = after.e->interval.lo();
pdd hi = before.e->interval.hi();
@ -1106,9 +1109,8 @@ From ZstJOJYeMR15.smt2
explain_kind conflict
v0: v4:5@0 value=16 v0:20@0
v0[5] := 16 v0[5] [-491520 ; 2^19[ := [17;16[ deps 16 == v0 [5]@0 src
v0[20] := 1048561 v0 [20*v1 + 21 ; 20*v1 + 1[ := [5;-15[ src -20 <= 20*v1 + -1*v0;
v0[5] := 16 v0[5] [-491520 ; 2^19[ := [17;16[ deps 16 == v0 [5]@0 src
v0[5] := 16 v0[5] [-491520 = (2^15*17) ; 2^15*16[ := [17;16[ deps 16 == v0 [5]@0 src
v0[20] := 1048561 v0 [20*v1 + 21 ; 20*v1 + 1[ := [5;-15[ src -20 <= 20*v1 + -1*v0;
*/
@ -1120,6 +1122,7 @@ v0[20] := 1048561 v0 [20*v1 + 21 ; 20*v1 + 1[ := [5;-15[ src -20 <= 20*v1 + -1*
t *= rational::power_of_two(aew - eew);
lo *= rational::power_of_two(aew - eew);
hi *= rational::power_of_two(aew - eew);
NOT_IMPLEMENTED_YET();
// TODO
}
@ -1153,6 +1156,14 @@ v0[20] := 1048561 v0 [20*v1 + 21 ; 20*v1 + 1[ := [5;-15[ src -20 <= 20*v1 + -1*
* - Encode: ceil(hi/2^k')[ew] - ceil(lo/2^k)[ew] < 2^hole_bits
*
*
* (If aw == bw)
* If bew < aew:
* ceil(hi/2^k')[bew] - ceil(lo/2^k)[bew] < 2^hole_bits
* 2^k*ceil(hi/2^k') - 2^k*ceil(lo/2^k) < 2^(k+hole_bits)
* (note hole_bits < bew, thus k + hole_bits < k + bew = bw)
*
*
*
*
*/
void viable::explain_hole_size(explanation const& before, explanation const& after, unsigned hole_bits, dependency_vector& deps) {
@ -1216,14 +1227,24 @@ v0[20] := 1048561 v0 [20*v1 + 21 ; 20*v1 + 1[ := [5;-15[ src -20 <= 20*v1 + -1*
if (aw != bw) {
// TODO: eval bounds?
NOT_IMPLEMENTED_YET();
// TODO: eval t1 because it is a "high" value, and project/embed into pdd of t2
return;
NOT_IMPLEMENTED_YET();
}
if (bew != bw || aew != aw) {
if (aew != bew) {
// TODO: multiply with 2^k appropriately
NOT_IMPLEMENTED_YET();
SASSERT(aw == bw);
if (bew < aew)
t1 *= rational::power_of_two(aew - bew);
if (aew < bew)
t2 *= rational::power_of_two(bew - aew);
return;
NOT_IMPLEMENTED_YET();
}
if (bew != bw || aew != aw) {
return;
NOT_IMPLEMENTED_YET();
}
auto sc = cs.ult(t2 - t1, rational::power_of_two(hole_bits));