bindings-yices (empty) → 0.1
raw patch · 4 files changed
+813/−0 lines, 4 filesdep +basesetup-changed
Dependencies added: base
Files
- Bindings/Yices.hs +218/−0
- Bindings/Yices/Internal.hsc +529/−0
- Setup.hs +3/−0
- bindings-yices.cabal +63/−0
+ Bindings/Yices.hs view
@@ -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
+ Bindings/Yices/Internal.hsc view
@@ -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 ()++--+
+ Setup.hs view
@@ -0,0 +1,3 @@+#!/usr/bin/env runhaskell+import Distribution.Simple+main = defaultMain
+ bindings-yices.cabal view
@@ -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