diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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