diff --git a/scripts/mk_make.py b/scripts/mk_make.py
index 58a2907a5..27cfdc575 100644
--- a/scripts/mk_make.py
+++ b/scripts/mk_make.py
@@ -72,5 +72,5 @@ update_version(4, 2, 0, 0)
mk_auto_src()
mk_bindings(API_files)
-mk_makefile()
+# mk_makefile()
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index cd7660950..5d92be0db 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -681,6 +681,7 @@ def mk_def_files():
def mk_bindings(api_files):
mk_z3consts_py(api_files)
+ mk_z3consts_donet(api_files)
# Extract enumeration types from API files, and add python definitions.
def mk_z3consts_py(api_files):
@@ -760,5 +761,90 @@ def mk_z3consts_py(api_files):
print "Generated '%s'" % ('%s/z3consts.py' % PYTHON_DIR)
+# Extract enumeration types from z3_api.h, and add .Net definitions
+def mk_z3consts_donet(api_files):
+ blank_pat = re.compile("^ *$")
+ comment_pat = re.compile("^ *//.*$")
+ typedef_pat = re.compile("typedef enum *")
+ typedef2_pat = re.compile("typedef enum { *")
+ openbrace_pat = re.compile("{ *")
+ closebrace_pat = re.compile("}.*;")
+
+ dotnet = _Name2Component['dotnet']
+
+ DeprecatedEnums = { 'Z3_search_failure' }
+ z3consts = open('%s/Enumerations.cs' % dotnet.src_dir, 'w')
+ z3consts.write('// Automatically generated file\n\n')
+ z3consts.write('using System;\n\n'
+ '#pragma warning disable 1591\n\n'
+ 'namespace Microsoft.Z3\n'
+ '{\n');
+
+ for api_file in api_files:
+ api_file_c = dotnet.find_file(api_file, dotnet.name)
+ api_file = '%s/%s' % (api_file_c.src_dir, api_file)
+
+ api = open(api_file, 'r')
+
+ SEARCHING = 0
+ FOUND_ENUM = 1
+ IN_ENUM = 2
+
+ mode = SEARCHING
+ decls = {}
+ idx = 0
+
+ linenum = 1
+ for line in api:
+ m1 = blank_pat.match(line)
+ m2 = comment_pat.match(line)
+ if m1 or m2:
+ # skip blank lines and comments
+ linenum = linenum + 1
+ elif mode == SEARCHING:
+ m = typedef_pat.match(line)
+ if m:
+ mode = FOUND_ENUM
+ m = typedef2_pat.match(line)
+ if m:
+ mode = IN_ENUM
+ decls = {}
+ idx = 0
+ elif mode == FOUND_ENUM:
+ m = openbrace_pat.match(line)
+ if m:
+ mode = IN_ENUM
+ decls = {}
+ idx = 0
+ else:
+ assert False, "Invalid %s, line: %s" % (api_file, linenum)
+ else:
+ assert mode == IN_ENUM
+ words = re.split('[^\-a-zA-Z0-9_]+', line)
+ m = closebrace_pat.match(line)
+ if m:
+ name = words[1]
+ if name not in DeprecatedEnums:
+ z3consts.write(' /// %s\n' % name)
+ z3consts.write(' public enum %s {\n' % name)
+ z3consts.write
+ for k, i in decls.iteritems():
+ z3consts.write(' %s = %s,\n' % (k, i))
+ z3consts.write(' }\n\n')
+ mode = SEARCHING
+ else:
+ if words[2] != '':
+ if len(words[2]) > 1 and words[2][1] == 'x':
+ idx = int(words[2], 16)
+ else:
+ idx = int(words[2])
+ decls[words[1]] = idx
+ idx = idx + 1
+ linenum = linenum + 1
+ z3consts.write('}\n');
+ if VERBOSE:
+ print "Generated '%s'" % ('%s/Enumerations.cs' % dotnet.src_dir)
+
+
def get_component(name):
return _Name2Component[name]
diff --git a/scripts/update_api.py b/scripts/update_api.py
index ba5db8f06..28bd94172 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -18,83 +18,6 @@ add_api_file('lib', 'z3_api.h')
add_api_file('lib', 'z3_internal_types.h')
add_api_file('lib', 'z3_poly.h')
-# Extract enumeration types from z3_api.h, and add .Net definitions
-def mk_z3consts_donet():
- blank_pat = re.compile("^ *$")
- comment_pat = re.compile("^ *//.*$")
- typedef_pat = re.compile("typedef enum *")
- typedef2_pat = re.compile("typedef enum { *")
- openbrace_pat = re.compile("{ *")
- closebrace_pat = re.compile("}.*;")
-
- DeprecatedEnums = { 'Z3_search_failure' }
- z3consts = open('Microsoft.Z3%sEnumerations.cs' % os.sep, 'w')
- z3consts.write('// Automatically generated file, generator: update_api.py\n\n')
- z3consts.write('using System;\n\n'
- '#pragma warning disable 1591\n\n'
- 'namespace Microsoft.Z3\n'
- '{\n');
-
- for api_file in API_FILES:
- api = open(api_file, 'r')
-
- SEARCHING = 0
- FOUND_ENUM = 1
- IN_ENUM = 2
-
- mode = SEARCHING
- decls = {}
- idx = 0
-
- linenum = 1
- for line in api:
- m1 = blank_pat.match(line)
- m2 = comment_pat.match(line)
- if m1 or m2:
- # skip blank lines and comments
- linenum = linenum + 1
- elif mode == SEARCHING:
- m = typedef_pat.match(line)
- if m:
- mode = FOUND_ENUM
- m = typedef2_pat.match(line)
- if m:
- mode = IN_ENUM
- decls = {}
- idx = 0
- elif mode == FOUND_ENUM:
- m = openbrace_pat.match(line)
- if m:
- mode = IN_ENUM
- decls = {}
- idx = 0
- else:
- assert False, "Invalid %s, line: %s" % (api_file, linenum)
- else:
- assert mode == IN_ENUM
- words = re.split('[^\-a-zA-Z0-9_]+', line)
- m = closebrace_pat.match(line)
- if m:
- name = words[1]
- if name not in DeprecatedEnums:
- z3consts.write(' /// %s\n' % name)
- z3consts.write(' public enum %s {\n' % name)
- z3consts.write
- for k, i in decls.iteritems():
- z3consts.write(' %s = %s,\n' % (k, i))
- z3consts.write(' }\n\n')
- mode = SEARCHING
- else:
- if words[2] != '':
- if len(words[2]) > 1 and words[2][1] == 'x':
- idx = int(words[2], 16)
- else:
- idx = int(words[2])
- decls[words[1]] = idx
- idx = idx + 1
- linenum = linenum + 1
- z3consts.write('}\n');
-
#
# Generate logging support and bindings
diff --git a/src/bindings/dotnet/Microsoft.Z3/Enumerations.cs b/src/bindings/dotnet/Microsoft.Z3/Enumerations.cs
deleted file mode 100644
index 36f49005e..000000000
--- a/src/bindings/dotnet/Microsoft.Z3/Enumerations.cs
+++ /dev/null
@@ -1,258 +0,0 @@
-// Automatically generated file, generator: update_api.py
-
-using System;
-
-#pragma warning disable 1591
-
-namespace Microsoft.Z3
-{
- /// Z3_lbool
- public enum Z3_lbool {
- Z3_L_TRUE = 1,
- Z3_L_UNDEF = 0,
- Z3_L_FALSE = -1,
- }
-
- /// Z3_symbol_kind
- public enum Z3_symbol_kind {
- Z3_INT_SYMBOL = 0,
- Z3_STRING_SYMBOL = 1,
- }
-
- /// Z3_parameter_kind
- public 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_sort_kind
- public 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_ast_kind
- public 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_decl_kind
- public 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_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_param_kind
- public 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_ast_print_mode
- public 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_error_code
- public 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_goal_prec
- public enum Z3_goal_prec {
- Z3_GOAL_UNDER = 1,
- Z3_GOAL_PRECISE = 0,
- Z3_GOAL_UNDER_OVER = 3,
- Z3_GOAL_OVER = 2,
- }
-
-}