From 6602803850d84ef0e09c142c6133721b9692a8cf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 20 Dec 2012 17:47:38 -0800 Subject: [PATCH] Add Python 3.x support Signed-off-by: Leonardo de Moura --- RELEASE_NOTES | 2 + examples/python/example.py | 4 +- scripts/mk_util.py | 209 ++++++++--------- scripts/update_api.py | 61 +++-- src/api/python/z3.py | 449 +++++++++++++++++++----------------- src/api/python/z3printer.py | 59 +++-- 6 files changed, 426 insertions(+), 358 deletions(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 234ba03fb..694a6d635 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -9,6 +9,8 @@ Version 4.3.2 - Added support for FreeBSD. Z3 can be compiled on FreeBSD using g++. +- Added support for Python 3.x. + - Reverted to `(set-option :global-decls false)` as the default. In Z3 4.3.0 and Z3 4.3.1, this option was set to true. Thanks to Julien Henry for reporting this problem. diff --git a/examples/python/example.py b/examples/python/example.py index a8a764a4d..879c17c43 100644 --- a/examples/python/example.py +++ b/examples/python/example.py @@ -4,5 +4,5 @@ x = Real('x') y = Real('y') s = Solver() s.add(x + y > 5, x > 1, y > 1) -print s.check() -print s.model() +print(s.check()) +print(s.model()) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 3ffa7e313..268a6d27b 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -7,11 +7,6 @@ # Author: Leonardo de Moura (leonardo) ############################################ import sys - -if sys.version >= "3": - print "ERROR: python 2.x required." - exit(1) - import os import glob import re @@ -134,8 +129,7 @@ def exec_cmd(cmd): first = True for e in cmd: if first: - # Allow spaces in the executable name - first = False + first = False new_cmd.append(e) else: if e != "": @@ -166,7 +160,7 @@ def exec_compiler_cmd(cmd): def test_cxx_compiler(cc): if is_verbose(): - print "Testing %s..." % cc + print("Testing %s..." % cc) t = TempFile('tst.cpp') t.add('#include\nint main() { return 0; }\n') t.commit() @@ -174,7 +168,7 @@ def test_cxx_compiler(cc): def test_c_compiler(cc): if is_verbose(): - print "Testing %s..." % cc + print("Testing %s..." % cc) t = TempFile('tst.c') t.add('#include\nint main() { return 0; }\n') t.commit() @@ -182,7 +176,7 @@ def test_c_compiler(cc): def test_gmp(cc): if is_verbose(): - print "Testing GMP..." + print("Testing GMP...") t = TempFile('tstgmp.cpp') t.add('#include\nint main() { mpz_t t; mpz_init(t); mpz_clear(t); return 0; }\n') t.commit() @@ -190,7 +184,7 @@ def test_gmp(cc): def test_openmp(cc): if is_verbose(): - print "Testing OpenMP..." + print("Testing OpenMP...") t = TempFile('tstomp.cpp') t.add('#include\nint main() { return omp_in_parallel() ? 1 : 0; }\n') t.commit() @@ -201,12 +195,12 @@ def check_java(): t.add('public class Hello { public static void main(String[] args) { System.out.println("Hello, World"); }}\n') t.commit() if is_verbose(): - print "Testing %s..." % JAVAC + print("Testing %s..." % JAVAC) r = exec_cmd([JAVAC, 'Hello.java']) if r != 0: raise MKException('Failed testing Java compiler. Set environment variable JAVAC with the path to the Java compiler') if is_verbose(): - print "Testing %s..." % JAVA + print("Testing %s..." % JAVA) r = exec_cmd([JAVA, 'Hello']) rmf('Hello.class') if r != 0: @@ -224,11 +218,11 @@ def find_java_home(): global JAVA_HOME if JAVA_HOME != None: if is_verbose(): - print "Checking jni.h..." + print("Checking jni.h...") if os.path.exists(os.path.join(JAVA_HOME, 'include', 'jni.h')): return if is_verbose(): - print "Finding JAVA_HOME..." + print("Finding JAVA_HOME...") t = TempFile('output') null = open(os.devnull, 'wb') try: @@ -242,17 +236,17 @@ def find_java_home(): m = open_pat.match(line) if m: # Remove last 3 directives from m.group(1) - print m.group(1) + print(m.group(1)) tmp = m.group(1).split(os.sep) path = string.join(tmp[:len(tmp) - 3], os.sep) if is_verbose(): - print "Checking jni.h..." + print("Checking jni.h...") jni_dir = find_jni_h(path) if not jni_dir: raise MKException("Failed to detect jni.h at '%s'.Possible solution: set JAVA_HOME with the path to JDK." % os.path.join(path, 'include')) JAVA_HOME = os.path.split(jni_dir)[0] if is_verbose(): - print 'JAVA_HOME=%s' % JAVA_HOME + print('JAVA_HOME=%s' % JAVA_HOME) return raise MKException('Failed to find JAVA_HOME') @@ -261,7 +255,7 @@ def is64(): def check_ar(): if is_verbose(): - print "Testing ar..." + print("Testing ar...") if which('ar')== None: raise MKException('ar (archive tool) was not found') @@ -322,7 +316,7 @@ def dos2unix(fname): fout.close() shutil.move(fname_new, fname) if is_verbose(): - print "dos2unix '%s'" % fname + print("dos2unix '%s'" % fname) def dos2unix_tree_core(pattern, dir, files): for filename in files: @@ -339,7 +333,7 @@ def check_eol(): # Linux/OSX/BSD check if the end-of-line is cr/lf if is_cr_lf('LICENSE.txt'): if is_verbose(): - print "Fixing end of line..." + print("Fixing end of line...") dos2unix_tree() if os.name == 'nt': @@ -355,42 +349,42 @@ elif os.name == 'posix': IS_LINUX=True def display_help(exit_code): - print "mk_make.py: Z3 Makefile generator\n" - print "This script generates the Makefile for the Z3 theorem prover." - print "It must be executed from the Z3 root directory." - print "\nOptions:" - print " -h, --help display this message." - print " -s, --silent do not print verbose messages." + print("mk_make.py: Z3 Makefile generator\n") + print("This script generates the Makefile for the Z3 theorem prover.") + print("It must be executed from the Z3 root directory.") + print("\nOptions:") + print(" -h, --help display this message.") + print(" -s, --silent do not print verbose messages.") if not IS_WINDOWS: - print " -p , --prefix= installation prefix (default: %s)." % PREFIX - print " -y , --pydir= installation prefix for Z3 python bindings (default: %s)." % PYTHON_PACKAGE_DIR + print(" -p , --prefix= installation prefix (default: %s)." % PREFIX) + print(" -y , --pydir= installation prefix for Z3 python bindings (default: %s)." % PYTHON_PACKAGE_DIR) else: - print " --parallel=num use cl option /MP with 'num' parallel processes" - print " -b , --build= subdirectory where Z3 will be built (default: build)." - print " -d, --debug compile Z3 in debug mode." - print " -t, --trace enable tracing in release mode." + print(" --parallel=num use cl option /MP with 'num' parallel processes") + print(" -b , --build= subdirectory where Z3 will be built (default: build).") + print(" -d, --debug compile Z3 in debug mode.") + print(" -t, --trace enable tracing in release mode.") if IS_WINDOWS: - print " -x, --x64 create 64 binary when using Visual Studio." - print " -m, --makefiles generate only makefiles." + print(" -x, --x64 create 64 binary when using Visual Studio.") + print(" -m, --makefiles generate only makefiles.") if IS_WINDOWS: - print " -v, --vsproj generate Visual Studio Project Files." + print(" -v, --vsproj generate Visual Studio Project Files.") if IS_WINDOWS: - print " -n, --nodotnet do not generate Microsoft.Z3.dll make rules." - print " -j, --java generate Java bindinds." - print " --staticlib build Z3 static library." + print(" -n, --nodotnet do not generate Microsoft.Z3.dll make rules.") + print(" -j, --java generate Java bindinds.") + print(" --staticlib build Z3 static library.") if not IS_WINDOWS: - print " -g, --gmp use GMP." - print "" - print "Some influential environment variables:" + print(" -g, --gmp use GMP.") + print("") + print("Some influential environment variables:") if not IS_WINDOWS: - print " CXX C++ compiler" - print " CC C compiler" - print " LDFLAGS Linker flags, e.g., -L if you have libraries in a non-standard directory" - print " CPPFLAGS Preprocessor flags, e.g., -I if you have header files in a non-standard directory" - print " CXXFLAGS C++ compiler flags" - print " JAVA Java virtual machine (only relevant if -j or --java option is provided)" - print " JAVAC Java compiler (only relevant if -j or --java option is provided)" - print " JAVA_HOME JDK installation directory (only relevant if -j or --java option is provided)" + print(" CXX C++ compiler") + print(" CC C compiler") + print(" LDFLAGS Linker flags, e.g., -L if you have libraries in a non-standard directory") + print(" CPPFLAGS Preprocessor flags, e.g., -I if you have header files in a non-standard directory") + print(" CXXFLAGS C++ compiler flags") + print(" JAVA Java virtual machine (only relevant if -j or --java option is provided)") + print(" JAVAC Java compiler (only relevant if -j or --java option is provided)") + print(" JAVA_HOME JDK installation directory (only relevant if -j or --java option is provided)") exit(exit_code) # Parse configuration option for mk_make script @@ -403,7 +397,7 @@ def parse_options(): ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'java', 'pydir=', 'parallel=']) except: - print "ERROR: Invalid command line option" + print("ERROR: Invalid command line option") display_help(1) for opt, arg in options: @@ -446,7 +440,7 @@ def parse_options(): elif opt in ('-j', '--java'): JAVA_ENABLED = True else: - print "ERROR: Invalid command line option '%s'" % opt + print("ERROR: Invalid command line option '%s'" % opt) display_help(1) # Return a list containing a file names included using '#include' in @@ -497,7 +491,7 @@ def set_z3py_dir(p): raise MKException("Python bindings directory '%s' does not exist" % full) Z3PY_SRC_DIR = full if VERBOSE: - print "Python bindinds directory was detected." + print("Python bindinds directory was detected.") _UNIQ_ID = 0 @@ -781,7 +775,7 @@ def comp_components(c1, c2): # Sort components based on (reverse) definition time def sort_components(cnames): - return sorted(cnames, cmp=comp_components) + return sorted(cnames, key=lambda c: get_component(c).id, reverse=True) class ExeComponent(Component): def __init__(self, name, exe_name, path, deps, install): @@ -1196,7 +1190,7 @@ class PythonExampleComponent(ExampleComponent): for py in filter(lambda f: f.endswith('.py'), os.listdir(full)): shutil.copyfile(os.path.join(full, py), os.path.join(BUILD_DIR, py)) if is_verbose(): - print "Copied Z3Py example '%s' to '%s'" % (py, BUILD_DIR) + print("Copied Z3Py example '%s' to '%s'" % (py, BUILD_DIR)) out.write('_ex_%s: \n\n' % self.name) @@ -1208,7 +1202,7 @@ def reg_component(name, c): _ComponentNames.add(name) _Name2Component[name] = c if VERBOSE: - print "New component: '%s'" % name + print("New component: '%s'" % name) def add_lib(name, deps=[], path=None, includes2install=[]): c = LibComponent(name, path, deps, includes2install) @@ -1315,11 +1309,11 @@ def mk_config(): # End of Windows VS config.mk if is_verbose(): - print '64-bit: %s' % is64() + print('64-bit: %s' % is64()) if is_java_enabled(): - print 'Java Home: %s' % JAVA_HOME - print 'Java Compiler: %s' % JAVAC - print 'Java VM: %s' % JAVA + print('Java Home: %s' % JAVA_HOME) + print('Java Compiler: %s' % JAVAC) + print('Java VM: %s' % JAVA) else: global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS ARITH = "internal" @@ -1401,17 +1395,17 @@ def mk_config(): config.write('SLINK_EXTRA_FLAGS=%s\n' % SLIBEXTRAFLAGS) config.write('SLINK_OUT_FLAG=-o \n') if is_verbose(): - print 'Host platform: %s' % sysname - print 'C++ Compiler: %s' % CXX - print 'C Compiler : %s' % CC - print 'Arithmetic: %s' % ARITH - print 'OpenMP: %s' % HAS_OMP - print 'Prefix: %s' % PREFIX - print '64-bit: %s' % is64() + print('Host platform: %s' % sysname) + print('C++ Compiler: %s' % CXX) + print('C Compiler : %s' % CC) + print('Arithmetic: %s' % ARITH) + print('OpenMP: %s' % HAS_OMP) + print('Prefix: %s' % PREFIX) + print('64-bit: %s' % is64()) if is_java_enabled(): - print 'Java Home: %s' % JAVA_HOME - print 'Java Compiler: %s' % JAVAC - print 'Java VM: %s' % JAVA + print('Java Home: %s' % JAVA_HOME) + print('Java Compiler: %s' % JAVAC) + print('Java VM: %s' % JAVA) def mk_install(out): out.write('install:\n') @@ -1437,7 +1431,7 @@ def mk_makefile(): mk_dir(BUILD_DIR) mk_config() if VERBOSE: - print "Writing %s" % os.path.join(BUILD_DIR, 'Makefile') + print("Writing %s" % os.path.join(BUILD_DIR, 'Makefile')) out = open(os.path.join(BUILD_DIR, 'Makefile'), 'w') out.write('# Automatically generated file.\n') out.write('include config.mk\n') @@ -1465,24 +1459,24 @@ def mk_makefile(): mk_uninstall(out) # Finalize if VERBOSE: - print "Makefile was successfully generated." + print("Makefile was successfully generated.") if not IS_WINDOWS: - print " python packages dir:", PYTHON_PACKAGE_DIR + print(" python packages dir: %s" % PYTHON_PACKAGE_DIR) if DEBUG_MODE: - print " compilation mode: Debug" + print(" compilation mode: Debug") else: - print " compilation mode: Release" + print(" compilation mode: Release") if IS_WINDOWS: if VS_X64: - print " platform: x64\n" - print "To build Z3, open a [Visual Studio x64 Command Prompt], then" + print(" platform: x64\n") + print("To build Z3, open a [Visual Studio x64 Command Prompt], then") else: - print " platform: x86" - print "To build Z3, open a [Visual Studio Command Prompt], then" - print "type 'cd %s && nmake'\n" % os.path.join(os.getcwd(), BUILD_DIR) - print 'Remark: to open a Visual Studio Command Prompt, go to: "Start > All Programs > Visual Studio > Visual Studio Tools"' + print(" platform: x86") + print("To build Z3, open a [Visual Studio Command Prompt], then") + print("type 'cd %s && nmake'\n" % os.path.join(os.getcwd(), BUILD_DIR)) + print('Remark: to open a Visual Studio Command Prompt, go to: "Start > All Programs > Visual Studio > Visual Studio Tools"') else: - print "Type 'cd %s; make' to build Z3" % BUILD_DIR + print("Type 'cd %s; make' to build Z3" % BUILD_DIR) # Generate automatically generated source code def mk_auto_src(): @@ -1577,7 +1571,7 @@ def def_module_params(module_name, export, params, class_name=None, description= out.write('};\n') out.write('#endif\n') if is_verbose(): - print "Generated '%s'" % hpp + print("Generated '%s'" % hpp) def max_memory_param(): return ('max_memory', UINT, UINT_MAX, 'maximum amount of memory in megabytes') @@ -1591,6 +1585,10 @@ PYG_GLOBALS = { 'UINT' : UINT, 'BOOL' : BOOL, 'DOUBLE' : DOUBLE, 'STRING' : STRI 'max_steps_param' : max_steps_param, 'def_module_params' : def_module_params } +def _execfile(file, globals=globals(), locals=locals()): + with open(file, "r") as fh: + exec(fh.read()+"\n", globals, locals) + # Execute python auxiliary scripts that generate extra code for Z3. def exec_pyg_scripts(): global CURR_PYG @@ -1599,7 +1597,7 @@ def exec_pyg_scripts(): if f.endswith('.pyg'): script = os.path.join(root, f) CURR_PYG = script - execfile(script, PYG_GLOBALS) + _execfile(script, PYG_GLOBALS) # TODO: delete after src/ast/pattern/expr_pattern_match # database.smt ==> database.h @@ -1612,7 +1610,7 @@ def mk_pat_db(): fout.write('"%s\\n"\n' % line.strip('\n')) fout.write(';\n') if VERBOSE: - print "Generated '%s'" % os.path.join(c.src_dir, 'database.h') + print("Generated '%s'" % os.path.join(c.src_dir, 'database.h')) # Update version numbers def update_version(): @@ -1637,7 +1635,7 @@ def mk_version_dot_h(major, minor, build, revision): fout.write('#define Z3_BUILD_NUMBER %s\n' % build) fout.write('#define Z3_REVISION_NUMBER %s\n' % revision) if VERBOSE: - print "Generated '%s'" % os.path.join(c.src_dir, 'version.h') + print("Generated '%s'" % os.path.join(c.src_dir, 'version.h')) # Update version number in AssemblyInfo.cs files def update_all_assembly_infos(major, minor, build, revision): @@ -1686,13 +1684,13 @@ def update_assembly_info_version(assemblyinfo, major, minor, build, revision, is else: fout.write(line) # if VERBOSE: - # print "%s version numbers updated at '%s'" % (num_updates, assemblyinfo) + # print("%s version numbers updated at '%s'" % (num_updates, assemblyinfo)) assert num_updates == 2, "unexpected number of version number updates" fin.close() fout.close() shutil.move(tmp, assemblyinfo) if VERBOSE: - print "Updated '%s'" % assemblyinfo + print("Updated '%s'" % assemblyinfo) ADD_TACTIC_DATA=[] ADD_PROBE_DATA=[] @@ -1734,7 +1732,7 @@ def mk_install_tactic_cpp(cnames, path): added_include = True fout.write('#include"%s"\n' % h_file) try: - exec line.strip('\n ') in globals() + exec(line.strip('\n '), globals()) except: raise MKException("Failed processing ADD_TACTIC command at '%s'\n%s" % (fullname, line)) if probe_pat.match(line): @@ -1742,7 +1740,7 @@ def mk_install_tactic_cpp(cnames, path): added_include = True fout.write('#include"%s"\n' % h_file) try: - exec line.strip('\n ') in globals() + exec(line.strip('\n '), globals()) except: raise MKException("Failed processing ADD_PROBE command at '%s'\n%s" % (fullname, line)) # First pass will just generate the tactic factories @@ -1761,7 +1759,7 @@ def mk_install_tactic_cpp(cnames, path): fout.write(' ADD_PROBE("%s", "%s", %s);\n' % data) fout.write('}\n') if VERBOSE: - print "Generated '%s'" % fullname + print("Generated '%s'" % fullname) def mk_all_install_tactic_cpps(): if not ONLY_MAKEFILES: @@ -1824,7 +1822,7 @@ def mk_mem_initializer_cpp(cnames, path): fout.write('\n') fout.write('}\n') if VERBOSE: - print "Generated '%s'" % fullname + print("Generated '%s'" % fullname) def mk_all_mem_initializer_cpps(): if not ONLY_MAKEFILES: @@ -1881,7 +1879,7 @@ def mk_gparams_register_modules(cnames, path): fout.write('gparams::register_module_descr("%s", "%s");\n' % (mod, descr)) fout.write('}\n') if VERBOSE: - print "Generated '%s'" % fullname + print("Generated '%s'" % fullname) def mk_all_gparams_register_modules(): if not ONLY_MAKEFILES: @@ -1914,7 +1912,7 @@ def mk_def_file(c): i = i + 1 num = num + 1 if VERBOSE: - print "Generated '%s'" % defname + print("Generated '%s'" % defname) def mk_def_files(): if not ONLY_MAKEFILES: @@ -1934,7 +1932,7 @@ def cp_z3pyc_to_build(): shutil.copyfile(os.path.join(Z3PY_SRC_DIR, pyc), os.path.join(BUILD_DIR, pyc)) os.remove(os.path.join(Z3PY_SRC_DIR, pyc)) if is_verbose(): - print "Generated '%s'" % pyc + print("Generated '%s'" % pyc) def mk_bindings(api_files): if not ONLY_MAKEFILES: @@ -1945,12 +1943,12 @@ def mk_bindings(api_files): for api_file in api_files: api_file_path = api.find_file(api_file, api.name) new_api_files.append(os.path.join(api_file_path.src_dir, api_file)) - g = {} + g = globals() g["API_FILES"] = new_api_files if is_java_enabled(): check_java() mk_z3consts_java(api_files) - execfile(os.path.join('scripts', 'update_api.py'), g) # HACK + _execfile(os.path.join('scripts', 'update_api.py'), g) # HACK cp_z3pyc_to_build() # Extract enumeration types from API files, and add python definitions. @@ -2014,7 +2012,8 @@ def mk_z3consts_py(api_files): if m: name = words[1] z3consts.write('# enum %s\n' % name) - for k, i in decls.iteritems(): + for k in decls: + i = decls[k] z3consts.write('%s = %s\n' % (k, i)) z3consts.write('\n') mode = SEARCHING @@ -2028,7 +2027,7 @@ def mk_z3consts_py(api_files): idx = idx + 1 linenum = linenum + 1 if VERBOSE: - print "Generated '%s'" % os.path.join(Z3PY_SRC_DIR, 'z3consts.py') + print("Generated '%s'" % os.path.join(Z3PY_SRC_DIR, 'z3consts.py')) # Extract enumeration types from z3_api.h, and add .Net definitions @@ -2098,7 +2097,8 @@ def mk_z3consts_dotnet(api_files): z3consts.write(' /// %s\n' % name) z3consts.write(' public enum %s {\n' % name) z3consts.write - for k, i in decls.iteritems(): + for k in decls: + i = decls[k] z3consts.write(' %s = %s,\n' % (k, i)) z3consts.write(' }\n\n') mode = SEARCHING @@ -2113,7 +2113,7 @@ def mk_z3consts_dotnet(api_files): linenum = linenum + 1 z3consts.write('}\n'); if VERBOSE: - print "Generated '%s'" % os.path.join(dotnet.src_dir, 'Enumerations.cs') + print("Generated '%s'" % os.path.join(dotnet.src_dir, 'Enumerations.cs')) # Extract enumeration types from z3_api.h, and add Java definitions @@ -2187,7 +2187,8 @@ def mk_z3consts_java(api_files): efile.write('public enum %s {\n' % name) efile.write first = True - for k, i in decls.iteritems(): + for k in decls: + i = decls[k] if first: first = False else: @@ -2218,7 +2219,7 @@ def mk_z3consts_java(api_files): idx = idx + 1 linenum = linenum + 1 if VERBOSE: - print "Generated '%s'" % ('%s' % gendir) + print("Generated '%s'" % ('%s' % gendir)) def mk_gui_str(id): return '4D2F40D8-E5F9-473B-B548-%012d' % id @@ -2305,7 +2306,7 @@ def mk_vs_proj(name, components): f.write(' \n') f.write('\n') if is_verbose(): - print "Generated '%s'" % proj_name + print("Generated '%s'" % proj_name) def mk_win_dist(build_path, dist_path): for c in get_components(): diff --git a/scripts/update_api.py b/scripts/update_api.py index a636a1a02..08dd012e3 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -84,6 +84,19 @@ def lib(): raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python") return _lib +def _to_ascii(s): + if isinstance(s, str): + return s.encode('ascii') + else: + return s + +if sys.version < '3': + def _to_pystr(s): + return s +else: + def _to_pystr(s): + return s.decode('utf-8') + def init(PATH): global _lib _lib = ctypes.CDLL(PATH) @@ -146,20 +159,22 @@ next_type_id = FIRST_OBJ_ID def def_Type(var, c_type, py_type): global next_type_id - exec ('%s = %s' % (var, next_type_id)) in globals() + exec('%s = %s' % (var, next_type_id), globals()) Type2Str[next_type_id] = c_type Type2PyStr[next_type_id] = py_type next_type_id = next_type_id + 1 def def_Types(): - pat1 = re.compile(" *def_Type.*") + import re + pat1 = re.compile(" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*") for api_file in API_FILES: api = open(api_file, 'r') for line in api: m = pat1.match(line) if m: - eval(line) - for k, v in Type2Str.iteritems(): + def_Type(m.group(1), m.group(2), m.group(3)) + for k in Type2Str: + v = Type2Str[k] if is_obj(k): Type2Dotnet[k] = v @@ -258,7 +273,7 @@ def param2java(p): elif param_type(p) == STRING: return "StringPtr" else: - print "ERROR: unreachable code" + print("ERROR: unreachable code") assert(False) exit(1) if k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: @@ -313,6 +328,17 @@ def display_args(num): core_py.write(", ") core_py.write("a%s" % i) +def display_args_to_z3(params): + i = 0 + for p in params: + if i > 0: + core_py.write(", ") + if param_type(p) == STRING: + core_py.write("_to_ascii(a%s)" % i) + else: + core_py.write("a%s" % i) + i = i + 1 + def mk_py_wrappers(): core_py.write("\n") for sig in _API2PY: @@ -327,13 +353,15 @@ def mk_py_wrappers(): core_py.write(" r = lib().%s(" % name) else: core_py.write(" lib().%s(" % name) - display_args(num) + display_args_to_z3(params) core_py.write(")\n") if len(params) > 0 and param_type(params[0]) == CONTEXT: core_py.write(" err = lib().Z3_get_error_code(a0)\n") core_py.write(" if err != Z3_OK:\n") core_py.write(" raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))\n") - if result != VOID: + if result == STRING: + core_py.write(" return _to_pystr(r)\n") + elif result != VOID: core_py.write(" return r\n") core_py.write("\n") @@ -356,7 +384,8 @@ def mk_dotnet(): dotnet.write('#pragma warning disable 1591\n\n'); dotnet.write('namespace Microsoft.Z3\n') dotnet.write('{\n') - for k, v in Type2Str.iteritems(): + for k in Type2Str: + v = Type2Str[k] if is_obj(k): dotnet.write(' using %s = System.IntPtr;\n' % v) dotnet.write('\n'); @@ -579,7 +608,7 @@ def mk_java(): java_wrapper.write(' } \n\n') java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n') java_wrapper.write(' delete [] NEW; \n\n') - java_wrapper.write('#define GETLONGAREGION(T,OLD,Z,SZ,NEW) \\\n') + java_wrapper.write('#define GETLONGAREGION(T,OLD,Z,SZ,NEW) \\\n') java_wrapper.write(' { \\\n') java_wrapper.write(' jlong * temp = new jlong[SZ]; \\\n') java_wrapper.write(' jenv->GetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)temp); \\\n') @@ -702,7 +731,7 @@ def mk_java(): java_wrapper.write('}\n') java_wrapper.write('#endif\n') if is_verbose(): - print "Generated '%s'" % java_nativef + print("Generated '%s'" % java_nativef) def mk_log_header(file, name, params): file.write("void log_%s(" % name) @@ -710,7 +739,7 @@ def mk_log_header(file, name, params): for p in params: if i > 0: file.write(", "); - file.write("%s a%s" % (param2str(p), i)) + file.write("%s a%s" % (param2str(p), i)) i = i + 1 file.write(")"); @@ -981,8 +1010,8 @@ exe_c.close() core_py.close() if is_verbose(): - print "Generated '%s'" % os.path.join(api_dir, 'api_log_macros.h') - print "Generated '%s'" % os.path.join(api_dir, 'api_log_macros.cpp') - print "Generated '%s'" % os.path.join(api_dir, 'api_commands.cpp') - print "Generated '%s'" % os.path.join(get_z3py_dir(), 'z3core.py') - print "Generated '%s'" % os.path.join(dotnet_dir, 'Native.cs') + print("Generated '%s'" % os.path.join(api_dir, 'api_log_macros.h')) + print("Generated '%s'" % os.path.join(api_dir, 'api_log_macros.cpp')) + print("Generated '%s'" % os.path.join(api_dir, 'api_commands.cpp')) + print("Generated '%s'" % os.path.join(get_z3py_dir(), 'z3core.py')) + print("Generated '%s'" % os.path.join(dotnet_dir, 'Native.cs')) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 8a13c7a99..169152ff4 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -37,15 +37,23 @@ Z3 exceptions: ... # the expression x + y is type incorrect ... n = x + y ... except Z3Exception as ex: -... print "failed:", ex +... print("failed: %s" % ex) failed: 'sort mismatch' """ from z3core import * from z3types import * from z3consts import * from z3printer import * +import sys import io +if sys.version < '3': + def _is_int(v): + return isinstance(v, int) or isinstance(v, long) +else: + def _is_int(v): + return isinstance(v, int) + def enable_trace(msg): Z3_enable_trace(msg) @@ -102,12 +110,12 @@ _error_handler_fptr = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint) # list of arguments. def _get_args(args): try: - if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)): - return args[0] - else: - return args + if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)): + return args[0] + else: + return args except: # len is not necessarily defined when args is not a sequence (use reflection?) - return args + return args def _Z3python_error_handler_core(c, e): # Do nothing error handler, just avoid exit(0) @@ -140,7 +148,8 @@ class Context: if __debug__: _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.") conf = Z3_mk_config() - for key, value in kws.iteritems(): + for key in kws: + value = kws[key] Z3_set_param_value(conf, str(key).upper(), _to_param_value(value)) prev = None for a in args: @@ -209,10 +218,12 @@ def set_param(*args, **kws): if __debug__: _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.") new_kws = {} - for k, v in kws.iteritems(): + for k in kws: + v = kws[k] if not set_pp_option(k, v): new_kws[k] = v - for key, value in new_kws.iteritems(): + for key in new_kws: + value = new_kws[key] Z3_global_param_set(str(key).upper(), _to_param_value(value)) prev = None for a in args: @@ -240,7 +251,7 @@ def get_param(name): """ ptr = (ctypes.c_char_p * 1)() if Z3_global_param_get(str(name), ptr): - r = str(ptr[0]) + r = z3core._to_pystr(ptr[0]) return r raise Z3Exception("failed to retrieve value for '%s'" % name) @@ -899,11 +910,22 @@ def _coerce_exprs(a, b, ctx=None): b = s.cast(b) return (a, b) +def _reduce(f, l, a): + r = a + for e in l: + r = f(r, e) + return r + def _coerce_expr_list(alist, ctx=None): - if filter(is_expr, alist) == []: - alist = map(lambda a: _py2expr(a, ctx), alist) - s = reduce(_coerce_expr_merge, alist, None) - return map(lambda a: s.cast(a), alist) + has_expr = False + for a in alist: + if is_expr(a): + has_expr = True + break + if not has_expr: + alist = [ _py2expr(a, ctx) for a in alist ] + s = _reduce(_coerce_expr_merge, alist, None) + return [ s.cast(a) for a in alist ] def is_expr(a): """Return `True` if `a` is a Z3 expression. @@ -1518,7 +1540,7 @@ def MultiPattern(*args): """ if __debug__: _z3_assert(len(args) > 0, "At least one argument expected") - _z3_assert(all(map(is_expr, args)), "Z3 expressions expected") + _z3_assert(all([ is_expr(a) for a in args ]), "Z3 expressions expected") ctx = args[0].ctx args, sz = _to_ast_array(args) return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx) @@ -1695,9 +1717,9 @@ def is_quantifier(a): def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): if __debug__: _z3_assert(is_bool(body), "Z3 expression expected") - _z3_assert(is_const(vs) or (len(vs) > 0 and all(map(is_const, vs))), "Invalid bounded variable(s)") - _z3_assert(all(map(lambda a: is_pattern(a) or is_expr(a), patterns)), "Z3 patterns expected") - _z3_assert(all(map(is_expr, no_patterns)), "no patterns are Z3 expressions") + _z3_assert(is_const(vs) or (len(vs) > 0 and all([ is_const(v) for v in vs])), "Invalid bounded variable(s)") + _z3_assert(all([is_pattern(a) or is_expr(a) for a in patterns]), "Z3 patterns expected") + _z3_assert(all([is_expr(p) for p in no_patterns]), "no patterns are Z3 expressions") ctx = body.ctx if is_app(vs): vs = [vs] @@ -1706,7 +1728,7 @@ def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], for i in range(num_vars): ## TODO: Check if is constant _vs[i] = vs[i].as_ast() - patterns = map(_to_pattern, patterns) + patterns = [ _to_pattern(p) for p in patterns ] num_pats = len(patterns) _pats = (Pattern * num_pats)() for i in range(num_pats): @@ -2008,7 +2030,7 @@ class ArithRef(ExprRef): def __truediv__(self, other): """Create the Z3 expression `other/self`.""" - self.__div__(other) + return self.__div__(other) def __rdiv__(self, other): """Create the Z3 expression `other/self`. @@ -2029,7 +2051,7 @@ class ArithRef(ExprRef): def __rtruediv__(self, other): """Create the Z3 expression `other/self`.""" - self.__rdiv__(other) + return self.__rdiv__(other) def __mod__(self, other): """Create the Z3 expression `other%self`. @@ -2413,11 +2435,11 @@ class IntNumRef(ArithRef): >>> v + 1 1 + 1 >>> v.as_long() + 1 - 2L + 2 """ if __debug__: _z3_assert(self.is_int(), "Integer value expected") - return long(self.as_string()) + return int(self.as_string()) def as_string(self): """Return a Z3 integer numeral as a Python string. @@ -2465,7 +2487,7 @@ class RatNumRef(ArithRef): >>> v + 1 10000000000 + 1 >>> v.numerator_as_long() + 1 - 10000000001L + 10000000001 """ return self.numerator().as_long() @@ -2476,7 +2498,7 @@ class RatNumRef(ArithRef): >>> v 1/3 >>> v.denominator_as_long() - 3L + 3 """ return self.denominator().as_long() @@ -2529,7 +2551,7 @@ class AlgebraicNumRef(ArithRef): def _py2expr(a, ctx=None): if isinstance(a, bool): return BoolVal(a, ctx) - if isinstance(a, int) or isinstance(a, long): + if _is_int(a): return IntVal(a, ctx) if isinstance(a, float): return RealVal(a, ctx) @@ -2576,9 +2598,7 @@ def _to_int_str(val): return "1" else: return "0" - elif isinstance(val, int): - return str(val) - elif isinstance(val, long): + elif _is_int(val): return str(val) elif isinstance(val, str): return val @@ -2625,8 +2645,8 @@ def RatVal(a, b, ctx=None): Real """ if __debug__: - _z3_assert(isinstance(a, int) or isinstance(a, str) or isinstance(a, long), "First argument cannot be converted into an integer") - _z3_assert(isinstance(b, int) or isinstance(b, str) or isinstance(a, long), "Second argument cannot be converted into an integer") + _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer") + _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer") return simplify(RealVal(a, ctx)/RealVal(b, ctx)) def Q(a, b, ctx=None): @@ -3078,7 +3098,7 @@ class BitVecRef(ExprRef): def __truediv__(self, other): """Create the Z3 expression (signed) division `self / other`.""" - self.__div__(other) + return self.__div__(other) def __rdiv__(self, other): """Create the Z3 expression (signed) division `other / self`. @@ -3098,7 +3118,7 @@ class BitVecRef(ExprRef): def __rtruediv__(self, other): """Create the Z3 expression (signed) division `other / self`.""" - self.__rdiv__(other) + return self.__rdiv__(other) def __mod__(self, other): """Create the Z3 expression (signed) mod `self % other`. @@ -3218,9 +3238,9 @@ class BitVecRef(ExprRef): >>> BitVecVal(4, 3) 4 >>> BitVecVal(4, 3).as_signed_long() - -4L + -4 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long() - -2L + -2 >>> simplify(BitVecVal(4, 3) >> 1) 6 >>> simplify(LShR(BitVecVal(4, 3), 1)) @@ -3284,32 +3304,32 @@ class BitVecNumRef(BitVecRef): >>> v = BitVecVal(0xbadc0de, 32) >>> v 195936478 - >>> print "0x%.8x" % v.as_long() + >>> print("0x%.8x" % v.as_long()) 0x0badc0de """ - return long(self.as_string()) + return int(self.as_string()) def as_signed_long(self): """Return a Z3 bit-vector numeral as a Python long (bignum) numeral. The most significant bit is assumed to be the sign. >>> BitVecVal(4, 3).as_signed_long() - -4L + -4 >>> BitVecVal(7, 3).as_signed_long() - -1L + -1 >>> BitVecVal(3, 3).as_signed_long() - 3L - >>> BitVecVal(2L**32 - 1, 32).as_signed_long() - -1L - >>> BitVecVal(2L**64 - 1, 64).as_signed_long() - -1L + 3 + >>> BitVecVal(2**32 - 1, 32).as_signed_long() + -1 + >>> BitVecVal(2**64 - 1, 64).as_signed_long() + -1 """ - sz = long(self.size()) + sz = self.size() val = self.as_long() - if val >= 2L**(sz - 1): - val = val - 2L**sz - if val < -2L**(sz - 1): - val = val + 2L**sz - return val + if val >= 2**(sz - 1): + val = val - 2**sz + if val < -2**(sz - 1): + val = val + 2**sz + return int(val) def as_string(self): return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) @@ -3379,7 +3399,7 @@ def BitVecVal(val, bv, ctx=None): >>> v = BitVecVal(10, 32) >>> v 10 - >>> print "0x%.8x" % v.as_long() + >>> print("0x%.8x" % v.as_long()) 0x0000000a """ if is_bv_sort(bv): @@ -3440,12 +3460,12 @@ def Concat(*args): Concat(Concat(1, 1 + 1), 1) >>> simplify(Concat(v, v+1, v)) 289 - >>> print "%.3x" % simplify(Concat(v, v+1, v)).as_long() + >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long()) 121 """ args = _get_args(args) if __debug__: - _z3_assert(all(map(is_bv, args)), "All arguments must be Z3 bit-vector expressions.") + _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.") _z3_assert(len(args) >= 2, "At least two arguments expected.") ctx = args[0].ctx r = args[0] @@ -3615,9 +3635,9 @@ def LShR(a, b): >>> BitVecVal(4, 3) 4 >>> BitVecVal(4, 3).as_signed_long() - -4L + -4 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long() - -2L + -2 >>> simplify(BitVecVal(4, 3) >> 1) 6 >>> simplify(LShR(BitVecVal(4, 3), 1)) @@ -3682,7 +3702,7 @@ def SignExt(n, a): 254 >>> v.size() 8 - >>> print "%.x" % v.as_long() + >>> print("%.x" % v.as_long()) fe """ if __debug__: @@ -3727,12 +3747,12 @@ def RepeatBitVec(n, a): >>> n.size() 32 >>> v0 = BitVecVal(10, 4) - >>> print "%.x" % v0.as_long() + >>> print("%.x" % v0.as_long()) a >>> v = simplify(RepeatBitVec(4, v0)) >>> v.size() 16 - >>> print "%.x" % v.as_long() + >>> print("%.x" % v.as_long()) aaaa """ if __debug__: @@ -4006,7 +4026,7 @@ def Map(f, *args): if __debug__: _z3_assert(len(args) > 0, "At least one Z3 array expression expected") _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration") - _z3_assert(all(map(is_array, args)), "Z3 array expected expected") + _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected") _z3_assert(len(args) == f.arity(), "Number of arguments mismatch") _args, sz = _to_ast_array(args) ctx = f.ctx @@ -4100,7 +4120,7 @@ class Datatype: if __debug__: _z3_assert(isinstance(name, str), "String expected") _z3_assert(isinstance(rec_name, str), "String expected") - _z3_assert(all(map(_valid_accessor, args)), "Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)") + _z3_assert(all([_valid_accessor(a) for a in args]), "Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)") self.constructors.append((name, rec_name, args)) def declare(self, name, *args): @@ -4187,9 +4207,9 @@ def CreateDatatypes(*ds): ds = _get_args(ds) if __debug__: _z3_assert(len(ds) > 0, "At least one Datatype must be specified") - _z3_assert(all(map(lambda d: isinstance(d, Datatype), ds)), "Arguments must be Datatypes") - _z3_assert(all(map(lambda d: d.ctx == ds[0].ctx, ds)), "Context mismatch") - _z3_assert(all(map(lambda d: d.constructors != [], ds)), "Non-empty Datatypes expected") + _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes") + _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch") + _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected") ctx = ds[0].ctx num = len(ds) names = (Symbol * num)() @@ -4355,7 +4375,7 @@ def EnumSort(name, values, ctx=None): """ if __debug__: _z3_assert(isinstance(name, str), "Name must be a string") - _z3_assert(all(map(lambda v: isinstance(v, str), values)), "Eumeration sort values must be strings") + _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings") _z3_assert(len(values) > 0, "At least one value expected") ctx = _get_ctx(ctx) num = len(values) @@ -4369,7 +4389,7 @@ def EnumSort(name, values, ctx=None): V = [] for i in range(num): V.append(FuncDeclRef(_values[i], ctx)) - V = map(lambda a: a(), V) + V = [a() for a in V] return S, V ######################################### @@ -4432,7 +4452,8 @@ def args2params(arguments, keywords, ctx=None): else: r.set(prev, a) prev = None - for k, v in keywords.iteritems(): + for k in keywords: + v = keywords[k] r.set(k, v) return r @@ -4469,7 +4490,7 @@ class ParamDescrsRef: return Z3_param_descrs_get_kind(self.ctx.ref(), self.descr, to_symbol(n, self.ctx)) def __getitem__(self, arg): - if isinstance(arg, int) or isinstance(arg, long): + if _is_int(arg): return self.get_name(arg) else: return self.get_kind(arg) @@ -5057,7 +5078,7 @@ class FuncEntry: >>> try: ... e.arg_value(2) ... except IndexError: - ... print "index error" + ... print("index error") index error """ if idx >= self.num_args(): @@ -5435,7 +5456,7 @@ class ModelRef(Z3PPObject): 1 >>> m[f] [1 -> 0, else -> 0] - >>> for d in m: print "%s -> %s" % (d, m[d]) + >>> for d in m: print("%s -> %s" % (d, m[d])) x -> 1 f -> [1 -> 0, else -> 0] """ @@ -5506,16 +5527,16 @@ class Statistics: if in_html_mode(): out = io.StringIO() even = True - out.write(u'') + out.write(u('
')) for k, v in self: if even: - out.write(u'') + out.write(u('')) even = False else: - out.write(u'') + out.write(u('')) even = True - out.write(u'' % (k, v)) - out.write(u'
%s%s
') + out.write(u('%s%s' % (k, v))) + out.write(u('')) return out.getvalue() else: return Z3_stats_to_string(self.ctx.ref(), self.stats) @@ -5813,7 +5834,7 @@ class Solver(Z3PPObject): >>> s.assert_and_track(x > 0, 'p1') >>> s.assert_and_track(x != 1, 'p2') >>> s.assert_and_track(x < 0, p3) - >>> print s.check() + >>> print(s.check()) unsat >>> c = s.unsat_core() >>> len(c) @@ -5961,7 +5982,7 @@ class Solver(Z3PPObject): def help(self): """Display a string describing all available options.""" - print Z3_solver_get_help(self.ctx.ref(), self.solver) + print(Z3_solver_get_help(self.ctx.ref(), self.solver)) def param_descrs(self): """Return the parameter description set.""" @@ -6032,7 +6053,7 @@ class Fixedpoint(Z3PPObject): else: self.fixedpoint = fixedpoint Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint) - self.vars = [] + self.vars = [] def __del__(self): if self.fixedpoint != None: @@ -6046,8 +6067,8 @@ class Fixedpoint(Z3PPObject): def help(self): """Display a string describing all available options.""" - print Z3_fixedpoint_get_help(self.ctx.ref(), self.fixedpoint) - + print(Z3_fixedpoint_get_help(self.ctx.ref(), self.fixedpoint)) + def param_descrs(self): """Return the parameter description set.""" return ParamDescrsRef(Z3_fixedpoint_get_param_descrs(self.ctx.ref(), self.fixedpoint), self.ctx) @@ -6059,11 +6080,11 @@ class Fixedpoint(Z3PPObject): for arg in args: if isinstance(arg, Goal) or isinstance(arg, AstVector): for f in arg: - f = self.abstract(f) + f = self.abstract(f) Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, f.as_ast()) else: arg = s.cast(arg) - arg = self.abstract(arg) + arg = self.abstract(arg) Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, arg.as_ast()) def add(self, *args): @@ -6079,38 +6100,38 @@ class Fixedpoint(Z3PPObject): self.assert_exprs(*args) def add_rule(self, head, body = None, name = None): - """Assert rules defining recursive predicates to the fixedpoint solver. + """Assert rules defining recursive predicates to the fixedpoint solver. >>> a = Bool('a') - >>> b = Bool('b') + >>> b = Bool('b') >>> s = Fixedpoint() - >>> s.register_relation(a.decl()) - >>> s.register_relation(b.decl()) - >>> s.fact(a) + >>> s.register_relation(a.decl()) + >>> s.register_relation(b.decl()) + >>> s.fact(a) >>> s.rule(b, a) - >>> s.query(b) - sat - """ - if name == None: - name = "" + >>> s.query(b) + sat + """ + if name == None: + name = "" name = to_symbol(name, self.ctx) - if body == None: - head = self.abstract(head) - Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name) - else: - body = _get_args(body) - f = self.abstract(Implies(And(body),head)) - Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name) - + if body == None: + head = self.abstract(head) + Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name) + else: + body = _get_args(body) + f = self.abstract(Implies(And(body),head)) + Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name) + def rule(self, head, body = None, name = None): - """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" - self.add_rule(head, body, name) - + """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" + self.add_rule(head, body, name) + def fact(self, head, name = None): - """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" - self.add_rule(head, None, name) + """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" + self.add_rule(head, None, name) def query(self, *query): - """Query the fixedpoint engine whether formula is derivable. + """Query the fixedpoint engine whether formula is derivable. You can also pass an tuple or list of recursive predicates. """ query = _get_args(query) @@ -6141,17 +6162,17 @@ class Fixedpoint(Z3PPObject): def update_rule(self, head, body, name): """update rule""" - if name == None: - name = "" + if name == None: + name = "" name = to_symbol(name, self.ctx) body = _get_args(body) f = self.abstract(Implies(And(body),head)) - Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name) + Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name) - def get_answer(self): - """Retrieve answer from last query call.""" - r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint) - return _to_expr_ref(r, self.ctx) + def get_answer(self): + """Retrieve answer from last query call.""" + r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint) + return _to_expr_ref(r, self.ctx) def get_num_levels(self, predicate): """Retrieve number of levels used for predicate in PDR engine""" @@ -6167,40 +6188,40 @@ class Fixedpoint(Z3PPObject): Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast) def register_relation(self, *relations): - """Register relation as recursive""" - relations = _get_args(relations) - for f in relations: - Z3_fixedpoint_register_relation(self.ctx.ref(), self.fixedpoint, f.ast) + """Register relation as recursive""" + relations = _get_args(relations) + for f in relations: + Z3_fixedpoint_register_relation(self.ctx.ref(), self.fixedpoint, f.ast) def set_predicate_representation(self, f, *representations): - """Control how relation is represented""" - representations = _get_args(representations) - representations = map(to_symbol, representations) - sz = len(representations) - args = (Symbol * sz)() - for i in range(sz): - args[i] = representations[i] - Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args) + """Control how relation is represented""" + representations = _get_args(representations) + representations = [to_symbol(s) for s in representations] + sz = len(representations) + args = (Symbol * sz)() + for i in range(sz): + args[i] = representations[i] + Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args) def parse_string(self, s): - """Parse rules and queries from a string""" - return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx) - + """Parse rules and queries from a string""" + return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx) + def parse_file(self, f): - """Parse rules and queries from a file""" - return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx) + """Parse rules and queries from a file""" + return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx) def get_rules(self): - """retrieve rules that have been added to fixedpoint context""" - return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx) + """retrieve rules that have been added to fixedpoint context""" + return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx) def get_assertions(self): - """retrieve assertions that have been added to fixedpoint context""" - return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx) + """retrieve assertions that have been added to fixedpoint context""" + return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx) def __repr__(self): """Return a formatted string with all added rules and constraints.""" - return self.sexpr() + return self.sexpr() def sexpr(self): """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format. @@ -6208,16 +6229,16 @@ class Fixedpoint(Z3PPObject): return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)()) def to_string(self, queries): - """Return a formatted string (in Lisp-like format) with all added constraints. + """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format. - Include also queries. + Include also queries. """ - args, len = _to_ast_array(queries) + args, len = _to_ast_array(queries) return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args) def statistics(self): """Return statistics for the last `query()`. - """ + """ return Statistics(Z3_fixedpoint_get_statistics(self.ctx.ref(), self.fixedpoint), self.ctx) def reason_unknown(self): @@ -6226,21 +6247,21 @@ class Fixedpoint(Z3PPObject): return Z3_fixedpoint_get_reason_unknown(self.ctx.ref(), self.fixedpoint) def declare_var(self, *vars): - """Add variable or several variables. - The added variable or variables will be bound in the rules - and queries - """ - vars = _get_args(vars) - for v in vars: - self.vars += [v] - + """Add variable or several variables. + The added variable or variables will be bound in the rules + and queries + """ + vars = _get_args(vars) + for v in vars: + self.vars += [v] + def abstract(self, fml, is_forall=True): - if self.vars == []: - return fml - if is_forall: - return ForAll(self.vars, fml) - else: - return Exists(self.vars, fml) + if self.vars == []: + return fml + if is_forall: + return ForAll(self.vars, fml) + else: + return Exists(self.vars, fml) ######################################### # @@ -6432,7 +6453,7 @@ class Tactic: def help(self): """Display a string containing a description of the available options for the `self` tactic.""" - print Z3_tactic_get_help(self.ctx.ref(), self.tactic) + print(Z3_tactic_get_help(self.ctx.ref(), self.tactic)) def param_descrs(self): """Return the parameter description set.""" @@ -6528,7 +6549,7 @@ def ParOr(*ts, **ks): if __debug__: _z3_assert(len(ts) >= 2, "At least two arguments expected") ctx = _get_ctx(ks.get('ctx', None)) - ts = map(lambda t: _to_tactic(t, ctx), ts) + ts = [ _to_tactic(t, ctx) for t in ts ] sz = len(ts) _args = (TacticObj * sz)() for i in range(sz): @@ -6573,7 +6594,7 @@ def Repeat(t, max=4294967295, ctx=None): >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y) >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip'))) >>> r = t(c) - >>> for subgoal in r: print subgoal + >>> for subgoal in r: print(subgoal) [x == 0, y == 0, x > y] [x == 0, y == 1, x > y] [x == 1, y == 0, x > y] @@ -6615,19 +6636,19 @@ def describe_tactics(): """Display a (tabular) description of all available tactics in Z3.""" if in_html_mode(): even = True - print '' + print('
') for t in tactics(): if even: - print '' + print('') even = False else: - print '' + print('') even = True - print '' % (t, insert_line_breaks(tactic_description(t), 40)) - print '
%s%s
' + print('%s%s' % (t, insert_line_breaks(tactic_description(t), 40))) + print('') else: for t in tactics(): - print '%s : %s' % (t, tactic_description(t)) + print('%s : %s' % (t, tactic_description(t))) class Probe: """Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used.""" @@ -6638,7 +6659,7 @@ class Probe: self.probe = probe elif isinstance(probe, float): self.probe = Z3_probe_const(self.ctx.ref(), probe) - elif isinstance(probe, int) or isinstance(probe, long): + elif _is_int(probe): self.probe = Z3_probe_const(self.ctx.ref(), float(probe)) elif isinstance(probe, bool): if probe: @@ -6803,19 +6824,19 @@ def describe_probes(): """Display a (tabular) description of all available probes in Z3.""" if in_html_mode(): even = True - print '' + print('
') for p in probes(): if even: - print '' + print('') even = False else: - print '' + print('') even = True - print '' % (p, insert_line_breaks(probe_description(p), 40)) - print '
%s%s
' + print('%s%s' % (p, insert_line_breaks(probe_description(p), 40))) + print('') else: for p in probes(): - print '%s : %s' % (p, probe_description(p)) + print('%s : %s' % (p, probe_description(p))) def _probe_nary(f, args, ctx): if __debug__: @@ -6911,7 +6932,7 @@ def simplify(a, *arguments, **keywords): def help_simplify(): """Return a string describing all options available for Z3 `simplify` procedure.""" - print Z3_simplify_get_help(main_ctx().ref()) + print(Z3_simplify_get_help(main_ctx().ref())) def simplify_param_descrs(): """Return the set of parameter descriptions for Z3 `simplify` procedure.""" @@ -6934,7 +6955,7 @@ def substitute(t, *m): m = _get_args(m1) if __debug__: _z3_assert(is_expr(t), "Z3 expression expected") - _z3_assert(all(map(lambda p: isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()), m)), "Z3 invalid substitution, expression pairs expected.") + _z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.") num = len(m) _from = (Ast * num)() _to = (Ast * num)() @@ -6956,7 +6977,7 @@ def substitute_vars(t, *m): """ if __debug__: _z3_assert(is_expr(t), "Z3 expression expected") - _z3_assert(all(map(is_expr, m)), "Z3 invalid substitution, list of expressions expected.") + _z3_assert(all([is_expr(n) for n in m]), "Z3 invalid substitution, list of expressions expected.") num = len(m) _to = (Ast * num)() for i in range(num): @@ -6983,7 +7004,7 @@ def Sum(*args): _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression") args = _coerce_expr_list(args, ctx) if is_bv(args[0]): - return reduce(lambda a, b: a + b, args, 0) + return _reduce(lambda a, b: a + b, args, 0) else: _args, sz = _to_ast_array(args) return ArithRef(Z3_mk_add(ctx.ref(), sz, _args), ctx) @@ -7008,7 +7029,7 @@ def Product(*args): _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression") args = _coerce_expr_list(args, ctx) if is_bv(args[0]): - return reduce(lambda a, b: a * b, args, 1) + return _reduce(lambda a, b: a * b, args, 1) else: _args, sz = _to_ast_array(args) return ArithRef(Z3_mk_mul(ctx.ref(), sz, _args), ctx) @@ -7028,18 +7049,18 @@ def solve(*args, **keywords): s.set(**keywords) s.add(*args) if keywords.get('show', False): - print s + print(s) r = s.check() if r == unsat: - print "no solution" + print("no solution") elif r == unknown: - print "failed to solve" + print("failed to solve") try: - print s.model() + print(s.model()) except Z3Exception: return else: - print s.model() + print(s.model()) def solve_using(s, *args, **keywords): """Solve the constraints `*args` using solver `s`. @@ -7054,21 +7075,21 @@ def solve_using(s, *args, **keywords): s.set(**keywords) s.add(*args) if keywords.get('show', False): - print "Problem:" - print s + print("Problem:") + print(s) r = s.check() if r == unsat: - print "no solution" + print("no solution") elif r == unknown: - print "failed to solve" + print("failed to solve") try: - print s.model() + print(s.model()) except Z3Exception: return else: if keywords.get('show', False): - print "Solution:" - print s.model() + print("Solution:") + print(s.model()) def prove(claim, **keywords): """Try to prove the given claim. @@ -7086,16 +7107,16 @@ def prove(claim, **keywords): s.set(**keywords) s.add(Not(claim)) if keywords.get('show', False): - print s + print(s) r = s.check() if r == unsat: - print "proved" + print("proved") elif r == unknown: - print "failed to prove" - print s.model() + print("failed to prove") + print(s.model()) else: - print "counterexample" - print s.model() + print("counterexample") + print(s.model()) def _solve_html(*args, **keywords): """Version of funcion `solve` used in RiSE4Fun.""" @@ -7103,21 +7124,21 @@ def _solve_html(*args, **keywords): s.set(**keywords) s.add(*args) if keywords.get('show', False): - print "Problem:" - print s + print("Problem:") + print(s) r = s.check() if r == unsat: - print "no solution" + print("no solution") elif r == unknown: - print "failed to solve" + print("failed to solve") try: - print s.model() + print(s.model()) except Z3Exception: return else: if keywords.get('show', False): - print "Solution:" - print s.model() + print("Solution:") + print(s.model()) def _solve_using_html(s, *args, **keywords): """Version of funcion `solve_using` used in RiSE4Fun.""" @@ -7126,21 +7147,21 @@ def _solve_using_html(s, *args, **keywords): s.set(**keywords) s.add(*args) if keywords.get('show', False): - print "Problem:" - print s + print("Problem:") + print(s) r = s.check() if r == unsat: - print "no solution" + print("no solution") elif r == unknown: - print "failed to solve" + print("failed to solve") try: - print s.model() + print(s.model()) except Z3Exception: return else: if keywords.get('show', False): - print "Solution:" - print s.model() + print("Solution:") + print(s.model()) def _prove_html(claim, **keywords): """Version of funcion `prove` used in RiSE4Fun.""" @@ -7150,23 +7171,24 @@ def _prove_html(claim, **keywords): s.set(**keywords) s.add(Not(claim)) if keywords.get('show', False): - print s + print(s) r = s.check() if r == unsat: - print "proved" + print("proved") elif r == unknown: - print "failed to prove" - print s.model() + print("failed to prove") + print(s.model()) else: - print "counterexample" - print s.model() + print("counterexample") + print(s.model()) def _dict2sarray(sorts, ctx): sz = len(sorts) _names = (Symbol * sz)() _sorts = (Sort * sz) () i = 0 - for k, v in sorts.iteritems(): + for k in sorts: + v = sorts[k] if __debug__: _z3_assert(isinstance(k, str), "String expected") _z3_assert(is_sort(v), "Z3 sort expected") @@ -7180,7 +7202,8 @@ def _dict2darray(decls, ctx): _names = (Symbol * sz)() _decls = (FuncDecl * sz) () i = 0 - for k, v in decls.iteritems(): + for k in decls: + v = decls[k] if __debug__: _z3_assert(isinstance(k, str), "String expected") _z3_assert(is_func_decl(v) or is_const(v), "Z3 declaration or constant expected") diff --git a/src/api/python/z3printer.py b/src/api/python/z3printer.py index 3ad8f21b9..d3dc43d3e 100644 --- a/src/api/python/z3printer.py +++ b/src/api/python/z3printer.py @@ -74,6 +74,15 @@ def _is_add(k): def _is_sub(k): return k == Z3_OP_SUB or k == Z3_OP_BSUB +import sys +if sys.version < '3': + import codecs + def u(x): + return codecs.unicode_escape_decode(x)[0] +else: + def u(x): + return x + _z3_infix_compact = [ Z3_OP_MUL, Z3_OP_BMUL, Z3_OP_POWER, Z3_OP_DIV, Z3_OP_IDIV, Z3_OP_MOD, Z3_OP_BSDIV, Z3_OP_BSMOD ] _ellipses = '...' @@ -161,15 +170,19 @@ def _get_precedence(k): return _z3_precedence.get(k, 100000) _z3_html_op_to_str = {} -for _k, _v in _z3_op_to_str.iteritems(): +for _k in _z3_op_to_str: + _v = _z3_op_to_str[_k] _z3_html_op_to_str[_k] = _v -for _k, _v in _z3_pre_html_op_to_str.iteritems(): +for _k in _z3_pre_html_op_to_str: + _v = _z3_pre_html_op_to_str[_k] _z3_html_op_to_str[_k] = _v _z3_html_precedence = {} -for _k, _v in _z3_precedence.iteritems(): +for _k in _z3_precedence: + _v = _z3_precedence[_k] _z3_html_precedence[_k] = _v -for _k, _v in _z3_pre_html_precedence.iteritems(): +for _k in _z3_pre_html_precedence: + _v = _z3_pre_html_precedence[_k] _z3_html_precedence[_k] = _v _html_infix_map = {} @@ -237,7 +250,7 @@ class FormatObject: class NAryFormatObject(FormatObject): def __init__(self, fs): - assert all(map(lambda a: isinstance(a, FormatObject), fs)) + assert all([isinstance(a, FormatObject) for a in fs]) self.children = fs def children(self): return self.children @@ -246,7 +259,7 @@ class ComposeFormatObject(NAryFormatObject): def is_compose(sef): return True def as_tuple(self): - return ('compose', map(lambda a: a.as_tuple(), self.children)) + return ('compose', [ a.as_tuple() for a in self.children ]) def space_upto_nl(self): r = 0 for child in self.children: @@ -256,13 +269,13 @@ class ComposeFormatObject(NAryFormatObject): return (r, True) return (r, False) def flat(self): - return compose(map(lambda a: a.flat(), self.children)) + return compose([a.flat() for a in self.children ]) class ChoiceFormatObject(NAryFormatObject): def is_choice(sef): return True def as_tuple(self): - return ('choice', map(lambda a: a.as_tuple(), self.children)) + return ('choice', [ a.as_tuple() for a in self.children ]) def space_upto_nl(self): return self.children[0].space_upto_nl() def flat(self): @@ -388,11 +401,11 @@ class PP: if not self.bounded or self.pos <= self.max_width: sz = _len(f) if self.bounded and self.pos + sz > self.max_width: - self.out.write(_ellipses) + self.out.write(u(_ellipses)) else: self.pos = self.pos + sz self.ribbon_pos = self.ribbon_pos + sz - self.out.write(unicode(f.string)) + self.out.write(u(f.string)) def pp_compose(self, f, indent): for c in f.children: @@ -410,11 +423,11 @@ class PP: self.ribbon_pos = 0 self.line = self.line + 1 if self.line < self.max_lines: - self.out.write(unicode('\n')) + self.out.write(u('\n')) for i in range(indent): - self.out.write(unicode(' ')) + self.out.write(u(' ')) else: - self.out.write(unicode('\n...')) + self.out.write(u('\n...')) raise StopPPException() def pp(self, f, indent): @@ -957,23 +970,23 @@ def in_html_mode(): def pp(a): if _support_pp(a): - print obj_to_string(a) + print(obj_to_string(a)) else: - print a + print(a) def print_matrix(m): z3._z3_assert(isinstance(m, list) or isinstance(m, tuple), "matrix expected") if not in_html_mode(): - print obj_to_string(m) + print(obj_to_string(m)) else: - print '' + print('
') for r in m: z3._z3_assert(isinstance(r, list) or isinstance(r, tuple), "matrix expected") - print '' + print('') for c in r: - print '' % c - print '' - print '
%s
' + print('%s' % c) + print('') + print('') def insert_line_breaks(s, width): """Break s in lines of size width (approx)""" @@ -984,9 +997,9 @@ def insert_line_breaks(s, width): w = 0 for i in range(sz): if w > width and s[i] == ' ': - new_str.write(u'
') + new_str.write(u('
')) w = 0 else: - new_str.write(unicode(s[i])) + new_str.write(u(s[i])) w = w + 1 return new_str.getvalue()