Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Data Structures | Enumerations
Package Microsoft.Z3

Data Structures

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  AST
 The abstract syntax tree (AST) class. More...
class  ASTMap
 Map from AST to AST. More...
class  ASTVector
 Vectors of ASTs. More...
class  Constructor
 Constructors are used for datatype sorts. More...
class  Context
 The main interaction with Z3 happens via the Context. More...
class  Expr
 Expressions are terms. 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  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  Log
 Interaction logging for Z3.
class  Model
 A Model contains interpretations (assignments) of constants and functions. More...
class  Native
class  Params
 A ParameterSet 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
 Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used. The complete list of probes may be obtained using the procedures Context.NumProbes and Context.ProbeNames. It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end. More...
class  Quantifier
 Quantifier expressions. 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  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-tactics) in the SMT 2.0 front-end. 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  Z3_lbool { Z3_L_TRUE = 1, Z3_L_UNDEF = 0, Z3_L_FALSE = -1 }
 Z3_lbool. More...
enum  Z3_symbol_kind { Z3_INT_SYMBOL = 0, Z3_STRING_SYMBOL = 1 }
 Z3_symbol_kind. More...
enum  Z3_parameter_kind {
  Z3_PARAMETER_FUNC_DECL = 6, Z3_PARAMETER_DOUBLE = 1, Z3_PARAMETER_SYMBOL = 3, Z3_PARAMETER_INT = 0,
  Z3_PARAMETER_AST = 5, Z3_PARAMETER_SORT = 4, Z3_PARAMETER_RATIONAL = 2
}
 Z3_parameter_kind. More...
enum  Z3_sort_kind {
  Z3_BV_SORT = 4, Z3_FINITE_DOMAIN_SORT = 8, Z3_ARRAY_SORT = 5, Z3_UNKNOWN_SORT = 1000,
  Z3_RELATION_SORT = 7, Z3_REAL_SORT = 3, Z3_INT_SORT = 2, Z3_UNINTERPRETED_SORT = 0,
  Z3_BOOL_SORT = 1, Z3_DATATYPE_SORT = 6
}
 Z3_sort_kind. More...
enum  Z3_ast_kind {
  Z3_VAR_AST = 2, Z3_SORT_AST = 4, Z3_QUANTIFIER_AST = 3, Z3_UNKNOWN_AST = 1000,
  Z3_FUNC_DECL_AST = 5, Z3_NUMERAL_AST = 0, Z3_APP_AST = 1
}
 Z3_ast_kind. More...
