-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Bindings for the Z3 Theorem Prover
--
-- Bindings for the Z3 4.x Theorem Prover
-- (https://github.com/Z3Prover/z3).
--
--
-- - Z3.Base.C provides the raw foreign imports from Z3's C
-- API.
-- - Z3.Base does the marshaling of values between Haskell and
-- C, and transparently handles reference counting of Z3 objects for
-- you.
-- - Z3.Monad provides a convenient monadic wrapper for the
-- common usage scenario.
--
--
-- Examples:
-- https://github.com/IagoAbal/haskell-z3/tree/master/examples
--
-- Changelog:
-- https://github.com/IagoAbal/haskell-z3/blob/master/CHANGES.md
--
-- Installation:
--
--
-- - Unix-like: Just be sure to use the standard locations for
-- dynamic libraries (/usr/lib) and header files (/usr/include), or else
-- use the --extra-lib-dirs and --extra-include-dirs Cabal flags.
--
--
-- (Hackage reports a build failure because Z3's library is missing.)
@package z3
@version 4.3
-- | Z3 API foreign imports.
module Z3.Base.C
data Z3_config
data Z3_context
data Z3_symbol
data Z3_ast
data Z3_sort
data Z3_func_decl
data Z3_app
data Z3_pattern
data Z3_constructor
data Z3_constructor_list
data Z3_model
data Z3_goal
data Z3_tactic
data Z3_apply_result
data Z3_func_interp
data Z3_func_entry
data Z3_fixedpoint
data Z3_solver
data Z3_params
data Z3_ast_vector
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga6c2de6ea89b244e37c3ffb17a9ea2a89
newtype Z3_lbool
Z3_lbool :: CInt -> Z3_lbool
z3_l_true :: Z3_lbool
z3_l_false :: Z3_lbool
z3_l_undef :: Z3_lbool
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga3a65ded0ada3ee285865759a21140eeb
newtype Z3_bool
Z3_bool :: CInt -> Z3_bool
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga311274c8a65a5d25cf715ebdf0c68747
type Z3_error_handler = Ptr Z3_context -> Z3_error_code -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gad86c8730a2e4e61bac585b240a6288d4
z3_true :: Z3_bool
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga1d9cee57472b2c7623642f123b8f1781
z3_false :: Z3_bool
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga49f047b93b0282e686956678da5b86b1
type Z3_string = CString
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga0112dc1e8e08a19bf7a4299bb09a9727
type Z3_ast_print_mode = CInt
z3_print_smtlib_full :: Z3_ast_print_mode
z3_print_low_level :: Z3_ast_print_mode
z3_print_smtlib2_compliant :: Z3_ast_print_mode
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaa9f9e7b1b5b81381fab96debbaaa638f
type Z3_error_code = CInt
z3_ok :: Z3_error_code
z3_sort_error :: Z3_error_code
z3_iob :: Z3_error_code
z3_invalid_arg :: Z3_error_code
z3_parser_error :: Z3_error_code
z3_no_parser :: Z3_error_code
z3_invalid_pattern :: Z3_error_code
z3_memout_fail :: Z3_error_code
z3_file_access_error :: Z3_error_code
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga4cd6ad05aba48f4b679f0c13310ed2a4
type Z3_sort_kind = CInt
z3_uninterpreted_sort :: Z3_sort_kind
z3_internal_fatal :: Z3_error_code
z3_bool_sort :: Z3_sort_kind
z3_invalid_usage :: Z3_error_code
z3_int_sort :: Z3_sort_kind
z3_dec_ref_error :: Z3_error_code
z3_real_sort :: Z3_sort_kind
z3_exception :: Z3_error_code
z3_bv_sort :: Z3_sort_kind
z3_array_sort :: Z3_sort_kind
z3_datatype_sort :: Z3_sort_kind
z3_relation_sort :: Z3_sort_kind
z3_finite_domain_sort :: Z3_sort_kind
z3_floating_point_sort :: Z3_sort_kind
z3_rounding_mode_sort :: Z3_sort_kind
z3_unknown_sort :: Z3_sort_kind
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga015148ad21a032e79a496629651dedb8
type Z3_ast_kind = CInt
z3_numeral_ast :: Z3_ast_kind
z3_app_ast :: Z3_ast_kind
z3_var_ast :: Z3_ast_kind
z3_quantifier_ast :: Z3_ast_kind
z3_sort_ast :: Z3_ast_kind
z3_func_decl_ast :: Z3_ast_kind
z3_unknown_ast :: Z3_ast_kind
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga7d6c40d9b79fe8a8851cc8540970787f
z3_mk_config :: IO (Ptr Z3_config)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga5e620acf5d55d0271097c9bb97219774
z3_del_config :: Ptr Z3_config -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga001ade87a1671fe77d7e53ed0f4f1ec3
z3_set_param_value :: Ptr Z3_config -> Z3_string -> Z3_string -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga98acd59d946eceb4f261bc50489216ee
z3_mk_context_rc :: Ptr Z3_config -> IO (Ptr Z3_context)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga556eae80ed43ab13e1e7dc3b38c35200
z3_del_context :: Ptr Z3_context -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga4a11514494fbf3467b89f0a80ac81e7a
z3_inc_ref :: Ptr Z3_context -> Ptr Z3_ast -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga9cd52225142c085630495044acc68bd2
z3_dec_ref :: Ptr Z3_context -> Ptr Z3_ast -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga3df806baf6124df3e63a58cf23e12411
z3_mk_int_symbol :: Ptr Z3_context -> CInt -> IO (Ptr Z3_symbol)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae
z3_mk_string_symbol :: Ptr Z3_context -> Z3_string -> IO (Ptr Z3_symbol)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga57c27f2c4e9eccf17072a84c6cecb1db
z3_sort_to_ast :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga736e88741af1c178cbebf94c49aa42de
z3_mk_uninterpreted_sort :: Ptr Z3_context -> Ptr Z3_symbol -> IO (Ptr Z3_sort)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gacdc73510b69a010b71793d429015f342
z3_mk_bool_sort :: Ptr Z3_context -> IO (Ptr Z3_sort)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015
z3_mk_int_sort :: Ptr Z3_context -> IO (Ptr Z3_sort)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0
z3_mk_real_sort :: Ptr Z3_context -> IO (Ptr Z3_sort)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaeed000a1bbb84b6ca6fdaac6cf0c1688
z3_mk_bv_sort :: Ptr Z3_context -> CUInt -> IO (Ptr Z3_sort)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gafe617994cce1b516f46128e448c84445
z3_mk_array_sort :: Ptr Z3_context -> Ptr Z3_sort -> Ptr Z3_sort -> IO (Ptr Z3_sort)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga7156b9c0a76a28fae46c81f8e3cdf0f1
z3_mk_tuple_sort :: Ptr Z3_context -> Ptr Z3_symbol -> CUInt -> Ptr (Ptr Z3_symbol) -> Ptr (Ptr Z3_sort) -> Ptr (Ptr Z3_func_decl) -> Ptr (Ptr Z3_func_decl) -> IO (Ptr Z3_sort)
-- | Reference
-- http://z3prover.github.io/api/html/group__capi.html#gaa779e39f7050b9d51857887954b5f9b0
z3_mk_constructor :: Ptr Z3_context -> Ptr Z3_symbol -> Ptr Z3_symbol -> CUInt -> Ptr (Ptr Z3_symbol) -> Ptr (Ptr Z3_sort) -> Ptr CUInt -> IO (Ptr Z3_constructor)
-- | Reference
-- http://z3prover.github.io/api/html/group__capi.html#ga63816efdbce93734c72f395b6a6a9e35
z3_del_constructor :: Ptr Z3_context -> Ptr Z3_constructor -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gab6809d53327d807da9158abdf75df387
z3_mk_datatype :: Ptr Z3_context -> Ptr Z3_symbol -> CUInt -> Ptr (Ptr Z3_constructor) -> IO (Ptr Z3_sort)
-- | Reference
-- http://z3prover.github.io/api/html/group__capi.html#gac9305d5d4eb1ce68d17300f5af19fafd
z3_mk_constructor_list :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_constructor) -> IO (Ptr Z3_constructor_list)
-- | Reference
-- http://z3prover.github.io/api/html/group__capi.html#gaa7a2e823e23fdfba407ea5088c8d1709
z3_del_constructor_list :: Ptr Z3_context -> Ptr (Z3_constructor_list) -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gac9305d5d4eb1ce68d17300f5af19fafd
z3_mk_datatypes :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_symbol) -> Ptr (Ptr Z3_sort) -> Ptr (Ptr Z3_constructor_list) -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga6865879523e7e882d7e50a2d8445ac8b
z3_mk_set_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaa5c5e2602a44d5f1373f077434859ca2
z3_mk_func_decl :: Ptr Z3_context -> Ptr Z3_symbol -> CUInt -> Ptr (Ptr Z3_sort) -> Ptr Z3_sort -> IO (Ptr Z3_func_decl)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga33a202d86bf628bfab9b6f437536cebe
z3_mk_app :: Ptr Z3_context -> Ptr Z3_func_decl -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga093c9703393f33ae282ec5e8729354ef
z3_mk_const :: Ptr Z3_context -> Ptr Z3_symbol -> Ptr Z3_sort -> IO (Ptr Z3_ast)
z3_mk_fresh_const :: Ptr Z3_context -> Z3_string -> Ptr Z3_sort -> IO (Ptr Z3_ast)
z3_mk_fresh_func_decl :: Ptr z3_context -> Z3_string -> CUInt -> Ptr (Ptr Z3_sort) -> Ptr Z3_sort -> IO (Ptr Z3_func_decl)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7
z3_mk_true :: Ptr Z3_context -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga5952ac17671117a02001fed6575c778d
z3_mk_false :: Ptr Z3_context -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga95a19ce675b70e22bb0401f7137af37c
z3_mk_eq :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaa076d3a668e0ec97d61744403153ecf7
z3_mk_distinct :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga3329538091996eb7b3dc677760a61072
z3_mk_not :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547
z3_mk_ite :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga930a8e844d345fbebc498ac43a696042
z3_mk_iff :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gac829c0e25bbbd30343bf073f7b524517
z3_mk_implies :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec
z3_mk_xor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gacde98ce4a8ed1dde50b9669db4838c61
z3_mk_and :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga00866d16331d505620a6c515302021f9
z3_mk_or :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5
z3_mk_add :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gab9affbf8401a18eea474b59ad4adc890
z3_mk_mul :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9
z3_mk_sub :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gadcd2929ad732937e25f34277ce4988ea
z3_mk_unary_minus :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3
z3_mk_div :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713
z3_mk_mod :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff
z3_mk_rem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534
z3_mk_lt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bf
z3_mk_le :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga46167b86067586bb742c0557d7babfd3
z3_mk_gt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gad9245cbadb80b192323d01a8360fb942
z3_mk_ge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21
z3_mk_int2real :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga759b6563ba1204aae55289009a3fdc6d
z3_mk_real2int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3
z3_mk_is_int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga36cf75c92c54c1ca633a230344f23080
z3_mk_bvnot :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaccc04f2b58903279b1b3be589b00a7d8
z3_mk_bvredand :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gafd18e127c0586abf47ad9cd96895f7d2
z3_mk_bvredor :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gab96e0ea55334cbcd5a0e79323b57615d
z3_mk_bvand :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga77a6ae233fb3371d187c6d559b2843f5
z3_mk_bvor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga0a3821ea00b1c762205f73e4bc29e7d8
z3_mk_bvxor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga96dc37d36efd658fff5b2b4df49b0e61
z3_mk_bvnand :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gabf15059e9e8a2eafe4929fdfd259aadb
z3_mk_bvnor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga784f5ca36a4b03b93c67242cc94b21d6
z3_mk_bvxnor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- <http://z3prover.github.io/api/html/group__capi.html#ga0c78be00c03eda4ed6a983224ed5c7b7
z3_mk_bvneg :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga819814e33573f3f9948b32fdc5311158
z3_mk_bvadd :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga688c9aa1347888c7a51be4e46c19178e
z3_mk_bvsub :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga6abd3dde2a1ceff1704cf7221a72258c
z3_mk_bvmul :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga56ce0cd61666c6f8cf5777286f590544
z3_mk_bvudiv :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gad240fedb2fda1c1005b8e9d3c7f3d5a0
z3_mk_bvsdiv :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga5df4298ec835e43ddc9e3e0bae690c8d
z3_mk_bvurem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga46c18a3042fca174fe659d3185693db1
z3_mk_bvsrem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga95dac8e6eecb50f63cb82038560e0879
z3_mk_bvsmod :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga5774b22e93abcaf9b594672af6c7c3c4
z3_mk_bvult :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga8ce08af4ed1fbdf08d4d6e63d171663a
z3_mk_bvslt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gab738b89de0410e70c089d3ac9e696e87
z3_mk_bvule :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gab7c026feb93e7d2eab180e96f1e6255d
z3_mk_bvsle :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gade58fbfcf61b67bf8c4a441490d3c4df
z3_mk_bvuge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaeec3414c0e8a90a6aa5a23af36bf6dc5
z3_mk_bvsge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga063ab9f16246c99e5c1c893613927ee3
z3_mk_bvugt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga4e93a985aa2a7812c7c11a2c65d7c5f0
z3_mk_bvsgt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gae774128fa5e9ff7458a36bd10e6ca0fa
z3_mk_concat :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga32d2fe7563f3e6b114c1b97b205d4317
z3_mk_extract :: Ptr Z3_context -> CUInt -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gad29099270b36d0680bb54b560353c10e
z3_mk_sign_ext :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gac9322fae11365a78640baf9078c428b3
z3_mk_zero_ext :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga03e81721502ea225c264d1f556c9119d
z3_mk_repeat :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gac8d5e776c786c1172fa0d7dfede454e1
z3_mk_bvshl :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gac59645a6edadad79a201f417e4e0c512
z3_mk_bvlshr :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga674b580ad605ba1c2c9f9d3748be87c4
z3_mk_bvashr :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga4932b7d08fea079dd903cd857a52dcda
z3_mk_rotate_left :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga3b94e1bf87ecd1a1858af8ebc1da4a1c
z3_mk_rotate_right :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaf46f1cb80e5a56044591a76e7c89e5e7
z3_mk_ext_rotate_left :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gabb227526c592b523879083f12aab281f
z3_mk_ext_rotate_right :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga35f89eb05df43fbd9cce7200cc1f30b5
z3_mk_int2bv :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gac87b227dc3821d57258d7f53a28323d4
z3_mk_bv2int :: Ptr Z3_context -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga88f6b5ec876f05e0d7ba51e96c4b077f
z3_mk_bvadd_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga1e2b1927cf4e50000c1600d47a152947
z3_mk_bvadd_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga785f8127b87e0b42130e6d8f52167d7c
z3_mk_bvsub_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga6480850f9fa01e14aea936c88ff184c4
z3_mk_bvsub_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaa17e7b2c33dfe2abbd74d390927ae83e
z3_mk_bvsdiv_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gae9c5d72605ddcd0e76657341eaccb6c7
z3_mk_bvneg_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga86f4415719d295a2f6845c70b3aaa1df
z3_mk_bvmul_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga501ccc01d737aad3ede5699741717fda
z3_mk_bvmul_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga38f423f3683379e7f597a7fe59eccb67
z3_mk_select :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gae305a4f54b4a64f7e5973ae6ccb13593
z3_mk_store :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga84ea6f0c32b99c70033feaa8f00e8f2d
z3_mk_const_array :: Ptr Z3_context -> Ptr Z3_sort -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga9150242d9430a8c3d55d2ca3b9a4362d
z3_mk_map :: Ptr Z3_context -> Ptr Z3_func_decl -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga78e89cca82f0ab4d5f4e662e5e5fba7d
z3_mk_array_default :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga358b6b80509a567148f1c0ca9252118c
z3_mk_empty_set :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga5e92662c657374f7332aa32ce4503dd2
z3_mk_full_set :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga856c3d0e28ce720f53912c2bbdd76175
z3_mk_set_add :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga80e883f39dd3b88f9d0745c8a5b91d1d
z3_mk_set_del :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga4050162a13d539b8913200963bb4743c
z3_mk_set_union :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga8a8abff0ebe6aeeaa6c919eaa013049d
z3_mk_set_intersect :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gabb49c62f70b8198362e1a29ba6d8bde1
z3_mk_set_difference :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga5c57143c9229cdf730c5103ff696590f
z3_mk_set_complement :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gac6e516f3dce0bdd41095c6d6daf56063
z3_mk_set_member :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga139c5803af0e86464adc7cedc53e7f3a
z3_mk_set_subset :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gac8aca397e32ca33618d8024bff32948c
z3_mk_numeral :: Ptr Z3_context -> Z3_string -> Ptr Z3_sort -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gabe0bbc1e01a084a75506a62e5e6900b3
z3_mk_real :: Ptr Z3_context -> CInt -> CInt -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga8779204998136569c3e166c34cfd3e2c
z3_mk_int :: Ptr Z3_context -> CInt -> Ptr Z3_sort -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga7201b6231b61421c005457206760a121
z3_mk_unsigned_int :: Ptr Z3_context -> CUInt -> Ptr Z3_sort -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga42cc319787d485d9cb665d80e02d206f
z3_mk_int64 :: Ptr Z3_context -> CLLong -> Ptr Z3_sort -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga88a165138162a8bac401672f0a1b7891
z3_mk_unsigned_int64 :: Ptr Z3_context -> CULLong -> Ptr Z3_sort -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaf15c95b66dc3b0af735774ee401a6f85
z3_mk_pattern :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_pattern)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga1d4da8849fca699b345322f8ee1fa31e
z3_mk_bound :: Ptr Z3_context -> CUInt -> Ptr Z3_sort -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga7e975b7d7ac96de1db73d8f71166c663
z3_mk_forall :: Ptr Z3_context -> CUInt -> CUInt -> Ptr (Ptr Z3_pattern) -> CUInt -> Ptr (Ptr Z3_sort) -> Ptr (Ptr Z3_symbol) -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Referece:
-- http://z3prover.github.io/api/html/group__capi.html#ga4ffce34ff9117e6243283f11d87c1407
z3_mk_exists :: Ptr Z3_context -> CUInt -> CUInt -> Ptr (Ptr Z3_pattern) -> CUInt -> Ptr (Ptr Z3_sort) -> Ptr (Ptr Z3_symbol) -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference
-- http://z3prover.github.io/api/html/group__capi.html#gabdb40b3ac220bce5a3801e6d29fb3bb6
z3_mk_forall_const :: Ptr Z3_context -> CUInt -> CUInt -> Ptr (Ptr Z3_app) -> CUInt -> Ptr (Ptr Z3_pattern) -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga2011bea0f4445d58ec4d7cefe4499ceb
z3_mk_exists_const :: Ptr Z3_context -> CUInt -> CUInt -> Ptr (Ptr Z3_app) -> CUInt -> Ptr (Ptr Z3_pattern) -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gadc82da786f3b558de8ded05bf6478902
z3_func_decl_to_ast :: Ptr Z3_context -> Ptr Z3_func_decl -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga4c43608feea4cae363ef9c520c239a5c
z3_get_ast_kind :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_ast_kind
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga87a4f9add28db792a24476a1082b4fe4
z3_is_app :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool
z3_get_app_num_args :: Ptr Z3_context -> Ptr Z3_app -> IO CUInt
z3_get_app_arg :: Ptr Z3_context -> Ptr Z3_app -> CUInt -> IO (Ptr Z3_ast)
z3_get_app_decl :: Ptr Z3_context -> Ptr Z3_app -> IO (Ptr Z3_func_decl)
z3_get_datatype_sort_num_constructors :: Ptr Z3_context -> Ptr Z3_sort -> IO CUInt
z3_get_datatype_sort_constructor :: Ptr Z3_context -> Ptr Z3_sort -> CUInt -> IO (Ptr Z3_func_decl)
z3_get_datatype_sort_recognizer :: Ptr Z3_context -> Ptr Z3_sort -> CUInt -> IO (Ptr Z3_func_decl)
z3_get_datatype_sort_constructor_accessor :: Ptr Z3_context -> Ptr Z3_sort -> CUInt -> CUInt -> IO (Ptr Z3_func_decl)
z3_get_decl_name :: Ptr Z3_context -> Ptr Z3_func_decl -> IO (Ptr Z3_symbol)
z3_get_symbol_string :: Ptr Z3_context -> Ptr Z3_symbol -> IO Z3_string
z3_get_sort_kind :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_sort_kind
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga8fc3550edace7bc046e16d1f96ddb419
z3_get_bv_sort_size :: Ptr Z3_context -> Ptr Z3_sort -> IO CUInt
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gae259256eb0f2c10e48fc6227760b7fda
z3_app_to_ast :: Ptr Z3_context -> Ptr Z3_app -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga0a4dac7e9397ff067136354cd33cb933
z3_get_sort :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_sort)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga6ffa46d55e4632d761db4dfae7441c09
z3_get_array_sort_domain :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gaa6f84f1b2b178f6fe5bc3b9a5762a73b
z3_get_array_sort_range :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4
z3_get_bool_value :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_lbool
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga94617ef18fa7157e1a3f85db625d2f4b
z3_get_numeral_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga203f32e3b904955f703f61f91a8626a4
z3_get_arity :: Ptr Z3_context -> Ptr Z3_func_decl -> IO CUInt
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gad025402a9cac1a8d8facddba3f8cbddc
z3_get_domain :: Ptr Z3_context -> Ptr Z3_func_decl -> CUInt -> IO (Ptr Z3_sort)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga913ecf28cd4bddc8255f77f80b6aafe9
z3_get_range :: Ptr Z3_context -> Ptr Z3_func_decl -> IO (Ptr Z3_sort)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaf9345fd0822d7e9928dd4ab14a09765b
z3_to_app :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_app)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gafe4334258b639fa1f8754375b9b56fd7
z3_pattern_to_ast :: Ptr Z3_context -> Ptr Z3_pattern -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gada433553406475e5dd6a494ea957844c
z3_simplify :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga34329d4c83ca8c98e18b2884b679008c
z3_simplify_ex :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_params -> IO (Ptr Z3_ast)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gac47b42af13aee024d34bb37ffaa0ad75
z3_is_quantifier_forall :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gaa5820368b5ae944bd17f10c2f8247c11
z3_get_quantifier_weight :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga3e5cb3bd6e9b9de0d6e6a6e80eb36bba
z3_get_quantifier_num_patterns :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gad48dd00ca5ebce768c66dca447f50037
z3_get_quantifier_pattern_ast :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_ast)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga6b2c35b148f0bb05e9ebf8ab17c2b16e
z3_get_quantifier_num_no_patterns :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga7b68758cbe05352eca541e4028f9a8d8
z3_get_quantifier_no_pattern_ast :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_ast)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gac85bd38ea5c41ec9e0e956a8a1734a7d
z3_get_quantifier_num_bound :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga3e6914c9186de8e588da66af78aa271f
z3_get_quantifier_bound_name :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_symbol)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gae9a7280ad96d05c8266aad869efb9b25
z3_get_quantifier_bound_sort :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_sort)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga94b1bdd4d3351afc860f6cbd2a2ada9f
z3_get_quantifier_body :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gad6e8afe205259b3d924f460d22665e90
z3_substitute_vars :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga99d6a99e914fcb11e5dcf9fcc3584425
z3_ast_vector_size :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO CUInt
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga3a90216036017ce16db63fb3aa5f6047
z3_ast_vector_get :: Ptr Z3_context -> Ptr Z3_ast_vector -> CUInt -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaea0024e05e6f82434ff31e6ec6fab432
z3_ast_vector_inc_ref :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gab0e22d719f55f93fb8788fa4534cc342
z3_ast_vector_dec_ref :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gac06a904e7ac6209d8019c606412d3cec
z3_model_inc_ref :: Ptr Z3_context -> Ptr Z3_model -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gacc2df0767d4a94d7216d3db49c41547f
z3_model_dec_ref :: Ptr Z3_context -> Ptr Z3_model -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga86670c291a16640b932e7892176a9d1b
z3_model_eval :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_ast -> Z3_bool -> Ptr (Ptr Z3_ast) -> IO Z3_bool
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga01bc2993f3eb358f7bd3b2d2d4cf5e51
z3_model_get_const_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> IO (Ptr Z3_ast)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gaf5e9adb229e98b29cbeb7cebf41433a3
z3_model_get_func_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> IO (Ptr Z3_func_interp)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga3c7f8f6ce7c9f30710d3b73fa091f6b3
z3_model_has_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> IO Z3_bool
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga3ff26c1c0f55d17ebf2c152a74eac743
z3_model_get_num_consts :: Ptr Z3_context -> Ptr Z3_model -> IO CUInt
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gaab062a06c0789b432885f4813dd9633b
z3_model_get_num_funcs :: Ptr Z3_context -> Ptr Z3_model -> IO CUInt
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga8e70ac56fe6748301b7776191395184a
z3_model_get_const_decl :: Ptr Z3_context -> Ptr Z3_model -> CUInt -> IO (Ptr Z3_func_decl)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga2a1a4524289574ae34ce2eecdade84d7
z3_model_get_func_decl :: Ptr Z3_context -> Ptr Z3_model -> CUInt -> IO (Ptr Z3_func_decl)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga4674da67d226bfb16861829b9f129cfa
z3_is_as_array :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga7d9262dc6e79f2aeb23fd4a383589dda
z3_get_as_array_func_decl :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_func_decl)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga1f30176bce864257bebb1fb30a103779
z3_add_func_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> Ptr Z3_ast -> IO (Ptr Z3_func_interp)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga73b1de0ec17bb4f2e47d256a7628925c
z3_add_const_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> Ptr Z3_ast -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga80218e1d50bdc4dac5ba18bd13a8ddfb
z3_func_interp_inc_ref :: Ptr Z3_context -> Ptr Z3_func_interp -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gabe3aefc84db4fc3ce5349e958f1ec34b
z3_func_interp_dec_ref :: Ptr Z3_context -> Ptr Z3_func_interp -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga2bab9ae1444940e7593729beec279844
z3_func_interp_get_num_entries :: Ptr Z3_context -> Ptr Z3_func_interp -> IO CUInt
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaf157e1e1cd8c0cfe6a21be6370f659da
z3_func_interp_get_entry :: Ptr Z3_context -> Ptr Z3_func_interp -> CUInt -> IO (Ptr Z3_func_entry)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga46de7559826ba71b8488d727cba1fb64
z3_func_interp_get_else :: Ptr Z3_context -> Ptr Z3_func_interp -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaca22cbdb6f7787aaae5d814f2ab383d8
z3_func_interp_get_arity :: Ptr Z3_context -> Ptr Z3_func_interp -> IO CUInt
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga82cd36e7b02c432436950d5c2301245e
z3_func_entry_inc_ref :: Ptr Z3_context -> Ptr Z3_func_entry -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga9a9a2a75d7fc3d842839662e53365903
z3_func_entry_dec_ref :: Ptr Z3_context -> Ptr Z3_func_entry -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga9fd65e2ab039aa8e40608c2ecf7084da
z3_func_entry_get_value :: Ptr Z3_context -> Ptr Z3_func_entry -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga51aed8c5bc4b1f53f0c371312de3ce1a
z3_func_entry_get_num_args :: Ptr Z3_context -> Ptr Z3_func_entry -> IO CUInt
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga6fe03fe3c824fceb52766a4d8c2cbeab
z3_func_entry_get_arg :: Ptr Z3_context -> Ptr Z3_func_entry -> CUInt -> IO (Ptr Z3_ast)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gab3c5c7eadcfd209eec72ec0ac0ad2e96
z3_get_index_value :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaf36d49862a8c0d20dd5e6508eef5f8af
z3_model_to_string :: Ptr Z3_context -> Ptr Z3_model -> IO Z3_string
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gac7f883536538ab0ad234fde58988e673
z3_mk_params :: Ptr Z3_context -> IO (Ptr Z3_params)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga3a91c9f749b89e1dcf1493177d395d0c
z3_params_inc_ref :: Ptr Z3_context -> Ptr Z3_params -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gae4df28ba713b81ee99abd929e32484ea
z3_params_dec_ref :: Ptr Z3_context -> Ptr Z3_params -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga39e3df967eaad45b343256d56c54e91c
z3_params_set_bool :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> Z3_bool -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga4974397cb652c7f7f479012eb465e250
z3_params_set_uint :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> CUInt -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga11498ce4b25d294f5f89ab7ac1b74c62
z3_params_set_double :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> CDouble -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gac2e899a4906b6133a23fdb60ef992ec9
z3_params_set_symbol :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> Ptr Z3_symbol -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga624e692e180a8b2f617156b1e1ae9722
z3_params_to_string :: Ptr Z3_context -> Ptr Z3_params -> IO Z3_string
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga0d5e342cd83ed43185bcfdc583513959
z3_mk_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga1fd3d3fe7bc4426c4787c3cc8cf92864
z3_mk_interpolation_context :: Ptr Z3_config -> IO (Ptr Z3_context)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gad4417737993c62d39a6624118427f506
z3_get_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_params -> IO (Ptr Z3_ast_vector)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaf62f6b456349886273e15d3cfe8656fe
z3_compute_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_params -> Ptr (Ptr Z3_ast_vector) -> Ptr (Ptr Z3_model) -> IO Z3_lbool
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga2bf6a92d53d65fc32163792bedd5d31f
z3_read_interpolation_problem :: Ptr Z3_context -> Ptr CUInt -> Ptr (Ptr Z3_ast) -> Ptr (Ptr CUInt) -> Ptr CChar -> Ptr Z3_string -> Ptr CUInt -> Ptr (Ptr Z3_ast) -> IO Z3_bool
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gadf50d7093abe5a892593baef552bbf89
z3_check_interpolant :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> Ptr CUInt -> Ptr (Ptr Z3_ast) -> Ptr Z3_string -> CUInt -> Ptr (Ptr Z3_ast) -> IO Z3_lbool
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gad45c5746cd1eefe4f2fc6df956c9cd8e
z3_interpolation_profile :: Ptr Z3_context -> IO Z3_string
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga2a8ee59130e23e10568a1f70e387c608
z3_write_interpolation_problem :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> Ptr CUInt -> Ptr CChar -> CUInt -> Ptr (Ptr Z3_ast) -> IO ()
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gaa4b9d53ba194d2d3a8bb2f55bec7e78e
z3_mk_tactic :: Ptr Z3_context -> Ptr CChar -> IO (Ptr Z3_tactic)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gaf53dac8f6c9b615cd21b9a2eeb006005
z3_tactic_and_then :: Ptr Z3_context -> Ptr Z3_tactic -> Ptr Z3_tactic -> IO (Ptr Z3_tactic)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gad9964357958dd12ab20f0b315ddc219b
z3_tactic_or_else :: Ptr Z3_context -> Ptr Z3_tactic -> Ptr Z3_tactic -> IO (Ptr Z3_tactic)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gab940c1401643ece97517ff27838313c4
z3_tactic_skip :: Ptr Z3_context -> IO (Ptr Z3_tactic)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gac0670bd04fa76af71b2abbc2f8b62889
z3_tactic_try_for :: Ptr Z3_context -> Ptr Z3_tactic -> CUInt -> IO (Ptr Z3_tactic)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gabd0874d8777b3bc426782a87c04206b9
z3_tactic_inc_ref :: Ptr Z3_context -> Ptr Z3_tactic -> IO ()
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga8feaef3d36dcb136fa7812a8c10cf178
z3_tactic_dec_ref :: Ptr Z3_context -> Ptr Z3_tactic -> IO ()
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gac9e9da38d6a9acff293bc22bf0cf1a20
z3_tactic_apply :: Ptr Z3_context -> Ptr Z3_tactic -> Ptr Z3_goal -> IO (Ptr Z3_apply_result)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga1f182e7ef80015e8f2dcde219371aedc
z3_apply_result_inc_ref :: Ptr Z3_context -> Ptr Z3_apply_result -> IO ()
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gac0fa60e39840a704f201ced90cde0ef9
z3_apply_result_dec_ref :: Ptr Z3_context -> Ptr Z3_apply_result -> IO ()
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga5ab8e77bdbfecc6f8845734cd7a729f7
z3_apply_result_get_num_subgoals :: Ptr Z3_context -> Ptr Z3_apply_result -> IO CUInt
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gac4f8342eed2de1c1caaa2fbf492439a9
z3_apply_result_get_subgoal :: Ptr Z3_context -> Ptr Z3_apply_result -> CUInt -> IO (Ptr Z3_goal)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga631394a36c83a1e0db7825fe92d8aebe
z3_mk_goal :: Ptr Z3_context -> Z3_bool -> Z3_bool -> Z3_bool -> IO (Ptr Z3_goal)
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga63a581c33213fb14efe9e6175c74546b
z3_goal_inc_ref :: Ptr Z3_context -> Ptr Z3_goal -> IO ()
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gad65f4f9f7035b6eef161ee93bb694e52
z3_goal_dec_ref :: Ptr Z3_context -> Ptr Z3_goal -> IO ()
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga3052a11993ce35250f108c365bc09ff7
z3_goal_assert :: Ptr Z3_context -> Ptr Z3_goal -> Ptr Z3_ast -> IO ()
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#ga5badc99b0a1e154ef3cef17ff35fd021
z3_goal_size :: Ptr Z3_context -> Ptr Z3_goal -> IO CUInt
-- | Reference:
-- https://z3prover.github.io/api/html/group__capi.html#gaec43d4d20ed7e7bf4c7a57d37dc3bfc6
z3_goal_formula :: Ptr Z3_context -> Ptr Z3_goal -> CUInt -> IO (Ptr Z3_ast)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga5735499ef0b46846c5d45982eaa0e74c
z3_mk_solver :: Ptr Z3_context -> IO (Ptr Z3_solver)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga5735499ef0b46846c5d45982eaa0e74c
z3_mk_simple_solver :: Ptr Z3_context -> IO (Ptr Z3_solver)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga54244cfc9d9cd2ca8f08c3909d700628
z3_mk_solver_for_logic :: Ptr Z3_context -> Ptr Z3_symbol -> IO (Ptr Z3_solver)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga047bb9dff9d57c7d3a71b7af4555956b
z3_solver_get_help :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga887441b3468a1bc605bbf564ddebf2ae
z3_solver_set_params :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_params -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga388e25a8b477abbd49f08c6c29dfa12d
z3_solver_inc_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga2362dcef4e9b8ede41298a50428902ff
z3_solver_dec_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gae41bebe15b1b1105f9abb8690188d1e2
z3_solver_push :: Ptr Z3_context -> Ptr Z3_solver -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga40aa98e15aceffa5be3afad2e065478a
z3_solver_pop :: Ptr Z3_context -> Ptr Z3_solver -> CUInt -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gafd4b4a6465601835341b477b75725b28
z3_solver_get_num_scopes :: Ptr Z3_context -> Ptr Z3_solver -> IO CUInt
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga4a4a215b9130d7980e3c393fe857335f
z3_solver_reset :: Ptr Z3_context -> Ptr Z3_solver -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga72afadf5e8b216f2c6ae675e872b8be4
z3_solver_assert :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_ast -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaf46fb6f3aa3ef451d6be01a737697810
z3_solver_assert_and_track :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_ast -> Ptr Z3_ast -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga000e369de7b71caa4ee701089709c526
z3_solver_check :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_lbool
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga45b40829aaa382bbf427a744911452f9
z3_solver_check_assumptions :: Ptr Z3_context -> Ptr Z3_solver -> CUInt -> Ptr (Ptr Z3_ast) -> IO Z3_lbool
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaf14a54d904a7e45eecc00c5fb8a9d5c9
z3_solver_get_model :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_model)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gabb4f8ed6a09873f5aeefe9cc01010864
z3_solver_get_unsat_core :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_ast_vector)
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaed5d19000004b43dd75e487682e91b55
z3_solver_get_reason_unknown :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaf52e41db4b12a84188b80255454d3abb
z3_solver_to_string :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga20d66dac19b6d6a06537843d0e25f761
z3_set_ast_print_mode :: Ptr Z3_context -> Z3_ast_print_mode -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gab1aa4b78298fe00b3167bf7bfd88aea3
z3_ast_to_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga51b048ddbbcd88708e7aa4fe1c2462d6
z3_pattern_to_string :: Ptr Z3_context -> Ptr Z3_pattern -> IO Z3_string
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaf90c72f63eab298e1dd750f6a26fb945
z3_sort_to_string :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_string
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga15243dcad77f5571e28e8aa1da465675
z3_func_decl_to_string :: Ptr Z3_context -> Ptr Z3_func_decl -> IO Z3_string
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaf93844a5964ad8dee609fac3470d86e4
z3_benchmark_to_smtlib_string :: Ptr Z3_context -> Z3_string -> Z3_string -> Z3_string -> Z3_string -> CUInt -> Ptr (Ptr Z3_ast) -> Ptr Z3_ast -> IO Z3_string
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga74e6e5107c4143be3929e80bdaf73d6d
z3_parse_smtlib2_string :: Ptr Z3_context -> Z3_string -> CUInt -> Ptr (Ptr Z3_symbol) -> Ptr (Ptr Z3_sort) -> CUInt -> Ptr (Ptr Z3_symbol) -> Ptr (Ptr Z3_func_decl) -> IO (Ptr Z3_ast)
-- | Referece
-- http://z3prover.github.io/api/html/group__capi.html#ga6168be4babb03fbbccff1fa7df451300
z3_parse_smtlib2_file :: Ptr Z3_context -> Z3_string -> CUInt -> Ptr (Ptr Z3_symbol) -> Ptr (Ptr Z3_sort) -> CUInt -> Ptr (Ptr Z3_symbol) -> Ptr (Ptr Z3_func_decl) -> IO (Ptr Z3_ast)
-- | Referece
-- http://z3prover.github.io/api/html/group__capi.html#ga96b11da43464071c4ec35418d1cc3483
z3_get_parser_error :: Ptr Z3_context -> IO Z3_string
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga8ac771e68b28d2c86f40aa84889b3807
z3_get_error_code :: Ptr Z3_context -> IO Z3_error_code
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gadaa12e9990f37b0c1e2bf1dd502dbf39
z3_set_error_handler :: Ptr Z3_context -> FunPtr Z3_error_handler -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga41cf70319c4802ab7301dd168d6f5e45
z3_set_error :: Ptr Z3_context -> Z3_error_code -> IO ()
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gaf06357c49299efb8a0bdaeb3bc96c6d6
z3_get_error_msg :: Z3_error_code -> IO Z3_string
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gae0aba52b5738b2ea78e0d6ad67ef1f92
z3_get_error_msg_ex :: Ptr Z3_context -> Z3_error_code -> IO Z3_string
-- | Reference:
-- http://z3prover.github.io/api/html/group__capi.html#ga45fcd18a00379b13a536c5b6117190ae
z3_get_version :: Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> IO ()
z3_mk_fixedpoint :: Ptr Z3_context -> IO (Ptr Z3_fixedpoint)
z3_fixedpoint_push :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO ()
z3_fixedpoint_pop :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO ()
z3_fixedpoint_inc_ref :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO ()
z3_fixedpoint_dec_ref :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO ()
z3_fixedpoint_set_params :: Ptr Z3_context -> Ptr Z3_fixedpoint -> Ptr Z3_params -> IO ()
z3_fixedpoint_add_rule :: Ptr Z3_context -> Ptr Z3_fixedpoint -> Ptr Z3_ast -> Ptr Z3_symbol -> IO ()
z3_fixedpoint_register_relation :: Ptr Z3_context -> Ptr Z3_fixedpoint -> Ptr Z3_func_decl -> IO ()
z3_fixedpoint_get_answer :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO (Ptr Z3_ast)
z3_fixedpoint_get_assertions :: Ptr Z3_context -> Ptr Z3_fixedpoint -> IO (Ptr Z3_ast_vector)
z3_fixedpoint_query_relations :: Ptr Z3_context -> Ptr Z3_fixedpoint -> CUInt -> Ptr (Ptr Z3_func_decl) -> IO Z3_lbool
instance GHC.Classes.Eq Z3.Base.C.Z3_bool
instance GHC.Classes.Eq Z3.Base.C.Z3_lbool
-- | Low-level bindings to Z3 API.
--
-- There is (mostly) a one-to-one correspondence with Z3 C API, thus see
-- http://z3prover.github.io/api/html/group__capi.html for further
-- details.
module Z3.Base
-- | A Z3 configuration object.
data Config
-- | A Z3 logical context.
data Context
-- | A Z3 symbol.
--
-- Used to name types, constants and functions.
data Symbol
-- | A Z3 AST node.
--
-- This is the data-structure used in Z3 to represent terms, formulas and
-- types.
data AST
-- | A kind of AST representing types.
data Sort
-- | A kind of AST representing function symbols.
data FuncDecl
-- | A kind of AST representing constant and function declarations.
data App
-- | A kind of AST representing pattern and multi-patterns to guide
-- quantifier instantiation.
data Pattern
-- | A type contructor for a (recursive) datatype.
data Constructor
-- | A model for the constraints asserted into the logical context.
data Model
-- | An interpretation of a function in a model.
data FuncInterp
-- | Representation of the value of a Z3_func_interp at a particular
-- point.
data FuncEntry
-- | A Z3 parameter set.
--
-- Starting at Z3 4.0, parameter sets are used to configure many
-- components such as: simplifiers, tactics, solvers, etc.
data Params
-- | A Z3 solver engine.
--
-- A(n) (incremental) solver, possibly specialized by a particular tactic
-- or logic.
data Solver
-- | Different kinds of Z3 types.
data SortKind
Z3_UNINTERPRETED_SORT :: SortKind
Z3_BOOL_SORT :: SortKind
Z3_INT_SORT :: SortKind
Z3_REAL_SORT :: SortKind
Z3_BV_SORT :: SortKind
Z3_ARRAY_SORT :: SortKind
Z3_DATATYPE_SORT :: SortKind
Z3_RELATION_SORT :: SortKind
Z3_FINITE_DOMAIN_SORT :: SortKind
Z3_FLOATING_POINT_SORT :: SortKind
Z3_ROUNDING_MODE_SORT :: SortKind
Z3_UNKNOWN_SORT :: SortKind
-- | Different kinds of Z3 AST nodes.
data ASTKind
Z3_NUMERAL_AST :: ASTKind
Z3_APP_AST :: ASTKind
Z3_VAR_AST :: ASTKind
Z3_QUANTIFIER_AST :: ASTKind
Z3_SORT_AST :: ASTKind
Z3_FUNC_DECL_AST :: ASTKind
Z3_UNKNOWN_AST :: ASTKind
-- | A tactic
data Tactic
-- | A result of applying a tactic
data ApplyResult
-- | A goal (aka problem)
data Goal
-- | Result of a satisfiability check.
--
-- This corresponds to the z3_lbool type in the C API.
data Result
Sat :: Result
Unsat :: Result
Undef :: Result
-- | Create a configuration.
--
-- See withConfig.
mkConfig :: IO Config
-- | Delete a configuration.
--
-- See withConfig.
delConfig :: Config -> IO ()
-- | Set a configuration parameter.
setParamValue :: Config -> String -> String -> IO ()
-- | Run a computation using a temporally created configuration.
--
-- Note that the configuration object can be thrown away once it has been
-- used to create the Z3 Context.
withConfig :: (Config -> IO a) -> IO a
-- | Create a context using the given configuration.
--
-- Z3_del_context is called by Haskell's garbage collector before
-- freeing the Context object.
mkContext :: Config -> IO Context
withContext :: Context -> (Ptr Z3_context -> IO r) -> IO r
-- | Create a Z3 (empty) parameter set.
--
-- Starting at Z3 4.0, parameter sets are used to configure many
-- components such as: simplifiers, tactics, solvers, etc.
mkParams :: Context -> IO Params
-- | Add a Boolean parameter k with value v to the parameter
-- set p.
paramsSetBool :: Context -> Params -> Symbol -> Bool -> IO ()
-- | Add a unsigned parameter k with value v to the parameter
-- set p.
paramsSetUInt :: Context -> Params -> Symbol -> Word -> IO ()
-- | Add a double parameter k with value v to the parameter
-- set p.
paramsSetDouble :: Context -> Params -> Symbol -> Double -> IO ()
-- | Add a symbol parameter k with value v to the parameter
-- set p.
paramsSetSymbol :: Context -> Params -> Symbol -> Symbol -> IO ()
-- | Convert a parameter set into a string.
--
-- This function is mainly used for printing the contents of a parameter
-- set.
paramsToString :: Context -> Params -> IO String
-- | Create a Z3 symbol using an integer.
--
-- mkIntSymbol c i requires 0 <= i < 2^30
mkIntSymbol :: Integral int => Context -> int -> IO Symbol
-- | Create a Z3 symbol using a String.
mkStringSymbol :: Context -> String -> IO Symbol
-- | Create a free (uninterpreted) type using the given name (symbol).
--
-- Two free types are considered the same iff the have the same name.
mkUninterpretedSort :: Context -> Symbol -> IO Sort
-- | Create the boolean type.
--
-- This type is used to create propositional variables and predicates.
mkBoolSort :: Context -> IO Sort
-- | Create the integer type.
--
-- This is the type of arbitrary precision integers. A machine integer
-- can be represented using bit-vectors, see mkBvSort.
mkIntSort :: Context -> IO Sort
-- | Create the real type.
--
-- This type is not a floating point number. Z3 does not have support for
-- floating point numbers yet.
mkRealSort :: Context -> IO Sort
-- | Create a bit-vector type of the given size.
--
-- This type can also be seen as a machine integer.
--
-- mkBvSort c sz requires sz >= 0
mkBvSort :: Integral int => Context -> int -> IO Sort
-- | Create an array type
--
-- We usually represent the array type as: [domain -> range]. Arrays
-- are usually used to model the heap/memory in software verification.
mkArraySort :: Context -> Sort -> Sort -> IO Sort
-- | Create a tuple type
--
-- A tuple with n fields has a constructor and n projections. This
-- function will also declare the constructor and projection functions.
mkTupleSort :: Context -> Symbol -> [(Symbol, Sort)] -> IO (Sort, FuncDecl, [FuncDecl])
-- | Create a contructor
mkConstructor :: Context -> Symbol -> Symbol -> [(Symbol, Maybe Sort, Int)] -> IO Constructor
-- | Create datatype, such as lists, trees, records, enumerations or unions
-- of records.
--
-- The datatype may be recursive. Returns the datatype sort.
mkDatatype :: Context -> Symbol -> [Constructor] -> IO Sort
-- | Create mutually recursive datatypes, such as a tree and forest.
--
-- Returns the datatype sorts
mkDatatypes :: Context -> [Symbol] -> [[Constructor]] -> IO ([Sort])
-- | Create an set type with a given domain type
mkSetSort :: Context -> Sort -> IO Sort
-- | Declare a constant or function.
mkFuncDecl :: Context -> Symbol -> [Sort] -> Sort -> IO FuncDecl
-- | Create a constant or function application.
mkApp :: Context -> FuncDecl -> [AST] -> IO AST
-- | Declare and create a constant.
--
-- This is a shorthand for: do xd <- mkFunDecl c x [] s; mkApp c
-- xd []
mkConst :: Context -> Symbol -> Sort -> IO AST
-- | Declare a fresh constant or function.
mkFreshFuncDecl :: Context -> String -> [Sort] -> Sort -> IO FuncDecl
-- | Declare and create a fresh constant.
mkFreshConst :: Context -> String -> Sort -> IO AST
-- | Declare and create a variable (aka constant).
--
-- An alias for mkConst.
mkVar :: Context -> Symbol -> Sort -> IO AST
-- | Declarate and create a variable of sort bool.
--
-- See mkVar.
mkBoolVar :: Context -> Symbol -> IO AST
-- | Declarate and create a variable of sort real.
--
-- See mkVar.
mkRealVar :: Context -> Symbol -> IO AST
-- | Declarate and create a variable of sort int.
--
-- See mkVar.
mkIntVar :: Context -> Symbol -> IO AST
-- | Declarate and create a variable of sort bit-vector.
--
-- See mkVar.
mkBvVar :: Context -> Symbol -> Int -> IO AST
-- | Declare and create a fresh variable (aka constant).
--
-- An alias for mkFreshConst.
mkFreshVar :: Context -> String -> Sort -> IO AST
-- | Declarate and create a fresh variable of sort bool.
--
-- See mkFreshVar.
mkFreshBoolVar :: Context -> String -> IO AST
-- | Declarate and create a fresh variable of sort real.
--
-- See mkFreshVar.
mkFreshRealVar :: Context -> String -> IO AST
-- | Declarate and create a fresh variable of sort int.
--
-- See mkFreshVar.
mkFreshIntVar :: Context -> String -> IO AST
-- | Declarate and create a fresh variable of sort
-- bit-vector.
--
-- See mkFreshVar.
mkFreshBvVar :: Context -> String -> Int -> IO AST
-- | Create an AST node representing true.
mkTrue :: Context -> IO AST
-- | Create an AST node representing false.
mkFalse :: Context -> IO AST
-- | Create an AST node representing l = r.
mkEq :: Context -> AST -> AST -> IO AST
-- | Create an AST node representing not(a).
mkNot :: Context -> AST -> IO AST
-- | Create an AST node representing an if-then-else: ite(t1, t2,
-- t3).
mkIte :: Context -> AST -> AST -> AST -> IO AST
-- | Create an AST node representing t1 iff t2.
mkIff :: Context -> AST -> AST -> IO AST
-- | Create an AST node representing t1 implies t2.
mkImplies :: Context -> AST -> AST -> IO AST
-- | Create an AST node representing t1 xor t2.
mkXor :: Context -> AST -> AST -> IO AST
-- | Create an AST node representing args[0] and ... and args[num_args-1].
mkAnd :: Context -> [AST] -> IO AST
-- | Create an AST node representing args[0] or ... or args[num_args-1].
mkOr :: Context -> [AST] -> IO AST
-- | The distinct construct is used for declaring the arguments pairwise
-- distinct.
--
-- That is, and [ args!!i /= args!!j | i <- [0..length(args)-1], j
-- <- [i+1..length(args)-1] ]
mkDistinct :: Context -> [AST] -> IO AST
-- | Create an AST node representing the given boolean.
mkBool :: Context -> Bool -> IO AST
-- | Create an AST node representing args[0] + ... + args[num_args-1].
mkAdd :: Context -> [AST] -> IO AST
-- | Create an AST node representing args[0] * ... * args[num_args-1].
mkMul :: Context -> [AST] -> IO AST
-- | Create an AST node representing args[0] - ... - args[num_args - 1].
mkSub :: Context -> [AST] -> IO AST
-- | Create an AST node representing -arg.
mkUnaryMinus :: Context -> AST -> IO AST
-- | Create an AST node representing arg1 div arg2.
mkDiv :: Context -> AST -> AST -> IO AST
-- | Create an AST node representing arg1 mod arg2.
mkMod :: Context -> AST -> AST -> IO AST
-- | Create an AST node representing arg1 rem arg2.
mkRem :: Context -> AST -> AST -> IO AST
-- | Create less than.
mkLt :: Context -> AST -> AST -> IO AST
-- | Create less than or equal to.
mkLe :: Context -> AST -> AST -> IO AST
-- | Create greater than.
mkGt :: Context -> AST -> AST -> IO AST
-- | Create greater than or equal to.
mkGe :: Context -> AST -> AST -> IO AST
-- | Coerce an integer to a real.
mkInt2Real :: Context -> AST -> IO AST
-- | Coerce a real to an integer.
mkReal2Int :: Context -> AST -> IO AST
-- | Check if a real number is an integer.
mkIsInt :: Context -> AST -> IO AST
-- | Bitwise negation.
mkBvnot :: Context -> AST -> IO AST
-- | Take conjunction of bits in vector, return vector of length 1.
mkBvredand :: Context -> AST -> IO AST
-- | Take disjunction of bits in vector, return vector of length 1.
mkBvredor :: Context -> AST -> IO AST
-- | Bitwise and.
mkBvand :: Context -> AST -> AST -> IO AST
-- | Bitwise or.
mkBvor :: Context -> AST -> AST -> IO AST
-- | Bitwise exclusive-or.
mkBvxor :: Context -> AST -> AST -> IO AST
-- | Bitwise nand.
mkBvnand :: Context -> AST -> AST -> IO AST
-- | Bitwise nor.
mkBvnor :: Context -> AST -> AST -> IO AST
-- | Bitwise xnor.
mkBvxnor :: Context -> AST -> AST -> IO AST
-- | Standard two's complement unary minus.
mkBvneg :: Context -> AST -> IO AST
-- | Standard two's complement addition.
mkBvadd :: Context -> AST -> AST -> IO AST
-- | Standard two's complement subtraction.
mkBvsub :: Context -> AST -> AST -> IO AST
-- | Standard two's complement multiplication.
mkBvmul :: Context -> AST -> AST -> IO AST
-- | Unsigned division.
mkBvudiv :: Context -> AST -> AST -> IO AST
-- | Two's complement signed division.
mkBvsdiv :: Context -> AST -> AST -> IO AST
-- | Unsigned remainder.
mkBvurem :: Context -> AST -> AST -> IO AST
-- | Two's complement signed remainder (sign follows dividend).
mkBvsrem :: Context -> AST -> AST -> IO AST
-- | Two's complement signed remainder (sign follows divisor).
mkBvsmod :: Context -> AST -> AST -> IO AST
-- | Unsigned less than.
mkBvult :: Context -> AST -> AST -> IO AST
-- | Two's complement signed less than.
mkBvslt :: Context -> AST -> AST -> IO AST
-- | Unsigned less than or equal to.
mkBvule :: Context -> AST -> AST -> IO AST
-- | Two's complement signed less than or equal to.
mkBvsle :: Context -> AST -> AST -> IO AST
-- | Unsigned greater than or equal to.
mkBvuge :: Context -> AST -> AST -> IO AST
-- | Two's complement signed greater than or equal to.
mkBvsge :: Context -> AST -> AST -> IO AST
-- | Unsigned greater than.
mkBvugt :: Context -> AST -> AST -> IO AST
-- | Two's complement signed greater than.
mkBvsgt :: Context -> AST -> AST -> IO AST
-- | Concatenate the given bit-vectors.
mkConcat :: Context -> AST -> AST -> IO AST
-- | Extract the bits high down to low from a bitvector of size m to yield
-- a new bitvector of size n, where n = high - low + 1.
mkExtract :: Context -> Int -> Int -> AST -> IO AST
-- | Sign-extend of the given bit-vector to the (signed) equivalent
-- bitvector of size m+i, where m is the size of the given
-- bit-vector.
mkSignExt :: Context -> Int -> AST -> IO AST
-- | Extend the given bit-vector with zeros to the (unsigned) equivalent
-- bitvector of size m+i, where m is the size of the given
-- bit-vector.
mkZeroExt :: Context -> Int -> AST -> IO AST
-- | Repeat the given bit-vector up length i.
mkRepeat :: Context -> Int -> AST -> IO AST
-- | Shift left.
mkBvshl :: Context -> AST -> AST -> IO AST
-- | Logical shift right.
mkBvlshr :: Context -> AST -> AST -> IO AST
-- | Arithmetic shift right.
mkBvashr :: Context -> AST -> AST -> IO AST
-- | Rotate bits of t1 to the left i times.
mkRotateLeft :: Context -> Int -> AST -> IO AST
-- | Rotate bits of t1 to the right i times.
mkRotateRight :: Context -> Int -> AST -> IO AST
-- | Rotate bits of t1 to the left t2 times.
mkExtRotateLeft :: Context -> AST -> AST -> IO AST
-- | Rotate bits of t1 to the right t2 times.
mkExtRotateRight :: Context -> AST -> AST -> IO AST
-- | Create an n bit bit-vector from the integer argument t1.
mkInt2bv :: Context -> Int -> AST -> IO AST
-- | Create an integer from the bit-vector argument t1.
--
-- If is_signed is false, then the bit-vector t1 is treated
-- as unsigned. So the result is non-negative and in the range
-- [0..2^N-1], where N are the number of bits in t1.
-- If is_signed is true, t1 is treated as a signed
-- bit-vector.
mkBv2int :: Context -> AST -> Bool -> IO AST
-- | Check that bit-wise negation does not overflow when t1 is
-- interpreted as a signed bit-vector.
mkBvnegNoOverflow :: Context -> AST -> IO AST
-- | Create a predicate that checks that the bit-wise addition of t1
-- and t2 does not overflow.
mkBvaddNoOverflow :: Context -> AST -> AST -> Bool -> IO AST
-- | Create a predicate that checks that the bit-wise signed addition of
-- t1 and t2 does not underflow.
mkBvaddNoUnderflow :: Context -> AST -> AST -> IO AST
-- | Create a predicate that checks that the bit-wise signed subtraction of
-- t1 and t2 does not overflow.
mkBvsubNoOverflow :: Context -> AST -> AST -> IO AST
-- | Create a predicate that checks that the bit-wise subtraction of
-- t1 and t2 does not underflow.
mkBvsubNoUnderflow :: Context -> AST -> AST -> IO AST
-- | Create a predicate that checks that the bit-wise multiplication of
-- t1 and t2 does not overflow.
mkBvmulNoOverflow :: Context -> AST -> AST -> Bool -> IO AST
-- | Create a predicate that checks that the bit-wise signed multiplication
-- of t1 and t2 does not underflow.
mkBvmulNoUnderflow :: Context -> AST -> AST -> IO AST
-- | Create a predicate that checks that the bit-wise signed division of
-- t1 and t2 does not overflow.
mkBvsdivNoOverflow :: Context -> AST -> AST -> IO AST
-- | Array read. The argument a is the array and i is the index of the
-- array that gets read.
mkSelect :: Context -> AST -> AST -> IO AST
-- | Array update.
--
-- The result of this function is an array that is equal to the input
-- array (with respect to select) on all indices except for i, where it
-- maps to v.
--
-- The semantics of this function is given by the theory of arrays
-- described in the SMT-LIB standard. See http://smtlib.org for
-- more details.
mkStore :: Context -> AST -> AST -> AST -> IO AST
-- | Create the constant array.
--
-- The resulting term is an array, such that a select on an arbitrary
-- index produces the value v.
mkConstArray :: Context -> Sort -> AST -> IO AST
-- | Map a function f on the the argument arrays.
--
-- The n nodes args must be of array sorts [domain -> range_i].
-- The function declaration f must have type range_1 .. range_n
-- -> range. The sort of the result is [domain -> range].
mkMap :: Context -> FuncDecl -> [AST] -> IO AST
-- | Access the array default value.
--
-- Produces the default range value, for arrays that can be represented
-- as finite maps with a default range value.
mkArrayDefault :: Context -> AST -> IO AST
-- | Create the empty set.
mkEmptySet :: Context -> Sort -> IO AST
-- | Create the full set.
mkFullSet :: Context -> Sort -> IO AST
-- | Add an element to a set.
mkSetAdd :: Context -> AST -> AST -> IO AST
-- | Remove an element from a set.
mkSetDel :: Context -> AST -> AST -> IO AST
-- | Take the union of a list of sets.
mkSetUnion :: Context -> [AST] -> IO AST
-- | Take the intersection of a list of sets.
mkSetIntersect :: Context -> [AST] -> IO AST
-- | Take the set difference between two sets.
mkSetDifference :: Context -> AST -> AST -> IO AST
-- | Take the complement of a set.
mkSetComplement :: Context -> AST -> IO AST
-- | Check for set membership.
mkSetMember :: Context -> AST -> AST -> IO AST
-- | Check if the first set is a subset of the second set.
mkSetSubset :: Context -> AST -> AST -> IO AST
-- | Create a numeral of a given sort.
mkNumeral :: Context -> String -> Sort -> IO AST
-- | Create a real from a fraction.
mkReal :: Context -> Int -> Int -> IO AST
-- | Create a numeral of an int, bit-vector, or finite-domain sort.
--
-- This function can be use to create numerals that fit in a machine
-- integer. It is slightly faster than mkNumeral since it is
-- not necessary to parse a string.
mkInt :: Context -> Int -> Sort -> IO AST
-- | Create a numeral of an int, bit-vector, or finite-domain sort.
--
-- This function can be use to create numerals that fit in a machine
-- unsigned integer. It is slightly faster than mkNumeral
-- since it is not necessary to parse a string.
mkUnsignedInt :: Context -> Word -> Sort -> IO AST
-- | Create a numeral of an int, bit-vector, or finite-domain sort.
--
-- This function can be use to create numerals that fit in a machine
-- 64-bit integer. It is slightly faster than mkNumeral since
-- it is not necessary to parse a string.
mkInt64 :: Context -> Int64 -> Sort -> IO AST
-- | Create a numeral of an int, bit-vector, or finite-domain sort.
--
-- This function can be use to create numerals that fit in a machine
-- unsigned 64-bit integer. It is slightly faster than
-- mkNumeral since it is not necessary to parse a string.
mkUnsignedInt64 :: Context -> Word64 -> Sort -> IO AST
-- | Create a numeral of an int, bit-vector, or finite-domain sort.
mkIntegral :: Integral a => Context -> a -> Sort -> IO AST
-- | Create a numeral of sort real from a Rational.
mkRational :: Context -> Rational -> IO AST
-- | Create a numeral of sort real from a Fixed.
mkFixed :: HasResolution a => Context -> Fixed a -> IO AST
-- | Create a numeral of sort real from a Real.
mkRealNum :: Real r => Context -> r -> IO AST
-- | Create a numeral of sort int from an Integer.
mkInteger :: Context -> Integer -> IO AST
-- | Create a numeral of sort int from an Integral.
mkIntNum :: Integral a => Context -> a -> IO AST
-- | Create a numeral of sort Bit-vector from an Integer.
mkBitvector :: Context -> Int -> Integer -> IO AST
-- | Create a numeral of sort Bit-vector from an Integral.
mkBvNum :: Integral i => Context -> Int -> i -> IO AST
-- | Create a pattern for quantifier instantiation.
--
-- Z3 uses pattern matching to instantiate quantifiers. If a pattern is
-- not provided for a quantifier, then Z3 will automatically compute a
-- set of patterns for it. However, for optimal performance, the user
-- should provide the patterns.
--
-- Patterns comprise a list of terms. The list should be non-empty. If
-- the list comprises of more than one term, it is a called a
-- multi-pattern.
--
-- In general, one can pass in a list of (multi-)patterns in the
-- quantifier constructor.
mkPattern :: Context -> [AST] -> IO Pattern
-- | Create a bound variable.
--
-- Bound variables are indexed by de-Bruijn indices.
--
-- See
-- http://z3prover.github.io/api/html/group__capi.html#ga1d4da8849fca699b345322f8ee1fa31e
mkBound :: Context -> Int -> Sort -> IO AST
-- | Create a forall formula.
--
-- The bound variables are de-Bruijn indices created using
-- mkBound.
--
-- Z3 applies the convention that the last element in xs refers to
-- the variable with index 0, the second to last element of xs
-- refers to the variable with index 1, etc.
mkForall :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
-- | Create an exists formula.
--
-- Similar to mkForall.
mkExists :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
-- | Create a universal quantifier using a list of constants that will form
-- the set of bound variables.
mkForallConst :: Context -> [Pattern] -> [App] -> AST -> IO AST
-- | Create a existential quantifier using a list of constants that will
-- form the set of bound variables.
mkExistsConst :: Context -> [Pattern] -> [App] -> AST -> IO AST
-- | Return the symbol name.
getSymbolString :: Context -> Symbol -> IO String
-- | Return the sort kind of the given sort.
getSortKind :: Context -> Sort -> IO SortKind
-- | Return the size of the given bit-vector sort.
getBvSortSize :: Context -> Sort -> IO Int
-- | Get list of constructors for datatype.
getDatatypeSortConstructors :: Context -> Sort -> IO [FuncDecl]
-- | Get list of recognizers for datatype.
getDatatypeSortRecognizers :: Context -> Sort -> IO [FuncDecl]
-- | Get list of accessors for the datatype constructor.
getDatatypeSortConstructorAccessors :: Context -> Sort -> IO [[FuncDecl]]
-- | Return the constant declaration name as a symbol.
getDeclName :: Context -> FuncDecl -> IO Symbol
-- | Returns the number of parameters of the given declaration
getArity :: Context -> FuncDecl -> IO Int
-- | Returns the sort of the i-th parameter of the given function
-- declaration
getDomain :: Context -> FuncDecl -> Int -> IO Sort
-- | Returns the range of the given declaration.
getRange :: Context -> FuncDecl -> IO Sort
-- | Convert an app into AST. This is just type casting.
appToAst :: Context -> App -> IO AST
-- | Return the declaration of a constant or function application.
getAppDecl :: Context -> App -> IO FuncDecl
-- | Return the number of argument of an application. If t is an constant,
-- then the number of arguments is 0.
getAppNumArgs :: Context -> App -> IO Int
-- | Return the i-th argument of the given application.
getAppArg :: Context -> App -> Int -> IO AST
-- | Return a list of all the arguments of the given application.
getAppArgs :: Context -> App -> IO [AST]
-- | Return the sort of an AST node.
getSort :: Context -> AST -> IO Sort
getArraySortDomain :: Context -> Sort -> IO Sort
getArraySortRange :: Context -> Sort -> IO Sort
-- | Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and
-- Z3_L_UNDEF otherwise.
getBoolValue :: Context -> AST -> IO (Maybe Bool)
-- | Return the kind of the given AST.
getAstKind :: Context -> AST -> IO ASTKind
-- | Return True if an ast is APP_AST, False otherwise.
isApp :: Context -> AST -> IO Bool
-- | Convert an ast into an APP_AST. This is just type casting.
toApp :: Context -> AST -> IO App
-- | Return numeral value, as a string of a numeric constant term.
getNumeralString :: Context -> AST -> IO String
simplify :: Context -> AST -> IO AST
simplifyEx :: Context -> AST -> Params -> IO AST
getIndexValue :: Context -> AST -> IO Int
isQuantifierForall :: Context -> AST -> IO Bool
isQuantifierExists :: Context -> AST -> IO Bool
getQuantifierWeight :: Context -> AST -> IO Int
getQuantifierNumPatterns :: Context -> AST -> IO Int
getQuantifierPatternAST :: Context -> AST -> Int -> IO AST
getQuantifierPatterns :: Context -> AST -> IO [AST]
getQuantifierNumNoPatterns :: Context -> AST -> IO Int
getQuantifierNoPatternAST :: Context -> AST -> Int -> IO AST
getQuantifierNoPatterns :: Context -> AST -> IO [AST]
getQuantifierNumBound :: Context -> AST -> IO Int
getQuantifierBoundName :: Context -> AST -> Int -> IO Symbol
getQuantifierBoundSort :: Context -> AST -> Int -> IO Sort
getQuantifierBoundVars :: Context -> AST -> IO [AST]
getQuantifierBody :: Context -> AST -> IO AST
-- | Read a Bool value from an AST
getBool :: Context -> AST -> IO Bool
-- | Read an Integer value from an AST
getInt :: Context -> AST -> IO Integer
-- | Read a Rational value from an AST
getReal :: Context -> AST -> IO Rational
-- | Read the Integer value from an AST of sort
-- bit-vector.
--
-- See mkBv2int.
getBv :: Context -> AST -> Bool -> IO Integer
substituteVars :: Context -> AST -> [AST] -> IO AST
-- | Evaluate an AST node in the given model.
--
-- The evaluation may fail for the following reasons:
--
--
-- - t contains a quantifier.
-- - the model m is partial.
-- - t is type incorrect.
--
modelEval :: Context -> Model -> AST -> Bool -> IO (Maybe AST)
-- | Evaluate an array as a function, if possible.
evalArray :: Context -> Model -> AST -> IO (Maybe FuncModel)
getConstInterp :: Context -> Model -> FuncDecl -> IO (Maybe AST)
-- | Return the interpretation of the function f in the model m. Return
-- NULL, if the model does not assign an interpretation for f. That
-- should be interpreted as: the f does not matter.
getFuncInterp :: Context -> Model -> FuncDecl -> IO (Maybe FuncInterp)
hasInterp :: Context -> Model -> FuncDecl -> IO Bool
numConsts :: Context -> Model -> IO Word
numFuncs :: Context -> Model -> IO Word
getConstDecl :: Context -> Model -> Word -> IO FuncDecl
getFuncDecl :: Context -> Model -> Word -> IO FuncDecl
getConsts :: Context -> Model -> IO [FuncDecl]
getFuncs :: Context -> Model -> IO [FuncDecl]
-- | The (_ as-array f) AST node is a construct for assigning
-- interpretations for arrays in Z3. It is the array such that forall
-- indices i we have that (select (_ as-array f) i) is equal to (f i).
-- This procedure returns Z3_TRUE if the a is an as-array AST node.
isAsArray :: Context -> AST -> IO Bool
addFuncInterp :: Context -> Model -> FuncDecl -> AST -> IO FuncInterp
addConstInterp :: Context -> Model -> FuncDecl -> AST -> IO ()
-- | Return the function declaration f associated with a (_ as_array f)
-- node.
getAsArrayFuncDecl :: Context -> AST -> IO FuncDecl
-- | Return the number of entries in the given function interpretation.
funcInterpGetNumEntries :: Context -> FuncInterp -> IO Int
-- | Return a _point_ of the given function intepretation. It represents
-- the value of f in a particular point.
funcInterpGetEntry :: Context -> FuncInterp -> Int -> IO FuncEntry
-- | Return the 'else' value of the given function interpretation.
funcInterpGetElse :: Context -> FuncInterp -> IO AST
-- | Return the arity (number of arguments) of the given function
-- interpretation.
funcInterpGetArity :: Context -> FuncInterp -> IO Int
-- | Return the value of this point.
funcEntryGetValue :: Context -> FuncEntry -> IO AST
-- | Return the number of arguments in a Z3_func_entry object.
funcEntryGetNumArgs :: Context -> FuncEntry -> IO Int
-- | Return an argument of a Z3_func_entry object.
funcEntryGetArg :: Context -> FuncEntry -> Int -> IO AST
-- | Convert the given model into a string.
modelToString :: Context -> Model -> IO String
-- | Alias for modelToString.
-- | Deprecated: Use modelToString instead.
showModel :: Context -> Model -> IO String
-- | Type of an evaluation function for AST.
--
-- Evaluation may fail (i.e. return Nothing) for a few reasons,
-- see modelEval.
type EvalAst a = Model -> AST -> IO (Maybe a)
-- | An alias for modelEval with model completion enabled.
eval :: Context -> EvalAst AST
-- | Evaluate an AST node of sort bool in the given model.
--
-- See modelEval and getBool.
evalBool :: Context -> EvalAst Bool
-- | Evaluate an AST node of sort int in the given model.
--
-- See modelEval and getInt.
evalInt :: Context -> EvalAst Integer
-- | Evaluate an AST node of sort real in the given model.
--
-- See modelEval and getReal.
evalReal :: Context -> EvalAst Rational
-- | Evaluate an AST node of sort bit-vector in the given model.
--
-- The flag signed decides whether the bit-vector value is
-- interpreted as a signed or unsigned integer.
--
-- See modelEval and getBv.
evalBv :: Context -> Bool -> EvalAst Integer
-- | Run a evaluation function on a Traversable data structure of
-- ASTs (e.g. [AST], Vector AST, Maybe
-- AST, etc).
--
-- This a generic version of evalT which can be used in
-- combination with other helpers. For instance, mapEval (evalInt
-- c) can be used to obtain the Integer interpretation of a
-- list of AST of sort int.
mapEval :: Traversable t => EvalAst a -> Model -> t AST -> IO (Maybe (t a))
-- | Evaluate a collection of AST nodes in the given model.
evalT :: Traversable t => Context -> Model -> t AST -> IO (Maybe (t AST))
-- | The interpretation of a function.
data FuncModel
FuncModel :: [([AST], AST)] -> AST -> FuncModel
-- | Mapping from arguments to values.
[interpMap] :: FuncModel -> [([AST], AST)]
-- | Default value.
[interpElse] :: FuncModel -> AST
-- | Evaluate a function declaration to a list of argument/value pairs.
evalFunc :: Context -> Model -> FuncDecl -> IO (Maybe FuncModel)
mkTactic :: Context -> String -> IO Tactic
andThenTactic :: Context -> Tactic -> Tactic -> IO Tactic
orElseTactic :: Context -> Tactic -> Tactic -> IO Tactic
skipTactic :: Context -> IO Tactic
tryForTactic :: Context -> Tactic -> Int -> IO Tactic
mkQuantifierEliminationTactic :: Context -> IO Tactic
mkAndInverterGraphTactic :: Context -> IO Tactic
applyTactic :: Context -> Tactic -> Goal -> IO ApplyResult
getApplyResultNumSubgoals :: Context -> ApplyResult -> IO Int
getApplyResultSubgoal :: Context -> ApplyResult -> Int -> IO Goal
getApplyResultSubgoals :: Context -> ApplyResult -> IO [Goal]
mkGoal :: Context -> Bool -> Bool -> Bool -> IO Goal
goalAssert :: Context -> Goal -> AST -> IO ()
getGoalSize :: Context -> Goal -> IO Int
getGoalFormula :: Context -> Goal -> Int -> IO AST
getGoalFormulas :: Context -> Goal -> IO [AST]
-- | Pretty-printing mode for converting ASTs to strings. The mode can be
-- one of the following:
--
--
-- - Z3_PRINT_SMTLIB_FULL: Print AST nodes in SMTLIB verbose
-- format.
-- - Z3_PRINT_LOW_LEVEL: Print AST nodes using a low-level format.
-- - Z3_PRINT_SMTLIB_COMPLIANT: Print AST nodes in SMTLIB 1.x compliant
-- format.
-- - Z3_PRINT_SMTLIB2_COMPLIANT: Print AST nodes in SMTLIB 2.x
-- compliant format.
--
data ASTPrintMode
Z3_PRINT_SMTLIB_FULL :: ASTPrintMode
Z3_PRINT_LOW_LEVEL :: ASTPrintMode
Z3_PRINT_SMTLIB2_COMPLIANT :: ASTPrintMode
-- | Set the pretty-printing mode for converting ASTs to strings.
setASTPrintMode :: Context -> ASTPrintMode -> IO ()
-- | Convert an AST to a string.
astToString :: Context -> AST -> IO String
-- | Convert a pattern to a string.
patternToString :: Context -> Pattern -> IO String
-- | Convert a sort to a string.
sortToString :: Context -> Sort -> IO String
-- | Convert a FuncDecl to a string.
funcDeclToString :: Context -> FuncDecl -> IO String
-- | Convert the given benchmark into SMT-LIB formatted string.
--
-- The output format can be configured via setASTPrintMode.
benchmarkToSMTLibString :: Context -> String -> String -> String -> String -> [AST] -> AST -> IO String
parseSMTLib2String :: Context -> String -> [Symbol] -> [Sort] -> [Symbol] -> [FuncDecl] -> IO AST
parseSMTLib2File :: Context -> String -> [Symbol] -> [Sort] -> [Symbol] -> [FuncDecl] -> IO AST
getParserError :: Context -> IO String
-- | Z3 exceptions.
--
-- Z3 errors are re-thrown as Haskell Z3Error exceptions, see
-- Exception.
data Z3Error
Z3Error :: Z3ErrorCode -> String -> Z3Error
[errCode] :: Z3Error -> Z3ErrorCode
[errMsg] :: Z3Error -> String
-- | Z3 error codes.
data Z3ErrorCode
SortError :: Z3ErrorCode
IOB :: Z3ErrorCode
InvalidArg :: Z3ErrorCode
ParserError :: Z3ErrorCode
NoParser :: Z3ErrorCode
InvalidPattern :: Z3ErrorCode
MemoutFail :: Z3ErrorCode
FileAccessError :: Z3ErrorCode
InternalFatal :: Z3ErrorCode
InvalidUsage :: Z3ErrorCode
DecRefError :: Z3ErrorCode
Z3Exception :: Z3ErrorCode
data Version
Version :: !Int -> !Int -> !Int -> !Int -> Version
[z3Major] :: Version -> !Int
[z3Minor] :: Version -> !Int
[z3Build] :: Version -> !Int
[z3Revision] :: Version -> !Int
-- | Return Z3 version number information.
getVersion :: IO Version
newtype Fixedpoint
Fixedpoint :: ForeignPtr Z3_fixedpoint -> Fixedpoint
[unFixedpoint] :: Fixedpoint -> ForeignPtr Z3_fixedpoint
mkFixedpoint :: Context -> IO Fixedpoint
fixedpointPush :: Context -> Fixedpoint -> IO ()
fixedpointPop :: Context -> Fixedpoint -> IO ()
fixedpointAddRule :: Context -> Fixedpoint -> AST -> Symbol -> IO ()
fixedpointSetParams :: Context -> Fixedpoint -> Params -> IO ()
fixedpointRegisterRelation :: Context -> Fixedpoint -> FuncDecl -> IO ()
fixedpointQueryRelations :: Context -> Fixedpoint -> [FuncDecl] -> IO Result
fixedpointGetAnswer :: Context -> Fixedpoint -> IO AST
fixedpointGetAssertions :: Context -> Fixedpoint -> IO [AST]
-- | Interpolation problem formulation.
data InterpolationProblem
InterpolationProblem :: [AST] -> Maybe [Int] -> [AST] -> InterpolationProblem
[getConstraints] :: InterpolationProblem -> [AST]
[getParents] :: InterpolationProblem -> Maybe [Int]
[getTheoryTerms] :: InterpolationProblem -> [AST]
-- | Create an AST node marking a formula position for interpolation.
mkInterpolant :: Context -> AST -> IO AST
-- | Generate a Z3 context suitable for generation of interpolants.
mkInterpolationContext :: Config -> IO Context
-- | Extracts interpolants from a proof of unsatisfiability.
--
-- Interpolants are computed in pre-order for occurrences of
-- mkInterpolant within the second argument, which needs to be in
-- form of a conjunction.
getInterpolant :: Context -> AST -> AST -> Params -> IO [AST]
-- | Checks satisfiability of input conjunction.
--
-- Returns either a model witnessing satisfiability, or a (sequence)
-- interpolants between individual subformulae of the conjunction wrapped
-- in mkInterpolant.
--
-- Result: sat -> Just (Left model)
-- unsat -> Just (Right interp) unknown
-- -> Nothing
computeInterpolant :: Context -> AST -> Params -> IO (Maybe (Either Model [AST]))
-- | Read an interpolation problem from file.
readInterpolationProblem :: Context -> FilePath -> IO (Either String InterpolationProblem)
-- | Check the correctness of an interpolant.
--
-- The Z3 context must have no constraints asserted when this call is
-- made. That means that after interpolating, you must first fully pop
-- the Z3 context before calling this.
checkInterpolant :: Context -> InterpolationProblem -> [AST] -> IO (Result, Maybe String)
-- | Return a string summarizing cumulative time used for interpolation.
--
-- This string is purely for entertainment purposes and has no semantics.
interpolationProfile :: Context -> IO String
-- | Write an interpolation problem to file suitable for reading with
-- readInterpolationProblem.
--
-- The output file is a sequence of SMT-LIB2 format commands, suitable
-- for reading with command-line Z3 or other interpolating solvers.
writeInterpolationProblem :: Context -> FilePath -> InterpolationProblem -> IO ()
-- | Solvers available in Z3.
--
-- These are described at http://smtlib.cs.uiowa.edu/logics.html
data Logic
-- | Closed formulas over the theory of linear integer arithmetic and
-- arrays extended with free sort and function symbols but restricted to
-- arrays with integer indices and values.
AUFLIA :: Logic
-- | Closed linear formulas with free sort and function symbols over one-
-- and two-dimentional arrays of integer index and real value.
AUFLIRA :: Logic
-- | Closed formulas with free function and predicate symbols over a theory
-- of arrays of arrays of integer index and real value.
AUFNIRA :: Logic
-- | Closed linear formulas in linear real arithmetic.
LRA :: Logic
-- | Closed quantifier-free formulas over the theory of bitvectors and
-- bitvector arrays.
QF_ABV :: Logic
-- | Closed quantifier-free formulas over the theory of bitvectors and
-- bitvector arrays extended with free sort and function symbols.
QF_AUFBV :: Logic
-- | Closed quantifier-free linear formulas over the theory of integer
-- arrays extended with free sort and function symbols.
QF_AUFLIA :: Logic
-- | Closed quantifier-free formulas over the theory of arrays with
-- extensionality.
QF_AX :: Logic
-- | Closed quantifier-free formulas over the theory of fixed-size
-- bitvectors.
QF_BV :: Logic
-- | Difference Logic over the integers. In essence, Boolean combinations
-- of inequations of the form x - y < b where x and y are integer
-- variables and b is an integer constant.
QF_IDL :: Logic
-- | Unquantified linear integer arithmetic. In essence, Boolean
-- combinations of inequations between linear polynomials over integer
-- variables.
QF_LIA :: Logic
-- | Unquantified linear real arithmetic. In essence, Boolean combinations
-- of inequations between linear polynomials over real variables.
QF_LRA :: Logic
-- | Quantifier-free integer arithmetic.
QF_NIA :: Logic
-- | Quantifier-free real arithmetic.
QF_NRA :: Logic
-- | Difference Logic over the reals. In essence, Boolean combinations of
-- inequations of the form x - y < b where x and y are real variables
-- and b is a rational constant.
QF_RDL :: Logic
-- | Unquantified formulas built over a signature of uninterpreted (i.e.,
-- free) sort and function symbols.
QF_UF :: Logic
-- | Unquantified formulas over bitvectors with uninterpreted sort function
-- and symbols.
QF_UFBV :: Logic
-- | Difference Logic over the integers (in essence) but with uninterpreted
-- sort and function symbols.
QF_UFIDL :: Logic
-- | Unquantified linear integer arithmetic with uninterpreted sort and
-- function symbols.
QF_UFLIA :: Logic
-- | Unquantified linear real arithmetic with uninterpreted sort and
-- function symbols.
QF_UFLRA :: Logic
-- | Unquantified non-linear real arithmetic with uninterpreted sort and
-- function symbols.
QF_UFNRA :: Logic
-- | Linear real arithmetic with uninterpreted sort and function symbols.
UFLRA :: Logic
-- | Non-linear integer arithmetic with uninterpreted sort and function
-- symbols.
UFNIA :: Logic
mkSolver :: Context -> IO Solver
mkSimpleSolver :: Context -> IO Solver
mkSolverForLogic :: Context -> Logic -> IO Solver
-- | Return a string describing all solver available parameters.
solverGetHelp :: Context -> Solver -> IO String
-- | Set the given solver using the given parameters.
solverSetParams :: Context -> Solver -> Params -> IO ()
solverPush :: Context -> Solver -> IO ()
solverPop :: Context -> Solver -> Int -> IO ()
solverReset :: Context -> Solver -> IO ()
-- | Number of backtracking points.
solverGetNumScopes :: Context -> Solver -> IO Int
solverAssertCnstr :: Context -> Solver -> AST -> IO ()
solverAssertAndTrack :: Context -> Solver -> AST -> AST -> IO ()
-- | Check whether the assertions in a given solver are consistent or not.
solverCheck :: Context -> Solver -> IO Result
-- | Check whether the assertions in the given solver and optional
-- assumptions are consistent or not.
solverCheckAssumptions :: Context -> Solver -> [AST] -> IO Result
-- | Retrieve the model for the last solverCheck.
--
-- The error handler is invoked if a model is not available because the
-- commands above were not invoked for the given solver, or if the result
-- was Unsat.
solverGetModel :: Context -> Solver -> IO Model
-- | Retrieve the unsat core for the last solverCheckAssumptions;
-- the unsat core is a subset of the assumptions
solverGetUnsatCore :: Context -> Solver -> IO [AST]
-- | Return a brief justification for an Unknown result for the
-- commands solverCheck and solverCheckAssumptions.
solverGetReasonUnknown :: Context -> Solver -> IO String
-- | Convert the given solver into a string.
solverToString :: Context -> Solver -> IO String
solverCheckAndGetModel :: Context -> Solver -> IO (Result, Maybe Model)
instance GHC.Classes.Eq Z3.Base.Fixedpoint
instance GHC.Classes.Ord Z3.Base.Version
instance GHC.Classes.Eq Z3.Base.Version
instance GHC.Show.Show Z3.Base.Z3ErrorCode
instance GHC.Show.Show Z3.Base.ASTKind
instance GHC.Classes.Eq Z3.Base.ASTKind
instance GHC.Show.Show Z3.Base.SortKind
instance GHC.Classes.Eq Z3.Base.SortKind
instance GHC.Show.Show Z3.Base.Result
instance GHC.Read.Read Z3.Base.Result
instance GHC.Classes.Ord Z3.Base.Result
instance GHC.Classes.Eq Z3.Base.Result
instance GHC.Classes.Eq Z3.Base.Solver
instance GHC.Classes.Eq Z3.Base.Params
instance GHC.Classes.Eq Z3.Base.ApplyResult
instance GHC.Classes.Eq Z3.Base.Goal
instance GHC.Classes.Eq Z3.Base.Tactic
instance GHC.Classes.Eq Z3.Base.FuncEntry
instance GHC.Classes.Eq Z3.Base.FuncInterp
instance GHC.Classes.Eq Z3.Base.Model
instance GHC.Show.Show Z3.Base.ConstructorList
instance GHC.Classes.Ord Z3.Base.ConstructorList
instance GHC.Classes.Eq Z3.Base.ConstructorList
instance GHC.Show.Show Z3.Base.Constructor
instance GHC.Classes.Ord Z3.Base.Constructor
instance GHC.Classes.Eq Z3.Base.Constructor
instance GHC.Show.Show Z3.Base.Pattern
instance GHC.Classes.Ord Z3.Base.Pattern
instance GHC.Classes.Eq Z3.Base.Pattern
instance GHC.Show.Show Z3.Base.App
instance GHC.Classes.Ord Z3.Base.App
instance GHC.Classes.Eq Z3.Base.App
instance GHC.Show.Show Z3.Base.FuncDecl
instance GHC.Classes.Ord Z3.Base.FuncDecl
instance GHC.Classes.Eq Z3.Base.FuncDecl
instance GHC.Show.Show Z3.Base.Sort
instance GHC.Classes.Ord Z3.Base.Sort
instance GHC.Classes.Eq Z3.Base.Sort
instance GHC.Show.Show Z3.Base.AST
instance GHC.Classes.Ord Z3.Base.AST
instance GHC.Classes.Eq Z3.Base.AST
instance Foreign.Storable.Storable Z3.Base.Symbol
instance GHC.Show.Show Z3.Base.Symbol
instance GHC.Classes.Ord Z3.Base.Symbol
instance GHC.Classes.Eq Z3.Base.Symbol
instance GHC.Classes.Eq Z3.Base.Context
instance GHC.Classes.Eq Z3.Base.Config
instance GHC.Show.Show Z3.Base.Z3Error
instance GHC.Exception.Exception Z3.Base.Z3Error
instance GHC.Show.Show Z3.Base.Version
instance Z3.Base.Marshal Z3.Base.Fixedpoint (GHC.Ptr.Ptr Z3.Base.C.Z3_fixedpoint)
instance GHC.Show.Show Z3.Base.Logic
instance Z3.Base.Marshal h (GHC.Ptr.Ptr x) => Z3.Base.Marshal (GHC.Base.Maybe h) (GHC.Ptr.Ptr x)
instance Z3.Base.Marshal () ()
instance Z3.Base.Marshal GHC.Types.Bool Z3.Base.C.Z3_bool
instance Z3.Base.Marshal Z3.Base.Result Z3.Base.C.Z3_lbool
instance GHC.Real.Integral h => Z3.Base.Marshal h Foreign.C.Types.CInt
instance GHC.Real.Integral h => Z3.Base.Marshal h Foreign.C.Types.CUInt
instance GHC.Real.Integral h => Z3.Base.Marshal h Foreign.C.Types.CLLong
instance GHC.Real.Integral h => Z3.Base.Marshal h Foreign.C.Types.CULLong
instance Z3.Base.Marshal GHC.Types.Double Foreign.C.Types.CDouble
instance Z3.Base.Marshal GHC.Base.String Foreign.C.String.CString
instance Z3.Base.Marshal Z3.Base.App (GHC.Ptr.Ptr Z3.Base.C.Z3_app)
instance Z3.Base.Marshal Z3.Base.Params (GHC.Ptr.Ptr Z3.Base.C.Z3_params)
instance Z3.Base.Marshal Z3.Base.Symbol (GHC.Ptr.Ptr Z3.Base.C.Z3_symbol)
instance Z3.Base.Marshal Z3.Base.AST (GHC.Ptr.Ptr Z3.Base.C.Z3_ast)
instance Z3.Base.Marshal [Z3.Base.AST] (GHC.Ptr.Ptr Z3.Base.C.Z3_ast_vector)
instance Z3.Base.Marshal Z3.Base.Sort (GHC.Ptr.Ptr Z3.Base.C.Z3_sort)
instance Z3.Base.Marshal Z3.Base.FuncDecl (GHC.Ptr.Ptr Z3.Base.C.Z3_func_decl)
instance Z3.Base.Marshal Z3.Base.FuncEntry (GHC.Ptr.Ptr Z3.Base.C.Z3_func_entry)
instance Z3.Base.Marshal Z3.Base.FuncInterp (GHC.Ptr.Ptr Z3.Base.C.Z3_func_interp)
instance Z3.Base.Marshal Z3.Base.Model (GHC.Ptr.Ptr Z3.Base.C.Z3_model)
instance Z3.Base.Marshal Z3.Base.Pattern (GHC.Ptr.Ptr Z3.Base.C.Z3_pattern)
instance Z3.Base.Marshal Z3.Base.Constructor (GHC.Ptr.Ptr Z3.Base.C.Z3_constructor)
instance Z3.Base.Marshal Z3.Base.ConstructorList (GHC.Ptr.Ptr Z3.Base.C.Z3_constructor_list)
instance Z3.Base.Marshal Z3.Base.Solver (GHC.Ptr.Ptr Z3.Base.C.Z3_solver)
instance Z3.Base.Marshal Z3.Base.Tactic (GHC.Ptr.Ptr Z3.Base.C.Z3_tactic)
instance Z3.Base.Marshal Z3.Base.ApplyResult (GHC.Ptr.Ptr Z3.Base.C.Z3_apply_result)
instance Z3.Base.Marshal Z3.Base.Goal (GHC.Ptr.Ptr Z3.Base.C.Z3_goal)
-- | Configuring Z3.
--
-- Z3 has plenty of configuration options and these had varied quite a
-- lot from Z3 3.x to Z3 4.x. We decided to keep things simple.
--
-- Configurations are essentially sets of String pairs, assigning
-- values to parameters. We just provide a thin layer of abstraction on
-- top of this.
--
-- For instance, opt "proof" True creates a configuration where
-- proof generation is enabled. The first argument of opt is the
-- option name, the second is the option value. The same configuration is
-- created by opt "proof" "true". We do not check option names,
-- and we do not assign types to options ---any String is accepted
-- as a value. The OptValue class is a specialization of
-- Show to convert Haskell values into a proper String
-- representation for Z3.
--
-- Configurations can be combined with the +? operator, for
-- instance, opt "proof" True +? opt "model" True is a
-- configuration with both proof and model generation enabled.
-- Configurations are Monoids, and +? is just an alias for
-- mappend.
--
-- Configurations are set by setOpts if you are using
-- Z3.Base, or passing the configuration object (of type
-- Opts) to a runner if you are using the Z3.Monad
-- interface.
module Z3.Opts
-- | Z3 configuration.
data Opts
-- | Set configuration.
--
-- If you are using the Monad interface, you don't need to call
-- this function directly, just pass your Opts to evalZ3*
-- functions.
setOpts :: Config -> Opts -> IO ()
-- | Default configuration.
stdOpts :: Opts
-- | Append configurations.
(+?) :: Opts -> Opts -> Opts
-- | Set a configuration option.
opt :: OptValue val => String -> val -> Opts
-- | Values for Z3 options.
--
-- Any OptValue type can be passed to a Z3 option (and values will
-- be converted into an appropriate String).
--
-- Since 0.4 the Double instance has been replaced by a new
-- Fixed instance.
class OptValue val
instance GHC.Base.Monoid Z3.Opts.Opts
instance Z3.Opts.OptValue GHC.Types.Bool
instance Z3.Opts.OptValue GHC.Types.Int
instance Z3.Opts.OptValue GHC.Integer.Type.Integer
instance Data.Fixed.HasResolution a => Z3.Opts.OptValue (Data.Fixed.Fixed a)
instance Z3.Opts.OptValue [GHC.Types.Char]
-- | A simple monadic interface to Z3 API.
--
-- Examples:
-- https://bitbucket.org/iago/z3-haskell/src/tip/examples/Example/Monad
module Z3.Monad
class (Applicative m, Monad m, MonadIO m) => MonadZ3 m
getSolver :: MonadZ3 m => m Solver
getContext :: MonadZ3 m => m Context
data Z3 a
-- | Solvers available in Z3.
--
-- These are described at http://smtlib.cs.uiowa.edu/logics.html
data Logic
-- | Closed formulas over the theory of linear integer arithmetic and
-- arrays extended with free sort and function symbols but restricted to
-- arrays with integer indices and values.
AUFLIA :: Logic
-- | Closed linear formulas with free sort and function symbols over one-
-- and two-dimentional arrays of integer index and real value.
AUFLIRA :: Logic
-- | Closed formulas with free function and predicate symbols over a theory
-- of arrays of arrays of integer index and real value.
AUFNIRA :: Logic
-- | Closed linear formulas in linear real arithmetic.
LRA :: Logic
-- | Closed quantifier-free formulas over the theory of bitvectors and
-- bitvector arrays.
QF_ABV :: Logic
-- | Closed quantifier-free formulas over the theory of bitvectors and
-- bitvector arrays extended with free sort and function symbols.
QF_AUFBV :: Logic
-- | Closed quantifier-free linear formulas over the theory of integer
-- arrays extended with free sort and function symbols.
QF_AUFLIA :: Logic
-- | Closed quantifier-free formulas over the theory of arrays with
-- extensionality.
QF_AX :: Logic
-- | Closed quantifier-free formulas over the theory of fixed-size
-- bitvectors.
QF_BV :: Logic
-- | Difference Logic over the integers. In essence, Boolean combinations
-- of inequations of the form x - y < b where x and y are integer
-- variables and b is an integer constant.
QF_IDL :: Logic
-- | Unquantified linear integer arithmetic. In essence, Boolean
-- combinations of inequations between linear polynomials over integer
-- variables.
QF_LIA :: Logic
-- | Unquantified linear real arithmetic. In essence, Boolean combinations
-- of inequations between linear polynomials over real variables.
QF_LRA :: Logic
-- | Quantifier-free integer arithmetic.
QF_NIA :: Logic
-- | Quantifier-free real arithmetic.
QF_NRA :: Logic
-- | Difference Logic over the reals. In essence, Boolean combinations of
-- inequations of the form x - y < b where x and y are real variables
-- and b is a rational constant.
QF_RDL :: Logic
-- | Unquantified formulas built over a signature of uninterpreted (i.e.,
-- free) sort and function symbols.
QF_UF :: Logic
-- | Unquantified formulas over bitvectors with uninterpreted sort function
-- and symbols.
QF_UFBV :: Logic
-- | Difference Logic over the integers (in essence) but with uninterpreted
-- sort and function symbols.
QF_UFIDL :: Logic
-- | Unquantified linear integer arithmetic with uninterpreted sort and
-- function symbols.
QF_UFLIA :: Logic
-- | Unquantified linear real arithmetic with uninterpreted sort and
-- function symbols.
QF_UFLRA :: Logic
-- | Unquantified non-linear real arithmetic with uninterpreted sort and
-- function symbols.
QF_UFNRA :: Logic
-- | Linear real arithmetic with uninterpreted sort and function symbols.
UFLRA :: Logic
-- | Non-linear integer arithmetic with uninterpreted sort and function
-- symbols.
UFNIA :: Logic
-- | Eval a Z3 script with default configuration options.
evalZ3 :: Z3 a -> IO a
-- | Eval a Z3 script.
evalZ3With :: Maybe Logic -> Opts -> Z3 a -> IO a
-- | Z3 environment.
data Z3Env
-- | Create a new Z3 environment.
newEnv :: Maybe Logic -> Opts -> IO Z3Env
newItpEnv :: Maybe Logic -> Opts -> IO Z3Env
-- | Eval a Z3 script with a given environment.
--
-- Environments may facilitate running many queries under the same
-- logical context.
--
-- Note that an environment may change after each query. If you want to
-- preserve the same environment then use local, as in
-- evalZ3WithEnv env (local query).
evalZ3WithEnv :: Z3 a -> Z3Env -> IO a
-- | A Z3 symbol.
--
-- Used to name types, constants and functions.
data Symbol
-- | A Z3 AST node.
--
-- This is the data-structure used in Z3 to represent terms, formulas and
-- types.
data AST
-- | A kind of AST representing types.
data Sort
-- | A kind of AST representing function symbols.
data FuncDecl
-- | A kind of AST representing constant and function declarations.
data App
-- | A kind of AST representing pattern and multi-patterns to guide
-- quantifier instantiation.
data Pattern
-- | A type contructor for a (recursive) datatype.
data Constructor
-- | A model for the constraints asserted into the logical context.
data Model
-- | A Z3 logical context.
data Context
-- | An interpretation of a function in a model.
data FuncInterp
-- | Representation of the value of a Z3_func_interp at a particular
-- point.
data FuncEntry
-- | A Z3 parameter set.
--
-- Starting at Z3 4.0, parameter sets are used to configure many
-- components such as: simplifiers, tactics, solvers, etc.
data Params
-- | A Z3 solver engine.
--
-- A(n) (incremental) solver, possibly specialized by a particular tactic
-- or logic.
data Solver
-- | Different kinds of Z3 types.
data SortKind
Z3_UNINTERPRETED_SORT :: SortKind
Z3_BOOL_SORT :: SortKind
Z3_INT_SORT :: SortKind
Z3_REAL_SORT :: SortKind
Z3_BV_SORT :: SortKind
Z3_ARRAY_SORT :: SortKind
Z3_DATATYPE_SORT :: SortKind
Z3_RELATION_SORT :: SortKind
Z3_FINITE_DOMAIN_SORT :: SortKind
Z3_FLOATING_POINT_SORT :: SortKind
Z3_ROUNDING_MODE_SORT :: SortKind
Z3_UNKNOWN_SORT :: SortKind
-- | Different kinds of Z3 AST nodes.
data ASTKind
Z3_NUMERAL_AST :: ASTKind
Z3_APP_AST :: ASTKind
Z3_VAR_AST :: ASTKind
Z3_QUANTIFIER_AST :: ASTKind
Z3_SORT_AST :: ASTKind
Z3_FUNC_DECL_AST :: ASTKind
Z3_UNKNOWN_AST :: ASTKind
-- | Result of a satisfiability check.
--
-- This corresponds to the z3_lbool type in the C API.
data Result
Sat :: Result
Unsat :: Result
Undef :: Result
-- | Create a Z3 (empty) parameter set.
--
-- Starting at Z3 4.0, parameter sets are used to configure many
-- components such as: simplifiers, tactics, solvers, etc.
mkParams :: MonadZ3 z3 => z3 Params
-- | Add a Boolean parameter k with value v to the parameter
-- set p.
paramsSetBool :: MonadZ3 z3 => Params -> Symbol -> Bool -> z3 ()
-- | Add a unsigned parameter k with value v to the parameter
-- set p.
paramsSetUInt :: MonadZ3 z3 => Params -> Symbol -> Word -> z3 ()
-- | Add a double parameter k with value v to the parameter
-- set p.
paramsSetDouble :: MonadZ3 z3 => Params -> Symbol -> Double -> z3 ()
-- | Add a symbol parameter k with value v to the parameter
-- set p.
paramsSetSymbol :: MonadZ3 z3 => Params -> Symbol -> Symbol -> z3 ()
-- | Convert a parameter set into a string.
--
-- This function is mainly used for printing the contents of a parameter
-- set.
paramsToString :: MonadZ3 z3 => Params -> z3 String
-- | Create a Z3 symbol using an integer.
mkIntSymbol :: (MonadZ3 z3, Integral i) => i -> z3 Symbol
-- | Create a Z3 symbol using a string.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae
mkStringSymbol :: MonadZ3 z3 => String -> z3 Symbol
-- | Create a free (uninterpreted) type using the given name (symbol).
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga736e88741af1c178cbebf94c49aa42de
mkUninterpretedSort :: MonadZ3 z3 => Symbol -> z3 Sort
-- | Create the boolean type.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342
mkBoolSort :: MonadZ3 z3 => z3 Sort
-- | Create the integer type.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015
mkIntSort :: MonadZ3 z3 => z3 Sort
-- | Create the real type.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0
mkRealSort :: MonadZ3 z3 => z3 Sort
-- | Create a bit-vector type of the given size.
--
-- This type can also be seen as a machine integer.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeed000a1bbb84b6ca6fdaac6cf0c1688
mkBvSort :: MonadZ3 z3 => Int -> z3 Sort
-- | Create an array type
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafe617994cce1b516f46128e448c84445
mkArraySort :: MonadZ3 z3 => Sort -> Sort -> z3 Sort
-- | Create a tuple type
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7156b9c0a76a28fae46c81f8e3cdf0f1
mkTupleSort :: MonadZ3 z3 => Symbol -> [(Symbol, Sort)] -> z3 (Sort, FuncDecl, [FuncDecl])
-- | Create a contructor
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa779e39f7050b9d51857887954b5f9b0
mkConstructor :: MonadZ3 z3 => Symbol -> Symbol -> [(Symbol, Maybe Sort, Int)] -> z3 Constructor
-- | Create datatype, such as lists, trees, records, enumerations or unions
-- of records. The datatype may be recursive. Return the datatype sort.
--
-- Reference
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab6809d53327d807da9158abdf75df387
mkDatatype :: MonadZ3 z3 => Symbol -> [Constructor] -> z3 Sort
-- | Create mutually recursive datatypes, such as a tree and forest.
--
-- Returns the datatype sorts
mkDatatypes :: MonadZ3 z3 => [Symbol] -> [[Constructor]] -> z3 [Sort]
-- | Create a set type
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6865879523e7e882d7e50a2d8445ac8b
mkSetSort :: MonadZ3 z3 => Sort -> z3 Sort
-- | A Z3 function
mkFuncDecl :: MonadZ3 z3 => Symbol -> [Sort] -> Sort -> z3 FuncDecl
-- | Create a constant or function application.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga33a202d86bf628bfab9b6f437536cebe
mkApp :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST
-- | Declare and create a constant.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef
mkConst :: MonadZ3 z3 => Symbol -> Sort -> z3 AST
-- | Declare and create a constant.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef
mkFreshConst :: MonadZ3 z3 => String -> Sort -> z3 AST
-- | Declare a fresh constant or function.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1f60c7eb41c5603e55a188a14dc929ec
mkFreshFuncDecl :: MonadZ3 z3 => String -> [Sort] -> Sort -> z3 FuncDecl
-- | Declare and create a variable (aka constant).
--
-- An alias for mkConst.
mkVar :: MonadZ3 z3 => Symbol -> Sort -> z3 AST
-- | Declarate and create a variable of sort bool.
--
-- See mkVar.
mkBoolVar :: MonadZ3 z3 => Symbol -> z3 AST
-- | Declarate and create a variable of sort real.
--
-- See mkVar.
mkRealVar :: MonadZ3 z3 => Symbol -> z3 AST
-- | Declarate and create a variable of sort int.
--
-- See mkVar.
mkIntVar :: MonadZ3 z3 => Symbol -> z3 AST
-- | Declarate and create a variable of sort bit-vector.
--
-- See mkVar.
mkBvVar :: MonadZ3 z3 => Symbol -> Int -> z3 AST
-- | Declare and create a fresh variable (aka constant).
--
-- An alias for mkFreshConst.
mkFreshVar :: MonadZ3 z3 => String -> Sort -> z3 AST
-- | Declarate and create a fresh variable of sort bool.
--
-- See mkFreshVar.
mkFreshBoolVar :: MonadZ3 z3 => String -> z3 AST
-- | Declarate and create a fresh variable of sort real.
--
-- See mkFreshVar.
mkFreshRealVar :: MonadZ3 z3 => String -> z3 AST
-- | Declarate and create a fresh variable of sort int.
--
-- See mkFreshVar.
mkFreshIntVar :: MonadZ3 z3 => String -> z3 AST
-- | Declarate and create a fresh variable of sort
-- bit-vector.
--
-- See mkFreshVar.
mkFreshBvVar :: MonadZ3 z3 => String -> Int -> z3 AST
-- | Create an AST node representing true.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7
mkTrue :: MonadZ3 z3 => z3 AST
-- | Create an AST node representing false.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5952ac17671117a02001fed6575c778d
mkFalse :: MonadZ3 z3 => z3 AST
-- | Create an AST node representing l = r.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95a19ce675b70e22bb0401f7137af37c
mkEq :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create an AST node representing not(a).
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3329538091996eb7b3dc677760a61072
mkNot :: MonadZ3 z3 => AST -> z3 AST
-- | Create an AST node representing an if-then-else: ite(t1, t2,
-- t3).
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547
mkIte :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
-- | Create an AST node representing t1 iff t2.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga930a8e844d345fbebc498ac43a696042
mkIff :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create an AST node representing t1 implies t2.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac829c0e25bbbd30343bf073f7b524517
mkImplies :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create an AST node representing t1 xor t2.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec
mkXor :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create an AST node representing args[0] and ... and args[num_args-1].
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacde98ce4a8ed1dde50b9669db4838c61
mkAnd :: MonadZ3 z3 => [AST] -> z3 AST
-- | Create an AST node representing args[0] or ... or args[num_args-1].
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga00866d16331d505620a6c515302021f9
mkOr :: MonadZ3 z3 => [AST] -> z3 AST
-- | The distinct construct is used for declaring the arguments pairwise
-- distinct.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa076d3a668e0ec97d61744403153ecf7
mkDistinct :: MonadZ3 z3 => [AST] -> z3 AST
-- | Create an AST node representing the given boolean.
mkBool :: MonadZ3 z3 => Bool -> z3 AST
-- | Create an AST node representing args[0] + ... + args[num_args-1].
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5
mkAdd :: MonadZ3 z3 => [AST] -> z3 AST
-- | Create an AST node representing args[0] * ... * args[num_args-1].
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab9affbf8401a18eea474b59ad4adc890
mkMul :: MonadZ3 z3 => [AST] -> z3 AST
-- | Create an AST node representing args[0] - ... - args[num_args - 1].
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9
mkSub :: MonadZ3 z3 => [AST] -> z3 AST
-- | Create an AST node representing -arg.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadcd2929ad732937e25f34277ce4988ea
mkUnaryMinus :: MonadZ3 z3 => AST -> z3 AST
-- | Create an AST node representing arg1 div arg2.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3
mkDiv :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create an AST node representing arg1 mod arg2.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713
mkMod :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create an AST node representing arg1 rem arg2.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff
mkRem :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create less than.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534
mkLt :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create less than or equal to.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bf
mkLe :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create greater than.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46167b86067586bb742c0557d7babfd3
mkGt :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create greater than or equal to.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad9245cbadb80b192323d01a8360fb942
mkGe :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Coerce an integer to a real.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21
mkInt2Real :: MonadZ3 z3 => AST -> z3 AST
-- | Coerce a real to an integer.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga759b6563ba1204aae55289009a3fdc6d
mkReal2Int :: MonadZ3 z3 => AST -> z3 AST
-- | Check if a real number is an integer.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3
mkIsInt :: MonadZ3 z3 => AST -> z3 AST
-- | Bitwise negation.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga36cf75c92c54c1ca633a230344f23080
mkBvnot :: MonadZ3 z3 => AST -> z3 AST
-- | Take conjunction of bits in vector, return vector of length 1.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaccc04f2b58903279b1b3be589b00a7d8
mkBvredand :: MonadZ3 z3 => AST -> z3 AST
-- | Take disjunction of bits in vector, return vector of length 1.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafd18e127c0586abf47ad9cd96895f7d2
mkBvredor :: MonadZ3 z3 => AST -> z3 AST
-- | Bitwise and.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab96e0ea55334cbcd5a0e79323b57615d
mkBvand :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Bitwise or.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga77a6ae233fb3371d187c6d559b2843f5
mkBvor :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Bitwise exclusive-or.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a3821ea00b1c762205f73e4bc29e7d8
mkBvxor :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Bitwise nand.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga96dc37d36efd658fff5b2b4df49b0e61
mkBvnand :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Bitwise nor.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabf15059e9e8a2eafe4929fdfd259aadb
mkBvnor :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Bitwise xnor.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga784f5ca36a4b03b93c67242cc94b21d6
mkBvxnor :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Standard two's complement unary minus.
--
-- Reference:
-- <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0c78be00c03eda4ed6a983224ed5c7b7
mkBvneg :: MonadZ3 z3 => AST -> z3 AST
-- | Standard two's complement addition.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga819814e33573f3f9948b32fdc5311158
mkBvadd :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Standard two's complement subtraction.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga688c9aa1347888c7a51be4e46c19178e
mkBvsub :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Standard two's complement multiplication.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6abd3dde2a1ceff1704cf7221a72258c
mkBvmul :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Unsigned division.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga56ce0cd61666c6f8cf5777286f590544
mkBvudiv :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Two's complement signed division.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad240fedb2fda1c1005b8e9d3c7f3d5a0
mkBvsdiv :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Unsigned remainder.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5df4298ec835e43ddc9e3e0bae690c8d
mkBvurem :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Two's complement signed remainder (sign follows dividend).
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46c18a3042fca174fe659d3185693db1
mkBvsrem :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Two's complement signed remainder (sign follows divisor).
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95dac8e6eecb50f63cb82038560e0879
mkBvsmod :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Unsigned less than.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5774b22e93abcaf9b594672af6c7c3c4
mkBvult :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Two's complement signed less than.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8ce08af4ed1fbdf08d4d6e63d171663a
mkBvslt :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Unsigned less than or equal to.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab738b89de0410e70c089d3ac9e696e87
mkBvule :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Two's complement signed less than or equal to.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab7c026feb93e7d2eab180e96f1e6255d
mkBvsle :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Unsigned greater than or equal to.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gade58fbfcf61b67bf8c4a441490d3c4df
mkBvuge :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Two's complement signed greater than or equal to.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeec3414c0e8a90a6aa5a23af36bf6dc5
mkBvsge :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Unsigned greater than.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga063ab9f16246c99e5c1c893613927ee3
mkBvugt :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Two's complement signed greater than.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e93a985aa2a7812c7c11a2c65d7c5f0
mkBvsgt :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Concatenate the given bit-vectors.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae774128fa5e9ff7458a36bd10e6ca0fa
mkConcat :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Extract the bits high down to low from a bitvector of size m to yield
-- a new bitvector of size n, where n = high - low + 1.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga32d2fe7563f3e6b114c1b97b205d4317
mkExtract :: MonadZ3 z3 => Int -> Int -> AST -> z3 AST
-- | Sign-extend of the given bit-vector to the (signed) equivalent
-- bitvector of size m+i, where m is the size of the given
-- bit-vector.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad29099270b36d0680bb54b560353c10e
mkSignExt :: MonadZ3 z3 => Int -> AST -> z3 AST
-- | Extend the given bit-vector with zeros to the (unsigned) equivalent
-- bitvector of size m+i, where m is the size of the given
-- bit-vector.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac9322fae11365a78640baf9078c428b3
mkZeroExt :: MonadZ3 z3 => Int -> AST -> z3 AST
-- | Repeat the given bit-vector up length i.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga03e81721502ea225c264d1f556c9119d
mkRepeat :: MonadZ3 z3 => Int -> AST -> z3 AST
-- | Shift left.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8d5e776c786c1172fa0d7dfede454e1
mkBvshl :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Logical shift right.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac59645a6edadad79a201f417e4e0c512
mkBvlshr :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Arithmetic shift right.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga674b580ad605ba1c2c9f9d3748be87c4
mkBvashr :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Rotate bits of t1 to the left i times.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4932b7d08fea079dd903cd857a52dcda
mkRotateLeft :: MonadZ3 z3 => Int -> AST -> z3 AST
-- | Rotate bits of t1 to the right i times.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3b94e1bf87ecd1a1858af8ebc1da4a1c
mkRotateRight :: MonadZ3 z3 => Int -> AST -> z3 AST
-- | Rotate bits of t1 to the left t2 times.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf46f1cb80e5a56044591a76e7c89e5e7
mkExtRotateLeft :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Rotate bits of t1 to the right t2 times.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabb227526c592b523879083f12aab281f
mkExtRotateRight :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create an n bit bit-vector from the integer argument t1.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga35f89eb05df43fbd9cce7200cc1f30b5
mkInt2bv :: MonadZ3 z3 => Int -> AST -> z3 AST
-- | Create an integer from the bit-vector argument t1. If
-- is_signed is false, then the bit-vector t1 is treated as
-- unsigned. So the result is non-negative and in the range
-- [0..2^N-1], where N are the number of bits in t1.
-- If is_signed is true, t1 is treated as a signed
-- bit-vector.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac87b227dc3821d57258d7f53a28323d4
mkBv2int :: MonadZ3 z3 => AST -> Bool -> z3 AST
-- | Check that bit-wise negation does not overflow when t1 is
-- interpreted as a signed bit-vector.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae9c5d72605ddcd0e76657341eaccb6c7
mkBvnegNoOverflow :: MonadZ3 z3 => AST -> z3 AST
-- | Create a predicate that checks that the bit-wise addition of t1
-- and t2 does not overflow.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga88f6b5ec876f05e0d7ba51e96c4b077f
mkBvaddNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST
-- | Create a predicate that checks that the bit-wise signed addition of
-- t1 and t2 does not underflow.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1e2b1927cf4e50000c1600d47a152947
mkBvaddNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create a predicate that checks that the bit-wise signed subtraction of
-- t1 and t2 does not overflow.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga785f8127b87e0b42130e6d8f52167d7c
mkBvsubNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create a predicate that checks that the bit-wise subtraction of
-- t1 and t2 does not underflow.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6480850f9fa01e14aea936c88ff184c4
mkBvsubNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create a predicate that checks that the bit-wise multiplication of
-- t1 and t2 does not overflow.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga86f4415719d295a2f6845c70b3aaa1df
mkBvmulNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST
-- | Create a predicate that checks that the bit-wise signed multiplication
-- of t1 and t2 does not underflow.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga501ccc01d737aad3ede5699741717fda
mkBvmulNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create a predicate that checks that the bit-wise signed division of
-- t1 and t2 does not overflow.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa17e7b2c33dfe2abbd74d390927ae83e
mkBvsdivNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Array read. The argument a is the array and i is the index of the
-- array that gets read.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga38f423f3683379e7f597a7fe59eccb67
mkSelect :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Array update.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae305a4f54b4a64f7e5973ae6ccb13593
mkStore :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
-- | Create the constant array.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga84ea6f0c32b99c70033feaa8f00e8f2d
mkConstArray :: MonadZ3 z3 => Sort -> AST -> z3 AST
-- | map f on the the argument arrays.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9150242d9430a8c3d55d2ca3b9a4362d
mkMap :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST
-- | Access the array default value. Produces the default range value, for
-- arrays that can be represented as finite maps with a default range
-- value.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga78e89cca82f0ab4d5f4e662e5e5fba7d
mkArrayDefault :: MonadZ3 z3 => AST -> z3 AST
-- | Create the empty set.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga358b6b80509a567148f1c0ca9252118c
mkEmptySet :: MonadZ3 z3 => Sort -> z3 AST
-- | Create the full set.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5e92662c657374f7332aa32ce4503dd2
mkFullSet :: MonadZ3 z3 => Sort -> z3 AST
-- | Add an element to a set.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga856c3d0e28ce720f53912c2bbdd76175
mkSetAdd :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Remove an element from a set.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga80e883f39dd3b88f9d0745c8a5b91d1d
mkSetDel :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Take the union of a list of sets.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4050162a13d539b8913200963bb4743c
mkSetUnion :: MonadZ3 z3 => [AST] -> z3 AST
-- | Take the intersection of a list of sets.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8a8abff0ebe6aeeaa6c919eaa013049d
mkSetIntersect :: MonadZ3 z3 => [AST] -> z3 AST
-- | Take the set difference between two sets.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabb49c62f70b8198362e1a29ba6d8bde1
mkSetDifference :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Take the complement of a set.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5c57143c9229cdf730c5103ff696590f
mkSetComplement :: MonadZ3 z3 => AST -> z3 AST
-- | Check for set membership.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac6e516f3dce0bdd41095c6d6daf56063
mkSetMember :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Check if the first set is a subset of the second set.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga139c5803af0e86464adc7cedc53e7f3a
mkSetSubset :: MonadZ3 z3 => AST -> AST -> z3 AST
-- | Create a numeral of a given sort.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8aca397e32ca33618d8024bff32948c
mkNumeral :: MonadZ3 z3 => String -> Sort -> z3 AST
-- | Create a numeral of an int, bit-vector, or finite-domain sort.
--
-- This function can be use to create numerals that fit in a machine
-- integer. It is slightly faster than mkNumeral since it is
-- not necessary to parse a string.
mkInt :: MonadZ3 z3 => Int -> Sort -> z3 AST
-- | Create a numeral of sort real.
mkReal :: MonadZ3 z3 => Int -> Int -> z3 AST
-- | Create a numeral of an int, bit-vector, or finite-domain sort.
--
-- This function can be use to create numerals that fit in a machine
-- unsigned integer. It is slightly faster than mkNumeral
-- since it is not necessary to parse a string.
mkUnsignedInt :: MonadZ3 z3 => Word -> Sort -> z3 AST
-- | Create a numeral of an int, bit-vector, or finite-domain sort.
--
-- This function can be use to create numerals that fit in a machine
-- 64-bit integer. It is slightly faster than mkNumeral since
-- it is not necessary to parse a string.
mkInt64 :: MonadZ3 z3 => Int64 -> Sort -> z3 AST
-- | Create a numeral of an int, bit-vector, or finite-domain sort.
--
-- This function can be use to create numerals that fit in a machine
-- unsigned 64-bit integer. It is slightly faster than
-- mkNumeral since it is not necessary to parse a string.
mkUnsignedInt64 :: MonadZ3 z3 => Word64 -> Sort -> z3 AST
-- | Create a numeral of an int, bit-vector, or finite-domain sort.
mkIntegral :: (MonadZ3 z3, Integral a) => a -> Sort -> z3 AST
-- | Create a numeral of sort real from a Rational.
mkRational :: MonadZ3 z3 => Rational -> z3 AST
-- | Create a numeral of sort real from a Fixed.
mkFixed :: (MonadZ3 z3, HasResolution a) => Fixed a -> z3 AST
-- | Create a numeral of sort real from a Real.
mkRealNum :: (MonadZ3 z3, Real r) => r -> z3 AST
-- | Create a numeral of sort int from an Integer.
mkInteger :: MonadZ3 z3 => Integer -> z3 AST
-- | Create a numeral of sort int from an Integral.
mkIntNum :: (MonadZ3 z3, Integral a) => a -> z3 AST
-- | Create a numeral of sort Bit-vector from an Integer.
mkBitvector :: MonadZ3 z3 => Int -> Integer -> z3 AST
-- | Create a numeral of sort Bit-vector from an Integral.
mkBvNum :: (MonadZ3 z3, Integral i) => Int -> i -> z3 AST
mkPattern :: MonadZ3 z3 => [AST] -> z3 Pattern
mkBound :: MonadZ3 z3 => Int -> Sort -> z3 AST
mkForall :: MonadZ3 z3 => [Pattern] -> [Symbol] -> [Sort] -> AST -> z3 AST
mkExists :: MonadZ3 z3 => [Pattern] -> [Symbol] -> [Sort] -> AST -> z3 AST
mkForallConst :: MonadZ3 z3 => [Pattern] -> [App] -> AST -> z3 AST
mkExistsConst :: MonadZ3 z3 => [Pattern] -> [App] -> AST -> z3 AST
-- | Return the symbol name.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf1683d9464f377e5089ce6ebf2a9bd31
getSymbolString :: MonadZ3 z3 => Symbol -> z3 String
-- | Return the sort kind.
--
-- Reference:
-- http://z3prover.github.io/api/html/group__capi.html#gacd85d48842c7bfaa696596d16875681a
getSortKind :: MonadZ3 z3 => Sort -> z3 SortKind
-- | Return the size of the given bit-vector sort.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8fc3550edace7bc046e16d1f96ddb419
getBvSortSize :: MonadZ3 z3 => Sort -> z3 Int
-- | Get list of constructors for datatype.
getDatatypeSortConstructors :: MonadZ3 z3 => Sort -> z3 [FuncDecl]
-- | Get list of recognizers for datatype.
getDatatypeSortRecognizers :: MonadZ3 z3 => Sort -> z3 [FuncDecl]
-- | Get list of accessors for datatype.
getDatatypeSortConstructorAccessors :: MonadZ3 z3 => Sort -> z3 [[FuncDecl]]
-- | Return the constant declaration name as a symbol.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga741b1bf11cb92aa2ec9ef2fef73ff129
getDeclName :: MonadZ3 z3 => FuncDecl -> z3 Symbol
-- | Returns the number of parameters of the given declaration
getArity :: MonadZ3 z3 => FuncDecl -> z3 Int
-- | Returns the sort of the i-th parameter of the given function
-- declaration
getDomain :: MonadZ3 z3 => FuncDecl -> Int -> z3 Sort
-- | Returns the range of the given declaration.
getRange :: MonadZ3 z3 => FuncDecl -> z3 Sort
-- | Convert an app into AST. This is just type casting.
appToAst :: MonadZ3 z3 => App -> z3 AST
-- | Return the declaration of a constant or function application.
getAppDecl :: MonadZ3 z3 => App -> z3 FuncDecl
-- | Return the number of argument of an application. If t is an constant,
-- then the number of arguments is 0.
getAppNumArgs :: MonadZ3 z3 => App -> z3 Int
-- | Return the i-th argument of the given application.
getAppArg :: MonadZ3 z3 => App -> Int -> z3 AST
-- | Return a list of all the arguments of the given application.
getAppArgs :: MonadZ3 z3 => App -> z3 [AST]
-- | Return the sort of an AST node.
getSort :: MonadZ3 z3 => AST -> z3 Sort
getArraySortDomain :: MonadZ3 z3 => Sort -> z3 Sort
getArraySortRange :: MonadZ3 z3 => Sort -> z3 Sort
-- | Returns Just True, Just False, or Nothing
-- for undefined.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4
getBoolValue :: MonadZ3 z3 => AST -> z3 (Maybe Bool)
-- | Return the kind of the given AST.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4c43608feea4cae363ef9c520c239a5c
getAstKind :: MonadZ3 z3 => AST -> z3 ASTKind
-- | Return True if an ast is APP_AST, False otherwise.
isApp :: MonadZ3 z3 => AST -> z3 Bool
-- | Cast AST into an App.
toApp :: MonadZ3 z3 => AST -> z3 App
-- | Return numeral value, as a string of a numeric constant term.
getNumeralString :: MonadZ3 z3 => AST -> z3 String
-- | Simplify the expression.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gada433553406475e5dd6a494ea957844c
simplify :: MonadZ3 z3 => AST -> z3 AST
-- | Simplify the expression using the given parameters.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga34329d4c83ca8c98e18b2884b679008c
simplifyEx :: MonadZ3 z3 => AST -> Params -> z3 AST
getIndexValue :: MonadZ3 z3 => AST -> z3 Int
isQuantifierForall :: MonadZ3 z3 => AST -> z3 Bool
isQuantifierExists :: MonadZ3 z3 => AST -> z3 Bool
getQuantifierWeight :: MonadZ3 z3 => AST -> z3 Int
getQuantifierNumPatterns :: MonadZ3 z3 => AST -> z3 Int
getQuantifierPatternAST :: MonadZ3 z3 => AST -> Int -> z3 AST
getQuantifierPatterns :: MonadZ3 z3 => AST -> z3 [AST]
getQuantifierNumNoPatterns :: MonadZ3 z3 => AST -> z3 Int
getQuantifierNoPatternAST :: MonadZ3 z3 => AST -> Int -> z3 AST
getQuantifierNoPatterns :: MonadZ3 z3 => AST -> z3 [AST]
getQuantifierNumBound :: MonadZ3 z3 => AST -> z3 Int
getQuantifierBoundName :: MonadZ3 z3 => AST -> Int -> z3 Symbol
getQuantifierBoundSort :: MonadZ3 z3 => AST -> Int -> z3 Sort
getQuantifierBoundVars :: MonadZ3 z3 => AST -> z3 [AST]
getQuantifierBody :: MonadZ3 z3 => AST -> z3 AST
-- | Read a Bool value from an AST
getBool :: MonadZ3 z3 => AST -> z3 Bool
-- | Return the integer value
getInt :: MonadZ3 z3 => AST -> z3 Integer
-- | Return rational value
getReal :: MonadZ3 z3 => AST -> z3 Rational
-- | Read the Integer value from an AST of sort
-- bit-vector.
--
-- See mkBv2int.
getBv :: MonadZ3 z3 => AST -> Bool -> z3 Integer
substituteVars :: MonadZ3 z3 => AST -> [AST] -> z3 AST
-- | Evaluate an AST node in the given model.
--
-- The evaluation may fail for the following reasons:
--
--
-- - t contains a quantifier.
-- - the model m is partial.
-- - t is type incorrect.
--
modelEval :: MonadZ3 z3 => Model -> AST -> Bool -> z3 (Maybe AST)
-- | Get array as a list of argument/value pairs, if it is represented as a
-- function (ie, using as-array).
evalArray :: MonadZ3 z3 => Model -> AST -> z3 (Maybe FuncModel)
getConstInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe AST)
-- | Return the interpretation of the function f in the model m. Return
-- NULL, if the model does not assign an interpretation for f. That
-- should be interpreted as: the f does not matter.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafb9cc5eca9564d8a849c154c5a4a8633
getFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncInterp)
hasInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 Bool
numConsts :: MonadZ3 z3 => Model -> z3 Word
numFuncs :: MonadZ3 z3 => Model -> z3 Word
getConstDecl :: MonadZ3 z3 => Model -> Word -> z3 FuncDecl
getFuncDecl :: MonadZ3 z3 => Model -> Word -> z3 FuncDecl
getConsts :: MonadZ3 z3 => Model -> z3 [FuncDecl]
getFuncs :: MonadZ3 z3 => Model -> z3 [FuncDecl]
-- | The (_ as-array f) AST node is a construct for assigning
-- interpretations for arrays in Z3. It is the array such that forall
-- indices i we have that (select (_ as-array f) i) is equal to (f i).
-- This procedure returns Z3_TRUE if the a is an as-array AST node.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4674da67d226bfb16861829b9f129cfa
isAsArray :: MonadZ3 z3 => AST -> z3 Bool
addFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> AST -> z3 FuncInterp
addConstInterp :: MonadZ3 z3 => Model -> FuncDecl -> AST -> z3 ()
-- | Return the function declaration f associated with a (_ as_array f)
-- node.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d9262dc6e79f2aeb23fd4a383589dda
getAsArrayFuncDecl :: MonadZ3 z3 => AST -> z3 FuncDecl
-- | Return the number of entries in the given function interpretation.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2bab9ae1444940e7593729beec279844
funcInterpGetNumEntries :: MonadZ3 z3 => FuncInterp -> z3 Int
-- | Return a "point" of the given function intepretation. It represents
-- the value of f in a particular point.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf157e1e1cd8c0cfe6a21be6370f659da
funcInterpGetEntry :: MonadZ3 z3 => FuncInterp -> Int -> z3 FuncEntry
-- | Return the 'else' value of the given function interpretation.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46de7559826ba71b8488d727cba1fb64
funcInterpGetElse :: MonadZ3 z3 => FuncInterp -> z3 AST
-- | Return the arity (number of arguments) of the given function
-- interpretation.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaca22cbdb6f7787aaae5d814f2ab383d8
funcInterpGetArity :: MonadZ3 z3 => FuncInterp -> z3 Int
-- | Return the value of this point.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9fd65e2ab039aa8e40608c2ecf7084da
funcEntryGetValue :: MonadZ3 z3 => FuncEntry -> z3 AST
-- | Return the number of arguments in a Z3_func_entry object.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga51aed8c5bc4b1f53f0c371312de3ce1a
funcEntryGetNumArgs :: MonadZ3 z3 => FuncEntry -> z3 Int
-- | Return an argument of a Z3_func_entry object.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6fe03fe3c824fceb52766a4d8c2cbeab
funcEntryGetArg :: MonadZ3 z3 => FuncEntry -> Int -> z3 AST
-- | Convert the given model into a string.
modelToString :: MonadZ3 z3 => Model -> z3 String
-- | Alias for modelToString.
showModel :: MonadZ3 z3 => Model -> z3 String
-- | Type of an evaluation function for AST.
--
-- Evaluation may fail (i.e. return Nothing) for a few reasons,
-- see modelEval.
type EvalAst m a = Model -> AST -> m (Maybe a)
-- | An alias for modelEval with model completion enabled.
eval :: MonadZ3 z3 => EvalAst z3 AST
-- | Evaluate an AST node of sort bool in the given model.
--
-- See modelEval and getBool.
evalBool :: MonadZ3 z3 => EvalAst z3 Bool
-- | Evaluate an AST node of sort int in the given model.
--
-- See modelEval and getInt.
evalInt :: MonadZ3 z3 => EvalAst z3 Integer
-- | Evaluate an AST node of sort real in the given model.
--
-- See modelEval and getReal.
evalReal :: MonadZ3 z3 => EvalAst z3 Rational
-- | Evaluate an AST node of sort bit-vector in the given model.
--
-- The flag signed decides whether the bit-vector value is
-- interpreted as a signed or unsigned integer.
--
-- See modelEval and getBv.
evalBv :: MonadZ3 z3 => Bool -> EvalAst z3 Integer
-- | Evaluate a collection of AST nodes in the given model.
evalT :: (MonadZ3 z3, Traversable t) => Model -> t AST -> z3 (Maybe (t AST))
-- | Run a evaluation function on a Traversable data structure of
-- ASTs (e.g. [AST], Vector AST, Maybe
-- AST, etc).
--
-- This a generic version of evalT which can be used in
-- combination with other helpers. For instance, mapEval evalInt
-- can be used to obtain the Integer interpretation of a list of
-- AST of sort int.
mapEval :: (MonadZ3 z3, Traversable t) => EvalAst z3 a -> Model -> t AST -> z3 (Maybe (t a))
-- | The interpretation of a function.
data FuncModel
FuncModel :: [([AST], AST)] -> AST -> FuncModel
-- | Mapping from arguments to values.
[interpMap] :: FuncModel -> [([AST], AST)]
-- | Default value.
[interpElse] :: FuncModel -> AST
-- | Get function as a list of argument/value pairs.
evalFunc :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncModel)
mkTactic :: MonadZ3 z3 => String -> z3 Tactic
andThenTactic :: MonadZ3 z3 => Tactic -> Tactic -> z3 Tactic
orElseTactic :: MonadZ3 z3 => Tactic -> Tactic -> z3 Tactic
skipTactic :: MonadZ3 z3 => z3 Tactic
tryForTactic :: MonadZ3 z3 => Tactic -> Int -> z3 Tactic
mkQuantifierEliminationTactic :: MonadZ3 z3 => z3 Tactic
mkAndInverterGraphTactic :: MonadZ3 z3 => z3 Tactic
applyTactic :: MonadZ3 z3 => Tactic -> Goal -> z3 ApplyResult
getApplyResultNumSubgoals :: MonadZ3 z3 => ApplyResult -> z3 Int
getApplyResultSubgoal :: MonadZ3 z3 => ApplyResult -> Int -> z3 Goal
getApplyResultSubgoals :: MonadZ3 z3 => ApplyResult -> z3 [Goal]
mkGoal :: MonadZ3 z3 => Bool -> Bool -> Bool -> z3 Goal
goalAssert :: MonadZ3 z3 => Goal -> AST -> z3 ()
getGoalSize :: MonadZ3 z3 => Goal -> z3 Int
getGoalFormula :: MonadZ3 z3 => Goal -> Int -> z3 AST
getGoalFormulas :: MonadZ3 z3 => Goal -> z3 [AST]
-- | Pretty-printing mode for converting ASTs to strings. The mode can be
-- one of the following:
--
--
-- - Z3_PRINT_SMTLIB_FULL: Print AST nodes in SMTLIB verbose
-- format.
-- - Z3_PRINT_LOW_LEVEL: Print AST nodes using a low-level format.
-- - Z3_PRINT_SMTLIB_COMPLIANT: Print AST nodes in SMTLIB 1.x compliant
-- format.
-- - Z3_PRINT_SMTLIB2_COMPLIANT: Print AST nodes in SMTLIB 2.x
-- compliant format.
--
data ASTPrintMode
Z3_PRINT_SMTLIB_FULL :: ASTPrintMode
Z3_PRINT_LOW_LEVEL :: ASTPrintMode
Z3_PRINT_SMTLIB2_COMPLIANT :: ASTPrintMode
-- | Set the mode for converting expressions to strings.
setASTPrintMode :: MonadZ3 z3 => ASTPrintMode -> z3 ()
-- | Convert an AST to a string.
astToString :: MonadZ3 z3 => AST -> z3 String
-- | Convert a pattern to a string.
patternToString :: MonadZ3 z3 => Pattern -> z3 String
-- | Convert a sort to a string.
sortToString :: MonadZ3 z3 => Sort -> z3 String
-- | Convert a FuncDecl to a string.
funcDeclToString :: MonadZ3 z3 => FuncDecl -> z3 String
-- | Convert the given benchmark into SMT-LIB formatted string.
--
-- The output format can be configured via setASTPrintMode.
benchmarkToSMTLibString :: MonadZ3 z3 => String -> String -> String -> String -> [AST] -> AST -> z3 String
-- | Parse SMT expressions from a string
--
-- The sort and declaration arguments allow parsing in a context in which
-- variables and functions have already been declared. They are almost
-- never used.
parseSMTLib2String :: MonadZ3 z3 => String -> [Symbol] -> [Sort] -> [Symbol] -> [FuncDecl] -> z3 AST
-- | Parse SMT expressions from a file
--
-- The sort and declaration arguments allow parsing in a context in which
-- variables and functions have already been declared. They are almost
-- never used.
parseSMTLib2File :: MonadZ3 z3 => String -> [Symbol] -> [Sort] -> [Symbol] -> [FuncDecl] -> z3 AST
getParserError :: MonadZ3 z3 => z3 String
-- | Z3 exceptions.
--
-- Z3 errors are re-thrown as Haskell Z3Error exceptions, see
-- Exception.
data Z3Error
Z3Error :: Z3ErrorCode -> String -> Z3Error
[errCode] :: Z3Error -> Z3ErrorCode
[errMsg] :: Z3Error -> String
-- | Z3 error codes.
data Z3ErrorCode
SortError :: Z3ErrorCode
IOB :: Z3ErrorCode
InvalidArg :: Z3ErrorCode
ParserError :: Z3ErrorCode
NoParser :: Z3ErrorCode
InvalidPattern :: Z3ErrorCode
MemoutFail :: Z3ErrorCode
FileAccessError :: Z3ErrorCode
InternalFatal :: Z3ErrorCode
InvalidUsage :: Z3ErrorCode
DecRefError :: Z3ErrorCode
Z3Exception :: Z3ErrorCode
data Version
Version :: !Int -> !Int -> !Int -> !Int -> Version
[z3Major] :: Version -> !Int
[z3Minor] :: Version -> !Int
[z3Build] :: Version -> !Int
[z3Revision] :: Version -> !Int
-- | Return Z3 version number information.
getVersion :: MonadZ3 z3 => z3 Version
data Fixedpoint
fixedpointPush :: MonadFixedpoint z3 => z3 ()
fixedpointPop :: MonadFixedpoint z3 => z3 ()
fixedpointAddRule :: MonadFixedpoint z3 => AST -> Symbol -> z3 ()
fixedpointSetParams :: MonadFixedpoint z3 => Params -> z3 ()
fixedpointRegisterRelation :: MonadFixedpoint z3 => FuncDecl -> z3 ()
fixedpointQueryRelations :: MonadFixedpoint z3 => [FuncDecl] -> z3 Result
fixedpointGetAnswer :: MonadFixedpoint z3 => z3 AST
fixedpointGetAssertions :: MonadFixedpoint z3 => z3 [AST]
-- | Interpolation problem formulation.
data InterpolationProblem
InterpolationProblem :: [AST] -> Maybe [Int] -> [AST] -> InterpolationProblem
[getConstraints] :: InterpolationProblem -> [AST]
[getParents] :: InterpolationProblem -> Maybe [Int]
[getTheoryTerms] :: InterpolationProblem -> [AST]
mkInterpolant :: MonadZ3 z3 => AST -> z3 AST
-- | Generate a Z3 context suitable for generation of interpolants.
mkInterpolationContext :: Config -> IO Context
getInterpolant :: MonadZ3 z3 => AST -> AST -> Params -> z3 [AST]
computeInterpolant :: MonadZ3 z3 => AST -> Params -> z3 (Maybe (Either Model [AST]))
readInterpolationProblem :: MonadZ3 z3 => FilePath -> z3 (Either String InterpolationProblem)
checkInterpolant :: MonadZ3 z3 => InterpolationProblem -> [AST] -> z3 (Result, Maybe String)
interpolationProfile :: MonadZ3 z3 => z3 String
writeInterpolationProblem :: MonadZ3 z3 => FilePath -> InterpolationProblem -> z3 ()
-- | Return a string describing all solver available parameters.
solverGetHelp :: MonadZ3 z3 => z3 String
-- | Set the solver using the given parameters.
solverSetParams :: MonadZ3 z3 => Params -> z3 ()
-- | Create a backtracking point.
solverPush :: MonadZ3 z3 => z3 ()
-- | Backtrack n backtracking points.
solverPop :: MonadZ3 z3 => Int -> z3 ()
solverReset :: MonadZ3 z3 => z3 ()
-- | Number of backtracking points.
solverGetNumScopes :: MonadZ3 z3 => z3 Int
-- | Assert a constraing into the logical context.
--
-- Reference:
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1a05ff73a564ae7256a2257048a4680a
solverAssertCnstr :: MonadZ3 z3 => AST -> z3 ()
-- | Assert a constraint a into the solver, and track it (in the unsat)
-- core using the Boolean constant p.
--
-- This API is an alternative to Z3_solver_check_assumptions for
-- extracting unsat cores. Both APIs can be used in the same solver. The
-- unsat core will contain a combination of the Boolean variables
-- provided using Z3_solver_assert_and_track and the Boolean literals
-- provided using Z3_solver_check_assumptions.
solverAssertAndTrack :: MonadZ3 z3 => AST -> AST -> z3 ()
-- | Check whether the assertions in a given solver are consistent or not.
solverCheck :: MonadZ3 z3 => z3 Result
-- | Check whether the assertions in the given solver and optional
-- assumptions are consistent or not.
solverCheckAssumptions :: MonadZ3 z3 => [AST] -> z3 Result
-- | Retrieve the model for the last solverCheck.
--
-- The error handler is invoked if a model is not available because the
-- commands above were not invoked for the given solver, or if the result
-- was Unsat.
solverGetModel :: MonadZ3 z3 => z3 Model
-- | Retrieve the unsat core for the last solverCheckAssumptions;
-- the unsat core is a subset of the assumptions
solverGetUnsatCore :: MonadZ3 z3 => z3 [AST]
-- | Return a brief justification for an Unknown result for the
-- commands solverCheck and solverCheckAssumptions.
solverGetReasonUnknown :: MonadZ3 z3 => z3 String
-- | Convert the given solver into a string.
solverToString :: MonadZ3 z3 => z3 String
assert :: MonadZ3 z3 => AST -> z3 ()
-- | Check whether the given logical context is consistent or not.
check :: MonadZ3 z3 => z3 Result
-- | Check whether the assertions in the given solver and optional
-- assumptions are consistent or not.
checkAssumptions :: MonadZ3 z3 => [AST] -> z3 Result
solverCheckAndGetModel :: MonadZ3 z3 => z3 (Result, Maybe Model)
-- | Get model.
--
-- Reference :
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaff310fef80ac8a82d0a51417e073ec0a
getModel :: MonadZ3 z3 => z3 (Result, Maybe Model)
-- | Check satisfiability and, if sat, compute a value from the
-- given model.
--
-- E.g. withModel $ \m -> fromJust <$> evalInt m x
withModel :: (Applicative z3, MonadZ3 z3) => (Model -> z3 a) -> z3 (Result, Maybe a)
-- | Retrieve the unsat core for the last checkAssumptions; the
-- unsat core is a subset of the assumptions.
getUnsatCore :: MonadZ3 z3 => z3 [AST]
-- | Create a backtracking point.
--
-- For push; m; pop 1 see local.
push :: MonadZ3 z3 => z3 ()
-- | Backtrack n backtracking points.
--
-- Contrary to solverPop this funtion checks whether n is
-- within the size of the solver scope stack.
pop :: MonadZ3 z3 => Int -> z3 ()
-- | Run a query and restore the initial logical context.
--
-- This is a shorthand for push, run the query, and pop.
local :: MonadZ3 z3 => z3 a -> z3 a
-- | Backtrack all the way.
reset :: MonadZ3 z3 => z3 ()
-- | Get number of backtracking points.
getNumScopes :: MonadZ3 z3 => z3 Int
instance Control.Monad.Fix.MonadFix Z3.Monad.Z3
instance Control.Monad.IO.Class.MonadIO Z3.Monad.Z3
instance GHC.Base.Monad Z3.Monad.Z3
instance GHC.Base.Applicative Z3.Monad.Z3
instance GHC.Base.Functor Z3.Monad.Z3
instance Z3.Monad.MonadZ3 Z3.Monad.Z3
instance Z3.Monad.MonadFixedpoint Z3.Monad.Z3