Z3
Data Structures
|
Namespaces
|
Functions
|
Variables
doc/tmp/z3py.py File Reference
Go to the source code of this file.
Data Structures
class
Context
class
Z3PPObject
ASTs base class.
More...
class
AstRef
class
SortRef
class
FuncDeclRef
Function Declarations.
More...
class
ExprRef
Expressions.
More...
class
BoolSortRef
Booleans.
More...
class
BoolRef
class
PatternRef
Patterns.
More...
class
QuantifierRef
Quantifiers.
More...
class
ArithSortRef
Arithmetic.
More...
class
ArithRef
class
IntNumRef
class
RatNumRef
class
AlgebraicNumRef
class
BitVecSortRef
Bit-Vectors.
More...
class
BitVecRef
class
BitVecNumRef
class
ArraySortRef
Arrays.
More...
class
ArrayRef
class
Datatype
class
ScopedConstructor
class
ScopedConstructorList
class
DatatypeSortRef
class
DatatypeRef
class
ParamsRef
Parameter Sets.
More...
class
ParamDescrsRef
class
Goal
class
AstVector
class
AstMap
class
FuncEntry
class
FuncInterp
class
ModelRef
class
Statistics
Statistics
.
More...
class
CheckSatResult
class
Solver
class
Fixedpoint
Fixedpoint
.
More...
class
ApplyResult
class
Tactic
class
Probe
Namespaces
namespace
z3py
Functions
def
enable_trace
def
disable_trace
def
get_version_string
def
get_version
def
open_log
def
append_log
def
to_symbol
def
main_ctx
def
set_param
def
reset_params
def
set_option
def
get_param
def
is_ast
def
eq
def
is_sort
def
DeclareSort
def
is_func_decl
def
Function
def
is_expr
def
is_app
def
is_const
def
is_var
def
get_var_index
def
is_app_of
def
If
def
Distinct
def
Const
def
Consts
def
Var
def
RealVar
def
RealVarVector
def
is_bool
def
is_true
def
is_false
def
is_and
def
is_or
def
is_not
def
is_eq
def
is_distinct
def
BoolSort
def
BoolVal
def
Bool
def
Bools
def
BoolVector
def
FreshBool
def
Implies
def
Xor
def
Not
def
And
def
Or
def
is_pattern
def
MultiPattern
def
is_quantifier
def
ForAll
def
Exists
def
is_arith_sort
def
is_arith
def
is_int
def
is_real
def
is_int_value
def
is_rational_value
def
is_algebraic_value
def
is_add
def
is_mul
def
is_sub
def
is_div
def
is_idiv
def
is_mod
def
is_le
def
is_lt
def
is_ge
def
is_gt
def
is_is_int
def
is_to_real
def
is_to_int
def
IntSort
def
RealSort
def
IntVal
def
RealVal
def
RatVal
def
Q
def
Int
def
Ints
def
IntVector
def
FreshInt
def
Real
def
Reals
def
RealVector
def
FreshReal
def
ToReal
def
ToInt
def
IsInt
def
Sqrt
def
Cbrt
def
is_bv_sort
def
is_bv
def
is_bv_value
def
BV2Int
def
BitVecSort
def
BitVecVal
def
BitVec
def
BitVecs
def
Concat
def
Extract
def
ULE
def
ULT
def
UGE
def
UGT
def
UDiv
def
URem
def
SRem
def
LShR
def
RotateLeft
def
RotateRight
def
SignExt
def
ZeroExt
def
RepeatBitVec
def
is_array
def
is_const_array
def
is_K
def
is_map
def
get_map_func
def
ArraySort
def
Array
def
Update
def
Store
def
Select
def
Map
def
K
def
is_select
def
is_store
def
CreateDatatypes
def
EnumSort
def
args2params
def
is_as_array
def
get_as_array_func
def
SolverFor
def
SimpleSolver
def
AndThen
def
Then
def
OrElse
def
ParOr
def
ParThen
def
ParAndThen
def
With
def
Repeat
def
TryFor
def
tactics
def
tactic_description
def
describe_tactics
def
is_probe
def
probes
def
probe_description
def
describe_probes
def
FailIf
def
When
def
Cond
def
simplify
Utils.
def
help_simplify
def
simplify_param_descrs
def
substitute
def
substitute_vars
def
Sum
def
Product
def
solve
def
solve_using
def
prove
def
parse_smt2_string
def
parse_smt2_file
def
Interpolant
def
tree_interpolant
def
binary_interpolant
def
sequence_interpolant
Variables
tuple
_error_handler_fptr
= ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
tuple
_Z3Python_error_handler
= _error_handler_fptr(_Z3python_error_handler_core)
_main_ctx
= None
tuple
sat
= CheckSatResult(
Z3_L_TRUE
)
tuple
unsat
= CheckSatResult(
Z3_L_FALSE
)
tuple
unknown
= CheckSatResult(
Z3_L_UNDEF
)
All
Data Structures
Namespaces
Files
Functions
Variables
Typedefs
Enumerations
Enumerator
Properties
Friends
Defines
Generated on Sat Apr 2 2016 19:31:02 for Z3 by
1.7.6.1