From d40c62d8aa24b389ea07065ef303334cecfd301c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Oct 2012 17:30:38 -0700 Subject: [PATCH] auto gen for z3consts.py Signed-off-by: Leonardo de Moura --- scripts/mk_make.py | 7 +- scripts/mk_util.py | 91 ++++++++++++ scripts/update_api.py | 101 ------------- src/bindings/python/z3consts.py | 241 -------------------------------- 4 files changed, 96 insertions(+), 344 deletions(-) delete mode 100644 src/bindings/python/z3consts.py diff --git a/scripts/mk_make.py b/scripts/mk_make.py index 0d0891705..58a2907a5 100644 --- a/scripts/mk_make.py +++ b/scripts/mk_make.py @@ -62,12 +62,15 @@ add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig', 'muz_qe', add_lib('api', ['portfolio', 'user_plugin']) add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3') add_exe('test', ['api', 'fuzzing'], exe_name='test-z3') -add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', dll_name='z3', export_files=['z3_api.h', 'z3_poly.h']) +API_files = ['z3_api.h', 'z3_poly.h'] +add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', dll_name='z3', export_files=API_files) add_dot_net_dll('dotnet', ['api_dll'], 'bindings/dotnet/Microsoft.Z3', dll_name='Microsoft.Z3', assembly_info_dir='Properties') add_dot_net_dll('dotnetV3', ['api_dll'], 'bindings/dotnet/Microsoft.Z3V3', dll_name='Microsoft.Z3V3') +set_python_dir('bindings/python') -mk_auto_src() update_version(4, 2, 0, 0) +mk_auto_src() +mk_bindings(API_files) mk_makefile() diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 9935413f3..cd7660950 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -23,6 +23,7 @@ DEBUG_MODE=False SHOW_CPPS = True VS_X64 = False ONLY_MAKEFILES = False +PYTHON_DIR=None if os.name == 'nt': IS_WINDOW=True @@ -112,6 +113,15 @@ def set_build_dir(d): BUILD_DIR = d REV_BUILD_DIR = reverse_path(d) +def set_python_dir(p): + global SRC_DIR, PYTHON_DIR + full = '%s/%s' % (SRC_DIR, p) + if not os.path.exists(full): + raise MKException("Python bindings directory '%s' does not exist" % full) + PYTHON_DIR = full + if VERBOSE: + print "Python bindinds directory was detected." + _UNIQ_ID = 0 def mk_fresh_name(prefix): @@ -668,6 +678,87 @@ def mk_def_files(): for c in _Components: if c.require_def_file(): mk_def_file(c) + +def mk_bindings(api_files): + mk_z3consts_py(api_files) + +# Extract enumeration types from API files, and add python definitions. +def mk_z3consts_py(api_files): + if PYTHON_DIR == None: + raise MKException("You must invoke set_python_dir(path):") + + 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("}.*;") + + z3consts = open('%s/z3consts.py' % PYTHON_DIR, 'w') + z3consts.write('# Automatically generated file\n\n') + + api_dll = _Name2Component['api_dll'] + + for api_file in api_files: + api_file_c = api_dll.find_file(api_file, api_dll.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] + z3consts.write('# enum %s\n' % name) + for k, i in decls.iteritems(): + z3consts.write('%s = %s\n' % (k, i)) + z3consts.write('\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 + if VERBOSE: + print "Generated '%s'" % ('%s/z3consts.py' % PYTHON_DIR) + def get_component(name): return _Name2Component[name] diff --git a/scripts/update_api.py b/scripts/update_api.py index aefb08d2e..ba5db8f06 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -8,7 +8,6 @@ import re import sys import os -from sets import Set API_FILES = [] @@ -97,106 +96,6 @@ def mk_z3consts_donet(): z3consts.write('}\n'); -# Extract enumeration types from z3_api.h, and add python definitions. -def mk_z3consts_py(): - 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("}.*;") - - z3consts = open('python%sz3consts.py' % (os.sep), 'w') - z3consts.write('# Automatically generated file, generator: update_api.py\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] - z3consts.write('# enum %s\n' % name) - for k, i in decls.iteritems(): - z3consts.write('%s = %s\n' % (k, i)) - z3consts.write('\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 - -# Extract tactic and probe definitions from lib\install_tactics.cpp, and -# Add python function definitions for them. -def mk_z3tactics_py(): - tactic_pat = re.compile("^[ \t]*ADD_TACTIC_CMD") - probe_pat = re.compile("^[ \t]*ADD_PROBE") - - cppfile = open('lib%sinstall_tactics.cpp' % os.sep, 'r') - z3tactics = open('python%sz3tactics.py' % os.sep, 'w') - - z3tactics.write('# Automatically generated file, generator: update_api.py\n') - z3tactics.write('import z3core\n') - z3tactics.write('import z3\n\n') - - for line in cppfile: - m1 = tactic_pat.match(line) - m2 = probe_pat.match(line) - if m1: - words = re.split('[^\-a-zA-Z0-9_]+', line) - tactic = words[2] - py_tactic = tactic.replace('-', '_') - z3tactics.write('def %s_tactic(ctx=None):\n' % py_tactic) - z3tactics.write(' ctx = z3._get_ctx(ctx)\n') - z3tactics.write(' return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), \'%s\'), ctx)\n\n' % tactic) - elif m2: - words = re.split('[^\-a-zA-Z0-9_]+', line) - probe = words[2] - py_probe = probe.replace('-', '_') - z3tactics.write('def %s_probe(ctx=None):\n' % py_probe) - z3tactics.write(' ctx = z3._get_ctx(ctx)\n') - z3tactics.write(' return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), \'%s\'), ctx)\n\n' % probe) - - # # Generate logging support and bindings # diff --git a/src/bindings/python/z3consts.py b/src/bindings/python/z3consts.py deleted file mode 100644 index caa7daf4d..000000000 --- a/src/bindings/python/z3consts.py +++ /dev/null @@ -1,241 +0,0 @@ -# Automatically generated file, generator: update_api.py - -# enum Z3_lbool -Z3_L_TRUE = 1 -Z3_L_UNDEF = 0 -Z3_L_FALSE = -1 - -# enum Z3_symbol_kind -Z3_INT_SYMBOL = 0 -Z3_STRING_SYMBOL = 1 - -# 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 - -# 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 - -# 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 - -# 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 - -# 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 - -# enum Z3_search_failure -Z3_QUANTIFIERS = 7 -Z3_UNKNOWN = 1 -Z3_CANCELED = 4 -Z3_MEMOUT_WATERMARK = 3 -Z3_THEORY = 6 -Z3_NO_FAILURE = 0 -Z3_TIMEOUT = 2 -Z3_NUM_CONFLICTS = 5 - -# 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 - -# 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 - -# enum Z3_goal_prec -Z3_GOAL_UNDER = 1 -Z3_GOAL_PRECISE = 0 -Z3_GOAL_UNDER_OVER = 3 -Z3_GOAL_OVER = 2 -