Z3 |

Class Hierarchy

Go to the graphical class hierarchy

This inheritance list is sorted roughly, but not completely, alphabetically:
[detail level 1 2 3 4 5 6]

►C ArithExpr< IntSort > |
►C IntExpr |
C IntNum |
►C ArithExpr< RealSort > |
►C RealExpr |
C RatNum |
C array< T > |
►C ArrayExpr< Sort, R > |
C Lambda< R extends Sort > |
►C ArraySort< D, BoolSort > |
C SetSort< D extends Sort > |
C AstMap |
►C AutoCloseable |
C Context |
C cast_ast< T > |
C cast_ast< ast > |
C cast_ast< expr > |
C cast_ast< func_decl > |
C cast_ast< sort > |
C CheckSatResult |
►C Comparable |
►C AST |
C Expr< R extends Sort > |
C FuncDecl< R extends Sort > |
C Pattern |
►C Sort |
►C ArithSort |
C IntSort |
C RealSort |
C ArraySort< D extends Sort, R extends Sort > |
C BitVecSort |
C BoolSort |
C DatatypeSort< R > |
C EnumSort< R > |
C FPRMSort |
C FPSort |
C FiniteDomainSort< R > |
C ListSort< R extends Sort > |
C ReSort< R extends Sort > |
C RelationSort |
C SeqSort< R extends Sort > |
C TupleSort |
C UninterpretedSort |
C config | Z3 global configuration object
C context | A Context manages all other Z3 objects, global configuration options, etc
C Context |
C solver::cube_generator |
C solver::cube_iterator |
C Datatype |
C Deprecated | The main interaction with Z3 happens via the Context.
C Statistics.Entry |
C Statistics.Entry | Statistical data is organized into pairs of [Key, Entry], where every Entry is either a `DoubleEntry` or a `UIntEntry`
►C Exception |
►C Z3Exception | The exception base class for error reporting from Z3
C Model.ModelEvaluationFailedException | A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model.
►C exception |
C exception | Exception used to sign API usage errors
►C Expr< ArraySort< D, R > > |
C ArrayExpr< D extends Sort, R extends Sort > |
►C Expr< BitVecSort > |
►C BitVecExpr |
C BitVecNum |
►C Expr< BoolSort > |
►C BoolExpr |
C Quantifier |
►C Expr< DatatypeSort< R > > |
C DatatypeExpr< R extends Sort > |
►C Expr< FiniteDomainSort< R > > |
►C FiniteDomainExpr< R > |
C FiniteDomainNum< R > |
►C Expr< FPRMSort > |
►C FPRMExpr |
C FPRMNum |
►C Expr< FPSort > |
►C FPExpr |
C FPNum |
►C Expr< R > |
►C ArithExpr< R extends ArithSort > |
C AlgebraicNum |
►C Expr< ReSort< R > > |
C ReExpr< R extends Sort > |
►C Expr< SeqSort< R > > |
C SeqExpr< R extends Sort > |
C FuncDecl<?> |
C FuncEntry |
C Global |
C Optimize.Handle | Handle to objectives returned by objective functions.
C optimize::handle |
►C IComparable |
►C AST | The abstract syntax tree (AST) class.
►C Expr | Expressions are terms.
►C ArithExpr | Arithmetic expressions (int/real)
C AlgebraicNum | Algebraic numbers
►C IntExpr | Int expressions
C IntNum | Integer Numerals
►C RealExpr | Real expressions
C RatNum | Rational Numerals
►C ArrayExpr | Array expressions
C Lambda | Lambda expressions.
►C BitVecExpr | Bit-vector expressions
C BitVecNum | Bit-vector numerals
►C BoolExpr | Boolean expressions
C Quantifier | Quantifier expressions.
C DatatypeExpr | Datatype expressions
►C FPExpr | FloatingPoint Expressions
C FPNum | FloatiungPoint Numerals
►C FPRMExpr | FloatingPoint RoundingMode Expressions
C FPRMNum | Floating-point rounding mode numerals
►C FiniteDomainExpr | Finite-domain expressions
C FiniteDomainNum | Finite-domain numerals
C ReExpr | Regular expression expressions
C SeqExpr | Sequence expressions
C FuncDecl | Function declarations.
C Pattern | Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than one term, it is also called a multi-pattern.
►C Sort | The Sort class implements type information for ASTs.
►C ArithSort | An arithmetic sort, i.e., Int or Real.
C IntSort | An Integer sort
C RealSort | A real sort
C ArraySort | Array sorts.
C BitVecSort | Bit-vector sorts.
C BoolSort | A Boolean sort.
C DatatypeSort | Datatype sorts.
C EnumSort | Enumeration sorts.
C FPRMSort | The FloatingPoint RoundingMode sort
C FPSort | FloatingPoint sort
C FiniteDomainSort | Finite domain sorts.
C ListSort | List sorts.
C ReSort | A regular expression sort
C RelationSort | Relation sorts.
C SeqSort | A Sequence sort
C SetSort | Set sorts.
C TupleSort | Tuple sorts.
C UninterpretedSort | Uninterpreted Sorts
C IDecRefQueue< T extends Z3Object > |
►C IDecRefQueue | DecRefQueue interface
C DecRefQueueContracts |
C IDecRefQueue< ApplyResult > |
C IDecRefQueue< AST > |
C IDecRefQueue< ASTMap > |
C IDecRefQueue< ASTVector > |
►C IDecRefQueue< Constructor<?> > |
C ConstructorDecRefQueue |
►C IDecRefQueue< ConstructorList<?> > |
C ConstructorListDecRefQueue |
C IDecRefQueue< Fixedpoint > |
C IDecRefQueue< FuncInterp.Entry<?> > |
C IDecRefQueue< FuncInterp<?> > |
C IDecRefQueue< Goal > |
C IDecRefQueue< Model > |
C IDecRefQueue< Optimize > |
C IDecRefQueue< ParamDescrs > |
C IDecRefQueue< Params > |
C IDecRefQueue< Probe > |
C IDecRefQueue< Solver > |
C IDecRefQueue< Statistics > |
C IDecRefQueue< Tactic > |
►C IDisposable |
C Context | The main interaction with Z3 happens via the Context.
►C Z3Object | Internal base class for interfacing with native Z3 objects. Should not be used externally.
C AST | The abstract syntax tree (AST) class.
C ASTVector | Vectors of ASTs.
C ApplyResult | ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced.
C Constructor | Constructors are used for datatype sorts.
C ConstructorList | Lists of constructors
C Fixedpoint | Object for managing fixedpoints
C FuncInterp | A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments.
C FuncInterp.Entry | An Entry object represents an element in the finite map used to encode a function interpretation.
C Goal | A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.
C Model | A Model contains interpretations (assignments) of constants and functions.
C Optimize | Object for managing optimization context
C ParamDescrs | A ParamDescrs describes a set of parameters.
C Params | A Params objects represents a configuration in the form of Symbol/value pairs.
C 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. The complete list of probes may be obtained using the procedures `Context.NumProbes` and `Context.ProbeNames`. It may also be obtained using the command `(help-tactic)` in the SMT 2.0 front-end.
C Solver | Solvers.
C Statistics | Objects of this class track statistical information about solvers.
►C Symbol | Symbols are used to name several term and type constructors.
C IntSymbol | Numbered symbols
C StringSymbol | Named symbols
C Tactic | Tactics are the basic building block for creating custom solvers for specific problem domains. The complete list of tactics may be obtained using `Context.NumTactics` and `Context.TacticNames`. It may also be obtained using the command `(help-tactic)` in the SMT 2.0 front-end.
C ast_vector_tpl< T >::iterator |
C Log |
►C object |
C ast_vector_tpl< expr > |
C apply_result |
►C ast |
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 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 sort | A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort
C ast_vector_tpl< T > |
C fixedpoint |
C func_entry |
C func_interp |
C goal |
C model |
C optimize |
C param_descrs |
C params |
C probe |
C solver |
C stats |
C symbol |
C tactic |
C OptimizeObjective | Optimize
C ParamDescrsRef |
C FuncDecl.Parameter | Function declarations can have Parameters associated with them.
C ParamsRef | Parameter Sets
C Probe |
C PropClosures |
►C RuntimeException |
►C Z3Exception |
C Model.ModelEvaluationFailedException |
C scoped_context |
C ScopedConstructor |
C ScopedConstructorList |
C SeqSort< com.microsoft.z3.BitVecSort > |
C solver::simple |
C Statistics | Statistics
C Status |
C Tactic |
C model::translate |
C solver::translate |
C user_propagator_base |
C UserPropagateBase |
C Version |
►C Z3Object |
C AST |
C ASTVector |
C ApplyResult |
C Constructor< R > |
C ConstructorList< R > |
C Fixedpoint |
C FuncInterp< R extends Sort > |
C Goal |
C Model |
C Optimize |
C ParamDescrs |
C Params |
C Probe |
C Solver |
C Statistics |
►C Symbol |
C IntSymbol |
C StringSymbol |
C Tactic |
►C Z3PPObject | ASTs base class
C ApplyResult |
►C AstRef |
►C ExprRef | Expressions
►C ArithRef |
C AlgebraicNumRef |
C IntNumRef |
C RatNumRef |
C ArrayRef |
►C BitVecRef |
C BitVecNumRef |
►C BoolRef |
C QuantifierRef | Quantifiers
C DatatypeRef |
C FPRMRef |
►C FPRef |
C FPNumRef |
►C FiniteDomainRef |
C FiniteDomainNumRef |
C PatternRef | Patterns
C ReRef |
C SeqRef |
C FuncDeclRef | Function Declarations
►C SortRef |
C ArithSortRef | Arithmetic
C ArraySortRef | Arrays
C BitVecSortRef | Bit-Vectors
C BoolSortRef | Booleans
C DatatypeSortRef |
C FPRMSortRef |
C FPSortRef |
C FiniteDomainSortRef |
C ReSortRef |
C SeqSortRef | Strings, Sequences and Regular expressions
C AstVector |
C Fixedpoint | Fixedpoint
C FuncInterp |
C Goal |
C ModelRef |
C Optimize |
C Solver |