bindings-yices 0.1 → 0.2
raw patch · 3 files changed
+126/−113 lines, 3 files
Files
- Bindings/Yices.hs +11/−8
- Bindings/Yices/Internal.hsc +107/−103
- bindings-yices.cabal +8/−2
Bindings/Yices.hs view
@@ -48,6 +48,9 @@ isInconsistent :: Context -> IO Bool isInconsistent = liftM (toEnum.fromIntegral) . c_inconsistent +interrupt :: Context -> IO ()+interrupt = c_interrupt+ -- * Assertions assert :: Context -> Expr -> IO ()@@ -106,22 +109,22 @@ 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+class YEval a where getValue :: Model -> VarDecl -> IO (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+getBoolValue :: Model -> VarDecl -> IO YBool+getBoolValue m = liftM eatYBool . c_get_value m -getNatValue :: Model -> VarDecl -> YDef Int-getNatValue m vd = unsafePerformIO $ alloca $ \ptr -> do+getNatValue :: Model -> VarDecl -> IO (YDef Int)+getNatValue m vd = 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+evaluateInModel :: Model -> Expr -> IO YBool+evaluateInModel m = liftM eatYBool . c_evaluate_in_model m withVarIterator :: Context -> (VarIterator -> IO a) -> IO a withVarIterator ctx f = do@@ -210,7 +213,7 @@ then do v <- c_iterator_next iter name <- peekCString =<< c_get_var_decl_name v- let value = getValue m v+ value <- getValue m v rest <- go return ((name, value) : rest)
Bindings/Yices/Internal.hsc view
@@ -21,6 +21,10 @@ #include "yices_c.h" ++foreign import ccall "yices_c.h yices_interrupt"+ c_interrupt :: Ptr YContext -> IO (())+ -- ------------- -- Marshalling -- -------------@@ -37,492 +41,492 @@ -- Primitives -- ----------- -foreign import ccall unsafe "yices_c.h yices_set_verbosity"+foreign import ccall "yices_c.h yices_set_verbosity" c_set_verbosity :: CInt -> IO (()) -- -foreign import ccall unsafe "yices_c.h yices_version"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall safe "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"+foreign import ccall "yices_c.h yices_set_arith_only" c_set_arith_only :: CInt -> IO (()) -- -foreign import ccall unsafe "yices_c.h yices_enable_log_file"+foreign import ccall "yices_c.h yices_enable_log_file" c_enable_log_file :: Ptr (CChar) -> IO (()) -- -foreign import ccall unsafe "yices_c.h yices_mk_context"+foreign import ccall "yices_c.h yices_mk_context" c_mk_context :: IO (Ptr YContext) -- -foreign import ccall unsafe "yices_c.h yices_del_context"+foreign import ccall "yices_c.h yices_del_context" c_del_context :: Ptr YContext -> IO (()) -- -foreign import ccall unsafe "yices_c.h yices_reset"+foreign import ccall "yices_c.h yices_reset" c_reset :: Ptr YContext -> IO (()) -- -foreign import ccall unsafe "yices_c.h yices_dump_context"+foreign import ccall "yices_c.h yices_dump_context" c_dump_context :: Ptr YContext -> IO (()) -- -foreign import ccall unsafe "yices_c.h yices_push"+foreign import ccall "yices_c.h yices_push" c_push :: Ptr YContext -> IO (()) -- -foreign import ccall unsafe "yices_c.h yices_pop"+foreign import ccall "yices_c.h yices_pop" c_pop :: Ptr YContext -> IO (()) -- -foreign import ccall unsafe "yices_c.h yices_assert"+foreign import ccall "yices_c.h yices_assert" c_assert :: Ptr YContext -> Ptr YExpr -> IO (()) -- -foreign import ccall unsafe "yices_c.h yices_assert_weighted"+foreign import ccall "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"+foreign import ccall "yices_c.h yices_assert_retractable" c_assert_retractable :: Ptr YContext -> Ptr YExpr -> IO (CInt) -- -foreign import ccall unsafe "yices_c.h yices_retract"+foreign import ccall "yices_c.h yices_retract" c_retract :: Ptr YContext -> CInt -> IO (()) -- -foreign import ccall unsafe "yices_c.h yices_inconsistent"+foreign import ccall safe "yices_c.h yices_inconsistent" c_inconsistent :: Ptr YContext -> IO (CInt) -- -foreign import ccall unsafe "yices_c.h yices_check"+foreign import ccall safe "yices_c.h yices_check" c_check :: Ptr YContext -> IO (CInt) -- -foreign import ccall unsafe "yices_c.h yices_find_weighted_model"+foreign import ccall safe "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 "yices_c.h yices_evaluate_in_model"+ c_evaluate_in_model :: Ptr YModel -> Ptr YExpr -> IO CInt -- -foreign import ccall unsafe "yices_c.h yices_max_sat"+foreign import ccall safe "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"+foreign import ccall safe "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"+foreign import ccall safe "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"+foreign import ccall safe "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"+foreign import ccall safe "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 "yices_c.h yices_get_value"+ c_get_value :: Ptr YModel -> Ptr YVarDecl -> IO CInt -- -foreign import ccall unsafe "yices_c.h yices_get_int_value"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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 "yices_c.h yices_get_assertion_value"+ c_get_assertion_value :: Ptr YModel -> AssertionId -> IO CInt -- -foreign import ccall unsafe "yices_c.h yices_display_model"+foreign import ccall "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 "yices_c.h yices_get_cost"+ c_get_cost :: Ptr YModel -> IO CLLong -- -foreign import ccall unsafe "yices_c.h yices_get_cost_as_double"- c_get_cost_as_double :: Ptr YModel -> CDouble+foreign import ccall "yices_c.h yices_get_cost_as_double"+ c_get_cost_as_double :: Ptr YModel -> IO CDouble -- -foreign import ccall unsafe "yices_c.h yices_mk_true"+foreign import ccall "yices_c.h yices_mk_true" c_mk_true :: Ptr YContext -> IO (Ptr YExpr) -- -foreign import ccall unsafe "yices_c.h yices_mk_false"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "yices_c.h yices_iterator_next" c_iterator_next :: Ptr YVarIterator -> IO (Ptr YVarDecl) -- -foreign import ccall unsafe "yices_c.h yices_iterator_reset"+foreign import ccall "yices_c.h yices_iterator_reset" c_iterator_reset :: Ptr YVarIterator -> IO () -- -foreign import ccall unsafe "yices_c.h yices_del_iterator"+foreign import ccall "yices_c.h yices_del_iterator" c_del_iterator :: Ptr YVarIterator -> IO () -- -foreign import ccall unsafe "yices_c.h yices_mk_type"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "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"+foreign import ccall "yices_c.h yices_pp_expr" c_pp_expr :: Ptr YExpr -> IO () --
bindings-yices.cabal view
@@ -7,7 +7,7 @@ -- 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+Version: 0.2 -- A short (one-line) description of the package. Synopsis: Bindings to the Yices theorem prover@@ -42,13 +42,14 @@ -- Constraint on the version of Cabal needed to build this package. Cabal-version: >=1.2 +Flag yices-dynamic+ default: True 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 @@ -58,6 +59,11 @@ -- Extra tools (e.g. alex, hsc2hs, ...) needed to build the source. Build-tools: hsc2hs + extensions: ForeignFunctionInterface includes: yices_c.h ghc-prof-options: -auto++ extra-libraries: yices+ if flag(yices-dynamic)+ extra-libraries: gmp