Class Hierarchy
- java.lang.Object
- com.microsoft.z3.Context (implements java.lang.AutoCloseable)
- com.microsoft.z3.FuncDecl.Parameter
- com.microsoft.z3.Global
- com.microsoft.z3.IDecRefQueue<T>
- com.microsoft.z3.ConstructorDecRefQueue
- com.microsoft.z3.ConstructorListDecRefQueue
- com.microsoft.z3.Log
- com.microsoft.z3.Native
- com.microsoft.z3.Native.IntPtr
- com.microsoft.z3.Native.LongPtr
- com.microsoft.z3.Native.ObjArrayPtr
- com.microsoft.z3.Native.StringPtr
- com.microsoft.z3.Native.UIntArrayPtr
- com.microsoft.z3.Optimize.Handle<R>
- com.microsoft.z3.Statistics.Entry
- java.lang.Throwable (implements java.io.Serializable)
- java.lang.Exception
- java.lang.RuntimeException
- com.microsoft.z3.Z3Exception
- com.microsoft.z3.Model.ModelEvaluationFailedException
- com.microsoft.z3.Z3Exception
- java.lang.RuntimeException
- java.lang.Exception
- com.microsoft.z3.Version
- com.microsoft.z3.Z3Object
- com.microsoft.z3.ApplyResult
- com.microsoft.z3.AST (implements java.lang.Comparable<T>)
- com.microsoft.z3.Expr<R>
- com.microsoft.z3.ArithExpr<R>
- com.microsoft.z3.AlgebraicNum
- com.microsoft.z3.IntExpr
- com.microsoft.z3.IntNum
- com.microsoft.z3.RealExpr
- com.microsoft.z3.RatNum
- com.microsoft.z3.ArrayExpr<D,R>
- com.microsoft.z3.Lambda<R>
- com.microsoft.z3.BitVecExpr
- com.microsoft.z3.BitVecNum
- com.microsoft.z3.BoolExpr
- com.microsoft.z3.Quantifier
- com.microsoft.z3.DatatypeExpr<R>
- com.microsoft.z3.FiniteDomainExpr<R>
- com.microsoft.z3.FiniteDomainNum<R>
- com.microsoft.z3.FPExpr
- com.microsoft.z3.FPNum
- com.microsoft.z3.FPRMExpr
- com.microsoft.z3.FPRMNum
- com.microsoft.z3.ReExpr<R>
- com.microsoft.z3.SeqExpr<R>
- com.microsoft.z3.ArithExpr<R>
- com.microsoft.z3.FuncDecl<R>
- com.microsoft.z3.Pattern
- com.microsoft.z3.Sort
- com.microsoft.z3.ArithSort
- com.microsoft.z3.ArraySort<D,R>
- com.microsoft.z3.SetSort<D>
- com.microsoft.z3.BitVecSort
- com.microsoft.z3.BoolSort
- com.microsoft.z3.CharSort
- com.microsoft.z3.DatatypeSort<R>
- com.microsoft.z3.EnumSort<R>
- com.microsoft.z3.FiniteDomainSort<R>
- com.microsoft.z3.FPRMSort
- com.microsoft.z3.FPSort
- com.microsoft.z3.ListSort<R>
- com.microsoft.z3.RelationSort
- com.microsoft.z3.ReSort<R>
- com.microsoft.z3.SeqSort<R>
- com.microsoft.z3.TupleSort
- com.microsoft.z3.UninterpretedSort
- com.microsoft.z3.Expr<R>
- com.microsoft.z3.ASTVector
- com.microsoft.z3.Constructor<R>
- com.microsoft.z3.ConstructorList<R>
- com.microsoft.z3.Fixedpoint
- com.microsoft.z3.FuncInterp<R>
- com.microsoft.z3.FuncInterp.Entry<R>
- com.microsoft.z3.Goal
- com.microsoft.z3.Model
- com.microsoft.z3.Optimize
- com.microsoft.z3.ParamDescrs
- com.microsoft.z3.Params
- com.microsoft.z3.Probe
- com.microsoft.z3.Solver
- com.microsoft.z3.Statistics
- com.microsoft.z3.Symbol
- com.microsoft.z3.IntSymbol
- com.microsoft.z3.StringSymbol
- com.microsoft.z3.Tactic
Enum Hierarchy
- java.lang.Object
- java.lang.Enum<E> (implements java.lang.Comparable<T>, java.io.Serializable)
- com.microsoft.z3.Status
- com.microsoft.z3.enumerations.Z3_ast_kind
- com.microsoft.z3.enumerations.Z3_ast_print_mode
- com.microsoft.z3.enumerations.Z3_decl_kind
- com.microsoft.z3.enumerations.Z3_error_code
- com.microsoft.z3.enumerations.Z3_goal_prec
- com.microsoft.z3.enumerations.Z3_lbool
- com.microsoft.z3.enumerations.Z3_param_kind
- com.microsoft.z3.enumerations.Z3_parameter_kind
- com.microsoft.z3.enumerations.Z3_sort_kind
- com.microsoft.z3.enumerations.Z3_symbol_kind
- java.lang.Enum<E> (implements java.lang.Comparable<T>, java.io.Serializable)