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
	Container for labeled literals. More...
class	Constructor
	Container for constructor declarations. More...
class	Config
	Configuration. More...
interface	IRawParameter
	Z3 Parameter values. More...
class	RawArrayValue
	Z3 Array Value object. More...
class	RawFunctionEntry
	Z3 Function entry object. More...
class	RawFunctionGraph
	Z3 Function graph object. More...
class	RawModel
	Z3 RawModel object. More...
class	RawContext
	Z3 API object. More...
class	Context
	Type safe contexts. More...
Enumerations
enum	LBool
	Lifted Booleans. More...
enum	ErrorCode
	Z3 error codes. More...
enum	PrintMode
	Z3 pretty printing modes used when pretty printing terms. More...
enum	SymbolKind
	In Z3, a symbol can be represented using integers and strings (See GetSymbolKind). More...
enum	SortKind
	The different kinds of Z3 sorts (See GetSortKind). More...
enum	SearchFailureExplanation
	Different failure kinds. More...
enum	TermKind
	The different kinds of Z3 Terms. More...
enum	DeclKind
	Different kinds of Z3 built-in declarations (See GetDeclKind). More...

---

Enumeration Type Documentation

enum DeclKind

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

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

    {
        // Basic operators
        True,
        False,
        Eq,
        Distinct,
        Ite,
        And,
        Or,
        Iff,
        Xor,
        Not,
        Implies,
        // Arithmetic
        ArithNum,
        Le,
        Ge,
        Lt,
        Gt,
        Add,
        Sub,
        Uminus,
        Mul,
        Div,
        IDiv,
        Rem,
        Mod,
        // Arrays
        Store,
        Select,
        ConstArray,
        DefaultArray,
        MapArray,
        Union,
        Intersect,
        Difference,
        Complement,
        Subset,
        // Bit-vectors.            

        BitNum,
        Bit1,
        Bit0,
        BNeg,
        BAdd,
        BSub,
        BMul,
        BSDiv,
        BUDiv,
        BSRem,
        BURem,
        BSMod,

        BSDiv0,
        BUDiv0,
        BSRem0,
        BURem0,
        BSMod0,
        BULeq,
        BSLeq,
        BUGeq,
        BSGeq,
        BULt,
        BSLt,
        BUGt,
        BSGt,
        BAnd,
        BOr,
        BNot,
        BXor,
        BNand,
        BNor,
        BXnor,
        BConcat,
        BSignExt,
        BZeroExt,
        BExtract,
        BRepeat,
        BRedOr,
        BRedAnd,
        BComp,

        BShl,
        BLShr,
        BAShr,
        BRotateLeft,
        BRotateRight,
        BInt2Bv,
        BBv2Int,

        PrAsserted,
        PrGoal,
        PrModusPonens,
        PrReflexivity,
        PrTransitivity,
        PrTransitivityStar,
        PrSymmetry,
        PrMonotonicity,
        PrQuantIntro,
        PrDistributivity,
        PrAndElim,
        PrNotOrElim,
        PrRewrite,
        PrRewriteStar,
        PrPullQuant,
        PrPullQuantStar,
        PrPushQuant,
        PrElimUnusedVars,
        PrDer,
        PrQuantInst,
        PrHypothesis,
        PrLemma,
        PrUnitResolution,
        PrIffTrue,
        PrIffFalse,
        PrCommutativity,
        PrDefAxiom,
        PrDefIntro,
        PrApplyDef,
        PrIffOeq,            
        PrNnfPos,
        PrNnfNeg,
        PrNnfStar,
        PrSkolemize,
        PrCnfStar,
        PrModusPonensOeq,
        PrThLemma,
        Uninterpreted            
    };

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.
• InvalidPattern: An invalid pattern was used to build a quantifier.
• InternalFatal: An internal fatal error was encountered.
• FileAccessError: File access failed for an inaccessible file.
• NonDisposedConfig A configuration was not disposed explictly.
• NonDisposedContext: A context was not disposed explictly.
• NonDisposedLiterals: A conflict literal set was not disposed explicitly.
• NonDisposedModel: A model was not disposed of explicitly.

There is no error code for out of memory errors. Z3 will throw the library exception OutOfMemoryException if memory allocation fails. Users should call ResetMemory() to reclaim all allocated resources.

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

    {
        Ok,
        TypeError,
        IndexOutOfBounds,
        InvalidArgument,
        ParserError,
        NoParser,
        InvalidPattern,
        InternalFatal,
        FileAccessError,
        NonDisposedConfig,
        NonDisposedContext,
        NonDisposedLiterals,
        NonDisposedModel
    };

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.

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

    {
        True,
        False,
        Undef
    };

enum PrintMode

Z3 pretty printing modes used when pretty printing terms.

• SmtlibFull: Print AST nodes in SMTLIB verbose format.
• LowLevel: Print AST nodes using a low-level format.

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

    {
        SmtlibFull,
        LowLevel
    };

enum SearchFailureExplanation

Different failure kinds.

• NoFailure
• Unknown:
• TimeOut:
• MemOut:
• UserCanceled:
• MaxConflicts:
• Theory:
• Quantifiers:

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

    {
        NoFailure,
        Unknown,
        TimeOut,
        MemOut,
        UserCanceled,
        MaxConflicts,
        Theory,
        Quantifiers
    };

enum SortKind

The different kinds of Z3 sorts (See GetSortKind).

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

    {
        Uninterpreted,
        Bool,
        Int,
        Real,
        BitVector,
        Array,
        Datatype,
        Unknown
    };

enum SymbolKind

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

See also:

MkIntSymbol

MkStringSymbol

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

    {
        Int, 
        String
    };

enum TermKind

The different kinds of Z3 Terms.

• Numeral: numerals
• App: constant and applications
• Var: bound variables
• Quantifier: quantifiers
• Unknown: internal

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

    {
        Numeral,
        App,
        Var,
        Quantifier,
        Unknown
    };