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

  {    
    UNSATISFIABLE = -1,

    UNKNOWN = 0,

    SATISFIABLE = 1
  }