|
Z3
|
|
|
Z3
|
|
| ▼Ncom | |
| ▼Nmicrosoft | |
| ►Nz3 | |
| ▼NMicrosoft | |
| ▼NZ3 | |
| CApplyResult | ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced. |
| CAST | The abstract syntax tree (AST) class. |
| CConstructor | Constructors are used for datatype sorts. |
| CContext | The main interaction with Z3 happens via the Context. |
| CExpr | Expressions are terms. |
| ►CFuncDecl | Function declarations. |
| ►CFuncInterp | 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. |
| CGoal | A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers. |
| ►CModel | A Model contains interpretations (assignments) of constants and functions. |
| ►CNative | |
| CParams | A ParameterSet represents a configuration in the form of Symbol/value pairs. |
| CPattern | 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. |
| CProbe | 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. |
| CQuantifier | Quantifier expressions. |
| CSolver | Solvers. |
| CSort | The Sort class implements type information for ASTs. |
| ►CStatistics | Objects of this class track statistical information about solvers. |
| CSymbol | Symbols are used to name several term and type constructors. |
| CTactic | 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. |
| CZ3Exception | The exception base class for error reporting from Z3 |
| CZ3Object | Internal base class for interfacing with native Z3 objects. Should not be used externally. |
| ▼Nz3 | Z3 C++ namespace |
| Capply_result | |
| Carray | |
| Cast | |
| Cast_vector_tpl | |
| Ccast_ast | |
| Ccast_ast< ast > | |
| Ccast_ast< expr > | |
| Ccast_ast< func_decl > | |
| Ccast_ast< sort > | |
| Cconfig | Z3 global configuration object |
| Ccontext | A Context manages all other Z3 objects, global configuration options, etc |
| Cexception | Exception used to sign API usage errors |
| Cexpr | 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 |
| Cfunc_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 |
| Cfunc_entry | |
| Cfunc_interp | |
| Cgoal | |
| Cmodel | |
| Cobject | |
| Cparams | |
| Cprobe | |
| Csolver | |
| Csort | A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort |
| Cstats | |
| Csymbol | |
| Ctactic | |
| ▼Nz3py | |
| CAlgebraicNumRef | |
| CApplyResult | |
| CArithRef | |
| CArithSortRef | Arithmetic |
| CArrayRef | |
| CArraySortRef | Arrays |
| CAstMap | |
| CAstRef | |
| CAstVector | |
| CBitVecNumRef | |
| CBitVecRef | |
| CBitVecSortRef | Bit-Vectors |
| CBoolRef | |
| CBoolSortRef | Booleans |
| CCheckSatResult | |
| CContext | |
| CDatatype | |
| CDatatypeRef | |
| CDatatypeSortRef | |
| CExprRef | Expressions |
| CFixedpoint | Fixedpoint |
| CFuncDeclRef | Function Declarations |
| CFuncEntry | |
| CFuncInterp | |
| CGoal | |
| CIntNumRef | |
| CModelRef | |
| CParamDescrsRef | |
| CParamsRef | Parameter Sets |
| CPatternRef | Patterns |
| CProbe | |
| CQuantifierRef | Quantifiers |
| CRatNumRef | |
| CScopedConstructor | |
| CScopedConstructorList | |
| CSolver | |
| CSortRef | |
| CStatistics | Statistics |
| CTactic | |
| CZ3PPObject | ASTs base class |
| CBoolExpr | |
| CException | |
| CIComparable | |
| CIDecRefQueue | |
| CIDisposable |
1.8.9.1