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