Z3 Microsoft Research
Data Structures | Enumerations
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
    };
Last modified Fri Oct 5 2012 11:32:37