diff --git a/Bindings/Yices.hs b/Bindings/Yices.hs
new file mode 100644
--- /dev/null
+++ b/Bindings/Yices.hs
@@ -0,0 +1,218 @@
+{-# LANGUAGE EmptyDataDecls #-}
+
+module Bindings.Yices (YDef(..), module Bindings.Yices) where
+
+import Bindings.Yices.Internal
+import Control.Applicative
+import Control.Monad
+import Foreign
+import Foreign.Ptr
+import Foreign.C.Types
+import Foreign.C.String
+
+import qualified Data.Traversable as T
+
+type Context = Ptr YContext
+type Expr    = Ptr YExpr
+type Decl    = Ptr YDecl
+type VarDecl = Ptr YVarDecl
+type Type    = Ptr YType
+type Model   = Ptr YModel
+type VarIterator = Ptr YVarIterator
+
+type YBool  = YDef Bool
+
+data SAT a  = Sat a | Unknown a | Unsat
+
+-- * Initialization
+
+mkContext :: IO Context
+mkContext = c_mk_context
+
+delContext :: Context -> IO ()
+delContext = c_del_context
+
+withContext :: (Context -> IO a) -> IO a
+withContext f = do {ctx <- c_mk_context; f ctx <* c_del_context ctx}
+
+setVerbosity :: Int -> IO ()
+setVerbosity = c_set_verbosity . fromIntegral
+
+setLogFile :: FilePath -> IO ()
+setLogFile fp = withCString fp c_enable_log_file
+
+enableTypeChecker :: Bool -> IO ()
+enableTypeChecker True  = c_enable_type_checker 1
+enableTypeChecker False = c_enable_type_checker 0
+
+isInconsistent :: Context -> IO Bool
+isInconsistent = liftM (toEnum.fromIntegral) . c_inconsistent
+
+-- * Assertions
+
+assert :: Context -> Expr -> IO ()
+assert = c_assert
+
+assertWeighted :: Context -> Expr -> Int -> IO AssertionId
+assertWeighted ctx e = c_assert_weighted ctx e . fromIntegral
+
+-- * Proof Search
+
+check :: Context -> IO YBool
+check = liftM eatYBool . c_check
+
+maxSat :: Context -> IO YBool
+maxSat = liftM eatYBool . c_max_sat
+
+maxSatCost :: Context -> Int -> IO YBool
+maxSatCost ctx = liftM eatYBool . c_max_sat_cost_leq ctx . fromIntegral
+
+-- | Calls 'check' to ensure that the context is satisfiable and then returns a model
+getModel :: Context -> IO (SAT [(String, YBool)])
+getModel ctx = do
+  sat <- check ctx
+  case sat of
+    YDef True  -> Sat <$> (getBoolModel ctx =<< c_get_model ctx)
+    YUndef     -> Unknown <$> (getBoolModel ctx =<< c_get_model ctx)
+    YDef False -> pure Unsat
+
+getMaxSatModel :: Context -> Maybe Int -> IO (SAT [(String, YBool)])
+getMaxSatModel ctx cost = do
+  sat <- maybe (maxSat ctx) (maxSatCost ctx) cost
+  case sat of
+    YDef True  -> Sat <$> (getBoolModel ctx =<< c_get_model ctx)
+    YUndef     -> Unknown <$> (getBoolModel ctx =<< c_get_model ctx)
+    YDef False -> pure Unsat
+
+-- | Returns a model
+--   Assumes that you have evaluated the context already with 'check' or maxSat'.
+--   The behaviour if you haven't done so is unspecified.
+getModel' :: Context -> IO Model
+getModel' = c_get_model
+
+findWeightedModel :: Context -> Int -> IO YBool
+findWeightedModel ctx = liftM eatYBool . c_find_weighted_model ctx . fromIntegral
+
+-- Evaluation
+
+getVarDecl :: Context -> String -> IO(Maybe VarDecl)
+getVarDecl ctx name = do
+  ptr <- withCString name $ c_get_var_decl_from_name ctx
+  return $ if nullPtr == ptr then Nothing else Just ptr
+
+getVarFromDecl :: Context -> VarDecl -> IO Expr
+getVarFromDecl = c_mk_var_from_decl
+
+getVar :: Context -> String -> IO (Maybe Expr)
+getVar ctx name = getVarDecl ctx name >>= T.sequence . liftM (getVarFromDecl ctx)
+
+class YEval a where getValue :: Model -> VarDecl -> YDef a
+instance YEval Bool where getValue = getBoolValue
+instance YEval Int  where getValue = getNatValue
+
+getBoolValue :: Model -> VarDecl -> YBool
+getBoolValue m vd = eatYBool $ c_get_value m vd
+
+getNatValue :: Model -> VarDecl -> YDef Int
+getNatValue m vd = unsafePerformIO $ alloca $ \ptr -> do
+                              code <- c_get_int_value m vd ptr
+                              case code of
+                                0 -> return YUndef
+                                1 -> YDef . fromIntegral <$> peek ptr
+
+evaluateInModel :: Model -> Expr -> YBool
+evaluateInModel m = eatYBool . c_evaluate_in_model m
+
+withVarIterator :: Context -> (VarIterator -> IO a) -> IO a
+withVarIterator ctx f = do
+  iter <- c_create_var_decl_iterator ctx
+  f iter <* c_del_iterator iter
+
+hasNext :: VarIterator -> IO Bool
+hasNext = liftM (toEnum . fromIntegral) . c_iterator_has_next
+
+-- * Expressions
+
+mkTrue, mkFalse :: Context -> IO Expr
+mkTrue  = c_mk_true
+mkFalse = c_mk_false
+
+mkVar :: Context -> String -> Type -> IO Expr
+mkVar ctx name typ = withCString name (\n -> c_mk_var_decl ctx n typ) >>= c_mk_var_from_decl ctx
+
+mkBoolVar :: Context -> String -> IO Expr
+mkBoolVar ctx name = withCString name $ c_mk_bool_var ctx
+
+mkNatVar  :: Context -> String -> IO Expr
+mkNatVar  ctx name = mkVar ctx name =<< mkNatType ctx
+
+mkBoolType :: Context -> IO Type
+mkBoolType ctx = mkType ctx "bool"
+mkNatType :: Context -> IO Type
+mkNatType ctx = mkType ctx "nat"
+mkType :: Context -> String -> IO Type
+mkType ctx typ =  withCString typ $ c_mk_type ctx
+
+mkFreshBoolVar :: Context -> IO Expr
+mkFreshBoolVar = c_mk_fresh_bool_var
+
+mkNot :: Context -> Expr -> IO Expr
+mkNot = c_mk_not
+
+mkAnd,mkOr :: Context -> [Expr] -> IO Expr
+mkAnd ctx ee = withArray ee $ \ee_a -> c_mk_and ctx ee_a (fromIntegral $ length ee)
+mkOr  ctx ee = withArray ee $ \ee_a -> c_mk_or  ctx ee_a (fromIntegral $ length ee)
+
+mkAnd2,mkOr2 :: Context -> Expr -> Expr -> IO Expr
+mkAnd2 ctx e1 e2 = withArray [e1,e2] $ \ee_a -> c_mk_and ctx ee_a 2
+mkOr2  ctx e1 e2 = withArray [e1,e2] $ \ee_a -> c_mk_or  ctx ee_a 2
+
+mkEq, mkDiseq :: Context -> Expr -> Expr -> IO Expr
+mkEq = c_mk_eq
+mkDiseq = c_mk_diseq
+
+mkIte :: Context -> Expr -> Expr -> Expr -> IO Expr
+mkIte = c_mk_ite
+
+mkNum :: Context -> Int -> IO Expr
+mkNum ctx = c_mk_num ctx . fromIntegral
+
+mkGt, mkLt, mkGe, mkLe :: Context -> Expr -> Expr -> IO Expr
+mkLe = c_mk_le
+mkLt = c_mk_lt
+mkGt = c_mk_gt
+mkGe = c_mk_ge
+
+-- * Types
+
+-- -------------
+-- Marshalling
+-- -------------
+
+getAllVariables :: Context -> Model -> IO [VarDecl]
+getAllVariables ctx m = withVarIterator ctx $ \iter ->
+  let go = do
+        cont <- hasNext iter
+        if cont
+          then do
+             v     <- c_iterator_next iter
+             rest  <- go
+             return (v : rest)
+
+          else return []
+  in go
+
+getBoolModel :: Context -> Model -> IO [(String, YBool)]
+getBoolModel ctx m = withVarIterator ctx $ \iter ->
+  let go = do
+        cont <- hasNext iter
+        if cont
+          then do
+             v     <- c_iterator_next iter
+             name  <- peekCString =<< c_get_var_decl_name v
+             let value = getValue m v
+             rest  <- go
+             return ((name, value) : rest)
+
+          else return []
+  in go
diff --git a/Bindings/Yices/Internal.hsc b/Bindings/Yices/Internal.hsc
new file mode 100644
--- /dev/null
+++ b/Bindings/Yices/Internal.hsc
@@ -0,0 +1,529 @@
+{-# LANGUAGE ForeignFunctionInterface #-}
+{-# LANGUAGE EmptyDataDecls #-}
+
+module Bindings.Yices.Internal where
+
+import Foreign
+import Foreign.Ptr
+import Foreign.C.Types
+import Foreign.C.String
+
+data YContext
+data YExpr
+data YDecl
+data YVarDecl
+data YType
+data YModel
+data YVarIterator
+newtype AssertionId = AssertionId Int deriving (Eq, Ord)
+data YDef a = YDef !a | YUndef
+
+
+#include "yices_c.h"
+
+-- -------------
+-- Marshalling
+-- -------------
+
+eatYBool l = case l of
+    #const l_false
+        -> YDef False
+    #const l_true
+        -> YDef True
+    #const l_undef
+        -> YUndef
+
+-- -----------
+-- Primitives
+-- -----------
+
+foreign import ccall unsafe "yices_c.h yices_set_verbosity"
+  c_set_verbosity :: CInt -> IO (())
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_version"
+  c_version :: IO (Ptr (CChar))
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_set_max_num_conflicts_in_maxsat_iteration"
+  c_set_max_num_conflicts_in_maxsat_iteration :: CUInt -> IO (())
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_enable_type_checker"
+  c_enable_type_checker :: CInt -> IO (())
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_set_max_num_iterations_in_maxsat"
+  c_set_max_num_iterations_in_maxsat :: CUInt -> IO (())
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_set_maxsat_initial_cost"
+  c_set_maxsat_initial_cost :: CLLong -> IO (())
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_set_arith_only"
+  c_set_arith_only :: CInt -> IO (())
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_enable_log_file"
+  c_enable_log_file :: Ptr (CChar) -> IO (())
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_context"
+  c_mk_context :: IO (Ptr YContext)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_del_context"
+  c_del_context :: Ptr YContext -> IO (())
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_reset"
+  c_reset :: Ptr YContext -> IO (())
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_dump_context"
+  c_dump_context :: Ptr YContext -> IO (())
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_push"
+  c_push :: Ptr YContext -> IO (())
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_pop"
+  c_pop :: Ptr YContext -> IO (())
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_assert"
+  c_assert :: Ptr YContext -> Ptr YExpr -> IO (())
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_assert_weighted"
+  c_assert_weighted :: Ptr YContext -> Ptr YExpr -> CLLong -> IO AssertionId
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_assert_retractable"
+  c_assert_retractable :: Ptr YContext -> Ptr YExpr -> IO (CInt)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_retract"
+  c_retract :: Ptr YContext -> CInt -> IO (())
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_inconsistent"
+  c_inconsistent :: Ptr YContext -> IO (CInt)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_check"
+  c_check :: Ptr YContext -> IO (CInt)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_find_weighted_model"
+  c_find_weighted_model :: Ptr YContext -> CInt -> IO (CInt)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_evaluate_in_model"
+  c_evaluate_in_model :: Ptr YModel -> Ptr YExpr -> CInt
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_max_sat"
+  c_max_sat :: Ptr YContext -> IO (CInt)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_max_sat_cost_leq"
+  c_max_sat_cost_leq :: Ptr YContext -> CLLong -> IO (CInt)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_get_model"
+  c_get_model :: Ptr YContext -> IO (Ptr YModel)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_get_unsat_core_size"
+  c_get_unsat_core_size :: Ptr YContext -> IO (CUInt)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_get_unsat_core"
+  c_get_unsat_core :: Ptr YContext -> Ptr (CInt) -> IO (CUInt)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_get_value"
+  c_get_value :: Ptr YModel -> Ptr YVarDecl -> CInt
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_get_int_value"
+  c_get_int_value :: Ptr YModel -> Ptr YVarDecl -> Ptr (CLong) -> IO CInt
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_get_arith_value"
+  c_get_arith_value :: Ptr YModel -> Ptr YVarDecl -> Ptr (CLong) -> Ptr (CLong) -> IO CInt
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_get_double_value"
+  c_get_double_value :: Ptr YModel -> Ptr YVarDecl -> Ptr (CDouble) -> IO CInt
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_get_bitvector_value"
+  c_get_bitvector_value :: Ptr YModel -> Ptr YVarDecl -> CUInt -> Ptr (CInt) -> IO CInt
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_get_assertion_value"
+  c_get_assertion_value :: Ptr YModel -> AssertionId -> CInt
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_display_model"
+  c_display_model :: Ptr YModel -> IO ()
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_get_cost"
+  c_get_cost :: Ptr YModel -> CLLong
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_get_cost_as_double"
+  c_get_cost_as_double :: Ptr YModel -> CDouble
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_true"
+  c_mk_true :: Ptr YContext -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_false"
+  c_mk_false :: Ptr YContext -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bool_var"
+  c_mk_bool_var :: Ptr YContext -> Ptr (CChar) -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_fresh_bool_var"
+  c_mk_fresh_bool_var :: Ptr YContext -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_get_var_decl"
+  c_get_var_decl :: Ptr YExpr -> IO (Ptr YVarDecl)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bool_var_decl"
+  c_mk_bool_var_decl :: Ptr YContext -> Ptr CChar -> IO (Ptr YVarDecl)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_get_var_decl_name"
+  c_get_var_decl_name :: Ptr YVarDecl -> IO (Ptr CChar)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bool_var_from_decl"
+  c_mk_bool_var_from_decl :: Ptr YContext -> Ptr YDecl -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_or"
+  c_mk_or :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_and"
+  c_mk_and :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_eq"
+  c_mk_eq :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_diseq"
+  c_mk_diseq :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_ite"
+  c_mk_ite :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_not"
+  c_mk_not :: Ptr YContext -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_create_var_decl_iterator"
+  c_create_var_decl_iterator :: Ptr YContext -> IO (Ptr YVarIterator)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_iterator_has_next"
+  c_iterator_has_next :: Ptr YVarIterator -> IO CInt
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_iterator_next"
+  c_iterator_next :: Ptr YVarIterator -> IO (Ptr YVarDecl)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_iterator_reset"
+  c_iterator_reset :: Ptr YVarIterator -> IO ()
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_del_iterator"
+  c_del_iterator :: Ptr YVarIterator -> IO ()
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_type"
+  c_mk_type :: Ptr YContext -> Ptr CChar -> IO (Ptr YType)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_function_type"
+  c_mk_function_type :: Ptr YContext -> Ptr (Ptr YType) -> CUInt -> Ptr YType -> IO (Ptr YType)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bitvector_type"
+  c_mk_bitvector_type :: Ptr YContext -> CUInt -> IO (Ptr YType)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_tuple_type"
+  c_mk_tuple_type :: Ptr YContext -> Ptr (Ptr (Ptr YType)) -> CUInt -> IO (Ptr YType)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_var_decl"
+  c_mk_var_decl :: Ptr YContext -> Ptr CChar -> Ptr YType -> IO (Ptr YVarDecl)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_get_var_decl_from_name"
+  c_get_var_decl_from_name :: Ptr YContext -> Ptr CChar -> IO (Ptr YVarDecl)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_var_from_decl"
+  c_mk_var_from_decl :: Ptr YContext -> Ptr YVarDecl -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_app"
+  c_mk_app :: Ptr YContext -> Ptr YExpr -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_num"
+  c_mk_num :: Ptr YContext -> CInt -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_num_from_string"
+  c_mk_num_from_string :: Ptr YContext -> Ptr CChar -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_sum"
+  c_mk_sum :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_sub"
+  c_mk_sub :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_mul"
+  c_mk_mul :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_lt"
+  c_mk_lt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_le"
+  c_mk_le :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_gt"
+  c_mk_gt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_ge"
+  c_mk_ge :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_constant"
+  c_mk_bv_constant :: Ptr YContext -> CUInt -> CULong -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_constant_from_array"
+  c_mk_bv_constant_from_array :: Ptr YContext -> CUInt -> Ptr (CInt) -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_add"
+  c_mk_bv_add :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_sub"
+  c_mk_bv_sub :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_mul"
+  c_mk_bv_mul :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_minus"
+  c_mk_bv_minus :: Ptr YContext -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_concat"
+  c_mk_bv_concat :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_and"
+  c_mk_bv_and :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_or"
+  c_mk_bv_or :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_xor"
+  c_mk_bv_xor :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_not"
+  c_mk_bv_not :: Ptr YContext -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_extract"
+  c_mk_bv_extract :: Ptr YContext -> CUInt -> CUInt -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_sign_extend"
+  c_mk_bv_sign_extend :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_shift_left0"
+  c_mk_bv_shift_left0 :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_shift_left1"
+  c_mk_bv_shift_left1 :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_shift_right0"
+  c_mk_bv_shift_right0 :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_shift_right1"
+  c_mk_bv_shift_right1 :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_lt"
+  c_mk_bv_lt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_le"
+  c_mk_bv_le :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_gt"
+  c_mk_bv_gt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_ge"
+  c_mk_bv_ge :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_slt"
+  c_mk_bv_slt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_sle"
+  c_mk_bv_sle :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_sgt"
+  c_mk_bv_sgt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_mk_bv_sge"
+  c_mk_bv_sge :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)
+
+--
+
+foreign import ccall unsafe "yices_c.h yices_pp_expr"
+  c_pp_expr :: Ptr YExpr -> IO ()
+
+--
+
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,3 @@
+#!/usr/bin/env runhaskell
+import Distribution.Simple
+main = defaultMain
diff --git a/bindings-yices.cabal b/bindings-yices.cabal
new file mode 100644
--- /dev/null
+++ b/bindings-yices.cabal
@@ -0,0 +1,63 @@
+-- bindings-yices.cabal auto-generated by cabal init. For additional
+-- options, see
+-- http://www.haskell.org/cabal/release/cabal-latest/doc/users-guide/authors.html#pkg-descr.
+-- The name of the package.
+Name:                bindings-yices
+
+-- The package version. See the Haskell package versioning policy
+-- (http://www.haskell.org/haskellwiki/Package_versioning_policy) for
+-- standards guiding when and how versions should be incremented.
+Version:             0.1
+
+-- A short (one-line) description of the package.
+Synopsis:            Bindings to the Yices theorem prover
+
+-- A longer description of the package.
+-- Description:         
+
+-- The license under which the package is released.
+License:             PublicDomain
+
+-- The package author(s).
+Author:              Jose Iborra
+
+-- An email address to which users can send suggestions, bug reports,
+-- and patches.
+Maintainer:          pepeiborra@gmail.com
+
+-- A copyright notice.
+-- Copyright:           
+
+-- Stability of the pakcage (experimental, provisional, stable...)
+Stability:           Experimental
+
+Category:            Foreign, FFI, Theorem Provers
+
+Build-type:          Simple
+
+-- Extra files to be distributed with the package, such as examples or
+-- a README.
+-- Extra-source-files:  
+
+-- Constraint on the version of Cabal needed to build this package.
+Cabal-version:       >=1.2
+
+
+Library
+  -- Modules exported by the library.
+  Exposed-modules:     Bindings.Yices,
+                       Bindings.Yices.Internal
+
+  extra-libraries:     yices
+  -- Packages needed in order to build this package.
+  Build-depends:       base > 3 && < 5
+  
+  -- Modules not exported by this package.
+  -- Other-modules:       
+  
+  -- Extra tools (e.g. alex, hsc2hs, ...) needed to build the source.
+  Build-tools:         hsc2hs
+
+  includes:            yices_c.h
+
+  ghc-prof-options: -auto