Merge branch 'master' into doe

1 files changed, 36 insertions, 0 deletions

diff --git a/omega/examples/old_test/wak6.oc-rt b/omega/examples/old_test/wak6.oc-rt
new file mode 100644
index 0000000..458f5e9
--- /dev/null
+++ b/omega/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.