enum  Z3_decl_kind {
  Z3_OP_LABEL = 1792, Z3_OP_PR_REWRITE = 1294, Z3_OP_UNINTERPRETED = 2051, Z3_OP_SUB = 519,
  Z3_OP_ZERO_EXT = 1058, Z3_OP_ADD = 518, Z3_OP_IS_INT = 528, Z3_OP_BREDOR = 1061,
  Z3_OP_BNOT = 1051, Z3_OP_BNOR = 1054, Z3_OP_PR_CNF_STAR = 1315, Z3_OP_RA_JOIN = 1539,
  Z3_OP_LE = 514, Z3_OP_SET_UNION = 773, Z3_OP_PR_UNDEF = 1280, Z3_OP_BREDAND = 1062,
  Z3_OP_LT = 516, Z3_OP_RA_UNION = 1540, Z3_OP_BADD = 1028, Z3_OP_BUREM0 = 1039,
  Z3_OP_OEQ = 267, Z3_OP_PR_MODUS_PONENS = 1284, Z3_OP_RA_CLONE = 1548, Z3_OP_REPEAT = 1060,
  Z3_OP_RA_NEGATION_FILTER = 1544, Z3_OP_BSMOD0 = 1040, Z3_OP_BLSHR = 1065, Z3_OP_BASHR = 1066,
  Z3_OP_PR_UNIT_RESOLUTION = 1304, Z3_OP_ROTATE_RIGHT = 1068, Z3_OP_ARRAY_DEFAULT = 772, Z3_OP_PR_PULL_QUANT = 1296,
  Z3_OP_PR_APPLY_DEF = 1310, Z3_OP_PR_REWRITE_STAR = 1295, Z3_OP_IDIV = 523, Z3_OP_PR_GOAL = 1283,
  Z3_OP_PR_IFF_TRUE = 1305, Z3_OP_LABEL_LIT = 1793, Z3_OP_BOR = 1050, Z3_OP_PR_SYMMETRY = 1286,
  Z3_OP_TRUE = 256, Z3_OP_SET_COMPLEMENT = 776, Z3_OP_CONCAT = 1056, Z3_OP_PR_NOT_OR_ELIM = 1293,
  Z3_OP_IFF = 263, Z3_OP_BSHL = 1064, Z3_OP_PR_TRANSITIVITY = 1287, Z3_OP_SGT = 1048,
  Z3_OP_RA_WIDEN = 1541, Z3_OP_PR_DEF_INTRO = 1309, Z3_OP_NOT = 265, Z3_OP_PR_QUANT_INTRO = 1290,
  Z3_OP_UGT = 1047, Z3_OP_DT_RECOGNISER = 2049, Z3_OP_SET_INTERSECT = 774, Z3_OP_BSREM = 1033,
  Z3_OP_RA_STORE = 1536, Z3_OP_SLT = 1046, Z3_OP_ROTATE_LEFT = 1067, Z3_OP_PR_NNF_NEG = 1313,
  Z3_OP_PR_REFLEXIVITY = 1285, Z3_OP_ULEQ = 1041, Z3_OP_BIT1 = 1025, Z3_OP_BIT0 = 1026,
  Z3_OP_EQ = 258, Z3_OP_BMUL = 1030, Z3_OP_ARRAY_MAP = 771, Z3_OP_STORE = 768,
  Z3_OP_PR_HYPOTHESIS = 1302, Z3_OP_RA_RENAME = 1545, Z3_OP_AND = 261, Z3_OP_TO_REAL = 526,
  Z3_OP_PR_NNF_POS = 1312, Z3_OP_PR_AND_ELIM = 1292, Z3_OP_MOD = 525, Z3_OP_BUDIV0 = 1037,
  Z3_OP_PR_TRUE = 1281, Z3_OP_BNAND = 1053, Z3_OP_PR_ELIM_UNUSED_VARS = 1299, Z3_OP_RA_FILTER = 1543,
  Z3_OP_FD_LT = 1549, Z3_OP_RA_EMPTY = 1537, Z3_OP_DIV = 522, Z3_OP_ANUM = 512,
  Z3_OP_MUL = 521, Z3_OP_UGEQ = 1043, Z3_OP_BSREM0 = 1038, Z3_OP_PR_TH_LEMMA = 1318,
  Z3_OP_BXOR = 1052, Z3_OP_DISTINCT = 259, Z3_OP_PR_IFF_FALSE = 1306, Z3_OP_BV2INT = 1072,
  Z3_OP_EXT_ROTATE_LEFT = 1069, Z3_OP_PR_PULL_QUANT_STAR = 1297, Z3_OP_BSUB = 1029, Z3_OP_PR_ASSERTED = 1282,
  Z3_OP_BXNOR = 1055, Z3_OP_EXTRACT = 1059, Z3_OP_PR_DER = 1300, Z3_OP_DT_CONSTRUCTOR = 2048,
  Z3_OP_GT = 517, Z3_OP_BUREM = 1034, Z3_OP_IMPLIES = 266, Z3_OP_SLEQ = 1042,
  Z3_OP_GE = 515, Z3_OP_BAND = 1049, Z3_OP_ITE = 260, Z3_OP_AS_ARRAY = 778,
  Z3_OP_RA_SELECT = 1547, Z3_OP_CONST_ARRAY = 770, Z3_OP_BSDIV = 1031, Z3_OP_OR = 262,
  Z3_OP_PR_HYPER_RESOLVE = 1319, Z3_OP_AGNUM = 513, Z3_OP_PR_PUSH_QUANT = 1298, Z3_OP_BSMOD = 1035,
  Z3_OP_PR_IFF_OEQ = 1311, Z3_OP_INTERP = 268, Z3_OP_PR_LEMMA = 1303, Z3_OP_SET_SUBSET = 777,
  Z3_OP_SELECT = 769, Z3_OP_RA_PROJECT = 1542, Z3_OP_BNEG = 1027, Z3_OP_UMINUS = 520,
  Z3_OP_REM = 524, Z3_OP_TO_INT = 527, Z3_OP_PR_QUANT_INST = 1301, Z3_OP_SGEQ = 1044,
  Z3_OP_POWER = 529, Z3_OP_XOR3 = 1074, Z3_OP_RA_IS_EMPTY = 1538, Z3_OP_CARRY = 1073,
  Z3_OP_DT_ACCESSOR = 2050, Z3_OP_PR_TRANSITIVITY_STAR = 1288, Z3_OP_PR_NNF_STAR = 1314, Z3_OP_PR_COMMUTATIVITY = 1307,
  Z3_OP_ULT = 1045, Z3_OP_BSDIV0 = 1036, Z3_OP_SET_DIFFERENCE = 775, Z3_OP_INT2BV = 1071,
  Z3_OP_XOR = 264, Z3_OP_PR_MODUS_PONENS_OEQ = 1317, Z3_OP_BNUM = 1024, Z3_OP_BUDIV = 1032,
  Z3_OP_PR_MONOTONICITY = 1289, Z3_OP_PR_DEF_AXIOM = 1308, Z3_OP_FALSE = 257, Z3_OP_EXT_ROTATE_RIGHT = 1070,
  Z3_OP_PR_DISTRIBUTIVITY = 1291, Z3_OP_SIGN_EXT = 1057, Z3_OP_PR_SKOLEMIZE = 1316, Z3_OP_BCOMP = 1063,
  Z3_OP_RA_COMPLEMENT = 1546
}
 Z3_decl_kind. More...
