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

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