▼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 |