enum  Z3_param_kind {
  Z3_PK_BOOL = 1, Z3_PK_SYMBOL = 3, Z3_PK_OTHER = 5, Z3_PK_INVALID = 6,
  Z3_PK_UINT = 0, Z3_PK_STRING = 4, Z3_PK_DOUBLE = 2
}
 Z3_param_kind. More...
enum  Z3_ast_print_mode { Z3_PRINT_SMTLIB2_COMPLIANT = 3, Z3_PRINT_SMTLIB_COMPLIANT = 2, Z3_PRINT_SMTLIB_FULL = 0, Z3_PRINT_LOW_LEVEL = 1 }
 Z3_ast_print_mode. More...
enum  Z3_error_code {
  Z3_INVALID_PATTERN = 6, Z3_MEMOUT_FAIL = 7, Z3_NO_PARSER = 5, Z3_OK = 0,
  Z3_INVALID_ARG = 3, Z3_EXCEPTION = 12, Z3_IOB = 2, Z3_INTERNAL_FATAL = 9,
  Z3_INVALID_USAGE = 10, Z3_FILE_ACCESS_ERROR = 8, Z3_SORT_ERROR = 1, Z3_PARSER_ERROR = 4,
  Z3_DEC_REF_ERROR = 11
}
 Z3_error_code. More...
enum  Z3_goal_prec { Z3_GOAL_UNDER = 1, Z3_GOAL_PRECISE = 0, Z3_GOAL_UNDER_OVER = 3, Z3_GOAL_OVER = 2 }
 Z3_goal_prec. More...
enum  Status { UNSATISFIABLE = -1, UNKNOWN = 0, SATISFIABLE = 1 }
 Status values. More...

Enumeration Type Documentation

enum Status

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
  }

Z3_ast_kind.

Enumerator:
Z3_VAR_AST 
Z3_SORT_AST 
Z3_QUANTIFIER_AST 
Z3_UNKNOWN_AST 
Z3_FUNC_DECL_AST 
Z3_NUMERAL_AST 
Z3_APP_AST 

Definition at line 48 of file Enumerations.cs.

Z3_ast_print_mode.

Enumerator:
Z3_PRINT_SMTLIB2_COMPLIANT 
Z3_PRINT_SMTLIB_COMPLIANT 
Z3_PRINT_SMTLIB_FULL 
Z3_PRINT_LOW_LEVEL 

Definition at line 227 of file Enumerations.cs.

Z3_decl_kind.

