diff options
Diffstat (limited to 'omegalib/examples/old_test/wak6.oc-rt')
| -rw-r--r-- | omegalib/examples/old_test/wak6.oc-rt | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/omegalib/examples/old_test/wak6.oc-rt b/omegalib/examples/old_test/wak6.oc-rt new file mode 100644 index 0000000..458f5e9 --- /dev/null +++ b/omegalib/examples/old_test/wak6.oc-rt @@ -0,0 +1,36 @@ +# Omega Calculator v1.2 (based on Omega Library 1.2, August, 2000): +# T1 := {[k,i,j] -> [k',i,j] : 1 <= k < k' < i <= 1024 && k'+1 <= j <= 1024}; +# +# T2 := {[k,i,j] -> [j,i,j'] : 1 <= k < j < i <= 1024 && j < j' <= 1024}; +# +# T3 := {[k,k+1,k+1] -> [k+1,i',j'] : 1 <= k <= i'-2, j'-2 && j' <= 1024 && i' <= 1024}; +# +# +# # The following expression evaluates to FALSE, which I believe is incorrect: +# +# T3+; + +{[k,k+1,k+1] -> [Out_1,i,j] : 1 <= k < Out_1 < i <= 1024 && Out_1+1 <= j <= 1024} + +# +# +# # And the following cause assertion failures: +# +# (T2 union T3)+; + +{[k,k+1,k+1] -> [j',i',j''] : 1 <= k < j' < i' <= 1024 && j'+1 <= j'' <= 1024} union + {[k,i,i-1] -> [j',i',j''] : k+2 <= i <= j' < j'' <= 1024 && j' < i' <= 1024 && 1 <= k} union + {[k,i,j] -> [j',i',j''] : j+2 <= i <= j' < i' <= 1024 && 1 <= k < j && j' < j'' <= 1024} union + {[k,i,j] -> [j',i,j''] : 1 <= k < j < j' < i <= 1024 && j' < j'' <= 1024} union + {[k,i,j] -> [j,i,j''] : 1 <= k < j < i <= 1024 && j < j'' <= 1024} + +# +# (T1 union T2)+; + +{[k,i,j] -> [Out_1,i,j] : 1 <= k < Out_1 < i <= 1024 && Out_1+1 <= j <= 1024} union + {[k,i,j] -> [Out_1,i,j'] : 1 <= k < j < Out_1 < i <= 1024 && Out_1 < j' <= 1024} union + {[k,i,j] -> [j,i,j'] : 1 <= k < j < i <= 1024 && j < j' <= 1024} + +# +# +# # This comes from Guassian Elimination. |