diff options
Diffstat (limited to 'omega/examples/old_test/ddtest.oc-rt')
| -rw-r--r-- | omega/examples/old_test/ddtest.oc-rt | 152 |
1 files changed, 152 insertions, 0 deletions
diff --git a/omega/examples/old_test/ddtest.oc-rt b/omega/examples/old_test/ddtest.oc-rt new file mode 100644 index 0000000..1c3e009 --- /dev/null +++ b/omega/examples/old_test/ddtest.oc-rt @@ -0,0 +1,152 @@ +# Omega Calculator v1.2 (based on Omega Library 1.2, August, 2000): +# symbolic p(2), n, m1, m2, low; +# +# +# R := { [ir,jr] : 1 <= ir <= n && 1 <= jr <= m1 }; +# +# +# f1i := { [iw,jw] -> [ir,jr] : 1 <= ir <= n && 1 <= jr <= m1 && +# 1 <= iw <= n && 1 <= jw <= m2 && +# jw = jr && +# iw = ir }; +# +# f1f := { [iw,jw] -> [ir,jr] : 1 <= ir <= n && 1 <= jr <= m1 && +# 1 <= iw <= n && 1 <= jw <= m2 && +# jw = jr && +# iw < ir }; +# +# +# f3i := { [iw,jw] -> [ir,jr] : 1 <= ir <= n && 1 <= jr <= m1 && +# 1 <= iw <= n && 1 < low <= jw <= m1 && +# jw-1 = jr && +# iw = ir }; +# +# f3f := { [iw,jw] -> [ir,jr] : 1 <= ir <= n && 1 <= jr <= m1 && +# 1 <= iw <= n && 1 < low <= jw <= m1 && +# jw-1 = jr && +# iw < ir }; +# +# +# o31i := { [iw3,jw3] -> [iw1,jw1] : 1 <= iw1 <= n && 1 <= jw1 <= m2 && +# 1 <= iw3 <= n && 1 < low <= jw3 <= m1 && +# jw1 = jw3-1 && +# iw1 = iw3 }; +# +# +# o13f := { [iw1,jw1] -> [iw3,jw3] : 1 <= iw1 <= n && 1 <= jw1 <= m2 && +# 1 <= iw3 <= n && 1 < low <= jw3 <= m1 && +# jw1 = jw3-1 && +# iw1 < iw3 }; +# +# +# o31f := { [iw3,jw3] -> [iw1,jw1] : 1 <= iw1 <= n && 1 <= jw1 <= m2 && +# 1 <= iw3 <= n && 1 < low <= jw3 <= m1 && +# jw1 = jw3-1 && +# iw3 < iw1 }; +# +# +# o11f := { [iw1a,jw1a] -> [iw1b,jw1b] : 1 <=iw1a<= n && 1 <=jw1a<= m2 && +# 1 <=iw1b<= n && 1 <=jw1b<= m2 && +# jw1a = jw1b && +# iw1a < iw1b }; +# +# o33f := { [iw3a,jw3a] -> [iw3b,jw3b] : 1 <=iw3a<= n && 1 < low <=jw3a<= m1 && +# 1 <=iw3b<= n && 1 < low <=jw3b<= m1 && +# jw3a-1 = jw3b-1 && +# iw3a < iw3b }; +# +# +# +# # FIRST GROUP - 1i and 2i (NO POSSIBLE OUTPUT DEPS. BETWEEN) +# v1i := f1i; +# +# v1i; + +{[iw,jw] -> [iw,jw] : 1 <= jw <= m1, m2 && 1 <= iw <= n} + +# +# +# Exposed12i := R intersection complement domain f1i; +# +# Exposed12i; + +{[In_1,In_2]: 1, m2+1 <= In_2 <= m1 && 1 <= In_1 <= n} + +# +# +# # SECOND GROUP - 3i +# v3i := f3i / Exposed12i; +# # / is restrictRange +# v3i; + +{[iw,jw] -> [iw,jw-1] : 2 <= low <= jw <= m1 && 1 <= iw <= n && m2 <= jw-2} + +# +# +# Exposed3i := R intersection complement domain f3i; +# +# Exposed3i; + +{[In_1,In_2]: 1 <= In_1 <= n && 1 <= In_2 <= m1 && low <= 1} union + {[In_1,In_2]: 1 <= In_2 <= m1, low-1 && 1 <= In_1 <= n} + +# +# +# # THIRD GROUP - 1,2,3f (THERE ARE POSSIBLE OUTPUT DEPS BETWEEN THEM) +# +# v1f := ( f1f / Exposed3i ) +# intersection complement ( f3i compose o13f ) +# intersection complement ( f3f compose o13f ) +# intersection complement ( f1i compose o11f ) +# intersection complement ( f1f compose o11f ); +# +# v1f; + +{[iw1a,jw1a] -> [ir,jr] : FALSE } + +# +# +# # WE SHOULD BE ABLE TO DO v1f WITH SOME VALUE-BASED FLOW DD'S +# +# v1f_val := ( f1f / Exposed3i ) +# intersection complement ( v3i compose o13f ) +# intersection complement ( f3f compose o13f ) +# intersection complement ( v1i compose o11f ) +# intersection complement ( f1f compose o11f ); +# +# v1f_val; + +{[iw1a,jw1a] -> [ir,jr] : FALSE } + +# +# +# # +# # The effects of loop-independent flow have been taken out already, +# # so this should work. But it does not. Probably I am stupyd. +# # +# +# v1f_clever := ( f1f / Exposed3i ) +# intersection complement ( f3f compose o13f ) +# intersection complement ( f1f compose o11f ); +# +# v1f_clever; + +{[iw1a,jw1a] -> [iw1a+1,jw1a] : 1 <= jw1a <= m2, m1 && 1 <= iw1a < n && low <= 1} union + {[iw1a,jw1a] -> [iw1a+1,jw1a] : 1 <= jw1a <= m2, m1, low-1 && 1 <= iw1a < n} + +# +# +# # +# # NOW CHECK FOR EQUIVALENCES - THESE SHOULD BE TRUE +# # +# +# v1f subset v1f_val; + +True +# +# v1f_val subset v1f; + +True +# +# # v1f subset v1f_clever; +# # v1f_clever subset v1f; |