8 files changed, 117 insertions, 0 deletions
diff --git a/tests/examples/ex1.hs b/tests/examples/ex1.hs
new file mode 100644
index 0000000..7e924e0
--- /dev/null
+++ b/tests/examples/ex1.hs
@@ -0,0 +1,5 @@
+import Yices.Painless.Language
+
+main = print =<< solve p
+
+p = 0 ==* (1 :: Exp Int)
diff --git a/tests/examples/ex2.hs b/tests/examples/ex2.hs
new file mode 100644
index 0000000..fbf6a73
--- /dev/null
+++ b/tests/examples/ex2.hs
@@ -0,0 +1,5 @@
+import Yices.Painless.Language
+
+main = print =<< solve p
+
+p = false
diff --git a/tests/examples/ex24.hs b/tests/examples/ex24.hs
new file mode 100644
index 0000000..6327503
--- /dev/null
+++ b/tests/examples/ex24.hs
@@ -0,0 +1,16 @@
+import Yices.Painless.Language
+
+main = print =<< solve p
+
+data S = S1 | S2 | S3
+    deriving (Show, Enum)
+
+p x1 x2 x3 x4 = 
+    and 
+      [ (/=*) x1 x2
+      , (/=*) x1 x3
+      , (/=*) x1 x4
+      , (/=*) x2 x3
+      , (/=*) x2 x4
+      , (/=*) x3 x4
+      ]
diff --git a/tests/examples/ex3.hs b/tests/examples/ex3.hs
new file mode 100644
index 0000000..886f8f9
--- /dev/null
+++ b/tests/examples/ex3.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+import Yices.Painless.Language
+import Prelude hiding (and)
+
+main = print =<< solve p
+
+-- Currently, need to derive Int, then translate in and out.
+
+data PC = Sleeping | Trying | Critical
+    deriving (Show, Enum)
+
+p x1 x2 z1 z2 (w1 :: Exp Int) (w2 :: Exp Int) =
+  and
+    [ x1 ==* x2
+    , x1 ==* z1
+    , x2 ==* fromIntegral (fromEnum Critical)
+    , x2 ==* z2
+    , x2 ==* w1
+    , x1 ==* fromIntegral (fromEnum Trying)
+    ]
+
+{-
+-- (define-type pc (scalar sleeping trying critical))
+(define x1::pc)
+(define x2::pc)
+(define z1::pc)
+(define z2::pc)
+(define w1::pc)
+(define w2::pc)
+
+(assert (= x1 x2))
+(assert (= x1 z1))
+(assert (= x2 critical))
+(assert (= x2 z2))
+(assert (= z2 w1))
+(assert (= x1 trying))
+-}
diff --git a/tests/examples/ex5.ys b/tests/examples/ex5.ys
new file mode 100644
index 0000000..e813861
--- /dev/null
+++ b/tests/examples/ex5.ys
@@ -0,0 +1,18 @@
+
+(define-type pc (scalar sleeping trying critical))
+(define f::(-> pc pc))
+(define g::(-> pc pc))
+(define x1::pc)
+(define x2::pc)
+(define x3::pc)
+(define x4::pc)
+(define x5::pc)
+(define x6::pc)
+
+
+
+(assert (/= (g (f x1)) (g (f x2))))
+(assert (= x1 x3))
+(assert (= x1 x4))
+(assert (= x3 x2))
+
diff --git a/tests/examples/ex6.ys b/tests/examples/ex6.ys
new file mode 100644
index 0000000..0bd00f3
--- /dev/null
+++ b/tests/examples/ex6.ys
@@ -0,0 +1,18 @@
+
+(define-type pc (scalar sleeping trying critical))
+(define f::(-> pc pc))
+(define g::(-> pc pc))
+(define x1::pc)
+(define x2::pc)
+(define x3::pc)
+(define x4::pc)
+(define x5::pc)
+(define x6::pc)
+
+
+
+(assert (= x1 x3))
+(assert (= x1 x4))
+(assert (= x3 x2))
+(assert (/= (g (f x1)) (g (f x2))))
+
diff --git a/tests/examples/ex66.hs b/tests/examples/ex66.hs
new file mode 100644
index 0000000..d787cdb
--- /dev/null
+++ b/tests/examples/ex66.hs
@@ -0,0 +1,7 @@
+import Yices.Painless.Language
+
+main = print =<< solve p
+
+p :: Exp Int -> Exp Int -> Exp Int -> Exp Bool
+p x y z = (3 * x) + (6 * y) ==* 1
+
diff --git a/tests/examples/ex67.hs b/tests/examples/ex67.hs
new file mode 100644
index 0000000..ecf451c
--- /dev/null
+++ b/tests/examples/ex67.hs
@@ -0,0 +1,10 @@
+import Yices.Painless.Language
+
+main = print =<< solve p
+
+p :: Exp Int -> Exp Int -> Exp Int -> Exp Bool 
+p x y z =
+    (3 * x) + (6 * y) + z ==* 1
+  &&*
+    z ==* 2
+