diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py
index 2c017bd2c..482b13c94 100755
--- a/scripts/mk_consts_files.py
+++ b/scripts/mk_consts_files.py
@@ -16,6 +16,7 @@ def main(args):
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument("api_files", nargs="+")
parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None)
+ parser.add_argument("--dotnet-output-dir", dest="dotnet_output_dir", default=None)
pargs = parser.parse_args(args)
if not mk_genfile_common.check_files_exist(pargs.api_files):
@@ -31,6 +32,15 @@ def main(args):
logging.info('Generated "{}"'.format(output))
count += 1
+ if pargs.dotnet_output_dir:
+ if not mk_genfile_common.check_dir_exists(pargs.dotnet_output_dir):
+ return 1
+ output = mk_genfile_common.mk_z3consts_dotnet_internal(
+ pargs.api_files,
+ pargs.dotnet_output_dir)
+ logging.info('Generated "{}"'.format(output))
+ count += 1
+
if count == 0:
logging.info('No files generated. You need to specific an output directory'
' for the relevant langauge bindings')
diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py
index 38d173108..9c6431248 100644
--- a/scripts/mk_genfile_common.py
+++ b/scripts/mk_genfile_common.py
@@ -163,6 +163,98 @@ def mk_z3consts_py_internal(api_files, output_dir):
z3consts.close()
return z3consts_output_path
+def mk_z3consts_dotnet_internal(api_files, output_dir):
+ """
+ Generate ``Enumerations.cs`` from the list of API header files
+ in ``api_files`` and write the output file into
+ the ``output_dir`` directory
+
+ Returns the path to the generated file.
+ """
+ assert os.path.isdir(output_dir)
+ assert isinstance(api_files, list)
+ blank_pat = re.compile("^ *\r?$")
+ 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(os.path.join(output_dir, 'Enumerations.cs'), 'w')
+ z3consts_output_path = z3consts.name
+ 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 = 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(' /// <summary>%s</summary>\n' % name)
+ z3consts.write(' public enum %s {\n' % name)
+ z3consts.write
+ for k in decls:
+ i = decls[k]
+ z3consts.write(' %s = %s,\n' % (k, i))
+ z3consts.write(' }\n\n')
+ mode = SEARCHING
+ elif len(words) <= 2:
+ assert False, "Invalid %s, line: %s" % (api_file, linenum)
+ 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
+ api.close()
+ z3consts.write('}\n');
+ z3consts.close()
+ return z3consts_output_path
+
###############################################################################
# Functions for generating a "module definition file" for MSVC
###############################################################################
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index e6de3e8ea..dc85c2b76 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2738,96 +2738,17 @@ def mk_z3consts_py(api_files):
if VERBOSE:
print("Generated '{}".format(generated_file))
-
# Extract enumeration types from z3_api.h, and add .Net definitions
def mk_z3consts_dotnet(api_files):
- blank_pat = re.compile("^ *\r?$")
- 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 = get_component(DOTNET_COMPONENT)
-
- DeprecatedEnums = [ 'Z3_search_failure' ]
- z3consts = open(os.path.join(dotnet.src_dir, 'Enumerations.cs'), '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')
-
+ full_path_api_files = []
for api_file in api_files:
api_file_c = dotnet.find_file(api_file, dotnet.name)
api_file = os.path.join(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(' /// <summary>%s</summary>\n' % name)
- z3consts.write(' public enum %s {\n' % name)
- z3consts.write
- for k in decls:
- i = decls[k]
- z3consts.write(' %s = %s,\n' % (k, i))
- z3consts.write(' }\n\n')
- mode = SEARCHING
- elif len(words) <= 2:
- assert False, "Invalid %s, line: %s" % (api_file, linenum)
- 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
- api.close()
- z3consts.write('}\n');
- z3consts.close()
+ full_path_api_files.append(api_file)
+ generated_file = mk_genfile_common.mk_z3consts_dotnet_internal(full_path_api_files, dotnet.src_dir)
if VERBOSE:
- print("Generated '%s'" % os.path.join(dotnet.src_dir, 'Enumerations.cs'))
-
+ print("Generated '{}".format(generated_file))
# Extract enumeration types from z3_api.h, and add Java definitions
def mk_z3consts_java(api_files):