Data Structures | |
class | AlgebraicNum |
Algebraic numbers More... | |
class | ApplyResult |
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced. More... | |
class | ArithExpr |
Arithmetic expressions (int/real) More... | |
class | ArithSort |
An arithmetic sort, i.e., Int or Real. More... | |
class | ArrayExpr |
Array expressions More... | |
class | ArraySort |
Array sorts. More... | |
class | AST |
The abstract syntax tree (AST) class. More... | |
class | ASTMap |
Map from AST to AST | |
class | ASTVector |
Vectors of ASTs. More... | |
class | BitVecExpr |
Bit-vector expressions More... | |
class | BitVecNum |
Bit-vector numerals More... | |
class | BitVecSort |
Bit-vector sorts. More... | |
class | BoolExpr |
Boolean expressions More... | |
class | BoolSort |
A Boolean sort. More... | |
class | Constructor |
Constructors are used for datatype sorts. More... | |
class | ConstructorList |
Lists of constructors More... | |
class | Context |
The main interaction with Z3 happens via the Context. More... | |
class | DatatypeExpr |
Datatype expressions More... | |
class | DatatypeSort |
Datatype sorts. More... | |
class | DecRefQueueContracts |
class | Deprecated |
The main interaction with Z3 happens via the Context. More... | |
class | EnumSort |
Enumeration sorts. More... | |
class | Expr |
Expressions are terms. More... | |
class | FiniteDomainExpr |
Finite-domain expressions More... | |
class | FiniteDomainNum |
Finite-domain numerals More... | |
class | FiniteDomainSort |
Finite domain sorts. More... | |
class | Fixedpoint |
Object for managing fixedpoints More... | |
class | FPExpr |
FloatingPoint Expressions More... | |
class | FPNum |
FloatiungPoint Numerals More... | |
class | FPRMExpr |
FloatingPoint RoundingMode Expressions More... | |
class | FPRMNum |
Floating-point rounding mode numerals More... | |
class | FPRMSort |
The FloatingPoint RoundingMode sort More... | |
class | FPSort |
FloatingPoint sort More... | |
class | FuncDecl |
Function declarations. More... | |
class | 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. More... | |
class | Global |
Global functions for Z3. | |
class | Goal |
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers. More... | |
class | IDecRefQueue |
DecRefQueue interface More... | |
class | InterpolationContext |
The InterpolationContext is suitable for generation of interpolants. More... | |
class | IntExpr |
Int expressions More... | |
class | IntNum |
Integer Numerals More... | |
class | IntSort |
An Integer sort More... | |
class | IntSymbol |
Numbered symbols More... | |
class | ListSort |
List sorts. More... | |
class | Log |
Interaction logging for Z3. | |
class | Model |
A Model contains interpretations (assignments) of constants and functions. More... | |
class | Optimize |
Object for managing optimizization context More... | |
class | ParamDescrs |
A ParamDescrs describes a set of parameters. More... | |
class | Params |
A Params objects represents a configuration in the form of Symbol/value pairs. More... | |
class | 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. More... | |
class | 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. More... | |
class | Quantifier |
Quantifier expressions. More... | |
class | RatNum |
Rational Numerals More... | |
class | RealExpr |
Real expressions More... | |
class | RealSort |
A real sort More... | |
class | ReExpr |
Regular expression expressions More... | |
class | RelationSort |
Relation sorts. More... | |
class | ReSort |
A regular expression sort More... | |
class | SeqExpr |
Sequence expressions More... | |
class | SeqSort |
A Sequence sort More... | |
class | SetSort |
Set sorts. More... | |
class | Solver |
Solvers. More... | |
class | Sort |
The Sort class implements type information for ASTs. More... | |
class | Statistics |
Objects of this class track statistical information about solvers. More... | |
class | StringSymbol |
Named symbols More... | |
class | Symbol |
Symbols are used to name several term and type constructors. More... | |
class | 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. More... | |
class | TupleSort |
Tuple sorts. More... | |
class | UninterpretedSort |
Uninterpreted Sorts More... | |
class | Version |
Version information. | |
class | Z3Exception |
The exception base class for error reporting from Z3 More... | |
class | Z3Object |
Internal base class for interfacing with native Z3 objects. Should not be used externally. More... | |
Enumerations | |
enum | Status { UNSATISFIABLE = -1, UNKNOWN = 0, SATISFIABLE = 1 } |
Status values. More... | |
|
strong |
Status values.
Enumerator | |
---|---|
UNSATISFIABLE | Used to signify an unsatisfiable status. |
UNKNOWN | Used to signify an unknown status. |
SATISFIABLE | Used to signify a satisfiable status. |
Definition at line 27 of file Status.cs.