|
Z3
|
|
All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
|
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... | |
| 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 48 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 227 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 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,
}
| 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 235 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 252 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 216 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.
| 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_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,
}
| 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