Home	•	Docs	•	Download	•	Mail	•	FAQ	•	Awards	•	Status	•	MSR

An Efficient SMT Solver

Managed (.NET) API


Data Structures
class	Symbol
	Symbol. More...
class	Z3Error
	Z3 error exceptions contain an `ErrorCode`. More...
interface	IErrorHandler
	IErrorHandler is an abstract (interface) class for passing an error handler. More...
class	LabeledLiterals
class	Config
	Configuration. More...
class	TupleValue
	Z3 Tuple Value object. More...
class	ArrayValue
	Z3 Array Value object. More...
class	FunctionEntry
	Z3 Function entry object. More...
class	FunctionGraph
	Z3 Function graph object. More...
class	QuantifierPtr
class	ModelValue
	Wrapper class for values that contain a reference to the model. More...
class	Model
	Z3 Model object. More...
class	Context
	Z3 API object. More...
class	Ast
class	TypeAst
class	ConstDeclAst
class	TermAst
class	PatternAst
class	Quantifier
class	TypeSafeContext
	Type safe contexts. More...
class	TypeSafeTupleValue
class	TypeSafeArrayValue
class	TypeSafeFunctionEntry
class	TypeSafeFunctionGraph
class	TypeSafeModel
Enumerations
enum	LBool { True, True, False, False, Undef }
	Lifted Booleans. More...
enum	ErrorCode { Ok, TypeError, IndexOutOfBounds, InvalidArgument, ParserError, NoParser, TimeOut, InternalFatal, FileAccessError }
	Z3 error codes. More...
enum	RelationProperty { Symmetric = 0x1, AntiSymmetric = 0x2, Reflexive = 0x4, Ireflexive = 0x8, Total = 0x10, Transitive = 0x20 }
enum	SymbolKind { Int, Int, String }
	In Z3, a symbol can be represented using integers and strings (See GetSymbolKind). More...
enum	TypeKind { Uninterpreted, Uninterpreted, Bool, Bool, Int, Int, Real, Bv, Array, Array, Tuple, Tuple, Unknown, Unknown, Unknown }
	The different kinds of Z3 types (See GetTypeKind). More...
enum	AstKind { Numeral, Numeral, ConstDecl, Const, Type, Var, Pattern, Quantifier, Unknown, Unknown, Unknown }
	The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types. More...
enum	DeclKind { True, True, False, False, Eq, Distinct, Ite, And, Or, Iff, Xor, Not, Implies, Le, Ge, Lt, Gt, Add, Sub, Uminus, Mul, Div, IDiv, Rem, Mod, Store, Select, ConstArray, DefaultArray, StoreIte, Union, Intersect, Difference, Complement, Subset, Uninterpreted, Uninterpreted }
	Different kinds of Z3 built-in declarations (See GetDeclKind). More...
enum	ValueKind { Bool, Bool, Numeral, Numeral, Array, Array, Tuple, Tuple, Unknown, Unknown, Unknown }
	The different kinds of Z3 values (See GetValueKind). More...

Enumeration Type Documentation

enum AstKind

The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.

Numeral: numerals
ConstDecl: constant and function declarations
Const: constant and applications
Type: types
Var: bound variables
Pattern: patterns and multi-patterns
Quantifier: quantifiers
Unknown: internal

Enumerator:

Numeral
Numeral
ConstDecl
Const
Type
Var
Pattern
Quantifier
Unknown
Unknown
Unknown

Definition at line 224 of file Microsoft.Z3.h.

00225     {
00226         Numeral,
00227         ConstDecl,
00228         Const,
00229         Type,
00230         Var,
00231         Pattern,
00232         Quantifier,
00233         Unknown
00234     };

enum DeclKind

Different kinds of Z3 built-in declarations (See GetDeclKind).

Enumerator:

True
True
False
False
Eq
Distinct
Ite
And
Or
Iff
Xor
Not
Implies
Le
Ge
Lt
Gt
Add
Sub
Uminus
Mul
Div
IDiv
Rem
Mod
Store
Select
ConstArray
DefaultArray
StoreIte
Union
Intersect
Difference
Complement
Subset
Uninterpreted
Uninterpreted

