File: redundant.st

package info (click to toggle)
llvm-toolchain-9 1%3A9.0.1-16
  • links: PTS, VCS
  • area: main
  • in suites: bullseye
  • size: 882,436 kB
  • sloc: cpp: 4,167,636; ansic: 714,256; asm: 457,610; python: 155,927; objc: 65,094; sh: 42,856; lisp: 26,908; perl: 7,786; pascal: 7,722; makefile: 6,881; ml: 5,581; awk: 3,648; cs: 2,027; xml: 888; javascript: 381; ruby: 156
file content (6 lines) | stat: -rw-r--r-- 2,422 bytes parent folder | download | duplicates (37)
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)] }]"