Enumerator:
Z3_OP_LABEL 
Z3_OP_PR_REWRITE 
Z3_OP_UNINTERPRETED 
Z3_OP_SUB 
Z3_OP_ZERO_EXT 
Z3_OP_ADD 
Z3_OP_IS_INT 
Z3_OP_BREDOR 
Z3_OP_BNOT 
Z3_OP_BNOR 
Z3_OP_PR_CNF_STAR 
Z3_OP_RA_JOIN 
Z3_OP_LE 
Z3_OP_SET_UNION 
Z3_OP_PR_UNDEF 
Z3_OP_BREDAND 
Z3_OP_LT 
Z3_OP_RA_UNION 
Z3_OP_BADD 
Z3_OP_BUREM0 
Z3_OP_OEQ 
Z3_OP_PR_MODUS_PONENS 
Z3_OP_RA_CLONE 
Z3_OP_REPEAT 
Z3_OP_RA_NEGATION_FILTER 
Z3_OP_BSMOD0 
Z3_OP_BLSHR 
Z3_OP_BASHR 
Z3_OP_PR_UNIT_RESOLUTION 
Z3_OP_ROTATE_RIGHT 
Z3_OP_ARRAY_DEFAULT 
Z3_OP_PR_PULL_QUANT 
Z3_OP_PR_APPLY_DEF 
Z3_OP_PR_REWRITE_STAR 
Z3_OP_IDIV 
Z3_OP_PR_GOAL 
Z3_OP_PR_IFF_TRUE 
Z3_OP_LABEL_LIT 
Z3_OP_BOR 
Z3_OP_PR_SYMMETRY 
Z3_OP_TRUE 
Z3_OP_SET_COMPLEMENT 
Z3_OP_CONCAT 
Z3_OP_PR_NOT_OR_ELIM 
Z3_OP_IFF 
Z3_OP_BSHL 
Z3_OP_PR_TRANSITIVITY 
Z3_OP_SGT 
Z3_OP_RA_WIDEN 
Z3_OP_PR_DEF_INTRO 
Z3_OP_NOT 
Z3_OP_PR_QUANT_INTRO 
Z3_OP_UGT 
Z3_OP_DT_RECOGNISER 
Z3_OP_SET_INTERSECT 
Z3_OP_BSREM 
Z3_OP_RA_STORE 
Z3_OP_SLT 
Z3_OP_ROTATE_LEFT 
Z3_OP_PR_NNF_NEG 
Z3_OP_PR_REFLEXIVITY 
Z3_OP_ULEQ 
Z3_OP_BIT1 
Z3_OP_BIT0 
Z3_OP_EQ 
Z3_OP_BMUL 
Z3_OP_ARRAY_MAP 
Z3_OP_STORE 
Z3_OP_PR_HYPOTHESIS 
Z3_OP_RA_RENAME 
Z3_OP_AND 
Z3_OP_TO_REAL 
Z3_OP_PR_NNF_POS 
Z3_OP_PR_AND_ELIM 
Z3_OP_MOD 
Z3_OP_BUDIV0 
Z3_OP_PR_TRUE 
Z3_OP_BNAND 
Z3_OP_PR_ELIM_UNUSED_VARS 
Z3_OP_RA_FILTER 
Z3_OP_FD_LT 
Z3_OP_RA_EMPTY 
Z3_OP_DIV 
Z3_OP_ANUM 
Z3_OP_MUL 
Z3_OP_UGEQ 
Z3_OP_BSREM0 
Z3_OP_PR_TH_LEMMA 
Z3_OP_BXOR 
Z3_OP_DISTINCT 
Z3_OP_PR_IFF_FALSE 
Z3_OP_BV2INT 
Z3_OP_EXT_ROTATE_LEFT 
Z3_OP_PR_PULL_QUANT_STAR 
Z3_OP_BSUB 
Z3_OP_PR_ASSERTED 
Z3_OP_BXNOR 
Z3_OP_EXTRACT 
Z3_OP_PR_DER 
Z3_OP_DT_CONSTRUCTOR 
Z3_OP_GT 
Z3_OP_BUREM 
Z3_OP_IMPLIES 
Z3_OP_SLEQ 
Z3_OP_GE 
Z3_OP_BAND 
Z3_OP_ITE 
Z3_OP_AS_ARRAY 
Z3_OP_RA_SELECT 
Z3_OP_CONST_ARRAY 
Z3_OP_BSDIV 
Z3_OP_OR 
Z3_OP_PR_HYPER_RESOLVE 
Z3_OP_AGNUM 
Z3_OP_PR_PUSH_QUANT 
Z3_OP_BSMOD 
Z3_OP_PR_IFF_OEQ 
Z3_OP_INTERP 
Z3_OP_PR_LEMMA 
Z3_OP_SET_SUBSET 
Z3_OP_SELECT 
Z3_OP_RA_PROJECT 
Z3_OP_BNEG 
Z3_OP_UMINUS 
Z3_OP_REM 
Z3_OP_TO_INT 
Z3_OP_PR_QUANT_INST 
Z3_OP_SGEQ 
Z3_OP_POWER 
Z3_OP_XOR3 
Z3_OP_RA_IS_EMPTY 
Z3_OP_CARRY 
Z3_OP_DT_ACCESSOR 
Z3_OP_PR_TRANSITIVITY_STAR 
Z3_OP_PR_NNF_STAR 
Z3_OP_PR_COMMUTATIVITY 
Z3_OP_ULT 
Z3_OP_BSDIV0 
Z3_OP_SET_DIFFERENCE 
Z3_OP_INT2BV 
Z3_OP_XOR 
Z3_OP_PR_MODUS_PONENS_OEQ 
Z3_OP_BNUM 
Z3_OP_BUDIV 
Z3_OP_PR_MONOTONICITY 
Z3_OP_PR_DEF_AXIOM 
Z3_OP_FALSE 
Z3_OP_EXT_ROTATE_RIGHT 
Z3_OP_PR_DISTRIBUTIVITY 
Z3_OP_SIGN_EXT 
Z3_OP_PR_SKOLEMIZE 
Z3_OP_BCOMP 
Z3_OP_RA_COMPLEMENT 

