Z3 |

Data Structures | Enumerations
Microsoft.Z3 Namespace Reference

## 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 | IntExpr
| Int expressions More...
class | IntNum
| Integer Numerals More...
class | IntSort
| An Integer sort More...
class | IntSymbol
| Numbered symbols More...
class | Lambda
| Lambda expressions. 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 optimization 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...

## Enumeration Type Documentation

## ◆ Status

enum Status

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 28 of file Status.cs.

29 {
33 UNSATISFIABLE = -1,
34
38 UNKNOWN = 0,
39
43 SATISFIABLE = 1
44 }
Microsoft.Z3.Status.UNKNOWN
@ UNKNOWN
Used to signify an unknown status.
Microsoft.Z3.Status.UNSATISFIABLE
@ UNSATISFIABLE
Used to signify an unsatisfiable status.
Microsoft.Z3.Status.SATISFIABLE
@ SATISFIABLE
Used to signify a satisfiable status.