summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--LICENSE26
-rw-r--r--Setup.hs4
-rw-r--r--Yices/Easy.hs8
-rw-r--r--Yices/Easy/Build.hs151
-rw-r--r--Yices/Easy/Run.hs200
-rw-r--r--Yices/Easy/Sugar.hs169
-rw-r--r--Yices/Easy/Types.hs166
-rw-r--r--examples/graph-color.hs47
-rw-r--r--examples/latin.hs40
-rw-r--r--yices-easy.cabal43
10 files changed, 854 insertions, 0 deletions
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..3cf0e1b
--- /dev/null
+++ b/LICENSE
@@ -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.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
index 0000000..3c63ca4
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,4 @@
+#! /usr/bin/runhaskell
+
+import Distribution.Simple
+main = defaultMain
diff --git a/Yices/Easy.hs b/Yices/Easy.hs
new file mode 100644
index 0000000..7bde951
--- /dev/null
+++ b/Yices/Easy.hs
@@ -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
diff --git a/Yices/Easy/Build.hs b/Yices/Easy/Build.hs
new file mode 100644
index 0000000..10cef1d
--- /dev/null
+++ b/Yices/Easy/Build.hs
@@ -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)
diff --git a/Yices/Easy/Run.hs b/Yices/Easy/Run.hs
new file mode 100644
index 0000000..319dd2b
--- /dev/null
+++ b/Yices/Easy/Run.hs
@@ -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
diff --git a/Yices/Easy/Sugar.hs b/Yices/Easy/Sugar.hs
new file mode 100644
index 0000000..75bf433
--- /dev/null
+++ b/Yices/Easy/Sugar.hs
@@ -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
diff --git a/Yices/Easy/Types.hs b/Yices/Easy/Types.hs
new file mode 100644
index 0000000..e4d7b5f
--- /dev/null
+++ b/Yices/Easy/Types.hs
@@ -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)
diff --git a/examples/graph-color.hs b/examples/graph-color.hs
new file mode 100644
index 0000000..bb5b026
--- /dev/null
+++ b/examples/graph-color.hs
@@ -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
diff --git a/examples/latin.hs b/examples/latin.hs
new file mode 100644
index 0000000..8e29ddb
--- /dev/null
+++ b/examples/latin.hs
@@ -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
diff --git a/yices-easy.cabal b/yices-easy.cabal
new file mode 100644
index 0000000..74b137f
--- /dev/null
+++ b/yices-easy.cabal
@@ -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