Definition at line 59 of file Enumerations.cs.

                           {
  Z3_OP_LABEL = 1792,
  Z3_OP_PR_REWRITE = 1294,
  Z3_OP_UNINTERPRETED = 2051,
  Z3_OP_SUB = 519,
  Z3_OP_ZERO_EXT = 1058,
  Z3_OP_ADD = 518,
  Z3_OP_IS_INT = 528,
  Z3_OP_BREDOR = 1061,
  Z3_OP_BNOT = 1051,
  Z3_OP_BNOR = 1054,
  Z3_OP_PR_CNF_STAR = 1315,
  Z3_OP_RA_JOIN = 1539,
  Z3_OP_LE = 514,
  Z3_OP_SET_UNION = 773,
  Z3_OP_PR_UNDEF = 1280,
  Z3_OP_BREDAND = 1062,
  Z3_OP_LT = 516,
  Z3_OP_RA_UNION = 1540,
  Z3_OP_BADD = 1028,
  Z3_OP_BUREM0 = 1039,
  Z3_OP_OEQ = 267,
  Z3_OP_PR_MODUS_PONENS = 1284,
  Z3_OP_RA_CLONE = 1548,
  Z3_OP_REPEAT = 1060,
  Z3_OP_RA_NEGATION_FILTER = 1544,
  Z3_OP_BSMOD0 = 1040,
  Z3_OP_BLSHR = 1065,
  Z3_OP_BASHR = 1066,
  Z3_OP_PR_UNIT_RESOLUTION = 1304,
  Z3_OP_ROTATE_RIGHT = 1068,
  Z3_OP_ARRAY_DEFAULT = 772,
  Z3_OP_PR_PULL_QUANT = 1296,
  Z3_OP_PR_APPLY_DEF = 1310,
  Z3_OP_PR_REWRITE_STAR = 1295,
  Z3_OP_IDIV = 523,
  Z3_OP_PR_GOAL = 1283,
  Z3_OP_PR_IFF_TRUE = 1305,
  Z3_OP_LABEL_LIT = 1793,
  Z3_OP_BOR = 1050,
  Z3_OP_PR_SYMMETRY = 1286,
  Z3_OP_TRUE = 256,
  Z3_OP_SET_COMPLEMENT = 776,
  Z3_OP_CONCAT = 1056,
  Z3_OP_PR_NOT_OR_ELIM = 1293,
  Z3_OP_IFF = 263,
  Z3_OP_BSHL = 1064,
  Z3_OP_PR_TRANSITIVITY = 1287,
  Z3_OP_SGT = 1048,
  Z3_OP_RA_WIDEN = 1541,
  Z3_OP_PR_DEF_INTRO = 1309,
  Z3_OP_NOT = 265,
  Z3_OP_PR_QUANT_INTRO = 1290,
  Z3_OP_UGT = 1047,
  Z3_OP_DT_RECOGNISER = 2049,
  Z3_OP_SET_INTERSECT = 774,
  Z3_OP_BSREM = 1033,
  Z3_OP_RA_STORE = 1536,
  Z3_OP_SLT = 1046,
  Z3_OP_ROTATE_LEFT = 1067,
  Z3_OP_PR_NNF_NEG = 1313,
  Z3_OP_PR_REFLEXIVITY = 1285,
  Z3_OP_ULEQ = 1041,
  Z3_OP_BIT1 = 1025,
  Z3_OP_BIT0 = 1026,
  Z3_OP_EQ = 258,
  Z3_OP_BMUL = 1030,
  Z3_OP_ARRAY_MAP = 771,
  Z3_OP_STORE = 768,
  Z3_OP_PR_HYPOTHESIS = 1302,
  Z3_OP_RA_RENAME = 1545,
  Z3_OP_AND = 261,
  Z3_OP_TO_REAL = 526,
  Z3_OP_PR_NNF_POS = 1312,
  Z3_OP_PR_AND_ELIM = 1292,
  Z3_OP_MOD = 525,
  Z3_OP_BUDIV0 = 1037,
  Z3_OP_PR_TRUE = 1281,
  Z3_OP_BNAND = 1053,
  Z3_OP_PR_ELIM_UNUSED_VARS = 1299,
  Z3_OP_RA_FILTER = 1543,
  Z3_OP_FD_LT = 1549,
  Z3_OP_RA_EMPTY = 1537,
  Z3_OP_DIV = 522,
  Z3_OP_ANUM = 512,
  Z3_OP_MUL = 521,
  Z3_OP_UGEQ = 1043,
  Z3_OP_BSREM0 = 1038,
  Z3_OP_PR_TH_LEMMA = 1318,
  Z3_OP_BXOR = 1052,
  Z3_OP_DISTINCT = 259,
  Z3_OP_PR_IFF_FALSE = 1306,
  Z3_OP_BV2INT = 1072,
  Z3_OP_EXT_ROTATE_LEFT = 1069,
  Z3_OP_PR_PULL_QUANT_STAR = 1297,
  Z3_OP_BSUB = 1029,
  Z3_OP_PR_ASSERTED = 1282,
  Z3_OP_BXNOR = 1055,
  Z3_OP_EXTRACT = 1059,
  Z3_OP_PR_DER = 1300,
  Z3_OP_DT_CONSTRUCTOR = 2048,
  Z3_OP_GT = 517,
  Z3_OP_BUREM = 1034,
  Z3_OP_IMPLIES = 266,
  Z3_OP_SLEQ = 1042,
  Z3_OP_GE = 515,
  Z3_OP_BAND = 1049,
  Z3_OP_ITE = 260,
  Z3_OP_AS_ARRAY = 778,
  Z3_OP_RA_SELECT = 1547,
  Z3_OP_CONST_ARRAY = 770,
  Z3_OP_BSDIV = 1031,
  Z3_OP_OR = 262,
  Z3_OP_PR_HYPER_RESOLVE = 1319,
  Z3_OP_AGNUM = 513,
  Z3_OP_PR_PUSH_QUANT = 1298,
  Z3_OP_BSMOD = 1035,
  Z3_OP_PR_IFF_OEQ = 1311,
  Z3_OP_INTERP = 268,
  Z3_OP_PR_LEMMA = 1303,
  Z3_OP_SET_SUBSET = 777,
  Z3_OP_SELECT = 769,
  Z3_OP_RA_PROJECT = 1542,
  Z3_OP_BNEG = 1027,
  Z3_OP_UMINUS = 520,
  Z3_OP_REM = 524,
  Z3_OP_TO_INT = 527,
  Z3_OP_PR_QUANT_INST = 1301,
  Z3_OP_SGEQ = 1044,
  Z3_OP_POWER = 529,
  Z3_OP_XOR3 = 1074,
  Z3_OP_RA_IS_EMPTY = 1538,
  Z3_OP_CARRY = 1073,
  Z3_OP_DT_ACCESSOR = 2050,
  Z3_OP_PR_TRANSITIVITY_STAR = 1288,
  Z3_OP_PR_NNF_STAR = 1314,
  Z3_OP_PR_COMMUTATIVITY = 1307,
  Z3_OP_ULT = 1045,
  Z3_OP_BSDIV0 = 1036,
  Z3_OP_SET_DIFFERENCE = 775,
  Z3_OP_INT2BV = 1071,
  Z3_OP_XOR = 264,
  Z3_OP_PR_MODUS_PONENS_OEQ = 1317,
  Z3_OP_BNUM = 1024,
  Z3_OP_BUDIV = 1032,
  Z3_OP_PR_MONOTONICITY = 1289,
  Z3_OP_PR_DEF_AXIOM = 1308,
  Z3_OP_FALSE = 257,
  Z3_OP_EXT_ROTATE_RIGHT = 1070,
  Z3_OP_PR_DISTRIBUTIVITY = 1291,
  Z3_OP_SIGN_EXT = 1057,
  Z3_OP_PR_SKOLEMIZE = 1316,
  Z3_OP_BCOMP = 1063,
  Z3_OP_RA_COMPLEMENT = 1546,
  }

