  com | |
  microsoft | |
 z3 | |
 enumerations | |
  Z3_ast_kind | |
| Z3_ast_print_mode | |
| Z3_decl_kind | |
| Z3_error_code | |
| Z3_goal_prec | |
| Z3_lbool | |
| Z3_param_kind | |
| Z3_parameter_kind | |
| Z3_sort_kind | |
 Z3_symbol_kind | |
| AlgebraicNum | |
| ApplyResult | |
| ArithExpr | |
| ArithSort | |
| ArrayExpr | |
| ArraySort | |
| AST | |
| ASTVector | |
| BitVecExpr | |
| BitVecNum | |
| BitVecSort | |
| BoolExpr | |
| BoolSort | |
| Constructor | |
| ConstructorList | |
| Context | |
| DatatypeExpr | |
| DatatypeSort | |
| EnumSort | |
| Expr | |
| FiniteDomainSort | |
| Fixedpoint | |
| FPExpr | |
| FPNum | |
| FPRMExpr | |
| FPRMNum | |
| FPRMSort | |
| FPSort | |
| FuncDecl | |
| Parameter | |
| FuncInterp | |
| Entry | |
| Global | |
| Goal | |
| IDecRefQueue | |
| IDisposable | |
| InterpolationContext | |
| CheckInterpolantResult | |
| ComputeInterpolantResult | |
| ReadInterpolationProblemResult | |
| IntExpr | |
| IntNum | |
| IntSort | |
| IntSymbol | |
| ListSort | |
| Log | |
| Model | |
| ModelEvaluationFailedException | |
| Native | |
| Optimize | |
| Handle | |
| ParamDescrs | |
| Params | |
| Pattern | |
| Probe | |
| Quantifier | |
| RatNum | |
| RealExpr | |
| RealSort | |
| RelationSort | |
| SetSort | |
| Solver | |
| Sort | |
| Statistics | |
| Entry | |
| Status | |
| StringSymbol | |
| Symbol | |
| Tactic | |
| TupleSort | |
| UninterpretedSort | |
| Version | |
| Z3Exception | |
| Z3Object | |
| Microsoft | |
| Z3 | |
| AlgebraicNum | Algebraic numbers |
| ApplyResult | ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced. |
| ArithExpr | Arithmetic expressions (int/real) |
| ArithSort | An arithmetic sort, i.e., Int or Real. |
| ArrayExpr | Array expressions |
| ArraySort | 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. |
| Constructor | Constructors are used for datatype sorts. |
| ConstructorList | Lists of constructors |
| Context | The main interaction with Z3 happens via the Context. |
| DatatypeExpr | Datatype expressions |
| DatatypeSort | Datatype sorts. |
| Deprecated | The main interaction with Z3 happens via the Context. |
| EnumSort | Enumeration sorts. |
| Expr | Expressions are terms. |
| FiniteDomainSort | Finite domain sorts. |
| Fixedpoint | Object for managing fixedpoints |
| FPExpr | FloatingPoint Expressions |
| FPNum | FloatiungPoint Numerals |
| FPRMExpr | FloatingPoint RoundingMode Expressions |
| FPRMNum | Floating-point rounding mode numerals |
| FPRMSort | The FloatingPoint RoundingMode sort |
| FPSort | FloatingPoint sort |
| FuncDecl | Function declarations. |
| Parameter | Function declarations can have Parameters associated with them. |
| 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. |
| Entry | An Entry object represents an element in the finite map used to encode a function interpretation. |
| Goal | A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers. |
| IDecRefQueue | DecRefQueue interface |
| DecRefQueueContracts | |
| InterpolationContext | The InterpolationContext is suitable for generation of interpolants. |
| IntExpr | Int expressions |
| IntNum | Integer Numerals |
| IntSort | An Integer sort |
| IntSymbol | Numbered symbols |
| ListSort | List sorts. |
| Model | A Model contains interpretations (assignments) of constants and functions. |
| ModelEvaluationFailedException | A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model. |
| Native | |
| LIB | |
| Optimize | Object for managing optimizization context |
| Handle | Handle to objectives returned by objective functions. |
| ParamDescrs | A ParamDescrs describes a set of parameters. |
| Params | A Params objects represents a configuration in the form of Symbol/value pairs. |
| 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. |
| 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-tactics) in the SMT 2.0 front-end. |
| Quantifier | Quantifier expressions. |
| RatNum | Rational Numerals |
| RealExpr | Real expressions |
| RealSort | A real sort |
| RelationSort | Relation sorts. |
| SetSort | Set sorts. |
| Solver | Solvers. |
| Sort | The Sort class implements type information for ASTs. |
| Statistics | Objects of this class track statistical information about solvers. |
| Entry | Statistical data is organized into pairs of [Key, Entry], where every Entry is either a DoubleEntry or a UIntEntry |
| 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. The complete list of tactics may be obtained using Context.NumTactics and Context.TacticNames. It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end. |
| TupleSort | Tuple sorts. |
| UninterpretedSort | Uninterpreted Sorts |
| Z3Exception | The exception base class for error reporting from Z3 |
| Z3Object | Internal base class for interfacing with native Z3 objects. Should not be used externally. |
| z3 | Z3 C++ namespace |
| ast_vector_tpl | |
| exception | Exception used to sign API usage errors |
| config | Z3 global configuration object |
| context | A Context manages all other Z3 objects, global configuration options, etc |
| array | |
| object | |
| symbol | |
| params | |
| ast | |
| sort | A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort |
| 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 |
| 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 |
| cast_ast | |
| cast_ast< ast > | |
| cast_ast< expr > | |
| cast_ast< sort > | |
| cast_ast< func_decl > | |
| func_entry | |
| func_interp | |
| model | |
| stats | |
| solver | |
| goal | |
| apply_result | |
| tactic | |
| probe | |
| optimize | |
| handle | |
| z3py | |
| Context | |
| Z3PPObject | ASTs base class |
| AstRef | |
| SortRef | |
| FuncDeclRef | Function Declarations |
| ExprRef | Expressions |
| BoolSortRef | Booleans |
| BoolRef | |
| PatternRef | Patterns |
| QuantifierRef | Quantifiers |
| ArithSortRef | Arithmetic |
| ArithRef | |
| IntNumRef | |
| RatNumRef | |
| AlgebraicNumRef | |
| BitVecSortRef | Bit-Vectors |
| BitVecRef | |
| BitVecNumRef | |
| ArraySortRef | Arrays |
| ArrayRef | |
| Datatype | |
| ScopedConstructor | |
| ScopedConstructorList | |
| DatatypeSortRef | |
| DatatypeRef | |
| ParamsRef | Parameter Sets |
| ParamDescrsRef | |
| Goal | |
| AstVector | |
| AstMap | |
| FuncEntry | |
| FuncInterp | |
| ModelRef | |
| Statistics | Statistics |
| CheckSatResult | |
| Solver | |
| Fixedpoint | Fixedpoint |
| FiniteDomainSortRef | |
| OptimizeObjective | Optimize |
| Optimize | |
| ApplyResult | |
| Tactic | |
| Probe | |
| FPSortRef | FP Sorts |
| FPRMSortRef | |
| FPRef | FP Expressions |
| FPRMRef | |
| FPNumRef | FP Numerals |
| Comparable | |
| Exception | |
| IComparable | |
| IDisposable | |
| RuntimeException | |
1.8.5