mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
auto gen for z3consts.py
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
a9a46ec145
commit
d40c62d8aa
|
|
@ -62,12 +62,15 @@ add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig', 'muz_qe',
|
||||||
add_lib('api', ['portfolio', 'user_plugin'])
|
add_lib('api', ['portfolio', 'user_plugin'])
|
||||||
add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3')
|
add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3')
|
||||||
add_exe('test', ['api', 'fuzzing'], exe_name='test-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('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')
|
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)
|
update_version(4, 2, 0, 0)
|
||||||
|
mk_auto_src()
|
||||||
|
mk_bindings(API_files)
|
||||||
|
|
||||||
mk_makefile()
|
mk_makefile()
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -23,6 +23,7 @@ DEBUG_MODE=False
|
||||||
SHOW_CPPS = True
|
SHOW_CPPS = True
|
||||||
VS_X64 = False
|
VS_X64 = False
|
||||||
ONLY_MAKEFILES = False
|
ONLY_MAKEFILES = False
|
||||||
|
PYTHON_DIR=None
|
||||||
|
|
||||||
if os.name == 'nt':
|
if os.name == 'nt':
|
||||||
IS_WINDOW=True
|
IS_WINDOW=True
|
||||||
|
|
@ -112,6 +113,15 @@ def set_build_dir(d):
|
||||||
BUILD_DIR = d
|
BUILD_DIR = d
|
||||||
REV_BUILD_DIR = reverse_path(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
|
_UNIQ_ID = 0
|
||||||
|
|
||||||
def mk_fresh_name(prefix):
|
def mk_fresh_name(prefix):
|
||||||
|
|
@ -668,6 +678,87 @@ def mk_def_files():
|
||||||
for c in _Components:
|
for c in _Components:
|
||||||
if c.require_def_file():
|
if c.require_def_file():
|
||||||
mk_def_file(c)
|
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):
|
def get_component(name):
|
||||||
return _Name2Component[name]
|
return _Name2Component[name]
|
||||||
|
|
|
||||||
|
|
@ -8,7 +8,6 @@
|
||||||
import re
|
import re
|
||||||
import sys
|
import sys
|
||||||
import os
|
import os
|
||||||
from sets import Set
|
|
||||||
|
|
||||||
API_FILES = []
|
API_FILES = []
|
||||||
|
|
||||||
|
|
@ -97,106 +96,6 @@ def mk_z3consts_donet():
|
||||||
z3consts.write('}\n');
|
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
|
# Generate logging support and bindings
|
||||||
#
|
#
|
||||||
|
|
|
||||||
|
|
@ -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
|
|
||||||
|
|
||||||
Loading…
Reference in a new issue