Z3
src/api/dotnet/Enumerations.cs
Go to the documentation of this file.
00001 // Automatically generated file
00002 
00003 using System;
00004 
00005 #pragma warning disable 1591
00006 
00007 namespace Microsoft.Z3
00008 {
00010   public enum Z3_lbool {
00011   Z3_L_TRUE = 1,
00012   Z3_L_UNDEF = 0,
00013   Z3_L_FALSE = -1,
00014   }
00015 
00017   public enum Z3_symbol_kind {
00018   Z3_INT_SYMBOL = 0,
00019   Z3_STRING_SYMBOL = 1,
00020   }
00021 
00023   public enum Z3_parameter_kind {
00024   Z3_PARAMETER_FUNC_DECL = 6,
00025   Z3_PARAMETER_DOUBLE = 1,
00026   Z3_PARAMETER_SYMBOL = 3,
00027   Z3_PARAMETER_INT = 0,
00028   Z3_PARAMETER_AST = 5,
00029   Z3_PARAMETER_SORT = 4,
00030   Z3_PARAMETER_RATIONAL = 2,
00031   }
00032 
00034   public enum Z3_sort_kind {
00035   Z3_BV_SORT = 4,
00036   Z3_FINITE_DOMAIN_SORT = 8,
00037   Z3_ARRAY_SORT = 5,
00038   Z3_UNKNOWN_SORT = 1000,
00039   Z3_RELATION_SORT = 7,
00040   Z3_REAL_SORT = 3,
00041   Z3_INT_SORT = 2,
00042   Z3_UNINTERPRETED_SORT = 0,
00043   Z3_BOOL_SORT = 1,
00044   Z3_DATATYPE_SORT = 6,
00045   }
00046 
00048   public enum Z3_ast_kind {
00049   Z3_VAR_AST = 2,
00050   Z3_SORT_AST = 4,
00051   Z3_QUANTIFIER_AST = 3,
00052   Z3_UNKNOWN_AST = 1000,
00053   Z3_FUNC_DECL_AST = 5,
00054   Z3_NUMERAL_AST = 0,
00055   Z3_APP_AST = 1,
00056   }
00057 
00059   public enum Z3_decl_kind {
00060   Z3_OP_LABEL = 1792,
00061   Z3_OP_PR_REWRITE = 1294,
00062   Z3_OP_UNINTERPRETED = 2051,
00063   Z3_OP_SUB = 519,
00064   Z3_OP_ZERO_EXT = 1058,
00065   Z3_OP_ADD = 518,
00066   Z3_OP_IS_INT = 528,
00067   Z3_OP_BREDOR = 1061,
00068   Z3_OP_BNOT = 1051,
00069   Z3_OP_BNOR = 1054,
00070   Z3_OP_PR_CNF_STAR = 1315,
00071   Z3_OP_RA_JOIN = 1539,
00072   Z3_OP_LE = 514,
00073   Z3_OP_SET_UNION = 773,
00074   Z3_OP_PR_UNDEF = 1280,
00075   Z3_OP_BREDAND = 1062,
00076   Z3_OP_LT = 516,
00077   Z3_OP_RA_UNION = 1540,
00078   Z3_OP_BADD = 1028,
00079   Z3_OP_BUREM0 = 1039,
00080   Z3_OP_OEQ = 267,
00081   Z3_OP_PR_MODUS_PONENS = 1284,
00082   Z3_OP_RA_CLONE = 1548,
00083   Z3_OP_REPEAT = 1060,
00084   Z3_OP_RA_NEGATION_FILTER = 1544,
00085   Z3_OP_BSMOD0 = 1040,
00086   Z3_OP_BLSHR = 1065,
00087   Z3_OP_BASHR = 1066,
00088   Z3_OP_PR_UNIT_RESOLUTION = 1304,
00089   Z3_OP_ROTATE_RIGHT = 1068,
00090   Z3_OP_ARRAY_DEFAULT = 772,
00091   Z3_OP_PR_PULL_QUANT = 1296,
00092   Z3_OP_PR_APPLY_DEF = 1310,
00093   Z3_OP_PR_REWRITE_STAR = 1295,
00094   Z3_OP_IDIV = 523,
00095   Z3_OP_PR_GOAL = 1283,
00096   Z3_OP_PR_IFF_TRUE = 1305,
00097   Z3_OP_LABEL_LIT = 1793,
00098   Z3_OP_BOR = 1050,
00099   Z3_OP_PR_SYMMETRY = 1286,
00100   Z3_OP_TRUE = 256,
00101   Z3_OP_SET_COMPLEMENT = 776,
00102   Z3_OP_CONCAT = 1056,
00103   Z3_OP_PR_NOT_OR_ELIM = 1293,
00104   Z3_OP_IFF = 263,
00105   Z3_OP_BSHL = 1064,
00106   Z3_OP_PR_TRANSITIVITY = 1287,
00107   Z3_OP_SGT = 1048,
00108   Z3_OP_RA_WIDEN = 1541,
00109   Z3_OP_PR_DEF_INTRO = 1309,
00110   Z3_OP_NOT = 265,
00111   Z3_OP_PR_QUANT_INTRO = 1290,
00112   Z3_OP_UGT = 1047,
00113   Z3_OP_DT_RECOGNISER = 2049,
00114   Z3_OP_SET_INTERSECT = 774,
00115   Z3_OP_BSREM = 1033,
00116   Z3_OP_RA_STORE = 1536,
00117   Z3_OP_SLT = 1046,
00118   Z3_OP_ROTATE_LEFT = 1067,
00119   Z3_OP_PR_NNF_NEG = 1313,
00120   Z3_OP_PR_REFLEXIVITY = 1285,
00121   Z3_OP_ULEQ = 1041,
00122   Z3_OP_BIT1 = 1025,
00123   Z3_OP_BIT0 = 1026,
00124   Z3_OP_EQ = 258,
00125   Z3_OP_BMUL = 1030,
00126   Z3_OP_ARRAY_MAP = 771,
00127   Z3_OP_STORE = 768,
00128   Z3_OP_PR_HYPOTHESIS = 1302,
00129   Z3_OP_RA_RENAME = 1545,
00130   Z3_OP_AND = 261,
00131   Z3_OP_TO_REAL = 526,
00132   Z3_OP_PR_NNF_POS = 1312,
00133   Z3_OP_PR_AND_ELIM = 1292,
00134   Z3_OP_MOD = 525,
00135   Z3_OP_BUDIV0 = 1037,
00136   Z3_OP_PR_TRUE = 1281,
00137   Z3_OP_BNAND = 1053,
00138   Z3_OP_PR_ELIM_UNUSED_VARS = 1299,
00139   Z3_OP_RA_FILTER = 1543,
00140   Z3_OP_FD_LT = 1549,
00141   Z3_OP_RA_EMPTY = 1537,
00142   Z3_OP_DIV = 522,
00143   Z3_OP_ANUM = 512,
00144   Z3_OP_MUL = 521,
00145   Z3_OP_UGEQ = 1043,
00146   Z3_OP_BSREM0 = 1038,
00147   Z3_OP_PR_TH_LEMMA = 1318,
00148   Z3_OP_BXOR = 1052,
00149   Z3_OP_DISTINCT = 259,
00150   Z3_OP_PR_IFF_FALSE = 1306,
00151   Z3_OP_BV2INT = 1072,
00152   Z3_OP_EXT_ROTATE_LEFT = 1069,
00153   Z3_OP_PR_PULL_QUANT_STAR = 1297,
00154   Z3_OP_BSUB = 1029,
00155   Z3_OP_PR_ASSERTED = 1282,
00156   Z3_OP_BXNOR = 1055,
00157   Z3_OP_EXTRACT = 1059,
00158   Z3_OP_PR_DER = 1300,
00159   Z3_OP_DT_CONSTRUCTOR = 2048,
00160   Z3_OP_GT = 517,
00161   Z3_OP_BUREM = 1034,
00162   Z3_OP_IMPLIES = 266,
00163   Z3_OP_SLEQ = 1042,
00164   Z3_OP_GE = 515,
00165   Z3_OP_BAND = 1049,
00166   Z3_OP_ITE = 260,
00167   Z3_OP_AS_ARRAY = 778,
00168   Z3_OP_RA_SELECT = 1547,
00169   Z3_OP_CONST_ARRAY = 770,
00170   Z3_OP_BSDIV = 1031,
00171   Z3_OP_OR = 262,
00172   Z3_OP_PR_HYPER_RESOLVE = 1319,
00173   Z3_OP_AGNUM = 513,
00174   Z3_OP_PR_PUSH_QUANT = 1298,
00175   Z3_OP_BSMOD = 1035,
00176   Z3_OP_PR_IFF_OEQ = 1311,
00177   Z3_OP_INTERP = 268,
00178   Z3_OP_PR_LEMMA = 1303,
00179   Z3_OP_SET_SUBSET = 777,
00180   Z3_OP_SELECT = 769,
00181   Z3_OP_RA_PROJECT = 1542,
00182   Z3_OP_BNEG = 1027,
00183   Z3_OP_UMINUS = 520,
00184   Z3_OP_REM = 524,
00185   Z3_OP_TO_INT = 527,
00186   Z3_OP_PR_QUANT_INST = 1301,
00187   Z3_OP_SGEQ = 1044,
00188   Z3_OP_POWER = 529,
00189   Z3_OP_XOR3 = 1074,
00190   Z3_OP_RA_IS_EMPTY = 1538,
00191   Z3_OP_CARRY = 1073,
00192   Z3_OP_DT_ACCESSOR = 2050,
00193   Z3_OP_PR_TRANSITIVITY_STAR = 1288,
00194   Z3_OP_PR_NNF_STAR = 1314,
00195   Z3_OP_PR_COMMUTATIVITY = 1307,
00196   Z3_OP_ULT = 1045,
00197   Z3_OP_BSDIV0 = 1036,
00198   Z3_OP_SET_DIFFERENCE = 775,
00199   Z3_OP_INT2BV = 1071,
00200   Z3_OP_XOR = 264,
00201   Z3_OP_PR_MODUS_PONENS_OEQ = 1317,
00202   Z3_OP_BNUM = 1024,
00203   Z3_OP_BUDIV = 1032,
00204   Z3_OP_PR_MONOTONICITY = 1289,
00205   Z3_OP_PR_DEF_AXIOM = 1308,
00206   Z3_OP_FALSE = 257,
00207   Z3_OP_EXT_ROTATE_RIGHT = 1070,
00208   Z3_OP_PR_DISTRIBUTIVITY = 1291,
00209   Z3_OP_SIGN_EXT = 1057,
00210   Z3_OP_PR_SKOLEMIZE = 1316,
00211   Z3_OP_BCOMP = 1063,
00212   Z3_OP_RA_COMPLEMENT = 1546,
00213   }
00214 
00216   public enum Z3_param_kind {
00217   Z3_PK_BOOL = 1,
00218   Z3_PK_SYMBOL = 3,
00219   Z3_PK_OTHER = 5,
00220   Z3_PK_INVALID = 6,
00221   Z3_PK_UINT = 0,
00222   Z3_PK_STRING = 4,
00223   Z3_PK_DOUBLE = 2,
00224   }
00225 
00227   public enum Z3_ast_print_mode {
00228   Z3_PRINT_SMTLIB2_COMPLIANT = 3,
00229   Z3_PRINT_SMTLIB_COMPLIANT = 2,
00230   Z3_PRINT_SMTLIB_FULL = 0,
00231   Z3_PRINT_LOW_LEVEL = 1,
00232   }
00233 
00235   public enum Z3_error_code {
00236   Z3_INVALID_PATTERN = 6,
00237   Z3_MEMOUT_FAIL = 7,
00238   Z3_NO_PARSER = 5,
00239   Z3_OK = 0,
00240   Z3_INVALID_ARG = 3,
00241   Z3_EXCEPTION = 12,
00242   Z3_IOB = 2,
00243   Z3_INTERNAL_FATAL = 9,
00244   Z3_INVALID_USAGE = 10,
00245   Z3_FILE_ACCESS_ERROR = 8,
00246   Z3_SORT_ERROR = 1,
00247   Z3_PARSER_ERROR = 4,
00248   Z3_DEC_REF_ERROR = 11,
00249   }
00250 
00252   public enum Z3_goal_prec {
00253   Z3_GOAL_UNDER = 1,
00254   Z3_GOAL_PRECISE = 0,
00255   Z3_GOAL_UNDER_OVER = 3,
00256   Z3_GOAL_OVER = 2,
00257   }
00258 
00259 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines