Permalink
Browse files

Add more tests:

#2 demonstrates a bug in the formula rewriting
#3 shows a performance problem
  • Loading branch information...
1 parent 69ffa6d commit 4dac596e010091de12cee99270a6ccdb0887be0f @yav committed Mar 26, 2009
Showing with 23 additions and 0 deletions.
  1. +8 −0 tests/2.hs
  2. +15 −0 tests/3.hs
View
@@ -0,0 +1,8 @@
+import Data.Integer.Presburger
+
+mytest1 = Exists $ \i -> Exists $ \j -> i :<: j :/\: j :=: 3
+mytest2 = Exists $ \j -> j :=: 3 :/\: (Exists $ \i -> i :<: j)
+
+main = print (check mytest1 == check mytest2)
+
+
View
@@ -0,0 +1,15 @@
+import Data.Integer.Presburger
+
+mytest5 =
+ Not $ Forall $ \a ->
+ Forall $ \b ->
+ Forall $ \c ->
+ Forall $ \d ->
+ Forall $ \e ->
+ Not $ a :=: 2 .* b
+ :/\: b :=: c + 2
+ :/\: d :=: 2 * c
+ :/\: c :=: e + 1
+ :/\: e :=: 1
+
+

0 comments on commit 4dac596

Please sign in to comment.