|
Z3
|
|
All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
|
Z3
|
|
Data Structures | |
| class | AlgebraicNum |
| Algebraic numbers. More... | |
| 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 | ArithExpr |
| Arithmetic expressions (int/real) More... | |
| class | ArithSort |
| An arithmetic sort, i.e., Int or Real. More... | |
| class | ArrayExpr |
| Array expressions. More... | |
| class | ArraySort |
| Array sorts. 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 | BitVecExpr |
| Bit-vector expressions. More... | |
| class | BitVecNum |
| Bit-vector numerals. More... | |
| class | BitVecSort |
| Bit-vector sorts. More... | |
| class | BoolExpr |
| Boolean expressions. More... | |
| class | BoolSort |
| A Boolean sort. More... | |
| class | Constructor |
| Constructors are used for datatype sorts. More... | |
| class | ConstructorList |
| Lists of constructors. More... | |
| class | Context |
| The main interaction with Z3 happens via the Context. More... | |
| class | DatatypeExpr |
| Datatype expressions. More... | |
| class | DatatypeSort |
| Datatype sorts. More... | |
| class | Deprecated |
| The main interaction with Z3 happens via the Context. More... | |
| class | EnumSort |
| Enumeration sorts. More... | |
| class | Expr |
| Expressions are terms. More... | |
| class | FiniteDomainSort |
| Finite domain sorts. More... | |
| class | Fixedpoint |
| Object for managing fixedpoints. More... | |
| class | FPExpr |
| FloatingPoint Expressions. More... | |
| class | FPNum |
| FloatiungPoint Numerals. More... | |
| class | FPRMExpr |
| FloatingPoint RoundingMode Expressions. More... | |
| class | FPRMNum |
| Floating-point rounding mode numerals. More... | |
| class | FPRMSort |
| The FloatingPoint RoundingMode sort. More... | |
| class | FPSort |
| FloatingPoint sort. 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 | Global |
| Global functions for Z3. | |
| 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 | IDecRefQueue |
| DecRefQueue interface. More... | |
| class | DecRefQueueContracts |
| class | InterpolationContext |
| The InterpolationContext is suitable for generation of interpolants. More... | |
| class | IntExpr |
| Int expressions. More... | |
| class | IntNum |
| Integer Numerals. More... | |
| class | IntSort |
| An Integer sort. More... | |
| class | IntSymbol |
| Numbered symbols. More... | |
| class | ListSort |
| List sorts. More... | |
| class | Log |
| Interaction logging for Z3. | |
| class | Model |
| A Model contains interpretations (assignments) of constants and functions. More... | |
| class | Native |
| class | Optimize |
| Object for managing optimizization context. More... | |
| class | ParamDescrs |
| A ParamDescrs describes a set of parameters. More... | |
| class | Params |
| A Params objects 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 | RatNum |
| Rational Numerals. More... | |
| class | RealExpr |
| Real expressions. More... | |
| class | RealSort |
| A real sort. More... | |
| class | RelationSort |
| Relation sorts. More... | |
| class | SetSort |
| Set sorts. 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 | StringSymbol |
| Named symbols. 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 | TupleSort |
| Tuple sorts. More... | |
| class | UninterpretedSort |
| Uninterpreted Sorts. 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_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... | |
| enum | Status { UNSATISFIABLE = -1, UNKNOWN = 0, SATISFIABLE = 1 } |
| Status values. More... | |
| enum Status |
| enum Z3_ast_kind |
Z3_ast_kind.
| 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 50 of file Enumerations.cs.
{
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,
}
| enum Z3_ast_print_mode |
Z3_ast_print_mode.
| Z3_PRINT_SMTLIB2_COMPLIANT | |
| Z3_PRINT_SMTLIB_COMPLIANT | |
| Z3_PRINT_SMTLIB_FULL | |
| Z3_PRINT_LOW_LEVEL |
Definition at line 275 of file Enumerations.cs.
{
Z3_PRINT_SMTLIB2_COMPLIANT = 3,
Z3_PRINT_SMTLIB_COMPLIANT = 2,
Z3_PRINT_SMTLIB_FULL = 0,
Z3_PRINT_LOW_LEVEL = 1,
}
| enum Z3_decl_kind |
Z3_decl_kind.
Definition at line 61 of file Enumerations.cs.
{
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,
}
| enum Z3_error_code |
Z3_error_code.
| 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 283 of file Enumerations.cs.
{
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,
}
| enum Z3_goal_prec |
Z3_goal_prec.
Definition at line 300 of file Enumerations.cs.
{
Z3_GOAL_UNDER = 1,
Z3_GOAL_PRECISE = 0,
Z3_GOAL_UNDER_OVER = 3,
Z3_GOAL_OVER = 2,
}
| enum Z3_lbool |
Z3_lbool.
Definition at line 10 of file Enumerations.cs.
{
Z3_L_TRUE = 1,
Z3_L_UNDEF = 0,
Z3_L_FALSE = -1,
}
| enum Z3_param_kind |
Z3_param_kind.
Definition at line 264 of file Enumerations.cs.
{
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,
}
| enum Z3_parameter_kind |
Z3_parameter_kind.
| 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_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,
}
| enum Z3_sort_kind |
Z3_sort_kind.
Definition at line 34 of file Enumerations.cs.
{
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,
}
| enum Z3_symbol_kind |
Z3_symbol_kind.
Definition at line 17 of file Enumerations.cs.
{
Z3_INT_SYMBOL = 0,
Z3_STRING_SYMBOL = 1,
}
1.7.6.1