1
2
3
4
5
6
|
# Check that b1 >= 1 is not dropped by mistake in 4 * c0 + c1 >= 1 part
domain: "[b0] -> { write[i0, o1, o2, o3] : ((exists (e0 = floor((4 + o2)/8), e1 = floor((5 + o2)/8), e2 = floor((4 + o2)/262144), e3, e4: o1 <= 1 and o1 >= 0 and o2 <= 12 and o2 >= 1 and o3 <= 14 and o3 >= 1 and 8e0 <= 4 + o2 and 8e1 <= 5 + o2 and 262144e2 <= 4 - 8b0 + o2 and 262144e2 >= -262139 + o2 and 262144e2 <= 4 + o2 and 262144e2 >= -3 - 8b0 + o2 and 4e4 <= 1 - 8i0 + 2o1 - o2 + 8e0 and 4e4 <= 4 - 8i0 + 2o1 + o2 - 8e0 and 4e4 >= 2o1 + o2 - 8e1 - 8e3 and 4e4 >= -3 + 2o1 + o2 - 8e0 - 8e3 and 4e4 >= -6 + 2o1 - o2 + 8e0 - 8e3 and 2e4 >= -9 + o1 and 2e4 <= -1 + o1 and 4e4 <= -6 + 2o1 - o2 + 8e1 - 8e3 and 4e4 >= -3 - 8i0 + 2o1 + o2 - 8e0 and 4e4 >= -6 - 8i0 + 2o1 - o2 + 8e0)) or (exists (e0 = floor((4 + o2)/8), e1 = floor((5 + o2)/8), e2 = floor((4 + o2)/262144), e3, e4: o1 <= 1 and o1 >= 0 and o2 <= 12 and o2 >= 1 and o3 <= 14 and o3 >= 1 and 8e0 <= 4 + o2 and 8e1 >= -2 + o2 and 262144e2 <= 4 - 8b0 + o2 and 262144e2 >= -262139 + o2 and 262144e2 <= 4 + o2 and 262144e2 >= -3 - 8b0 + o2 and 4e4 <= 1 - 8i0 + 2o1 - o2 + 8e0 and 4e4 <= 4 - 8i0 + 2o1 + o2 - 8e0 and 4e4 >= -3 + 2o1 + o2 - 8e0 - 8e3 and 4e4 >= -6 + 2o1 - o2 + 8e0 - 8e3 and 2e4 >= -9 + o1 and 2e4 <= -1 + o1 and 4e4 <= 1 + 2o1 - o2 + 8e0 - 8e3 and 4e4 <= 4 + 2o1 + o2 - 8e0 - 8e3 and 4e4 <= -1 + 2o1 + o2 - 8e1 - 8e3 and 4e4 >= -3 - 8i0 + 2o1 + o2 - 8e0 and 4e4 >= -6 - 8i0 + 2o1 - o2 + 8e0)) or (exists (e0 = floor((2 + o2)/8), e1 = floor((4 + o2)/8), e2 = floor((4 + o2)/262144), e3, e4: o1 <= 1 and o1 >= 0 and o2 <= 13 and o2 >= 3 and o3 <= 14 and o3 >= 1 and 8e0 >= -5 + o2 and 8e1 <= 4 + o2 and 262144e2 <= 4 - 8b0 + o2 and 262144e2 >= -262139 + o2 and 262144e2 <= 4 + o2 and 262144e2 >= -3 - 8b0 + o2 and 4e4 <= 1 - 8i0 + 2o1 - o2 + 8e1 and 4e4 <= 4 - 8i0 + 2o1 + o2 - 8e1 and 4e4 >= -3 + 2o1 + o2 - 8e1 - 8e3 and 4e4 >= -6 + 2o1 - o2 + 8e1 - 8e3 and 2e4 >= -9 + o1 and 2e4 <= -1 + o1 and 4e4 <= 1 + 2o1 - o2 + 8e1 - 8e3 and 4e4 <= -4 + 2o1 + o2 - 8e0 - 8e3 and 4e4 <= 4 + 2o1 + o2 - 8e1 - 8e3 and 4e4 >= -3 - 8i0 + 2o1 + o2 - 8e1 and 4e4 >= -6 - 8i0 + 2o1 - o2 + 8e1))) and b0 >= 0 and i0 <= 2 and i0 >= 0 and b0 <= 2 }"
child:
context: "[b0] -> { [] : b0 <= 2 and b0 >= 0 }"
child:
schedule: "[b0] -> [{ write[i0, o1, o2, o3] -> [i0] }, { write[i0, i1, i2, i3] -> [(i1)] }, { write[i0, i1, i2, i3] -> [(5 - 8b0 + i2)] }, { write[i0,i1, i2, i3] -> [(i3)] }]"
|
