Z3 |

Data Structures
Here are the data structures with brief descriptions:
[detail level 1 2 3 4 5]

▼N com |
►N microsoft |
►N z3 |
C AlgebraicNum |
C ApplyResult |
C ArithExpr |
C ArithSort |
C ArrayExpr |
C ArraySort |
C AST |
C ASTVector |
C BitVecExpr |
C BitVecNum |
C BitVecSort |
C BoolExpr |
C BoolSort |
C Constructor |
C ConstructorDecRefQueue |
C ConstructorList |
C ConstructorListDecRefQueue |
C Context |
C DatatypeExpr |
C DatatypeSort |
C EnumSort |
C Expr |
C FiniteDomainExpr |
C FiniteDomainNum |
C FiniteDomainSort |
C Fixedpoint |
C FPExpr |
C FPNum |
C FPRMExpr |
C FPRMNum |
C FPRMSort |
C FPSort |
C FuncDecl |
C FuncInterp |
C Global |
C Goal |
C IDecRefQueue |
C IntExpr |
C IntNum |
C IntSort |
C IntSymbol |
C Lambda |
C ListSort |
C Log |
►C Model |
C ModelEvaluationFailedException |
C Optimize |
C ParamDescrs |
C Params |
C Pattern |
C Probe |
C Quantifier |
C RatNum |
C RealExpr |
C RealSort |
C ReExpr |
C RelationSort |
C ReSort |
C SeqExpr |
C SeqSort |
C SetSort |
C Solver |
C Sort |
►C Statistics |
C Entry |
C Status |
C StringSymbol |
C Symbol |
C Tactic |
C TupleSort |
C UninterpretedSort |
C Version |
C Z3Exception |
C Z3Object |
▼N Microsoft |
►N Z3 |
C AlgebraicNum | Algebraic numbers
C ApplyResult | ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced.
C ArithExpr | Arithmetic expressions (int/real)
C ArithSort | An arithmetic sort, i.e., Int or Real.
C ArrayExpr | Array expressions
C ArraySort | Array sorts.
C AST | The abstract syntax tree (AST) class.
C ASTVector | Vectors of ASTs.
C BitVecExpr | Bit-vector expressions
C BitVecNum | Bit-vector numerals
C BitVecSort | Bit-vector sorts.
C BoolExpr | Boolean expressions
C BoolSort | A Boolean sort.
C Constructor | Constructors are used for datatype sorts.
C ConstructorList | Lists of constructors
C Context | The main interaction with Z3 happens via the Context.
C DatatypeExpr | Datatype expressions
C DatatypeSort | Datatype sorts.
C DecRefQueueContracts |
C Deprecated | The main interaction with Z3 happens via the Context.
C EnumSort | Enumeration sorts.
C Expr | Expressions are terms.
C FiniteDomainExpr | Finite-domain expressions
C FiniteDomainNum | Finite-domain numerals
C FiniteDomainSort | Finite domain sorts.
C Fixedpoint | Object for managing fixedpoints
C FPExpr | FloatingPoint Expressions
C FPNum | FloatiungPoint Numerals
C FPRMExpr | FloatingPoint RoundingMode Expressions
C FPRMNum | Floating-point rounding mode numerals
C FPRMSort | The FloatingPoint RoundingMode sort
C FPSort | FloatingPoint sort
►C FuncDecl | Function declarations.
C Parameter | Function declarations can have Parameters associated with them.
►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 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 IDecRefQueue | DecRefQueue interface
C IntExpr | Int expressions
C IntNum | Integer Numerals
C IntSort | An Integer sort
C IntSymbol | Numbered symbols
C Lambda | Lambda expressions.
C ListSort | List sorts.
►C Model | A Model contains interpretations (assignments) of constants and functions.
C ModelEvaluationFailedException | A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model.
►C Optimize | Object for managing optimization context
C Handle | Handle to objectives returned by objective functions.
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 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 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 Quantifier | Quantifier expressions.
C RatNum | Rational Numerals
C RealExpr | Real expressions
C RealSort | A real sort
C ReExpr | Regular expression expressions
C RelationSort | Relation sorts.
C ReSort | A regular expression sort
C SeqExpr | Sequence expressions
C SeqSort | A Sequence sort
C SetSort | Set sorts.
C Solver | Solvers.
C Sort | The Sort class implements type information for ASTs.
►C Statistics | Objects of this class track statistical information about solvers.
C Entry | Statistical data is organized into pairs of [Key, Entry], where every Entry is either a `DoubleEntry` or a `UIntEntry`
C StringSymbol | Named symbols
C Symbol | Symbols are used to name several term and type constructors.
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 TupleSort | Tuple sorts.
C UninterpretedSort | Uninterpreted Sorts
C Z3Exception | The exception base class for error reporting from Z3
C Z3Object | Internal base class for interfacing with native Z3 objects. Should not be used externally.
▼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 |
C FPRef |
C FPRMRef |
C FPRMSortRef |
C FPSortRef |
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 |
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
C AutoCloseable |
C Comparable |
C Exception |
C IComparable |
C IDisposable |
C RuntimeException |