Definition at line 239 of file Microsoft.Z3.h.

00240     {
00241         // Basic operators
00242         True,
00243         False,
00244         Eq,
00245         Distinct,
00246         Ite,
00247         And,
00248         Or,
00249         Iff,
00250         Xor,
00251         Not,
00252         Implies,
00253         // Arithmetic
00254         Le,
00255         Ge,
00256         Lt,
00257         Gt,
00258         Add,
00259         Sub,
00260         Uminus,
00261         Mul,
00262         Div,
00263         IDiv,
00264         Rem,
00265         Mod,
00266         // Arrays
00267         Store,
00268         Select,
00269         ConstArray,
00270         DefaultArray,
00271                 StoreIte,
00272         Union,
00273         Intersect,
00274         Difference,
00275         Complement,
00276         Subset,
00277         // Bit-vectors TBD.            
00278 
00279         Uninterpreted            
00280     };

enum ErrorCode

Z3 error codes.

Ok,
TypeError: User tried to build an invalid (type incorrect) AST.
IndexOutOfBounds: Index out of bounds
InvalidArgument:: Invalid argument was provided
ParserError: An error occurred when parsing a string or file.
NoParser: parser output is not available, that is, user didn't invoke ParseSmtlibString or ParseSmtlibFile.

Enumerator:

Ok
TypeError
IndexOutOfBounds
InvalidArgument
ParserError
NoParser
TimeOut
InternalFatal
FileAccessError

Definition at line 89 of file Microsoft.Z3.h.

00090     {
00091         Ok,
00092         TypeError,
00093         IndexOutOfBounds,
00094         InvalidArgument,
00095         ParserError,
00096         NoParser,
00097         TimeOut, 
00098         InternalFatal,
00099         FileAccessError
00100     };

enum LBool

Lifted Booleans.

The result of m_context->Check() is a lifted Boolean. When Z3 is unable to decide whether the result is satisfiable or unsatisfiable it returns Undef.

Enumerator:

True
True
False
False
Undef

Definition at line 71 of file Microsoft.Z3.h.

00072     {
00073         True,
00074         False,
00075         Undef
00076     };

enum RelationProperty

Properties of binary relations. These properties are used by DeclareBinaryRelation. A relation should not be both symmetric and anti-symmtric, nor reflexive and ireflexive.

Enumerator:

Symmetric
AntiSymmetric
Reflexive
Ireflexive
Total
Transitive

Definition at line 173 of file Microsoft.Z3.h.

00174     {
00175         Symmetric     = 0x1,
00176         AntiSymmetric = 0x2,            
00177         Reflexive     = 0x4,
00178         Ireflexive    = 0x8,
00179         Total         = 0x10,
00180         Transitive    = 0x20
00181     };

enum SymbolKind

In Z3, a symbol can be represented using integers and strings (See GetSymbolKind).

See also:: MkIntSymbol
MkStringSymbol

Enumerator:

Int
Int
String

Definition at line 191 of file Microsoft.Z3.h.

00192     {
00193         Int, 
00194         String
00195     };

enum TypeKind

The different kinds of Z3 types (See GetTypeKind).

Enumerator:

Uninterpreted
Uninterpreted
Bool
Bool
Int
Int
Real
Bv
Array
Array
Tuple
Tuple
Unknown
Unknown
Unknown

Definition at line 200 of file Microsoft.Z3.h.

00201     {
00202         Uninterpreted,
00203         Bool,
00204         Int,
00205         Real,
00206         Bv,
00207         Array,
00208         Tuple,
00209         Unknown
00210     };

enum ValueKind

The different kinds of Z3 values (See GetValueKind).

Enumerator:

Bool
Bool
Numeral
Numeral
Array
Array
Tuple
Tuple
Unknown
Unknown
Unknown

Definition at line 285 of file Microsoft.Z3.h.

00286     {
00287         Bool,
00288         Numeral,
00289         Array,
00290         Tuple,
00291         Unknown
00292     };

Last modified Wed Sep 3 08:54:18 2008

Managed (.NET) API

Data Structures

Enumerations

Enumeration Type Documentation