diff --git a/Bindings/Yices.hs b/Bindings/Yices.hs --- a/Bindings/Yices.hs +++ b/Bindings/Yices.hs @@ -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) diff --git a/Bindings/Yices/Internal.hsc b/Bindings/Yices/Internal.hsc --- a/Bindings/Yices/Internal.hsc +++ b/Bindings/Yices/Internal.hsc @@ -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 () -- diff --git a/bindings-yices.cabal b/bindings-yices.cabal --- a/bindings-yices.cabal +++ b/bindings-yices.cabal @@ -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