Z3
Namespaces | Enumerations
Enumerations.cs File Reference

Go to the source code of this file.

Namespaces

namespace  Microsoft.Z3
 

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_FLOATING_POINT_SORT = 9,
  Z3_ROUNDING_MODE_SORT = 10, 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 = 2349, Z3_OP_SUB = 519,
  Z3_OP_ZERO_EXT = 1058, Z3_OP_ADD = 518, Z3_OP_FPA_ABS = 2324, Z3_OP_IS_INT = 528,
  Z3_OP_BREDOR = 1061, Z3_OP_FPA_IS_INF = 2336, Z3_OP_BNOT = 1051, Z3_OP_BNOR = 1054,
  Z3_OP_PR_CNF_STAR = 1315, Z3_OP_FPA_TO_UBV = 2345, Z3_OP_RA_JOIN = 1539, Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY = 2308,
  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_FPA_IS_SUBNORMAL = 2339, 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_FPA_NAN = 2315, Z3_OP_BSMOD0 = 1040,
  Z3_OP_FPA_GT = 2332, 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_FPA_RM_TOWARD_POSITIVE = 2309,
  Z3_OP_PR_IFF_TRUE = 1305, Z3_OP_FPA_LT = 2331, Z3_OP_FPA_IS_NORMAL = 2338, Z3_OP_LABEL_LIT = 1793,
  Z3_OP_FPA_TO_IEEE_BV = 2348, Z3_OP_FPA_LE = 2333, 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_FPA_ROUND_TO_INTEGRAL = 2329,
  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_FPA_PLUS_ZERO = 2316, Z3_OP_UGT = 1047, Z3_OP_FPA_NEG = 2320,
  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_FPA_EQ = 2330,
  Z3_OP_PR_REFLEXIVITY = 1285, Z3_OP_ULEQ = 1041, Z3_OP_BIT1 = 1025, Z3_OP_BIT0 = 1026,
  Z3_OP_FPA_MIN = 2325, Z3_OP_PB_AT_MOST = 2304, Z3_OP_EQ = 258, Z3_OP_FPA_SUB = 2319,
  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_DT_UPDATE_FIELD = 2051,
  Z3_OP_PR_NNF_POS = 1312, Z3_OP_PR_AND_ELIM = 1292, Z3_OP_FPA_TO_SBV = 2346, Z3_OP_MOD = 525,
  Z3_OP_BUDIV0 = 1037, Z3_OP_FPA_MAX = 2326, Z3_OP_PR_TRUE = 1281, Z3_OP_BNAND = 1053,
  Z3_OP_PR_ELIM_UNUSED_VARS = 1299, Z3_OP_RA_FILTER = 1543, Z3_OP_FPA_ADD = 2318, 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_FPA_MINUS_INF = 2314,
  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_FPA_IS_ZERO = 2337, 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_PB_GE = 2306, Z3_OP_BAND = 1049,
  Z3_OP_ITE = 260, Z3_OP_AS_ARRAY = 778, Z3_OP_FPA_IS_POSITIVE = 2341, Z3_OP_RA_SELECT = 1547,
  Z3_OP_CONST_ARRAY = 770, Z3_OP_FPA_TO_REAL = 2347, Z3_OP_BSDIV = 1031, Z3_OP_FPA_IS_NEGATIVE = 2340,
  Z3_OP_OR = 262, Z3_OP_FPA_FP = 2342, Z3_OP_PR_HYPER_RESOLVE = 1319, Z3_OP_AGNUM = 513,
  Z3_OP_FPA_IS_NAN = 2335, Z3_OP_PR_PUSH_QUANT = 1298, Z3_OP_FPA_FMA = 2327, Z3_OP_BSMOD = 1035,
  Z3_OP_PR_IFF_OEQ = 1311, Z3_OP_INTERP = 268, Z3_OP_PR_LEMMA = 1303, Z3_OP_FPA_TO_FP_UNSIGNED = 2344,
  Z3_OP_SET_SUBSET = 777, Z3_OP_FPA_SQRT = 2328, Z3_OP_PB_LE = 2305, Z3_OP_FPA_GE = 2334,
  Z3_OP_FPA_DIV = 2322, Z3_OP_FPA_RM_TOWARD_ZERO = 2311, Z3_OP_SELECT = 769, Z3_OP_RA_PROJECT = 1542,
  Z3_OP_BNEG = 1027, Z3_OP_UMINUS = 520, Z3_OP_REM = 524, Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN = 2307,
  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_FPA_MUL = 2321, Z3_OP_BSDIV0 = 1036, Z3_OP_SET_DIFFERENCE = 775, Z3_OP_INT2BV = 1071,
  Z3_OP_FPA_NUM = 2312, Z3_OP_FPA_MINUS_ZERO = 2317, Z3_OP_FPA_REM = 2323, Z3_OP_XOR = 264,
  Z3_OP_FPA_TO_FP = 2343, Z3_OP_PR_MODUS_PONENS_OEQ = 1317, Z3_OP_FPA_RM_TOWARD_NEGATIVE = 2310, 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_FPA_PLUS_INF = 2313,
  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...