packages feed

yices-easy (empty) → 0.1

raw patch · 10 files changed

+854/−0 lines, 10 filesdep +basedep +bindings-yicesdep +containerssetup-changed

Dependencies added: base, bindings-yices, containers, transformers

Files

+ LICENSE view
@@ -0,0 +1,26 @@+Copyright (c) Keegan McAllister 2010++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:+1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.+2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.+3. Neither the name of the author nor the names of his contributors+   may be used to endorse or promote products derived from this software+   without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS ``AS IS''+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR ANY+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,4 @@+#! /usr/bin/runhaskell++import Distribution.Simple+main = defaultMain
+ Yices/Easy.hs view
@@ -0,0 +1,8 @@+-- | Re-exports the core of this package.++module Yices.Easy+  ( module Yices.Easy.Types+  , module Yices.Easy.Run ) where++import Yices.Easy.Types+import Yices.Easy.Run
+ Yices/Easy/Build.hs view
@@ -0,0 +1,151 @@+{-# LANGUAGE+    GeneralizedNewtypeDeriving+  , StandaloneDeriving+  , NamedFieldPuns #-}++-- | Provides a monad transformer for constructing Yices queries.+--+-- This is not an essential part of the interface.  Expressions+-- may be built using @Yices.Easy.Types@ directly.+--+-- The monad is simply a convenient way to handle bookkeeping+-- regarding fresh names, accumulated declarations \/+-- assertions, and choosing variables to retrieve from the+-- @'Model'@.++module Yices.Easy.Build+  ( -- * The monad transformer+    BuildT+  , Build+  , runBuildT+  , execBuildT+  , runBuild+  , execBuild++    -- * Invoking Yices directly+  , solveBuildT+  , solveBuild++    -- * Fresh names+  , freshName++    -- * Declarations+  , declare+  , fresh++    -- * Assertions+  , assert++    -- * Getting variables+  , get++    -- * Declaring and getting variables+  , declInt+  , declBool+  , declBitvec+  ) where++import Yices.Easy.Types+import Yices.Easy.Run++import Data.Functor.Identity+import Control.Monad+import Control.Applicative++import qualified Data.Map                  as M+import qualified Control.Monad.Trans.State as S++data State = State+  { sNext    :: Integer+  , sDecls   :: [Declaration]+  , sAsserts :: [Assertion]+  , sGets    :: M.Map Ident VarType }++startState :: State+startState = State+  { sNext    = 0+  , sDecls   = []+  , sAsserts = []+  , sGets    = M.empty }++-- | Monad transformer for building Yices queries.+newtype BuildT m a = BuildT (S.StateT State m a)++type Build a = BuildT Identity a++deriving instance (Functor m) => Functor (BuildT m)+deriving instance (Monad   m) => Monad   (BuildT m)+deriving instance (Functor m, Monad m) => Applicative (BuildT m)++runBuildT :: (Monad m) => BuildT m a -> m (a, Query)+runBuildT (BuildT x) = do+  (v, State { sDecls, sAsserts, sGets }) <- S.runStateT x startState+  let gets = map (uncurry Get) $ M.assocs sGets+  return (v, Query (Context sDecls sAsserts) gets)++execBuildT :: (Monad m) => BuildT m a -> m Query+execBuildT x = snd `liftM` runBuildT x++runBuild :: Build a -> (a, Query)+runBuild = runIdentity . runBuildT++execBuild :: Build a -> Query+execBuild = runIdentity . execBuildT++-- | Invoke @'solve'@ on a @'Build'@ action directly.+solveBuild :: Build a -> IO Result+solveBuild = solve . execBuild++-- | Invoke @'solve'@ on a @'BuildT' 'IO'@ action directly.+solveBuildT :: BuildT IO a -> IO Result+solveBuildT x = execBuildT x >>= solve++-- | Generate a fresh name from a base string.+--+-- The name will not conflict with a user-specified name+-- unless that name begins with an underscore.+freshName :: (Monad m) => Ident -> BuildT m Ident+freshName x = BuildT $ do+  s@State { sNext=n } <- S.get+  S.put $ s { sNext=succ n }+  return $ concat ["_", x, "_", show n]++-- | Declare a variable.+declare :: (Monad m) => Ident -> Type -> BuildT m Expr+declare x t = BuildT $ do+  S.modify $ \s -> s { sDecls = Declare x t : sDecls s }+  return $ Var x++-- | Declare a fresh variable given a base name.+--+-- See @'freshName'@ for naming details.+fresh :: (Monad m) => Ident -> Type -> BuildT m Expr+fresh x t = freshName x >>= flip declare t++-- | Assert a Boolean truth.+assert :: (Monad m) => Expr -> BuildT m ()+assert e = BuildT . S.modify $ \s ->+  s { sAsserts = Assert e : sAsserts s }++-- | Arrange to get this variable in the resulting @'Model'@.+get :: (Monad m) => Ident -> VarType -> BuildT m ()+get x t = BuildT . S.modify $ \s ->+  s { sGets = M.insert x t $ sGets s }++declGet :: (Monad m) => Type -> VarType -> Ident -> BuildT m Expr+declGet t v x = do+  e <- declare x t+  get x v+  return e++-- | Declare an @int@ variable and @'get'@ it.+declInt :: (Monad m) => Ident -> BuildT m Expr+declInt = declGet (TyName "int") VarInt++-- | Declare a @bool@ variable and @'get'@ it.+declBool :: (Monad m) => Ident -> BuildT m Expr+declBool = declGet (TyName "bool") VarBool++-- | Declare a bitvector variable and @'get'@ it.+declBitvec :: (Monad m) => Size -> Ident -> BuildT m Expr+declBitvec n = declGet (TyBitvec n) (VarBitvec n)
+ Yices/Easy/Run.hs view
@@ -0,0 +1,200 @@+{-# LANGUAGE+    PatternGuards+  , Rank2Types #-}++-- | Running the Yices SMT solver.++module Yices.Easy.Run+  ( -- * Solving+    solve+    -- * Debugging+  , dump+  ) where++import Yices.Easy.Types++import Data.Maybe+import Data.Ratio+import Control.Applicative+import Control.Monad+import Control.Exception+import Foreign+import Foreign.C++import qualified Data.Map              as M+import qualified Foreign.Marshal.Utils as MU++import qualified Bindings.Yices.Internal as Y++type PExpr  = Ptr Y.YExpr+type PType  = Ptr Y.YType+type PCtx   = Ptr Y.YContext+type PVar   = Ptr Y.YVarDecl+type PModel = Ptr Y.YModel++type Env = M.Map Ident PVar++fI :: (Integral a, Num b) => a -> b+fI = fromIntegral++buildExpr :: Env -> PCtx -> Expr -> IO PExpr+buildExpr env ctx = go where+  lift1 x     f = go x >>= f+  lift2 x y   f = join $ liftM2 f (go x) (go y)+  lift3 x y z f = join $ liftM3 f (go x) (go y) (go z)+  liftN xs f = do+    ys <- mapM go xs+    withArrayLen ys $ \n a -> f a (fI n)++  go (LitBool b) = (if b then Y.c_mk_true else Y.c_mk_false) ctx+  go (LitNum (FromInt    i)) = Y.c_mk_num ctx $ fI i+  go (LitNum (FromString s)) = withCString s $ Y.c_mk_num_from_string ctx++  go (Var i)+    | Just d <- M.lookup i env = Y.c_mk_var_from_decl ctx d+    | otherwise                = error ("undefined variable: " ++ i)++  go (Apply   f xs ) = lift1 f $ \fp -> liftN xs $ Y.c_mk_app ctx fp+  go (Arith   o es ) = liftN es $ getArith o ctx+  go (Logic   o es ) = liftN es $ getLogic o ctx+  go (Compare o x y) = lift2 x y $ getCompare o ctx+  go (Not       x  ) = lift1 x $ Y.c_mk_not ctx++  go (IfThenElse x y z) = lift3 x y z $ Y.c_mk_ite ctx++  go (LitBitvec (FromULong n v)) = Y.c_mk_bv_constant ctx (fI n) v+  go (LitBitvec (FromBits bs)) = withArrayLen (map (fI.fromEnum) bs) $+    \n xs -> Y.c_mk_bv_constant_from_array ctx (fI n) xs++  go (BitArith     o x y) = lift2 x y $ getBArith     o  ctx+  go (BitLogic     o x y) = lift2 x y $ getBLogic     o  ctx+  go (BitCompare s o x y) = lift2 x y $ getBCompare s o  ctx+  go (BitMinus       x  ) = lift1 x   $ Y.c_mk_bv_minus  ctx+  go (BitNot         x  ) = lift1 x   $ Y.c_mk_bv_not    ctx+  go (BitConcat      x y) = lift2 x y $ Y.c_mk_bv_concat ctx++  go (BitShift d f  n  x) = lift1 x $ \p -> getBShift d f ctx p (fI n)+  go (BitExtract n0 n1 x) = lift1 x $ Y.c_mk_bv_extract ctx (fI n1) (fI n0)+  go (BitSignEx     n  x) = lift1 x $ \p -> Y.c_mk_bv_sign_extend ctx p (fI n)++  getArith Add = Y.c_mk_sum+  getArith Sub = Y.c_mk_sub+  getArith Mul = Y.c_mk_mul++  getLogic And = Y.c_mk_and+  getLogic Or  = Y.c_mk_or+  getLogic Xor = error "Yices.Easy.Run: no xor for booleans"++  getCompare Eq = Y.c_mk_eq+  getCompare Ne = Y.c_mk_diseq+  getCompare Gt = Y.c_mk_gt+  getCompare Ge = Y.c_mk_ge+  getCompare Lt = Y.c_mk_lt+  getCompare Le = Y.c_mk_le++  getBArith Add = Y.c_mk_bv_add+  getBArith Sub = Y.c_mk_bv_sub+  getBArith Mul = Y.c_mk_bv_mul++  getBLogic And = Y.c_mk_bv_and+  getBLogic Or  = Y.c_mk_bv_or+  getBLogic Xor = Y.c_mk_bv_xor++  getBCompare _ Eq = Y.c_mk_eq+  getBCompare _ Ne = Y.c_mk_diseq+  getBCompare Signed   Gt = Y.c_mk_bv_sgt+  getBCompare Signed   Ge = Y.c_mk_bv_sge+  getBCompare Signed   Lt = Y.c_mk_bv_slt+  getBCompare Signed   Le = Y.c_mk_bv_sle+  getBCompare Unsigned Gt = Y.c_mk_bv_gt+  getBCompare Unsigned Ge = Y.c_mk_bv_ge+  getBCompare Unsigned Lt = Y.c_mk_bv_lt+  getBCompare Unsigned Le = Y.c_mk_bv_le++  getBShift L B0 = Y.c_mk_bv_shift_left0+  getBShift L B1 = Y.c_mk_bv_shift_left1+  getBShift R B0 = Y.c_mk_bv_shift_right0+  getBShift R B1 = Y.c_mk_bv_shift_right1++buildType :: PCtx -> Type -> IO PType+buildType ctx = go where+  lift1 x     f = go x >>= f+  liftN xs f = do+    ys <- mapM go xs+    withArrayLen ys $ \n a -> f a (fI n)++  go (TyName xs) = withCString xs $ Y.c_mk_type ctx+  go (TyFun xs r) = lift1 r $ \rp -> liftN xs $ \xp n ->+    Y.c_mk_function_type ctx xp n rp+  go (TyBitvec n) = Y.c_mk_bitvector_type ctx (fI n)+  go (TyTuple xs) = liftN xs $ \xp n -> MU.with xp $ \xpp ->+    Y.c_mk_tuple_type ctx xpp n++withContext :: Context -> (Env -> PCtx -> IO a) -> IO a+withContext (Context ds as) act+    = bracket Y.c_mk_context Y.c_del_context $ \ctx -> do+  let mkD m (Declare x t) = do+        tp <- buildType ctx t+        dp <- withCString x $ \xp -> Y.c_mk_var_decl ctx xp tp+        return $ M.insert x dp m+  Y.c_enable_type_checker 1+  env <- foldM mkD M.empty ds+  let mkA (Assert e) = buildExpr env ctx e >>= Y.c_assert ctx+  mapM_ mkA as+  act env ctx ++-- | Dump some information about a context+-- and expression to standard output.+dump :: Context -> Expr -> IO ()+dump c e = withContext c $ \env ctx -> do+  ep <- buildExpr env ctx e+  Y.c_dump_context ctx+  putStrLn "expression:"+  Y.c_pp_expr ep+  putStrLn ""++get :: Env -> PModel -> Get -> IO (Maybe (Ident, Value))+get env mdl (Get v t) = do+  x <- go (M.lookup v env)+  return ((,) v <$> x) where++  go (Just dp) = case t of+    VarBool     -> (Just . fromLBool) <$>    Y.c_get_value mdl dp+    VarInt      -> chk ValInt    $ Y.c_get_int_value       mdl dp+    VarRational -> withRational  $ Y.c_get_arith_value     mdl dp+    VarDouble   -> chk ValDouble $ Y.c_get_double_value    mdl dp+    VarBitvec n -> withVec n     $ Y.c_get_bitvector_value mdl dp (fI n)+  go Nothing = return Nothing++  fromLBool 1 = ValBool True+  fromLBool _ = ValBool False++  chk f a = alloca $ \p -> do+    x <- a p+    if x /= 1+      then return Nothing+      else (Just . f) <$> peek p+  withRational a = alloca $ \n -> alloca $ \d -> do+    x <- a n d+    if x /= 1+      then return Nothing+      else (Just . ValRational) <$> liftM2 (%) (fI <$> peek n) (fI <$> peek d)+  withVec n a = allocaArray n $ \p -> do+    x <- a p+    if x /= 1+      then return Nothing+      else (Just . ValBitvec . map (toEnum.fI)) <$> peekArray n p++-- | Solve a satisfiability query.+--+-- If satisfiable, returns values for the specified+-- variables.+solve :: Query -> IO Result+solve (Query c ts) = withContext c $ \env ctx -> do+  sat <- Y.c_check ctx+  case sat of+    1 -> do+      mdl <- Y.c_get_model ctx+      (Sat . M.fromList . catMaybes) <$> mapM (get env mdl) ts+    0 -> return Unsat+    _ -> return Unknown
+ Yices/Easy/Sugar.hs view
@@ -0,0 +1,169 @@+-- | Syntactic sugar for embedding Yices expressions in Haskell.+--+-- Defines a number of aliases and infix operators, and a+-- @'Num'@ instance for @'Expr'@.+--+-- This is not an essential part of the interface. Expressions+-- may be built using @Yices.Easy.Types@ directly.+--+-- This is a quick hack.  There are several other projects working+-- on vastly more sophisticated SMT EDSLs, so this one is unlikely+-- to receive much attention.  That said, suggestions and patches+-- are always welcome.++{-# OPTIONS_GHC+  -fno-warn-orphans #-}++module Yices.Easy.Sugar+ ( -- * Types+   real, int, nat, bool++   -- * Booleans+ , true, false+ , (||.), (&&.)++   -- * Application+ , ($.)++   -- * Scalar arithmetic+   +   -- | We also provide @instance 'Num' 'Expr'@,+   -- so you can use @('+')@, @('*')@, @('-')@,+   -- @'negate'@, @'fromInteger'@, and integer+   -- literals.+ , add, mul, sub++   -- * Scalar comparison+ , (==.), (/=.), (>.), (>=.), (<.), (<=.)++   -- * Literal bitvectors+ , bv++   -- * Bitvector arithmetic+ , (+@), (-@), (*@)++   -- * Signed bitvector comarpsion+ , (>@), (>=@), (<@), (<=@)+ +   -- * Unsigned bitvector comparison+ , (>@@), (>=@@), (<@@), (<=@@)++   -- * Bitvector concatenation+ , (++@)++   -- * Bitwise operations+ , (|@), (&@), (^@)+ ) where+++import Yices.Easy.Types+++real, int, nat, bool :: Type+real = TyName "real"+int  = TyName "int"+nat  = TyName "nat"+bool = TyName "bool"+++true, false :: Expr+true  = LitBool True+false = LitBool False+++infixr 0 $.+($.) :: Expr -> [Expr] -> Expr+($.) = Apply+++instance Num Expr where+  x + y = Arith Add [x,y]+  x * y = Arith Mul [x,y]+  x - y = Arith Sub [x,y]+  abs    = error "Expr: cannot use abs"+  signum = error "Expr: cannot use signum"+  fromInteger = LitNum . FromString . show++add, mul, sub :: [Expr] -> Expr+add = Arith Add+mul = Arith Mul+sub = Arith Sub+++infix 4 ==.+infix 4 /=.+infix 4 >.+infix 4 >=.+infix 4 <.+infix 4 <=.++(==.), (/=.), (>.), (>=.), (<.), (<=.) :: Expr -> Expr -> Expr+(==.) = Compare Eq+(/=.) = Compare Ne+(>.)  = Compare Gt+(>=.) = Compare Ge+(<.)  = Compare Lt+(<=.) = Compare Le+++infixr 2 ||.+infixr 3 &&.++(||.), (&&.) :: Expr -> Expr -> Expr+x ||. y = Logic Or  [x,y]+x &&. y = Logic And [x,y]+++infixl 6 +@+infixl 6 -@+infixl 7 *@++(+@), (-@), (*@) :: Expr -> Expr -> Expr+(+@) = BitArith Add+(*@) = BitArith Mul+(-@) = BitArith Sub+++infix 4 >@+infix 4 >=@+infix 4 <@+infix 4 <=@+infix 4 >@@+infix 4 >=@@+infix 4 <@@+infix 4 <=@@++(>@), (>=@), (<@), (<=@), (>@@), (>=@@), (<@@), (<=@@) :: Expr -> Expr -> Expr+(>@)   = BitCompare Signed   Gt+(>=@)  = BitCompare Signed   Ge+(<@)   = BitCompare Signed   Lt+(<=@)  = BitCompare Signed   Le+(>@@)  = BitCompare Unsigned Gt+(>=@@) = BitCompare Unsigned Ge+(<@@)  = BitCompare Unsigned Lt+(<=@@) = BitCompare Unsigned Le+++infixr 5 ++@++(++@) :: Expr -> Expr -> Expr+(++@) = BitConcat+++infixr 5 |@+infixr 7 &@+infixr 7 ^@++(|@), (&@), (^@) :: Expr -> Expr -> Expr+(|@) = BitLogic Or+(&@) = BitLogic And+(^@) = BitLogic Xor+++-- | @bv s n@ has value @n@ and size at least @s@.+bv :: Size -> Integer -> Expr+bv _ n+  | n < 0 = error "Yices.Easy.Sugar.bv: negative Integer not allowed"+bv s n = LitBitvec . FromBits $ getBits s n where+  getBits b 0 = replicate b B0+  getBits b k = let (d,m) = k `divMod` 2 in toEnum (fromIntegral m) : getBits (b-1) d
+ Yices/Easy/Types.hs view
@@ -0,0 +1,166 @@+-- | Types for Yices syntax, in the subset we support.++module Yices.Easy.Types+  -- export everything+  where++import Foreign.C.Types ( CULong, CLong, CDouble )+import qualified Data.Map as M++-- * Top level++-- | Declare the existence of a variable.+data Declaration+  = Declare Ident Type+  deriving (Show)++-- | Assert a Boolean fact.+newtype Assertion+  = Assert Expr+  deriving (Show)++-- | Assert some facts in the context of some variables.+data Context+  = Context [Declaration] [Assertion]+  deriving (Show)++-- * Expressions++-- | Types.+data Type+  = TyName   Ident        -- ^ Named type.+  | TyFun    [Type] Type  -- ^ Function, with args and result type.+  | TyBitvec Size         -- ^ Bitvector.+  | TyTuple  [Type]       -- ^ Tuple.+  deriving (Show)++-- | Expressions.+data Expr+  = LitBool    Bool                          -- ^ Literal boolean.+  | LitNum     LitNum                        -- ^ Literal number.+  | Var        Ident                         -- ^ Variable.++  | Apply      Expr [Expr]                   -- ^ Function application.+  | Arith      Arith [Expr]                  -- ^ Arithmetic.+  | Logic      Logic [Expr]                  -- ^ Boolean logic operation.+  | Not        Expr                          -- ^ Boolean negation.+  | Compare    Compare Expr Expr             -- ^ Comparison.+  | IfThenElse Expr Expr Expr                -- ^ Conditional expression.++  | LitBitvec  LitBitvec                     -- ^ Literal bitvector.+  | BitArith   Arith Expr Expr               -- ^ Bitvector arithmetic.+  | BitMinus   Expr                          -- ^ Bitvector arithmetic negation.+  | BitConcat  Expr Expr                     -- ^ Concatenate bitvectors.+  | BitLogic   Logic Expr Expr               -- ^ Bitwise logical operation.+  | BitNot     Expr                          -- ^ Bitwise negate.+  | BitShift   Direction Bit Size Expr       -- ^ Bit shift with fill.+  | BitCompare Signedness Compare Expr Expr  -- ^ Bitvector comparison.+  | BitExtract Index Index Expr              -- ^ Extract a subvector.+  | BitSignEx  Size  Expr                    -- ^ Sign-extend /n/ extra bits.+  deriving (Show, Eq)  -- need Eq for Num++-- | Ways of specifying a literal number.+data LitNum+  = FromInt    Int+  | FromString String  -- ^ ASCII digits.+  deriving (Show, Eq)++-- | Ways of specifying a literal bitvector.+data LitBitvec+  = FromULong  Size CULong+  | FromBits   [Bit]         -- ^ Least-significant first.+  deriving (Show, Eq)++-- | Arithmetic operations.+data Arith+  = Add+  | Sub+  | Mul+  deriving (Show, Eq)++-- | Logical operations.+data Logic+  = And+  | Or+  | Xor -- ^ Bitvector only; a runtime error for scalars!+  deriving (Show, Eq)++-- | Comparison operations.+data Compare+  = Eq+  | Ne+  | Gt+  | Ge+  | Lt+  | Le+  deriving (Show, Eq)++-- | Direction of shifting.+data Direction+  = L+  | R+  deriving (Show, Eq)++-- | Bits.+data Bit+  = B0+  | B1+  deriving (Show, Enum, Eq)++-- | Signedness of bitvector operations.+data Signedness+  = Signed+  | Unsigned+  deriving (Show, Eq)++-- * Type synonyms++type Ident  = String+type Size   = Int+type Index  = Int++-- * Models++-- | Types of variables which can be queried+-- from a model.+data VarType+  = VarBool+  | VarInt+  | VarRational+  | VarDouble+  | VarBitvec Size+  deriving (Show)++-- | A variable to query from the model.+data Get+  = Get Ident VarType+  deriving (Show)++type ModelType = [Get]++-- | A query to the solver: solve for some variables in a context.+data Query+  = Query Context ModelType+  deriving (Show)++-- | A value produced from a model.+data Value+  = ValBool     Bool+  | ValInt      CLong+  | ValRational Rational+  | ValDouble   CDouble+  | ValBitvec   [Bit] -- ^ Least-significant first.+  deriving (Show)++-- | A model maps variables to values.+--+-- Some of the asked-for variables may be absent, if there was an+-- error or the model was underspecified.+type Model = M.Map Ident Value++-- | Result of trying to solve a model.+data Result+  = Sat Model  -- ^ Definitely satisfiable.+  | Unsat      -- ^ Definitely unsatisfiable.+  | Unknown    -- ^ Unknown, due to incompleteness or error.+  deriving (Show)
+ examples/graph-color.hs view
@@ -0,0 +1,47 @@+import Yices.Easy+import Yices.Easy.Sugar+import Yices.Easy.Build++import Control.Monad+import System+import Data.List++import qualified Data.Map      as M+import qualified Data.GraphViz as G++type Edge  = (Ident, Ident)+data Graph = Graph [Ident] [Edge]++-- graph file contains lines with edges as:+-- nodeA nodeB+parse :: String -> Graph+parse g = Graph vs es where+  es = map ((\[x,y] -> (x,y)) . words) $ lines g+  vs = nub $ concat [ [x,y] | (x,y) <- es ]++query :: Int -> Graph -> Query+query n (Graph vs es) = execBuild $ do+  forM_ vs $ \v -> do+    x <- declInt v+    assert ((x >=. 0) &&. (x <. fromIntegral n))+  forM_ es $ \(x,y) -> assert (Var x /=. Var y)++render :: Graph -> Model -> String+render (Graph vs es) m = G.printDotGraph g where+  g   = G.DotGraph False False Nothing $ G.DotStmts gbl [] vss ess+  gbl = [G.NodeAttrs [G.Style [G.SItem G.Filled []]]]+  vss = [G.DotNode v [G.Color [G.X11Color $ color v]] | v <- vs]+  ess = [G.DotEdge x y False [] | (x,y) <- es]+  colors = [G.Red, G.Green, G.Blue, G.Cyan, G.Magenta, G.Yellow, G.White]+  color v = case M.lookup v m of Just (ValInt i) -> colors !! fromIntegral i++-- runhaskell graph-color.hs <number of colors> <graph file>+main :: IO ()+main = do+  [nx,file] <- getArgs+  numColors <- readIO nx+  graph     <- parse `fmap` readFile file+  result    <- solve $ query numColors graph+  case result of+    Sat model -> writeFile "out.dot" $ render graph model+    _         -> putStrLn "No solution." >> exitFailure
+ examples/latin.hs view
@@ -0,0 +1,40 @@+import Yices.Easy+import Yices.Easy.Sugar+import Yices.Easy.Build++import Control.Monad ( forM_, liftM2 )++import qualified Data.Map as M++import System++cell :: (Int,Int) -> String+cell (x,y) = concat ["c", show x, "_", show y]++query :: Int -> Query+query n = execBuild $ do+  let cells = liftM2 (,) [1..n] [1..n]+  forM_ cells $ \c -> do+    x <- declInt $ cell c+    assert ((x >=. 0) &&. (x <. fromIntegral n))++  forM_ cells $ \c@(i0,j0) -> do+    let notEq c1 = assert (Var (cell c) /=. Var (cell c1))+    forM_ [i0+1..n] $ \i -> notEq (i, j0)+    forM_ [j0+1..n] $ \j -> notEq (i0,j )++run :: Int -> IO ()+run n = do+  Sat model <- solve $ query n+  let soln c = case M.lookup (cell c) model of Just (ValInt k) -> fromIntegral k+      chars  = ['A'..'Z']+      line i = forM_ [1..n] $ \j -> putChar (chars !! soln (i,j)) >> putChar ' '+  forM_ [1..n] $ \i -> line i >> putChar '\n'++-- generate latin squares+-- runhaskell latin.hs <size of square>+main :: IO ()+main = do+  [n] <- getArgs+  nn  <- readIO n+  run nn
+ yices-easy.cabal view
@@ -0,0 +1,43 @@+name:                yices-easy+version:             0.1+license:             BSD3+license-file:        LICENSE+synopsis:            Simple interface to the Yices SMT (SAT modulo theories) solver.+category:            Math, Algorithms, Theorem Provers+author:              Keegan McAllister <mcallister.keegan@gmail.com>+maintainer:          Keegan McAllister <mcallister.keegan@gmail.com>+homepage:            http://www.ugcs.caltech.edu/~keegan/haskell/yices-easy/+build-type:          Simple+cabal-version:       >=1.2+description:+  This library provides a simple interface to Yices, an SMT solver available+  from <http://yices.csl.sri.com/>.+  .+  It uses the Yices C API, which you will need to have installed.  The API is+  not installed on the Hackage server, so you may need to download this package+  in order to read its documentation.  Sorry.+  .++  The core functionality is provided by modules @Types@ and @Run@, and+  re-exported by @Yices.Easy@.  Module @Sugar@ provides optional syntactic+  sugar, and @Build@ provides optional monadic bookkeeping.+  .+  The library aims for simplicity, and not all features of Yices are supported.+  Suggestions and patches are welcome.+extra-source-files:+    examples/latin.hs+  , examples/graph-color.hs++library+  exposed-modules:  +      Yices.Easy+    , Yices.Easy.Types+    , Yices.Easy.Run+    , Yices.Easy.Sugar+    , Yices.Easy.Build+  ghc-options:       -Wall+  build-depends:+      base           >= 3 && < 5+    , containers     >= 0.3+    , transformers   >= 0.2+    , bindings-yices >= 0.2