{-# LANGUAGE ForeignFunctionInterface #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} -- | -- Module : Yices.Painless.Base.C -- Copyright : (c) Galois, Inc. 2010 -- License : BSD3 -- Maintainer: Don Stewart -- -- Low level bindings to the Yices SMT solver. -- -- A native, imperative Haskell layer is provided by "Yices.Painless.Base" -- -- A very high level EDSL is provided by "Yices.Painless.Language" -- -- Direct export of the underlying C API, with some convenient newtype -- wrappers adding a small level of type safety. -- -- The C interface preserves the semantics of the underlying C API. That -- is, calls to functions prefixed with @c_@ do /no/ additional error -- checking, and only a light amount of additional type checking. -- -- This module corresponds approximately to the /Internal/ modules of -- the /bindings-yices/ package, by Jose Iborra. -- -- * -- module Yices.Painless.Base.C ( -- * C types YExpr, YModel, YContext, YType, YVarDecl, YIterator, -- ** Value types YAssertId, YWeight, YCost, -- ** Booleans YBool, yFalse, yTrue, yUndef, -- * Context manipulation c_yices_mk_context, c_yices_del_context, c_yices_reset, c_yices_push, c_yices_pop, -- ** IO c_yices_dump_context, -- * Assertions c_yices_assert, c_yices_assert_weighted, c_yices_assert_retractable, c_yices_retract, -- * Solving c_yices_inconsistent, c_yices_check, c_yices_find_weighted_model, c_yices_max_sat, c_yices_evaluate_in_model, c_yices_get_model, c_yices_get_unsat_core, -- ** Cost of a solution c_yices_get_cost, c_yices_get_cost_as_double, c_yices_max_sat_cost_leq, c_yices_get_unsat_core_size, -- ** IO c_yices_display_model, -- * Extracting variable bindings c_yices_get_value, c_yices_get_int_value, c_yices_get_arith_value, c_yices_get_double_value, c_yices_get_bitvector_value, c_yices_get_assertion_value, -- * Expressions -- ** Literals c_yices_mk_true, c_yices_mk_false, c_yices_mk_bool_var, c_yices_mk_fresh_bool_var, c_yices_mk_bool_var_decl, -- ** Numbers c_yices_mk_num, c_yices_mk_num_from_string, -- ** Equality and Comparison c_yices_mk_or, c_yices_mk_and, c_yices_mk_eq, c_yices_mk_diseq, -- ** Negation c_yices_mk_not, -- ** Implication c_yices_mk_ite, -- ** Function application c_yices_mk_app, -- ** Numerical expressions c_yices_mk_sum, c_yices_mk_sub, c_yices_mk_mul, c_yices_mk_lt, c_yices_mk_le, c_yices_mk_gt, c_yices_mk_ge, -- * Types c_yices_mk_type, c_yices_mk_function_type, c_yices_mk_bitvector_type, c_yices_mk_tuple_type, -- * Bit vectors c_yices_mk_bv_constant, c_yices_mk_bv_constant_from_array, -- ** Bit vector arithmetic c_yices_mk_bv_add, c_yices_mk_bv_sub, c_yices_mk_bv_mul, c_yices_mk_bv_minus, -- ** Bit vector /string/ operations c_yices_mk_bv_concat, c_yices_mk_bv_extract, -- ** Bitwise operations c_yices_mk_bv_and, c_yices_mk_bv_or, c_yices_mk_bv_xor, c_yices_mk_bv_not, -- ** Shifting and signs c_yices_mk_bv_sign_extend, c_yices_mk_bv_shift_left0, c_yices_mk_bv_shift_left1, c_yices_mk_bv_shift_right0, c_yices_mk_bv_shift_right1, -- ** Comparisons c_yices_mk_bv_lt, c_yices_mk_bv_le, c_yices_mk_bv_gt, c_yices_mk_bv_ge, c_yices_mk_bv_slt, c_yices_mk_bv_sle, c_yices_mk_bv_sgt, c_yices_mk_bv_sge, -- *** IO c_yices_pp_expr, -- * Iterators c_yices_create_var_decl_iterator, c_yices_iterator_has_next, c_yices_iterator_next, c_yices_iterator_reset, c_yices_del_iterator, -- * Declarations c_yices_mk_var_decl, c_yices_mk_var_from_decl, c_yices_get_var_decl_from_name, c_yices_get_var_decl, c_yices_get_var_decl_name, c_yices_mk_bool_var_from_decl, -- * System info c_yices_version, -- * Configuring Yices c_yices_set_verbosity, c_yices_enable_type_checker, c_yices_set_maxsat_initial_cost, c_yices_set_max_num_conflicts_in_maxsat_iteration, c_yices_set_max_num_iterations_in_maxsat, c_yices_set_arith_only, c_yices_enable_log_file, ) where import Foreign import Foreign.C.Types import Foreign.C.String #include "yices_c.h" ------------------------------------------------------------------------ -- Types -- | Abstract type representing a Yices expression. -- -- Reference: -- data YExpr -- | Abstract type representing a Yices model. -- -- Reference: -- data YModel -- | Abstract type representing a Yices context. -- -- Reference: -- data YContext -- | Abstract type representing a Yices types. -- -- Reference: -- data YType -- | Abstract type for variable declarations. -- -- Reference: -- data YVarDecl -- | Abstract type for variable declaration iterators. -- -- Reference: -- data YIterator -- | Low level type for assertion ids. -- -- Reference: -- type YAssertId = CInt -- | Low level type for weights. type YWeight = CLLong -- | Low level type for costs. type YCost = CLLong -- | Low level type for boolean or undefined results. type YBool = CInt yFalse, yTrue, yUndef :: YBool yFalse = #const l_false yTrue = #const l_true yUndef = #const l_undef ------------------------------------------------------------------------ -- Function bindings -- Contexts -- | Reference: foreign import ccall unsafe "yices_mk_context" c_yices_mk_context :: IO (Ptr YContext) -- | Reference: foreign import ccall unsafe "yices_del_context" c_yices_del_context :: Ptr YContext -> IO () -- | Reference: foreign import ccall unsafe "yices_reset" c_yices_reset :: Ptr YContext -> IO () -- | Reference: foreign import ccall unsafe "yices_dump_context" c_yices_dump_context :: Ptr YContext -> IO () -- | Reference: foreign import ccall unsafe "yices_push" c_yices_push :: Ptr YContext -> IO () -- | Reference: foreign import ccall unsafe "yices_pop" c_yices_pop :: Ptr YContext -> IO () -- Assertions -- | Reference: foreign import ccall unsafe "yices_assert" c_yices_assert :: Ptr YContext -> Ptr YExpr -> IO () -- | Reference: foreign import ccall unsafe "yices_assert_weighted" c_yices_assert_weighted :: Ptr YContext -> Ptr YExpr -> YWeight -> IO YAssertId -- | Reference: foreign import ccall unsafe "yices_assert_retractable" c_yices_assert_retractable :: Ptr YContext -> Ptr YExpr -> IO YAssertId -- | Reference: foreign import ccall unsafe "yices_retract" c_yices_retract :: Ptr YContext -> YAssertId -> IO () -- Solving -- | Reference: foreign import ccall unsafe "yices_inconsistent" c_yices_inconsistent :: Ptr YContext -> IO CInt -- | Reference: foreign import ccall unsafe "yices_check" c_yices_check :: Ptr YContext -> IO YBool -- | Reference: foreign import ccall unsafe "yices_find_weighted_model" c_yices_find_weighted_model :: Ptr YContext -> CInt -> IO YBool -- | Reference: foreign import ccall unsafe "yices_get_cost" c_yices_get_cost :: Ptr YModel -> IO YCost -- | Reference: foreign import ccall unsafe "yices_get_cost_as_double" c_yices_get_cost_as_double :: Ptr YModel -> IO CDouble -- Models -- | Reference: foreign import ccall unsafe "yices_display_model" c_yices_display_model :: Ptr YModel -> IO () -- | Reference: foreign import ccall unsafe "yices_evaluate_in_model" c_yices_evaluate_in_model :: Ptr YModel -> Ptr YExpr -> IO YBool -- | Reference: foreign import ccall unsafe "yices_max_sat" c_yices_max_sat :: Ptr YContext -> IO YBool -- | Reference: foreign import ccall unsafe "yices_max_sat_cost_leq" c_yices_max_sat_cost_leq :: Ptr YContext -> YCost -> IO YBool -- | Reference: foreign import ccall unsafe "yices_get_model" c_yices_get_model :: Ptr YContext -> IO (Ptr YModel) -- Querying the result -- | Reference: foreign import ccall unsafe "yices_get_unsat_core_size" c_yices_get_unsat_core_size :: Ptr YContext -> IO CUInt -- | Reference: foreign import ccall unsafe "yices_get_unsat_core" c_yices_get_unsat_core :: Ptr YContext -> Ptr YAssertId -> IO CUInt -- Extracting bindings -- | Reference: foreign import ccall unsafe "yices_get_value" c_yices_get_value :: Ptr YModel -> Ptr YVarDecl -> IO YBool -- | Reference: foreign import ccall unsafe "yices_get_int_value" c_yices_get_int_value :: Ptr YModel -> Ptr YVarDecl -> Ptr CLong -> IO CInt -- | Reference: foreign import ccall unsafe "yices_get_arith_value" c_yices_get_arith_value :: Ptr YModel -> Ptr YVarDecl -> Ptr CLong -> Ptr CLong -> IO CInt -- | Reference: foreign import ccall unsafe "yices_get_double_value" c_yices_get_double_value :: Ptr YModel -> Ptr YVarDecl -> Ptr CDouble -> IO CInt {- -- TODO Integers can be supported, via low level casting to mpq values and back. -- Look at primitives in integer-gmp for ideas. -- Might be possible to allocate new primitive ByteArray#'s, pin, then copy mpq_t's in. -- Convert the value assigned to variable v in model m to a GMP rational (mpq_t). int yices_get_mpq_value ( yices_model m, yices_var_decl d, mpq_t value ) -- Convert the value assigned to variable v in model m to a GMP integer (mpz_t). int yices_get_mpz_value ( yices_model m, yices_var_decl d, mpz_t value ) -} -- | Reference: foreign import ccall unsafe "yices_get_bitvector_value" c_yices_get_bitvector_value :: Ptr YModel -> Ptr YVarDecl -> CUInt -> Ptr CInt -> IO CInt -- | Reference: foreign import ccall unsafe "yices_get_assertion_value" c_yices_get_assertion_value :: Ptr YModel -> YAssertId -> IO CInt -- Constructing values -- | Reference: foreign import ccall unsafe "yices_mk_true" c_yices_mk_true :: Ptr YContext -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_false" c_yices_mk_false :: Ptr YContext -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bool_var" c_yices_mk_bool_var :: Ptr YContext -> CString -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_fresh_bool_var" c_yices_mk_fresh_bool_var :: Ptr YContext -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bool_var_decl" c_yices_mk_bool_var_decl :: Ptr YContext -> CString -> IO (Ptr YVarDecl) -- | Reference: foreign import ccall unsafe "yices_get_var_decl_name" c_yices_get_var_decl_name :: Ptr YVarDecl -> IO CString -- | Reference: foreign import ccall unsafe "yices_mk_bool_var_from_decl" c_yices_mk_bool_var_from_decl :: Ptr YContext -> Ptr YVarDecl -> IO (Ptr YExpr) -- Logical operations -- | Reference: foreign import ccall unsafe "yices_mk_or" c_yices_mk_or :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_and" c_yices_mk_and :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_eq" c_yices_mk_eq :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_diseq" c_yices_mk_diseq :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_ite" c_yices_mk_ite :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_not" c_yices_mk_not :: Ptr YContext -> Ptr YExpr -> IO (Ptr YExpr) -- Types -- | Reference: foreign import ccall unsafe "yices_mk_type" c_yices_mk_type :: Ptr YContext -> CString -> IO (Ptr YType) -- | Reference: foreign import ccall unsafe "yices_mk_function_type" c_yices_mk_function_type :: Ptr YContext -> Ptr (Ptr YType) -> CUInt -> Ptr YType -> IO (Ptr YType) -- | Reference: foreign import ccall unsafe "yices_mk_bitvector_type" c_yices_mk_bitvector_type :: Ptr YContext -> CUInt -> IO (Ptr YType) -- | Reference: foreign import ccall unsafe "yices_mk_tuple_type" c_yices_mk_tuple_type :: Ptr YContext -> Ptr (Ptr (Ptr YType)) -> CUInt -> IO (Ptr YType) -- | Reference: foreign import ccall unsafe "yices_mk_var_decl" c_yices_mk_var_decl :: Ptr YContext -> CString -> Ptr YType -> IO (Ptr YVarDecl) -- | Reference: foreign import ccall unsafe "yices_get_var_decl_from_name" c_yices_get_var_decl_from_name :: Ptr YContext -> CString -> IO (Ptr YVarDecl) -- | Reference: foreign import ccall unsafe "yices_mk_var_from_decl" c_yices_mk_var_from_decl :: Ptr YContext -> Ptr YVarDecl -> IO (Ptr YExpr) -- Application -- | Reference: foreign import ccall unsafe "yices_mk_app" c_yices_mk_app :: Ptr YContext -> Ptr YExpr -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr) -- Numbers -- | Reference: foreign import ccall unsafe "yices_mk_num" c_yices_mk_num :: Ptr YContext -> CInt -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_num_from_string" c_yices_mk_num_from_string :: Ptr YContext -> CString -> IO (Ptr YExpr) {- TODO: yices_expr yices_mk_num_from_mpz (yices_context ctx, const mpz_t z) Construct a numerical expression form a GMP integer. yices_expr yices_mk_num_from_mpq (yices_context ctx, const mpq_t q) Construct a numerical expression form a GMP rational. -} -- Expressions -- | Reference: foreign import ccall unsafe "yices_mk_sum" c_yices_mk_sum :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_sub" c_yices_mk_sub :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_mul" c_yices_mk_mul :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_lt" c_yices_mk_lt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_le" c_yices_mk_le :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_gt" c_yices_mk_gt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_ge" c_yices_mk_ge :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- Operations on bit vectors -- | Reference: foreign import ccall unsafe "yices_mk_bv_constant" c_yices_mk_bv_constant :: Ptr YContext -> CUInt -> CULong -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_constant_from_array" c_yices_mk_bv_constant_from_array :: Ptr YContext -> CUInt -> Ptr CInt -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_add" c_yices_mk_bv_add :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_sub" c_yices_mk_bv_sub :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_mul" c_yices_mk_bv_mul :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_minus" c_yices_mk_bv_minus :: Ptr YContext -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_concat" c_yices_mk_bv_concat :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_and" c_yices_mk_bv_and :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_or" c_yices_mk_bv_or :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_xor" c_yices_mk_bv_xor :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_not" c_yices_mk_bv_not :: Ptr YContext -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_extract" c_yices_mk_bv_extract :: Ptr YContext -> CUInt -> CUInt -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_sign_extend" c_yices_mk_bv_sign_extend :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_shift_left0" c_yices_mk_bv_shift_left0 :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_shift_left1" c_yices_mk_bv_shift_left1 :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_shift_right0" c_yices_mk_bv_shift_right0 :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_shift_right1" c_yices_mk_bv_shift_right1 :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_lt" c_yices_mk_bv_lt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_le" c_yices_mk_bv_le :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_gt" c_yices_mk_bv_gt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_ge" c_yices_mk_bv_ge :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_slt" c_yices_mk_bv_slt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_sle" c_yices_mk_bv_sle :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_sgt" c_yices_mk_bv_sgt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_mk_bv_sge" c_yices_mk_bv_sge :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr) -- | Reference: foreign import ccall unsafe "yices_pp_expr" c_yices_pp_expr :: Ptr YExpr -> IO () -- Iterators -- | Reference: foreign import ccall unsafe "yices_create_var_decl_iterator" c_yices_create_var_decl_iterator :: Ptr YContext -> IO (Ptr YIterator) -- | Reference: foreign import ccall unsafe "yices_iterator_has_next" c_yices_iterator_has_next :: Ptr YIterator -> IO CInt -- | Reference: foreign import ccall unsafe "yices_iterator_next" c_yices_iterator_next :: Ptr YIterator -> IO (Ptr YVarDecl) -- | Reference: foreign import ccall unsafe "yices_iterator_reset" c_yices_iterator_reset :: Ptr YIterator -> IO () -- | Reference: foreign import ccall unsafe "yices_del_iterator" c_yices_del_iterator :: Ptr YIterator -> IO () -- Accessing declarations -- | Reference: foreign import ccall unsafe "yices_get_var_decl" c_yices_get_var_decl :: Ptr YExpr -> IO (Ptr YVarDecl) -- System information -- | Reference: foreign import ccall unsafe "yices_version" c_yices_version :: CString -- System configuration -- | Reference: foreign import ccall unsafe "yices yices_set_verbosity" c_yices_set_verbosity :: CInt -> IO () -- | Reference: foreign import ccall unsafe "yices_set_maxsat_initial_cost" c_yices_set_maxsat_initial_cost :: CLLong -> IO () -- | Reference: foreign import ccall unsafe "yices_set_max_num_conflicts_in_maxsat_iteration" c_yices_set_max_num_conflicts_in_maxsat_iteration :: CUInt -> IO () -- | Reference: foreign import ccall unsafe "yices_enable_type_checker" c_yices_enable_type_checker :: CInt -> IO () -- | Reference: foreign import ccall unsafe "yices_set_max_num_iterations_in_maxsat" c_yices_set_max_num_iterations_in_maxsat :: CUInt -> IO () -- | Reference: foreign import ccall unsafe "yices_set_arith_only" c_yices_set_arith_only :: CInt -> IO () -- | Reference: foreign import ccall unsafe "yices_enable_log_file" c_yices_enable_log_file :: CString -> IO ()