mirror of
https://github.com/Z3Prover/z3
synced 2025-04-26 18:45:33 +00:00
auto gen for Enumeration.cs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
d40c62d8aa
commit
639f66da0a
4 changed files with 87 additions and 336 deletions
|
|
@ -72,5 +72,5 @@ update_version(4, 2, 0, 0)
|
|||
mk_auto_src()
|
||||
mk_bindings(API_files)
|
||||
|
||||
mk_makefile()
|
||||
# mk_makefile()
|
||||
|
||||
|
|
|
|||
|
|
@ -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(' /// <summary>%s</summary>\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]
|
||||
|
|
|
|||
|
|
@ -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(' /// <summary>%s</summary>\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
|
||||
|
|
|
|||
|
|
@ -1,258 +0,0 @@
|
|||
// Automatically generated file, generator: update_api.py
|
||||
|
||||
using System;
|
||||
|
||||
#pragma warning disable 1591
|
||||
|
||||
namespace Microsoft.Z3
|
||||
{
|
||||
/// <summary>Z3_lbool</summary>
|
||||
public enum Z3_lbool {
|
||||
Z3_L_TRUE = 1,
|
||||
Z3_L_UNDEF = 0,
|
||||
Z3_L_FALSE = -1,
|
||||
}
|
||||
|
||||
/// <summary>Z3_symbol_kind</summary>
|
||||
public enum Z3_symbol_kind {
|
||||
Z3_INT_SYMBOL = 0,
|
||||
Z3_STRING_SYMBOL = 1,
|
||||
}
|
||||
|
||||
/// <summary>Z3_parameter_kind</summary>
|
||||
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,
|
||||
}
|
||||
|
||||
/// <summary>Z3_sort_kind</summary>
|
||||
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,
|
||||
}
|
||||
|
||||
/// <summary>Z3_ast_kind</summary>
|
||||
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,
|
||||
}
|
||||
|
||||
/// <summary>Z3_decl_kind</summary>
|
||||
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,
|
||||
}
|
||||
|
||||
/// <summary>Z3_param_kind</summary>
|
||||
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,
|
||||
}
|
||||
|
||||
/// <summary>Z3_ast_print_mode</summary>
|
||||
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,
|
||||
}
|
||||
|
||||
/// <summary>Z3_error_code</summary>
|
||||
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,
|
||||
}
|
||||
|
||||
/// <summary>Z3_goal_prec</summary>
|
||||
public enum Z3_goal_prec {
|
||||
Z3_GOAL_UNDER = 1,
|
||||
Z3_GOAL_PRECISE = 0,
|
||||
Z3_GOAL_UNDER_OVER = 3,
|
||||
Z3_GOAL_OVER = 2,
|
||||
}
|
||||
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue