diff options
Diffstat (limited to 'tests/examples')
-rw-r--r-- | tests/examples/ex1.hs | 5 | ||||
-rw-r--r-- | tests/examples/ex2.hs | 5 | ||||
-rw-r--r-- | tests/examples/ex24.hs | 16 | ||||
-rw-r--r-- | tests/examples/ex3.hs | 38 | ||||
-rw-r--r-- | tests/examples/ex5.ys | 18 | ||||
-rw-r--r-- | tests/examples/ex6.ys | 18 | ||||
-rw-r--r-- | tests/examples/ex66.hs | 7 | ||||
-rw-r--r-- | tests/examples/ex67.hs | 10 |
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 + |