Z3
Data Structures
Here are the data structures with brief descriptions:
[detail level
1
2
3
]
▼
N
z3
Z3 C++ namespace
C
apply_result
C
array
C
ast
▼
C
ast_vector_tpl
C
iterator
C
cast_ast
C
cast_ast< ast >
C
cast_ast< expr >
C
cast_ast< func_decl >
C
cast_ast< sort >
C
config
Z3 global configuration object
C
context
A Context manages all other Z3 objects, global configuration options, etc
C
exception
Exception used to sign API usage errors
C
expr
A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean. Every expression has a sort
C
fixedpoint
C
func_decl
Function declaration (aka function definition). It is the signature of interpreted and uninterpreted functions in Z3. The basic building block in Z3 is the function application
C
func_entry
C
func_interp
C
goal
▼
C
model
C
translate
C
object
▼
C
optimize
C
handle
C
param_descrs
C
params
C
probe
C
scoped_context
▼
C
solver
C
cube_generator
C
cube_iterator
C
simple
C
translate
C
sort
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort
C
stats
C
symbol
C
tactic
C
user_propagator_base
▼
N
z3py
C
AlgebraicNumRef
C
ApplyResult
C
ArithRef
C
ArithSortRef
Arithmetic
C
ArrayRef
C
ArraySortRef
Arrays
C
AstMap
C
AstRef
C
AstVector
C
BitVecNumRef
C
BitVecRef
C
BitVecSortRef
Bit-Vectors
C
BoolRef
C
BoolSortRef
Booleans
C
CheckSatResult
C
Context
C
Datatype
C
DatatypeRef
C
DatatypeSortRef
C
ExprRef
Expressions
C
FiniteDomainNumRef
C
FiniteDomainRef
C
FiniteDomainSortRef
C
Fixedpoint
Fixedpoint
C
FPNumRef
FP Numerals
C
FPRef
FP Expressions
C
FPRMRef
C
FPRMSortRef
C
FPSortRef
FP Sorts
C
FuncDeclRef
Function Declarations
C
FuncEntry
C
FuncInterp
C
Goal
C
IntNumRef
C
ModelRef
C
Optimize
C
OptimizeObjective
Optimize
C
ParamDescrsRef
C
ParamsRef
Parameter Sets
C
PatternRef
Patterns
C
Probe
C
PropClosures
C
QuantifierRef
Quantifiers
C
RatNumRef
C
ReRef
C
ReSortRef
Regular expressions
C
ScopedConstructor
C
ScopedConstructorList
C
SeqRef
C
SeqSortRef
Strings, Sequences and Regular expressions
C
Solver
C
SortRef
C
Statistics
Statistics
C
Tactic
C
UserPropagateBase
C
Z3PPObject
ASTs base class
Generated on Mon Nov 16 2020 00:00:00 for Z3 by
1.8.20