Z3_error_code.

Enumerator:
Z3_INVALID_PATTERN 
Z3_MEMOUT_FAIL 
Z3_NO_PARSER 
Z3_OK 
Z3_INVALID_ARG 
Z3_EXCEPTION 
Z3_IOB 
Z3_INTERNAL_FATAL 
Z3_INVALID_USAGE 
Z3_FILE_ACCESS_ERROR 
Z3_SORT_ERROR 
Z3_PARSER_ERROR 
Z3_DEC_REF_ERROR 

Definition at line 235 of file Enumerations.cs.

Z3_goal_prec.

Enumerator:
Z3_GOAL_UNDER 
Z3_GOAL_PRECISE 
Z3_GOAL_UNDER_OVER 
Z3_GOAL_OVER 

Definition at line 252 of file Enumerations.cs.

enum Z3_lbool

Z3_lbool.

Enumerator:
Z3_L_TRUE 
Z3_L_UNDEF 
Z3_L_FALSE 

Definition at line 10 of file Enumerations.cs.

                       {
  Z3_L_TRUE = 1,
  Z3_L_UNDEF = 0,
  Z3_L_FALSE = -1,
  }

Z3_param_kind.

Enumerator:
Z3_PK_BOOL 
Z3_PK_SYMBOL 
Z3_PK_OTHER 
Z3_PK_INVALID 
Z3_PK_UINT 
Z3_PK_STRING 
Z3_PK_DOUBLE 

Definition at line 216 of file Enumerations.cs.

Z3_parameter_kind.

Enumerator:
Z3_PARAMETER_FUNC_DECL 
Z3_PARAMETER_DOUBLE 
Z3_PARAMETER_SYMBOL 
Z3_PARAMETER_INT 
Z3_PARAMETER_AST 
Z3_PARAMETER_SORT 
Z3_PARAMETER_RATIONAL 

Definition at line 23 of file Enumerations.cs.

Z3_sort_kind.

Enumerator:
Z3_BV_SORT 
Z3_FINITE_DOMAIN_SORT 
Z3_ARRAY_SORT 
Z3_UNKNOWN_SORT 
Z3_RELATION_SORT 
Z3_REAL_SORT 
Z3_INT_SORT 
Z3_UNINTERPRETED_SORT 
Z3_BOOL_SORT 
Z3_DATATYPE_SORT 

Definition at line 34 of file Enumerations.cs.

Z3_symbol_kind.

Enumerator:
Z3_INT_SYMBOL 
Z3_STRING_SYMBOL 

Definition at line 17 of file Enumerations.cs.

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines