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	TermProof
	Term and optional proof object returned by user-simplifier. 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 336 of file Microsoft.Z3V3.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,
        ToReal,
        ToInt,
        IsInt,
        // Arrays
        Store,
        Select,
        ConstArray,
        DefaultArray,
        MapArray,
        Union,
        Intersect,
        Difference,
        Complement,
        Subset,
        AsArray,
        // 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,
        BExtRotateLeft,
        BExtRotateRight,
        BInt2Bv,
        BBv2Int,
        BCarry,
        BXor3,

        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,

        RaStore,
        RaEmpty,
        RaIsEmpty,
        RaJoin,
        RaUnion,
        RaWiden,
        RaProject,
        RaFilter,
        RaNegationFilter,
        RaRename,
        RaComplement,
        RaSelect,
        RaClone,

        Label,
        LabelLit,
        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.
• InvalidUsage: The API was used in an invalid context.
• 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 169 of file Microsoft.Z3V3.h.

    {
        Ok,
        TypeError,
        IndexOutOfBounds,
        InvalidArgument,
        ParserError,
        NoParser,
        InvalidPattern,
        InternalFatal,
        InvalidUsage,
        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 137 of file Microsoft.Z3V3.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.
• SmtlibCompliant Print AST in SMTLIB 1.x compliant format.
• Smtlib2Compliant Print AST in SMTLIB 1.x compliant format.

Definition at line 195 of file Microsoft.Z3V3.h.

    {
        SmtlibFull,
        LowLevel,
        SmtlibCompliant,
        Smtlib2Compliant
    };

enum SearchFailureExplanation

Different failure kinds.

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

Definition at line 302 of file Microsoft.Z3V3.h.

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

enum SortKind

The different kinds of Z3 sorts (See #GetSortKind).

Definition at line 277 of file Microsoft.Z3V3.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 268 of file Microsoft.Z3V3.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 323 of file Microsoft.Z3V3.h.

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