summaryrefslogtreecommitdiff
path: root/omega/examples/pufs.out
diff options
context:
space:
mode:
authorTuowen Zhao <ztuowen@gmail.com>2016-09-17 03:22:53 +0000
committerTuowen Zhao <ztuowen@gmail.com>2016-09-17 03:22:53 +0000
commit75ff98e4d65862ff5b36b533b4f6e3ea71ede1d5 (patch)
tree498ac06b4cf78568b807fafd2619856afff69c28 /omega/examples/pufs.out
parent29efa7b1a0d089e02a70f73f348f11878955287c (diff)
downloadchill-75ff98e4d65862ff5b36b533b4f6e3ea71ede1d5.tar.gz
chill-75ff98e4d65862ff5b36b533b4f6e3ea71ede1d5.tar.bz2
chill-75ff98e4d65862ff5b36b533b4f6e3ea71ede1d5.zip
cmake build
Diffstat (limited to 'omega/examples/pufs.out')
-rw-r--r--omega/examples/pufs.out50
1 files changed, 0 insertions, 50 deletions
diff --git a/omega/examples/pufs.out b/omega/examples/pufs.out
deleted file mode 100644
index df65564..0000000
--- a/omega/examples/pufs.out
+++ /dev/null
@@ -1,50 +0,0 @@
-# Omega Calculator [v1.1, Nov 96]:
-# #
-# # Examples of relations using uninterpreted function symbols
-# # from Omega Calculator documentation
-# #
-#
-# symbolic p(2), n, m;
-#
-# R := { [ir,jr] : 1 <= ir <= n && 1 <= jr <= m };
-#
-# W1 := { [iw,jw] : 1 <= iw <= n && 1 <= jw <= m && p(Set) >= 0 };
-#
-# W2 := { [iw,jw] : 1 <= iw <= n && 1 <= jw <= m && p(Set) < 0 };
-#
-# Exposed := R intersection complement ( W1 union W2 );
-#
-# Exposed;
-
-{[In_1,In_2] : FALSE }
-
-#
-#
-# symbolic f(1);
-#
-# R1 := { [i] -> [j] : 1 <= i = j <= 100 && f(In) <= f(Out)};
-#
-# R2 := { [i] -> [j] : 1 <= i <= j <= 100 && f(In) = f(Out)};
-#
-#
-# R1 intersection R2;
-
-{[i] -> [i] : 1 <= i <= 100}
-
-#
-# R1 union R2;
-
-{[i] -> [j] : f(j) = f(i) && 1 <= i < j <= 100} union
- {[i] -> [i] : 1 <= i <= 100}
-
-#
-# R1 intersection complement R2;
-
-{[i] -> [j] : FALSE }
-
-#
-# R1;
-
-{[i] -> [i] : 1 <= i <= 100}
-
-#