C.hsc

{-# LANGUAGE ForeignFunctionInterface   #-}
{-# LANGUAGE EmptyDataDecls             #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

-- |
-- Module    : Yices.Painless.Base.C
-- Copyright : (c) Galois, Inc. 2010
-- License   : BSD3
-- Maintainer: Don Stewart <dons@galois.com>
--
-- 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.
--
-- * <http://hackage.haskell.org/package/bindings-yices>
--
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: <http://yices.csl.sri.com/capi.shtml#ga0>
--
data YExpr

-- | Abstract type representing a Yices model.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga5>
--
data YModel

-- | Abstract type representing a Yices context.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga3>
--
data YContext

-- | Abstract type representing a Yices types.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga1>
--
data YType

-- | Abstract type for variable declarations.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga2>
--
data YVarDecl

-- | Abstract type for variable declaration iterators.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga6>
--
data YIterator

-- | Low level type for assertion ids.
--
-- Reference: <http://yices.csl.sri.com/capi.shtml#ga4>
--
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: <http://yices.csl.sri.com/capi.shtml#ga15>
foreign import ccall unsafe "yices_mk_context"
    c_yices_mk_context  :: IO (Ptr YContext)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga16>
foreign import ccall unsafe "yices_del_context"
    c_yices_del_context :: Ptr YContext -> IO ()

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga17>
foreign import ccall unsafe "yices_reset"
    c_yices_reset :: Ptr YContext -> IO ()

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga18>
foreign import ccall unsafe "yices_dump_context"
    c_yices_dump_context :: Ptr YContext -> IO ()

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga19>
foreign import ccall unsafe "yices_push"
    c_yices_push :: Ptr YContext -> IO ()

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga20>
foreign import ccall unsafe "yices_pop"
    c_yices_pop :: Ptr YContext -> IO ()

-- Assertions

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga21>
foreign import ccall unsafe "yices_assert"
    c_yices_assert :: Ptr YContext -> Ptr YExpr -> IO ()

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga22>
foreign import ccall unsafe "yices_assert_weighted"
    c_yices_assert_weighted :: Ptr YContext -> Ptr YExpr -> YWeight -> IO YAssertId

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga23>
foreign import ccall unsafe "yices_assert_retractable"
    c_yices_assert_retractable :: Ptr YContext -> Ptr YExpr -> IO YAssertId

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga24>
foreign import ccall unsafe "yices_retract"
    c_yices_retract :: Ptr YContext -> YAssertId -> IO ()

-- Solving

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga25>
foreign import ccall unsafe "yices_inconsistent"
    c_yices_inconsistent :: Ptr YContext -> IO CInt

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga26>
foreign import ccall unsafe "yices_check"
    c_yices_check :: Ptr YContext -> IO YBool

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga27>
foreign import ccall unsafe "yices_find_weighted_model"
    c_yices_find_weighted_model :: Ptr YContext -> CInt -> IO YBool

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga41>
foreign import ccall unsafe "yices_get_cost"
    c_yices_get_cost :: Ptr YModel -> IO YCost

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga42>
foreign import ccall unsafe "yices_get_cost_as_double"
    c_yices_get_cost_as_double :: Ptr YModel -> IO CDouble

-- Models

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga40>
foreign import ccall unsafe "yices_display_model"
    c_yices_display_model :: Ptr YModel -> IO ()

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga28>
foreign import ccall unsafe "yices_evaluate_in_model"
    c_yices_evaluate_in_model :: Ptr YModel -> Ptr YExpr -> IO YBool

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga29>
foreign import ccall unsafe "yices_max_sat"
    c_yices_max_sat :: Ptr YContext -> IO YBool

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga30>
foreign import ccall unsafe "yices_max_sat_cost_leq"
    c_yices_max_sat_cost_leq :: Ptr YContext -> YCost -> IO YBool

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga31>
foreign import ccall unsafe "yices_get_model"
    c_yices_get_model :: Ptr YContext -> IO (Ptr YModel)

-- Querying the result

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga110>
foreign import ccall unsafe "yices_get_unsat_core_size"
    c_yices_get_unsat_core_size :: Ptr YContext -> IO CUInt

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga111>
foreign import ccall unsafe "yices_get_unsat_core"
    c_yices_get_unsat_core :: Ptr YContext -> Ptr YAssertId  -> IO CUInt

-- Extracting bindings

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga32>
foreign import ccall unsafe "yices_get_value"
    c_yices_get_value :: Ptr YModel -> Ptr YVarDecl -> IO YBool

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga33>
foreign import ccall unsafe "yices_get_int_value"
    c_yices_get_int_value :: Ptr YModel -> Ptr YVarDecl -> Ptr CLong -> IO CInt

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga34>
foreign import ccall unsafe "yices_get_arith_value"
    c_yices_get_arith_value :: Ptr YModel -> Ptr YVarDecl -> Ptr CLong -> Ptr CLong -> IO CInt

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga35>
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: <http://yices.csl.sri.com/capi.shtml#ga38>
foreign import ccall unsafe "yices_get_bitvector_value"
    c_yices_get_bitvector_value :: Ptr YModel -> Ptr YVarDecl -> CUInt -> Ptr CInt -> IO CInt

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga39>
foreign import ccall unsafe "yices_get_assertion_value"
    c_yices_get_assertion_value :: Ptr YModel -> YAssertId -> IO CInt

-- Constructing values

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga43>
foreign import ccall unsafe "yices_mk_true"
    c_yices_mk_true :: Ptr YContext -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga44>
foreign import ccall unsafe "yices_mk_false"
    c_yices_mk_false :: Ptr YContext -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga45>
foreign import ccall unsafe "yices_mk_bool_var"
    c_yices_mk_bool_var :: Ptr YContext -> CString -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga46>
foreign import ccall unsafe "yices_mk_fresh_bool_var"
    c_yices_mk_fresh_bool_var :: Ptr YContext -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga48>
foreign import ccall unsafe "yices_mk_bool_var_decl"
    c_yices_mk_bool_var_decl :: Ptr YContext -> CString -> IO (Ptr YVarDecl)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga49>
foreign import ccall unsafe "yices_get_var_decl_name"
    c_yices_get_var_decl_name :: Ptr YVarDecl -> IO CString

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga50>
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: <http://yices.csl.sri.com/capi.shtml#ga51>
foreign import ccall unsafe "yices_mk_or"
    c_yices_mk_or :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga52>
foreign import ccall unsafe "yices_mk_and"
    c_yices_mk_and :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga53>
foreign import ccall unsafe "yices_mk_eq"
    c_yices_mk_eq :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga54>
foreign import ccall unsafe "yices_mk_diseq"
    c_yices_mk_diseq :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga55>
foreign import ccall unsafe "yices_mk_ite"
    c_yices_mk_ite :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga56>
foreign import ccall unsafe "yices_mk_not"
    c_yices_mk_not :: Ptr YContext -> Ptr YExpr -> IO (Ptr YExpr)

-- Types

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga62>
foreign import ccall unsafe "yices_mk_type"
    c_yices_mk_type :: Ptr YContext -> CString -> IO (Ptr YType)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga63>
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: <http://yices.csl.sri.com/capi.shtml#ga64>
foreign import ccall unsafe "yices_mk_bitvector_type"
    c_yices_mk_bitvector_type :: Ptr YContext -> CUInt -> IO (Ptr YType)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga65>
foreign import ccall unsafe "yices_mk_tuple_type"
    c_yices_mk_tuple_type :: Ptr YContext -> Ptr (Ptr (Ptr YType)) -> CUInt -> IO (Ptr YType)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga66>
foreign import ccall unsafe "yices_mk_var_decl"
    c_yices_mk_var_decl :: Ptr YContext -> CString -> Ptr YType -> IO (Ptr YVarDecl)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga67>
foreign import ccall unsafe "yices_get_var_decl_from_name"
    c_yices_get_var_decl_from_name :: Ptr YContext -> CString -> IO (Ptr YVarDecl)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga68>
foreign import ccall unsafe "yices_mk_var_from_decl"
    c_yices_mk_var_from_decl :: Ptr YContext -> Ptr YVarDecl -> IO (Ptr YExpr)

-- Application 

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga69>
foreign import ccall unsafe "yices_mk_app"
    c_yices_mk_app :: Ptr YContext -> Ptr YExpr -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr)

-- Numbers

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga70>
foreign import ccall unsafe "yices_mk_num"
    c_yices_mk_num :: Ptr YContext -> CInt -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga71>
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: <http://yices.csl.sri.com/capi.shtml#ga74>
foreign import ccall unsafe "yices_mk_sum"
    c_yices_mk_sum :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga75>
foreign import ccall unsafe "yices_mk_sub"
    c_yices_mk_sub :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga76>
foreign import ccall unsafe "yices_mk_mul"
    c_yices_mk_mul :: Ptr YContext -> Ptr (Ptr YExpr) -> CUInt -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga77>
foreign import ccall unsafe "yices_mk_lt"
    c_yices_mk_lt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga78>
foreign import ccall unsafe "yices_mk_le"
    c_yices_mk_le :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga79>
foreign import ccall unsafe "yices_mk_gt"
    c_yices_mk_gt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga80>
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: <http://yices.csl.sri.com/capi.shtml#ga81>
foreign import ccall unsafe "yices_mk_bv_constant"
    c_yices_mk_bv_constant :: Ptr YContext -> CUInt -> CULong -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga82>
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: <http://yices.csl.sri.com/capi.shtml#ga83>
foreign import ccall unsafe "yices_mk_bv_add"
    c_yices_mk_bv_add :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga84>
foreign import ccall unsafe "yices_mk_bv_sub"
    c_yices_mk_bv_sub :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga85>
foreign import ccall unsafe "yices_mk_bv_mul"
    c_yices_mk_bv_mul :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga86>
foreign import ccall unsafe "yices_mk_bv_minus"
    c_yices_mk_bv_minus :: Ptr YContext -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga87>
foreign import ccall unsafe "yices_mk_bv_concat"
    c_yices_mk_bv_concat :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga88>
foreign import ccall unsafe "yices_mk_bv_and"
    c_yices_mk_bv_and :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga89>
foreign import ccall unsafe "yices_mk_bv_or"
    c_yices_mk_bv_or :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga90>
foreign import ccall unsafe "yices_mk_bv_xor"
    c_yices_mk_bv_xor :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga91>
foreign import ccall unsafe "yices_mk_bv_not"
    c_yices_mk_bv_not :: Ptr YContext -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga92>
foreign import ccall unsafe "yices_mk_bv_extract"
    c_yices_mk_bv_extract :: Ptr YContext -> CUInt -> CUInt -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga93>
foreign import ccall unsafe "yices_mk_bv_sign_extend"
    c_yices_mk_bv_sign_extend :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga94>
foreign import ccall unsafe "yices_mk_bv_shift_left0"
    c_yices_mk_bv_shift_left0 :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga95>
foreign import ccall unsafe "yices_mk_bv_shift_left1"
    c_yices_mk_bv_shift_left1 :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga96>
foreign import ccall unsafe "yices_mk_bv_shift_right0"
    c_yices_mk_bv_shift_right0 :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga97>
foreign import ccall unsafe "yices_mk_bv_shift_right1"
    c_yices_mk_bv_shift_right1 :: Ptr YContext -> Ptr YExpr -> CUInt -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga98>
foreign import ccall unsafe "yices_mk_bv_lt"
    c_yices_mk_bv_lt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga99>
foreign import ccall unsafe "yices_mk_bv_le"
    c_yices_mk_bv_le :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga100>
foreign import ccall unsafe "yices_mk_bv_gt"
    c_yices_mk_bv_gt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga101>
foreign import ccall unsafe "yices_mk_bv_ge"
    c_yices_mk_bv_ge :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga102>
foreign import ccall unsafe "yices_mk_bv_slt"
    c_yices_mk_bv_slt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga103>
foreign import ccall unsafe "yices_mk_bv_sle"
    c_yices_mk_bv_sle :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga104>
foreign import ccall unsafe "yices_mk_bv_sgt"
    c_yices_mk_bv_sgt :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga105>
foreign import ccall unsafe "yices_mk_bv_sge"
    c_yices_mk_bv_sge :: Ptr YContext -> Ptr YExpr -> Ptr YExpr -> IO (Ptr YExpr)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga106>
foreign import ccall unsafe "yices_pp_expr"
    c_yices_pp_expr :: Ptr YExpr -> IO ()

-- Iterators

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga57>
foreign import ccall unsafe "yices_create_var_decl_iterator"
    c_yices_create_var_decl_iterator :: Ptr YContext -> IO (Ptr YIterator)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga58>
foreign import ccall unsafe "yices_iterator_has_next"
    c_yices_iterator_has_next :: Ptr YIterator -> IO CInt

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga59>
foreign import ccall unsafe "yices_iterator_next"
    c_yices_iterator_next :: Ptr YIterator -> IO (Ptr YVarDecl)

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga60>
foreign import ccall unsafe "yices_iterator_reset"
    c_yices_iterator_reset :: Ptr YIterator -> IO ()

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga61>
foreign import ccall unsafe "yices_del_iterator"
    c_yices_del_iterator :: Ptr YIterator -> IO ()

-- Accessing declarations

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga47>
foreign import ccall unsafe "yices_get_var_decl"
    c_yices_get_var_decl :: Ptr YExpr -> IO (Ptr YVarDecl)

-- System information

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga8>
foreign import ccall unsafe "yices_version"
    c_yices_version :: CString

-- System configuration

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga7>
foreign import ccall unsafe "yices yices_set_verbosity"
    c_yices_set_verbosity :: CInt -> IO ()

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga12>
foreign import ccall unsafe "yices_set_maxsat_initial_cost"
    c_yices_set_maxsat_initial_cost :: CLLong -> IO ()

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga9>
foreign import ccall unsafe "yices_set_max_num_conflicts_in_maxsat_iteration"
    c_yices_set_max_num_conflicts_in_maxsat_iteration :: CUInt -> IO ()

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga10>
foreign import ccall unsafe "yices_enable_type_checker"
    c_yices_enable_type_checker :: CInt -> IO ()

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga11>
foreign import ccall unsafe "yices_set_max_num_iterations_in_maxsat"
    c_yices_set_max_num_iterations_in_maxsat :: CUInt -> IO ()

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga13>
foreign import ccall unsafe "yices_set_arith_only"
    c_yices_set_arith_only :: CInt -> IO ()

-- | Reference: <http://yices.csl.sri.com/capi.shtml#ga14>
foreign import ccall unsafe "yices_enable_log_file"
    c_yices_enable_log_file :: CString -> IO ()