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
             ]