import Yices.Painless.Language
import Prelude hiding (and)
main = print =<< solve p
data PC = Sleeping | Trying | Critical
deriving (Show, Enum, Bounded)
p ::
(Exp Int -> Exp Int) ->
(Exp Int -> Exp Int) ->
Exp Int -> Exp Int -> Exp Int ->
Exp Int -> Exp Int -> Exp Int -> Exp Bool
p f g x1 x2 x3
x4 x5 x6 =
-- set the range
and [ x >=* (fromIntegral . fromEnum $ (minBound :: PC)) &&*
x <=* (fromIntegral . fromEnum $ (maxBound :: PC)) | x <- [x1,x2,x3,x4,x5,x6] ]
&&*
and [ g (f x1) /=* g (f x2)
, x1 ==* x3
, x1 ==* x4
, x3 ==* x2
]