1 files changed, 38 insertions, 0 deletions
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))
+-}