z3-408.2: Bindings for the Z3 Theorem Prover

Copyright(c) Iago Abal 2012-2014
(c) David Castro 2012-2013
LicenseBSD3
MaintainerIago Abal <mail@iagoabal.eu>, David Castro <david.castro.dcp@gmail.com>
Safe HaskellSafe
LanguageHaskell2010

Z3.Base.C

Contents

Description

Z3 API foreign imports.

Synopsis

Types

Create configuration

Create context

Symbols

Sorts

Constants and Applications

z3_mk_fresh_func_decl :: Ptr z3_context -> Z3_string -> CUInt -> Ptr (Ptr Z3_sort) -> Ptr Z3_sort -> IO (Ptr Z3_func_decl) Source #

Propositional Logic and Equality

Arithmetic: Integers and Reals

Bit-vectors

Arrays

z3_mk_store Source #

Arguments

:: Ptr Z3_context 
-> Ptr Z3_ast

array

-> Ptr Z3_ast

index

-> Ptr Z3_ast

value to store at array[index]

-> IO (Ptr Z3_ast) 

Sets

Numerals

Sequences and regular expressions

z3_mk_seq_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort) Source #

z3_mk_re_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort) Source #

z3_mk_seq_empty :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) Source #

z3_mk_seq_unit :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #

z3_mk_seq_concat :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) Source #

z3_mk_seq_prefix :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #

z3_mk_seq_suffix :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #

z3_mk_seq_contains :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #

z3_mk_seq_extract :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #

z3_mk_seq_replace :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #

z3_mk_seq_at :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #

z3_mk_seq_length :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #

z3_mk_seq_index :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #

z3_mk_str_to_int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #

z3_mk_int_to_str :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #

z3_mk_seq_to_re :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #

z3_mk_seq_in_re :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #

z3_mk_re_plus :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #

z3_mk_re_star :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #

z3_mk_re_option :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #

z3_mk_re_union :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) Source #

z3_mk_re_concat :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) Source #

z3_mk_re_range :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) Source #

z3_mk_re_loop :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> CUInt -> IO (Ptr Z3_ast) Source #

z3_mk_re_intersect :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) Source #

z3_mk_re_empty :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) Source #

z3_mk_re_full :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) Source #

Quantifiers

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) Source #

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) Source #

Accessors

z3_get_app_num_args :: Ptr Z3_context -> Ptr Z3_app -> IO CUInt Source #

z3_get_app_arg :: Ptr Z3_context -> Ptr Z3_app -> CUInt -> IO (Ptr Z3_ast) Source #

Modifiers

AST vectors

Models

Constraints

Parameters

Tactics

Solvers

String Conversion

z3_benchmark_to_smtlib_string Source #

Arguments

:: Ptr Z3_context 
-> Z3_string

name

-> Z3_string

logic

-> Z3_string

status

-> Z3_string

attributes

-> CUInt

assumptions#

-> Ptr (Ptr Z3_ast)

assumptions

-> Ptr Z3_ast

formula

-> IO Z3_string 

Parser Interface

Error Handling

Miscellaneous

z3_get_version :: Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> IO () Source #

Fixedpoint facilities

Optimization facilities

z3_optimize_assert :: Ptr Z3_context -> Ptr Z3_optimize -> Ptr Z3_ast -> IO () Source #

z3_optimize_assert_soft :: Ptr Z3_context -> Ptr Z3_optimize -> Ptr Z3_ast -> Z3_string -> Ptr Z3_symbol -> IO CUInt Source #

z3_optimize_maximize :: Ptr Z3_context -> Ptr Z3_optimize -> Ptr Z3_ast -> IO CUInt Source #

z3_optimize_minimize :: Ptr Z3_context -> Ptr Z3_optimize -> Ptr Z3_ast -> IO CUInt Source #

z3_optimize_check :: Ptr Z3_context -> Ptr Z3_optimize -> CUInt -> Ptr (Ptr Z3_ast) -> IO Z3_lbool Source #

z3_optimize_get_lower :: Ptr Z3_context -> Ptr Z3_optimize -> CUInt -> IO (Ptr Z3_ast) Source #

z3_optimize_get_upper :: Ptr Z3_context -> Ptr Z3_optimize -> CUInt -> IO (Ptr Z3_ast) Source #