All Classes and Interfaces

Class	Description
AlgebraicNum	Algebraic numbers
ApplyResult	ApplyResult objects represent the result of an application of a tactic to a goal.
ArithExpr<R extends ArithSort>	Arithmetic expressions (int/real)
ArithSort	An arithmetic sort, i.e., Int or Real.
ArrayExpr<D extends Sort,R extends Sort>	Array expressions
ArraySort<D extends Sort,R extends Sort>	Array sorts.
AST	The abstract syntax tree (AST) class.
ASTVector	Vectors of ASTs.
BitVecExpr	Bit-vector expressions
BitVecNum	Bit-vector numerals
BitVecSort	Bit-vector sorts.
BoolExpr	Boolean expressions
BoolSort	A Boolean sort.
CharSort	A Character sort
Constructor<R>	Constructors are used for datatype sorts.
ConstructorDecRefQueue
ConstructorList<R>	Lists of constructors
ConstructorListDecRefQueue
Context	The main interaction with Z3 happens via the Context.
DatatypeExpr<R extends Sort>	Datatype expressions
DatatypeSort<R>	Datatype sorts.
EnumSort<R>	Enumeration sorts.
Expr<R extends Sort>	Expressions are terms.
FiniteDomainExpr<R>	Finite-domain expressions
FiniteDomainNum<R>	Finite-domain Numerals
FiniteDomainSort<R>	Finite domain sorts.
Fixedpoint	Object for managing fixedpoints
FPExpr	FloatingPoint Expressions
FPNum	FloatingPoint Numerals
FPRMExpr	FloatingPoint RoundingMode Expressions
FPRMNum	FloatingPoint RoundingMode Numerals
FPRMSort	The FloatingPoint RoundingMode sort
FPSort	A FloatingPoint sort
FuncDecl<R extends Sort>	Function declarations.
FuncDecl.Parameter	Function declarations can have Parameters associated with them.
FuncInterp<R extends Sort>	A function interpretation is represented as a finite map and an 'else' value.
FuncInterp.Entry<R extends Sort>	An Entry object represents an element in the finite map used to encode a function interpretation.
Global	Global functions for Z3.
Goal	A goal (aka problem).
IDecRefQueue<T extends Z3Object>	A queue to handle management of native memory.
IntExpr	Int expressions
IntNum	Integer Numerals
IntSort	An Integer sort
IntSymbol	Numbered symbols
Lambda<R extends Sort>	Lambda expressions.
ListSort<R extends Sort>	List sorts.
Log	Interaction logging for Z3.
Model	A Model contains interpretations (assignments) of constants and functions.
Native
Native.IntPtr
Native.LongPtr
Native.ObjArrayPtr
Native.StringPtr
Native.UIntArrayPtr
Optimize	Object for managing optimization context
Optimize.Handle<R extends Sort>	Handle to objectives returned by objective functions.
ParamDescrs	A ParamDescrs describes a set of parameters.
Params	A ParameterSet represents a configuration in the form of Symbol/value pairs.
Pattern	Patterns comprise a list of terms.
Probe	Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used.
Quantifier	Quantifier expressions.
RatNum	Rational Numerals
RealExpr	Real expressions
RealSort	A real sort
ReExpr<R extends Sort>	Re expressions
RelationSort	Relation sorts.
ReSort<R extends Sort>	A Regular expression sort
SeqExpr<R extends Sort>	Seq expressions
SeqSort<R extends Sort>	A Sequence sort
SetSort<D extends Sort>	Set sorts.
Solver	Solvers.
Sort	The Sort class implements type information for ASTs.
Statistics	Objects of this class track statistical information about solvers.
Status	Status values.
StringSymbol	Named symbols
Symbol	Symbols are used to name several term and type constructors.
Tactic	Tactics are the basic building block for creating custom solvers for specific problem domains.
TupleSort	Tuple sorts.
UninterpretedSort	Uninterpreted Sorts
Version	Version information.
Z3_ast_kind	Z3_ast_kind
Z3_ast_print_mode	Z3_ast_print_mode
Z3_decl_kind	Z3_decl_kind
Z3_error_code	Z3_error_code
Z3_goal_prec	Z3_goal_prec
Z3_lbool	Z3_lbool
Z3_param_kind	Z3_param_kind
Z3_parameter_kind	Z3_parameter_kind
Z3_sort_kind	Z3_sort_kind
Z3_symbol_kind	Z3_symbol_kind
Z3Exception	The exception base class for error reporting from Z3
Z3Object	Internal base class for interfacing with native Z3 objects.