mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

Add Python 3.x support

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-20 17:47:38 -08:00
parent 7d97f407c2
commit 6602803850
6 changed files with 426 additions and 358 deletions
Download patch file Download diff file Expand all files Collapse all files

2
RELEASE_NOTES
View file

@ -9,6 +9,8 @@ Version 4.3.2
- Added support for FreeBSD. Z3 can be compiled on FreeBSD using g++. - 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. - 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. Thanks to Julien Henry for reporting this problem.

4
examples/python/example.py
View file

@ -4,5 +4,5 @@ x = Real('x')
y = Real('y') y = Real('y')
s = Solver() s = Solver()
s.add(x + y > 5, x > 1, y > 1) s.add(x + y > 5, x > 1, y > 1)
print s.check() print(s.check())
print s.model() print(s.model())

209
scripts/mk_util.py
View file

@ -7,11 +7,6 @@
# Author: Leonardo de Moura (leonardo) # Author: Leonardo de Moura (leonardo)
############################################ ############################################
import sys import sys
if sys.version >= "3":
print "ERROR: python 2.x required."
exit(1)
import os import os
import glob import glob
import re import re
@ -134,8 +129,7 @@ def exec_cmd(cmd):
first = True first = True
for e in cmd: for e in cmd:
if first: if first:
# Allow spaces in the executable name first = False
first = False
new_cmd.append(e) new_cmd.append(e)
else: else:
if e != "": if e != "":
@ -166,7 +160,7 @@ def exec_compiler_cmd(cmd):
def test_cxx_compiler(cc): def test_cxx_compiler(cc):
if is_verbose(): if is_verbose():
print "Testing %s..." % cc print("Testing %s..." % cc)
t = TempFile('tst.cpp') t = TempFile('tst.cpp')
t.add('#include<iostream>\nint main() { return 0; }\n') t.add('#include<iostream>\nint main() { return 0; }\n')
t.commit() t.commit()
@ -174,7 +168,7 @@ def test_cxx_compiler(cc):
def test_c_compiler(cc): def test_c_compiler(cc):
if is_verbose(): if is_verbose():
print "Testing %s..." % cc print("Testing %s..." % cc)
t = TempFile('tst.c') t = TempFile('tst.c')
t.add('#include<stdio.h>\nint main() { return 0; }\n') t.add('#include<stdio.h>\nint main() { return 0; }\n')
t.commit() t.commit()
@ -182,7 +176,7 @@ def test_c_compiler(cc):
def test_gmp(cc): def test_gmp(cc):
if is_verbose(): if is_verbose():
print "Testing GMP..." print("Testing GMP...")
t = TempFile('tstgmp.cpp') t = TempFile('tstgmp.cpp')
t.add('#include<gmp.h>\nint main() { mpz_t t; mpz_init(t); mpz_clear(t); return 0; }\n') t.add('#include<gmp.h>\nint main() { mpz_t t; mpz_init(t); mpz_clear(t); return 0; }\n')
t.commit() t.commit()
@ -190,7 +184,7 @@ def test_gmp(cc):
def test_openmp(cc): def test_openmp(cc):
if is_verbose(): if is_verbose():
print "Testing OpenMP..." print("Testing OpenMP...")
t = TempFile('tstomp.cpp') t = TempFile('tstomp.cpp')
t.add('#include<omp.h>\nint main() { return omp_in_parallel() ? 1 : 0; }\n') t.add('#include<omp.h>\nint main() { return omp_in_parallel() ? 1 : 0; }\n')
t.commit() 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.add('public class Hello { public static void main(String[] args) { System.out.println("Hello, World"); }}\n')
t.commit() t.commit()
if is_verbose(): if is_verbose():
print "Testing %s..." % JAVAC print("Testing %s..." % JAVAC)
r = exec_cmd([JAVAC, 'Hello.java']) r = exec_cmd([JAVAC, 'Hello.java'])
if r != 0: if r != 0:
raise MKException('Failed testing Java compiler. Set environment variable JAVAC with the path to the Java compiler') raise MKException('Failed testing Java compiler. Set environment variable JAVAC with the path to the Java compiler')
if is_verbose(): if is_verbose():
print "Testing %s..." % JAVA print("Testing %s..." % JAVA)
r = exec_cmd([JAVA, 'Hello']) r = exec_cmd([JAVA, 'Hello'])
rmf('Hello.class') rmf('Hello.class')
if r != 0: if r != 0:
@ -224,11 +218,11 @@ def find_java_home():
global JAVA_HOME global JAVA_HOME
if JAVA_HOME != None: if JAVA_HOME != None:
if is_verbose(): if is_verbose():
print "Checking jni.h..." print("Checking jni.h...")
if os.path.exists(os.path.join(JAVA_HOME, 'include', 'jni.h')): if os.path.exists(os.path.join(JAVA_HOME, 'include', 'jni.h')):
return return
if is_verbose(): if is_verbose():
print "Finding JAVA_HOME..." print("Finding JAVA_HOME...")
t = TempFile('output') t = TempFile('output')
null = open(os.devnull, 'wb') null = open(os.devnull, 'wb')
try: try:
@ -242,17 +236,17 @@ def find_java_home():
m = open_pat.match(line) m = open_pat.match(line)
if m: if m:
# Remove last 3 directives from m.group(1) # Remove last 3 directives from m.group(1)
print m.group(1) print(m.group(1))
tmp = m.group(1).split(os.sep) tmp = m.group(1).split(os.sep)
path = string.join(tmp[:len(tmp) - 3], os.sep) path = string.join(tmp[:len(tmp) - 3], os.sep)
if is_verbose(): if is_verbose():
print "Checking jni.h..." print("Checking jni.h...")
jni_dir = find_jni_h(path) jni_dir = find_jni_h(path)
if not jni_dir: 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')) 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] JAVA_HOME = os.path.split(jni_dir)[0]
if is_verbose(): if is_verbose():
print 'JAVA_HOME=%s' % JAVA_HOME print('JAVA_HOME=%s' % JAVA_HOME)
return return
raise MKException('Failed to find JAVA_HOME') raise MKException('Failed to find JAVA_HOME')
@ -261,7 +255,7 @@ def is64():
def check_ar(): def check_ar():
if is_verbose(): if is_verbose():
print "Testing ar..." print("Testing ar...")
if which('ar')== None: if which('ar')== None:
raise MKException('ar (archive tool) was not found') raise MKException('ar (archive tool) was not found')
@ -322,7 +316,7 @@ def dos2unix(fname):
fout.close() fout.close()
shutil.move(fname_new, fname) shutil.move(fname_new, fname)
if is_verbose(): if is_verbose():
print "dos2unix '%s'" % fname print("dos2unix '%s'" % fname)
def dos2unix_tree_core(pattern, dir, files): def dos2unix_tree_core(pattern, dir, files):
for filename in files: for filename in files:
@ -339,7 +333,7 @@ def check_eol():
# Linux/OSX/BSD check if the end-of-line is cr/lf # Linux/OSX/BSD check if the end-of-line is cr/lf
if is_cr_lf('LICENSE.txt'): if is_cr_lf('LICENSE.txt'):
if is_verbose(): if is_verbose():
print "Fixing end of line..." print("Fixing end of line...")
dos2unix_tree() dos2unix_tree()
if os.name == 'nt': if os.name == 'nt':
@ -355,42 +349,42 @@ elif os.name == 'posix':
IS_LINUX=True IS_LINUX=True
def display_help(exit_code): def display_help(exit_code):
print "mk_make.py: Z3 Makefile generator\n" print("mk_make.py: Z3 Makefile generator\n")
print "This script generates the Makefile for the Z3 theorem prover." print("This script generates the Makefile for the Z3 theorem prover.")
print "It must be executed from the Z3 root directory." print("It must be executed from the Z3 root directory.")
print "\nOptions:" print("\nOptions:")
print " -h, --help display this message." print(" -h, --help display this message.")
print " -s, --silent do not print verbose messages." print(" -s, --silent do not print verbose messages.")
if not IS_WINDOWS: if not IS_WINDOWS:
print " -p <dir>, --prefix=<dir> installation prefix (default: %s)." % PREFIX print(" -p <dir>, --prefix=<dir> installation prefix (default: %s)." % PREFIX)
print " -y <dir>, --pydir=<dir> installation prefix for Z3 python bindings (default: %s)." % PYTHON_PACKAGE_DIR print(" -y <dir>, --pydir=<dir> installation prefix for Z3 python bindings (default: %s)." % PYTHON_PACKAGE_DIR)
else: else:
print " --parallel=num use cl option /MP with 'num' parallel processes" print(" --parallel=num use cl option /MP with 'num' parallel processes")
print " -b <sudir>, --build=<subdir> subdirectory where Z3 will be built (default: build)." print(" -b <sudir>, --build=<subdir> subdirectory where Z3 will be built (default: build).")
print " -d, --debug compile Z3 in debug mode." print(" -d, --debug compile Z3 in debug mode.")
print " -t, --trace enable tracing in release mode." print(" -t, --trace enable tracing in release mode.")
if IS_WINDOWS: if IS_WINDOWS:
print " -x, --x64 create 64 binary when using Visual Studio." print(" -x, --x64 create 64 binary when using Visual Studio.")
print " -m, --makefiles generate only makefiles." print(" -m, --makefiles generate only makefiles.")
if IS_WINDOWS: if IS_WINDOWS:
print " -v, --vsproj generate Visual Studio Project Files." print(" -v, --vsproj generate Visual Studio Project Files.")
if IS_WINDOWS: if IS_WINDOWS:
print " -n, --nodotnet do not generate Microsoft.Z3.dll make rules." print(" -n, --nodotnet do not generate Microsoft.Z3.dll make rules.")
print " -j, --java generate Java bindinds." print(" -j, --java generate Java bindinds.")
print " --staticlib build Z3 static library." print(" --staticlib build Z3 static library.")
if not IS_WINDOWS: if not IS_WINDOWS:
print " -g, --gmp use GMP." print(" -g, --gmp use GMP.")
print "" print("")
print "Some influential environment variables:" print("Some influential environment variables:")
if not IS_WINDOWS: if not IS_WINDOWS:
print " CXX C++ compiler" print(" CXX C++ compiler")
print " CC C compiler" print(" CC C compiler")
print " LDFLAGS Linker flags, e.g., -L<lib dir> if you have libraries in a non-standard directory" print(" LDFLAGS Linker flags, e.g., -L<lib dir> if you have libraries in a non-standard directory")
print " CPPFLAGS Preprocessor flags, e.g., -I<include dir> if you have header files in a non-standard directory" print(" CPPFLAGS Preprocessor flags, e.g., -I<include dir> if you have header files in a non-standard directory")
print " CXXFLAGS C++ compiler flags" print(" CXXFLAGS C++ compiler flags")
print " JAVA Java virtual machine (only relevant if -j or --java option is provided)" 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(" 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(" JAVA_HOME JDK installation directory (only relevant if -j or --java option is provided)")
exit(exit_code) exit(exit_code)
# Parse configuration option for mk_make script # Parse configuration option for mk_make script
@ -403,7 +397,7 @@ def parse_options():
['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'java', 'pydir=', 'parallel=']) 'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'java', 'pydir=', 'parallel='])
except: except:
print "ERROR: Invalid command line option" print("ERROR: Invalid command line option")
display_help(1) display_help(1)
for opt, arg in options: for opt, arg in options:
@ -446,7 +440,7 @@ def parse_options():
elif opt in ('-j', '--java'): elif opt in ('-j', '--java'):
JAVA_ENABLED = True JAVA_ENABLED = True
else: else:
print "ERROR: Invalid command line option '%s'" % opt print("ERROR: Invalid command line option '%s'" % opt)
display_help(1) display_help(1)
# Return a list containing a file names included using '#include' in # 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) raise MKException("Python bindings directory '%s' does not exist" % full)
Z3PY_SRC_DIR = full Z3PY_SRC_DIR = full
if VERBOSE: if VERBOSE:
print "Python bindinds directory was detected." print("Python bindinds directory was detected.")
_UNIQ_ID = 0 _UNIQ_ID = 0
@ -781,7 +775,7 @@ def comp_components(c1, c2):
# Sort components based on (reverse) definition time # Sort components based on (reverse) definition time
def sort_components(cnames): 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): class ExeComponent(Component):
def __init__(self, name, exe_name, path, deps, install): 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)): 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)) shutil.copyfile(os.path.join(full, py), os.path.join(BUILD_DIR, py))
if is_verbose(): 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) out.write('_ex_%s: \n\n' % self.name)
@ -1208,7 +1202,7 @@ def reg_component(name, c):
_ComponentNames.add(name) _ComponentNames.add(name)
_Name2Component[name] = c _Name2Component[name] = c
if VERBOSE: if VERBOSE:
print "New component: '%s'" % name print("New component: '%s'" % name)
def add_lib(name, deps=[], path=None, includes2install=[]): def add_lib(name, deps=[], path=None, includes2install=[]):
c = LibComponent(name, path, deps, includes2install) c = LibComponent(name, path, deps, includes2install)
@ -1315,11 +1309,11 @@ def mk_config():
# End of Windows VS config.mk # End of Windows VS config.mk
if is_verbose(): if is_verbose():
print '64-bit: %s' % is64() print('64-bit: %s' % is64())
if is_java_enabled(): if is_java_enabled():
print 'Java Home: %s' % JAVA_HOME print('Java Home: %s' % JAVA_HOME)
print 'Java Compiler: %s' % JAVAC print('Java Compiler: %s' % JAVAC)
print 'Java VM: %s' % JAVA print('Java VM: %s' % JAVA)
else: else:
global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS
ARITH = "internal" ARITH = "internal"
@ -1401,17 +1395,17 @@ def mk_config():
config.write('SLINK_EXTRA_FLAGS=%s\n' % SLIBEXTRAFLAGS) config.write('SLINK_EXTRA_FLAGS=%s\n' % SLIBEXTRAFLAGS)
config.write('SLINK_OUT_FLAG=-o \n') config.write('SLINK_OUT_FLAG=-o \n')
if is_verbose(): if is_verbose():
print 'Host platform: %s' % sysname print('Host platform: %s' % sysname)
print 'C++ Compiler: %s' % CXX print('C++ Compiler: %s' % CXX)
print 'C Compiler : %s' % CC print('C Compiler : %s' % CC)
print 'Arithmetic: %s' % ARITH print('Arithmetic: %s' % ARITH)
print 'OpenMP: %s' % HAS_OMP print('OpenMP: %s' % HAS_OMP)
print 'Prefix: %s' % PREFIX print('Prefix: %s' % PREFIX)
print '64-bit: %s' % is64() print('64-bit: %s' % is64())
if is_java_enabled(): if is_java_enabled():
print 'Java Home: %s' % JAVA_HOME print('Java Home: %s' % JAVA_HOME)
print 'Java Compiler: %s' % JAVAC print('Java Compiler: %s' % JAVAC)
print 'Java VM: %s' % JAVA print('Java VM: %s' % JAVA)
def mk_install(out): def mk_install(out):
out.write('install:\n') out.write('install:\n')
@ -1437,7 +1431,7 @@ def mk_makefile():
mk_dir(BUILD_DIR) mk_dir(BUILD_DIR)
mk_config() mk_config()
if VERBOSE: 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 = open(os.path.join(BUILD_DIR, 'Makefile'), 'w')
out.write('# Automatically generated file.\n') out.write('# Automatically generated file.\n')
out.write('include config.mk\n') out.write('include config.mk\n')
@ -1465,24 +1459,24 @@ def mk_makefile():
mk_uninstall(out) mk_uninstall(out)
# Finalize # Finalize
if VERBOSE: if VERBOSE:
print "Makefile was successfully generated." print("Makefile was successfully generated.")
if not IS_WINDOWS: if not IS_WINDOWS:
print " python packages dir:", PYTHON_PACKAGE_DIR print(" python packages dir: %s" % PYTHON_PACKAGE_DIR)
if DEBUG_MODE: if DEBUG_MODE:
print " compilation mode: Debug" print(" compilation mode: Debug")
else: else:
print " compilation mode: Release" print(" compilation mode: Release")
if IS_WINDOWS: if IS_WINDOWS:
if VS_X64: if VS_X64:
print " platform: x64\n" print(" platform: x64\n")
print "To build Z3, open a [Visual Studio x64 Command Prompt], then" print("To build Z3, open a [Visual Studio x64 Command Prompt], then")
else: else:
print " platform: x86" print(" platform: x86")
print "To build Z3, open a [Visual Studio Command Prompt], then" 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("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('Remark: to open a Visual Studio Command Prompt, go to: "Start > All Programs > Visual Studio > Visual Studio Tools"')
else: 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 # Generate automatically generated source code
def mk_auto_src(): 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('};\n')
out.write('#endif\n') out.write('#endif\n')
if is_verbose(): if is_verbose():
print "Generated '%s'" % hpp print("Generated '%s'" % hpp)
def max_memory_param(): def max_memory_param():
return ('max_memory', UINT, UINT_MAX, 'maximum amount of memory in megabytes') 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, 'max_steps_param' : max_steps_param,
'def_module_params' : def_module_params } '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. # Execute python auxiliary scripts that generate extra code for Z3.
def exec_pyg_scripts(): def exec_pyg_scripts():
global CURR_PYG global CURR_PYG
@ -1599,7 +1597,7 @@ def exec_pyg_scripts():
if f.endswith('.pyg'): if f.endswith('.pyg'):
script = os.path.join(root, f) script = os.path.join(root, f)
CURR_PYG = script CURR_PYG = script
execfile(script, PYG_GLOBALS) _execfile(script, PYG_GLOBALS)
# TODO: delete after src/ast/pattern/expr_pattern_match # TODO: delete after src/ast/pattern/expr_pattern_match
# database.smt ==> database.h # database.smt ==> database.h
@ -1612,7 +1610,7 @@ def mk_pat_db():
fout.write('"%s\\n"\n' % line.strip('\n')) fout.write('"%s\\n"\n' % line.strip('\n'))
fout.write(';\n') fout.write(';\n')
if VERBOSE: 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 # Update version numbers
def update_version(): 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_BUILD_NUMBER %s\n' % build)
fout.write('#define Z3_REVISION_NUMBER %s\n' % revision) fout.write('#define Z3_REVISION_NUMBER %s\n' % revision)
if VERBOSE: 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 # Update version number in AssemblyInfo.cs files
def update_all_assembly_infos(major, minor, build, revision): 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: else:
fout.write(line) fout.write(line)
# if VERBOSE: # 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" assert num_updates == 2, "unexpected number of version number updates"
fin.close() fin.close()
fout.close() fout.close()
shutil.move(tmp, assemblyinfo) shutil.move(tmp, assemblyinfo)
if VERBOSE: if VERBOSE:
print "Updated '%s'" % assemblyinfo print("Updated '%s'" % assemblyinfo)
ADD_TACTIC_DATA=[] ADD_TACTIC_DATA=[]
ADD_PROBE_DATA=[] ADD_PROBE_DATA=[]
@ -1734,7 +1732,7 @@ def mk_install_tactic_cpp(cnames, path):
added_include = True added_include = True
fout.write('#include"%s"\n' % h_file) fout.write('#include"%s"\n' % h_file)
try: try:
exec line.strip('\n ') in globals() exec(line.strip('\n '), globals())
except: except:
raise MKException("Failed processing ADD_TACTIC command at '%s'\n%s" % (fullname, line)) raise MKException("Failed processing ADD_TACTIC command at '%s'\n%s" % (fullname, line))
if probe_pat.match(line): if probe_pat.match(line):
@ -1742,7 +1740,7 @@ def mk_install_tactic_cpp(cnames, path):
added_include = True added_include = True
fout.write('#include"%s"\n' % h_file) fout.write('#include"%s"\n' % h_file)
try: try:
exec line.strip('\n ') in globals() exec(line.strip('\n '), globals())
except: except:
raise MKException("Failed processing ADD_PROBE command at '%s'\n%s" % (fullname, line)) raise MKException("Failed processing ADD_PROBE command at '%s'\n%s" % (fullname, line))
# First pass will just generate the tactic factories # 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(' ADD_PROBE("%s", "%s", %s);\n' % data)
fout.write('}\n') fout.write('}\n')
if VERBOSE: if VERBOSE:
print "Generated '%s'" % fullname print("Generated '%s'" % fullname)
def mk_all_install_tactic_cpps(): def mk_all_install_tactic_cpps():
if not ONLY_MAKEFILES: if not ONLY_MAKEFILES:
@ -1824,7 +1822,7 @@ def mk_mem_initializer_cpp(cnames, path):
fout.write('\n') fout.write('\n')
fout.write('}\n') fout.write('}\n')
if VERBOSE: if VERBOSE:
print "Generated '%s'" % fullname print("Generated '%s'" % fullname)
def mk_all_mem_initializer_cpps(): def mk_all_mem_initializer_cpps():
if not ONLY_MAKEFILES: 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('gparams::register_module_descr("%s", "%s");\n' % (mod, descr))
fout.write('}\n') fout.write('}\n')
if VERBOSE: if VERBOSE:
print "Generated '%s'" % fullname print("Generated '%s'" % fullname)
def mk_all_gparams_register_modules(): def mk_all_gparams_register_modules():
if not ONLY_MAKEFILES: if not ONLY_MAKEFILES:
@ -1914,7 +1912,7 @@ def mk_def_file(c):
i = i + 1 i = i + 1
num = num + 1 num = num + 1
if VERBOSE: if VERBOSE:
print "Generated '%s'" % defname print("Generated '%s'" % defname)
def mk_def_files(): def mk_def_files():
if not ONLY_MAKEFILES: 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)) shutil.copyfile(os.path.join(Z3PY_SRC_DIR, pyc), os.path.join(BUILD_DIR, pyc))
os.remove(os.path.join(Z3PY_SRC_DIR, pyc)) os.remove(os.path.join(Z3PY_SRC_DIR, pyc))
if is_verbose(): if is_verbose():
print "Generated '%s'" % pyc print("Generated '%s'" % pyc)
def mk_bindings(api_files): def mk_bindings(api_files):
if not ONLY_MAKEFILES: if not ONLY_MAKEFILES:
@ -1945,12 +1943,12 @@ def mk_bindings(api_files):
for api_file in api_files: for api_file in api_files:
api_file_path = api.find_file(api_file, api.name) api_file_path = api.find_file(api_file, api.name)
new_api_files.append(os.path.join(api_file_path.src_dir, api_file)) new_api_files.append(os.path.join(api_file_path.src_dir, api_file))
g = {} g = globals()
g["API_FILES"] = new_api_files g["API_FILES"] = new_api_files
if is_java_enabled(): if is_java_enabled():
check_java() check_java()
mk_z3consts_java(api_files) 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() cp_z3pyc_to_build()
# Extract enumeration types from API files, and add python definitions. # Extract enumeration types from API files, and add python definitions.
@ -2014,7 +2012,8 @@ def mk_z3consts_py(api_files):
if m: if m:
name = words[1] name = words[1]
z3consts.write('# enum %s\n' % name) 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('%s = %s\n' % (k, i))
z3consts.write('\n') z3consts.write('\n')
mode = SEARCHING mode = SEARCHING
@ -2028,7 +2027,7 @@ def mk_z3consts_py(api_files):
idx = idx + 1 idx = idx + 1
linenum = linenum + 1 linenum = linenum + 1
if VERBOSE: 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 # Extract enumeration types from z3_api.h, and add .Net definitions
@ -2098,7 +2097,8 @@ def mk_z3consts_dotnet(api_files):
z3consts.write(' /// <summary>%s</summary>\n' % name) z3consts.write(' /// <summary>%s</summary>\n' % name)
z3consts.write(' public enum %s {\n' % name) z3consts.write(' public enum %s {\n' % name)
z3consts.write z3consts.write
for k, i in decls.iteritems(): for k in decls:
i = decls[k]
z3consts.write(' %s = %s,\n' % (k, i)) z3consts.write(' %s = %s,\n' % (k, i))
z3consts.write(' }\n\n') z3consts.write(' }\n\n')
mode = SEARCHING mode = SEARCHING
@ -2113,7 +2113,7 @@ def mk_z3consts_dotnet(api_files):
linenum = linenum + 1 linenum = linenum + 1
z3consts.write('}\n'); z3consts.write('}\n');
if VERBOSE: 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 # 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('public enum %s {\n' % name)
efile.write efile.write
first = True first = True
for k, i in decls.iteritems(): for k in decls:
i = decls[k]
if first: if first:
first = False first = False
else: else:
@ -2218,7 +2219,7 @@ def mk_z3consts_java(api_files):
idx = idx + 1 idx = idx + 1
linenum = linenum + 1 linenum = linenum + 1
if VERBOSE: if VERBOSE:
print "Generated '%s'" % ('%s' % gendir) print("Generated '%s'" % ('%s' % gendir))
def mk_gui_str(id): def mk_gui_str(id):
return '4D2F40D8-E5F9-473B-B548-%012d' % id return '4D2F40D8-E5F9-473B-B548-%012d' % id
@ -2305,7 +2306,7 @@ def mk_vs_proj(name, components):
f.write(' </ImportGroup>\n') f.write(' </ImportGroup>\n')
f.write('</Project>\n') f.write('</Project>\n')
if is_verbose(): if is_verbose():
print "Generated '%s'" % proj_name print("Generated '%s'" % proj_name)
def mk_win_dist(build_path, dist_path): def mk_win_dist(build_path, dist_path):
for c in get_components(): for c in get_components():

61
scripts/update_api.py
View file

@ -84,6 +84,19 @@ def lib():
raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python") raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")
return _lib 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): def init(PATH):
global _lib global _lib
_lib = ctypes.CDLL(PATH) _lib = ctypes.CDLL(PATH)
@ -146,20 +159,22 @@ next_type_id = FIRST_OBJ_ID
def def_Type(var, c_type, py_type): def def_Type(var, c_type, py_type):
global next_type_id 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 Type2Str[next_type_id] = c_type
Type2PyStr[next_type_id] = py_type Type2PyStr[next_type_id] = py_type
next_type_id = next_type_id + 1 next_type_id = next_type_id + 1
def def_Types(): def def_Types():
pat1 = re.compile(" *def_Type.*") import re
pat1 = re.compile(" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*")
for api_file in API_FILES: for api_file in API_FILES:
api = open(api_file, 'r') api = open(api_file, 'r')
for line in api: for line in api:
m = pat1.match(line) m = pat1.match(line)
if m: if m:
eval(line) def_Type(m.group(1), m.group(2), m.group(3))
for k, v in Type2Str.iteritems(): for k in Type2Str:
v = Type2Str[k]
if is_obj(k): if is_obj(k):
Type2Dotnet[k] = v Type2Dotnet[k] = v
@ -258,7 +273,7 @@ def param2java(p):
elif param_type(p) == STRING: elif param_type(p) == STRING:
return "StringPtr" return "StringPtr"
else: else:
print "ERROR: unreachable code" print("ERROR: unreachable code")
assert(False) assert(False)
exit(1) exit(1)
if k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: 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(", ")
core_py.write("a%s" % i) 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(): def mk_py_wrappers():
core_py.write("\n") core_py.write("\n")
for sig in _API2PY: for sig in _API2PY:
@ -327,13 +353,15 @@ def mk_py_wrappers():
core_py.write(" r = lib().%s(" % name) core_py.write(" r = lib().%s(" % name)
else: else:
core_py.write(" lib().%s(" % name) core_py.write(" lib().%s(" % name)
display_args(num) display_args_to_z3(params)
core_py.write(")\n") core_py.write(")\n")
if len(params) > 0 and param_type(params[0]) == CONTEXT: if len(params) > 0 and param_type(params[0]) == CONTEXT:
core_py.write(" err = lib().Z3_get_error_code(a0)\n") core_py.write(" err = lib().Z3_get_error_code(a0)\n")
core_py.write(" if err != Z3_OK:\n") core_py.write(" if err != Z3_OK:\n")
core_py.write(" raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))\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(" return r\n")
core_py.write("\n") core_py.write("\n")
@ -356,7 +384,8 @@ def mk_dotnet():
dotnet.write('#pragma warning disable 1591\n\n'); dotnet.write('#pragma warning disable 1591\n\n');
dotnet.write('namespace Microsoft.Z3\n') dotnet.write('namespace Microsoft.Z3\n')
dotnet.write('{\n') dotnet.write('{\n')
for k, v in Type2Str.iteritems(): for k in Type2Str:
v = Type2Str[k]
if is_obj(k): if is_obj(k):
dotnet.write(' using %s = System.IntPtr;\n' % v) dotnet.write(' using %s = System.IntPtr;\n' % v)
dotnet.write('\n'); dotnet.write('\n');
@ -579,7 +608,7 @@ def mk_java():
java_wrapper.write(' } \n\n') java_wrapper.write(' } \n\n')
java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n') java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n')
java_wrapper.write(' delete [] NEW; \n\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(' { \\\n')
java_wrapper.write(' jlong * temp = new jlong[SZ]; \\\n') java_wrapper.write(' jlong * temp = new jlong[SZ]; \\\n')
java_wrapper.write(' jenv->GetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)temp); \\\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('}\n')
java_wrapper.write('#endif\n') java_wrapper.write('#endif\n')
if is_verbose(): if is_verbose():
print "Generated '%s'" % java_nativef print("Generated '%s'" % java_nativef)
def mk_log_header(file, name, params): def mk_log_header(file, name, params):
file.write("void log_%s(" % name) file.write("void log_%s(" % name)
@ -710,7 +739,7 @@ def mk_log_header(file, name, params):
for p in params: for p in params:
if i > 0: if i > 0:
file.write(", "); file.write(", ");
file.write("%s a%s" % (param2str(p), i)) file.write("%s a%s" % (param2str(p), i))
i = i + 1 i = i + 1
file.write(")"); file.write(")");
@ -981,8 +1010,8 @@ exe_c.close()
core_py.close() core_py.close()
if is_verbose(): 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.h'))
print "Generated '%s'" % os.path.join(api_dir, 'api_log_macros.cpp') 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(api_dir, 'api_commands.cpp'))
print "Generated '%s'" % os.path.join(get_z3py_dir(), 'z3core.py') 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(dotnet_dir, 'Native.cs'))

449
src/api/python/z3.py
View file

@ -37,15 +37,23 @@ Z3 exceptions:
... # the expression x + y is type incorrect ... # the expression x + y is type incorrect
... n = x + y ... n = x + y
... except Z3Exception as ex: ... except Z3Exception as ex:
... print "failed:", ex ... print("failed: %s" % ex)
failed: 'sort mismatch' failed: 'sort mismatch'
""" """
from z3core import * from z3core import *
from z3types import * from z3types import *
from z3consts import * from z3consts import *
from z3printer import * from z3printer import *
import sys
import io 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): def enable_trace(msg):
Z3_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. # list of arguments.
def _get_args(args): def _get_args(args):
try: try:
if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)): if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)):
return args[0] return args[0]
else: else:
return args return args
except: # len is not necessarily defined when args is not a sequence (use reflection?) 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): def _Z3python_error_handler_core(c, e):
# Do nothing error handler, just avoid exit(0) # Do nothing error handler, just avoid exit(0)
@ -140,7 +148,8 @@ class Context:
if __debug__: if __debug__:
_z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.") _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
conf = Z3_mk_config() 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)) Z3_set_param_value(conf, str(key).upper(), _to_param_value(value))
prev = None prev = None
for a in args: for a in args:
@ -209,10 +218,12 @@ def set_param(*args, **kws):
if __debug__: if __debug__:
_z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.") _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
new_kws = {} new_kws = {}
for k, v in kws.iteritems(): for k in kws:
v = kws[k]
if not set_pp_option(k, v): if not set_pp_option(k, v):
new_kws[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)) Z3_global_param_set(str(key).upper(), _to_param_value(value))
prev = None prev = None
for a in args: for a in args:
@ -240,7 +251,7 @@ def get_param(name):
""" """
ptr = (ctypes.c_char_p * 1)() ptr = (ctypes.c_char_p * 1)()
if Z3_global_param_get(str(name), ptr): if Z3_global_param_get(str(name), ptr):
r = str(ptr[0]) r = z3core._to_pystr(ptr[0])
return r return r
raise Z3Exception("failed to retrieve value for '%s'" % name) raise Z3Exception("failed to retrieve value for '%s'" % name)
@ -899,11 +910,22 @@ def _coerce_exprs(a, b, ctx=None):
b = s.cast(b) b = s.cast(b)
return (a, 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): def _coerce_expr_list(alist, ctx=None):
if filter(is_expr, alist) == []: has_expr = False
alist = map(lambda a: _py2expr(a, ctx), alist) for a in alist:
s = reduce(_coerce_expr_merge, alist, None) if is_expr(a):
return map(lambda a: s.cast(a), alist) 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): def is_expr(a):
"""Return `True` if `a` is a Z3 expression. """Return `True` if `a` is a Z3 expression.
@ -1518,7 +1540,7 @@ def MultiPattern(*args):
""" """
if __debug__: if __debug__:
_z3_assert(len(args) > 0, "At least one argument expected") _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 ctx = args[0].ctx
args, sz = _to_ast_array(args) args, sz = _to_ast_array(args)
return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx) 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=[]): def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
if __debug__: if __debug__:
_z3_assert(is_bool(body), "Z3 expression expected") _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(is_const(vs) or (len(vs) > 0 and all([ is_const(v) for v in 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([is_pattern(a) or is_expr(a) for a in patterns]), "Z3 patterns expected")
_z3_assert(all(map(is_expr, no_patterns)), "no patterns are Z3 expressions") _z3_assert(all([is_expr(p) for p in no_patterns]), "no patterns are Z3 expressions")
ctx = body.ctx ctx = body.ctx
if is_app(vs): if is_app(vs):
vs = [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): for i in range(num_vars):
## TODO: Check if is constant ## TODO: Check if is constant
_vs[i] = vs[i].as_ast() _vs[i] = vs[i].as_ast()
patterns = map(_to_pattern, patterns) patterns = [ _to_pattern(p) for p in patterns ]
num_pats = len(patterns) num_pats = len(patterns)
_pats = (Pattern * num_pats)() _pats = (Pattern * num_pats)()
for i in range(num_pats): for i in range(num_pats):
@ -2008,7 +2030,7 @@ class ArithRef(ExprRef):
def __truediv__(self, other): def __truediv__(self, other):
"""Create the Z3 expression `other/self`.""" """Create the Z3 expression `other/self`."""
self.__div__(other) return self.__div__(other)
def __rdiv__(self, other): def __rdiv__(self, other):
"""Create the Z3 expression `other/self`. """Create the Z3 expression `other/self`.
@ -2029,7 +2051,7 @@ class ArithRef(ExprRef):
def __rtruediv__(self, other): def __rtruediv__(self, other):
"""Create the Z3 expression `other/self`.""" """Create the Z3 expression `other/self`."""
self.__rdiv__(other) return self.__rdiv__(other)
def __mod__(self, other): def __mod__(self, other):
"""Create the Z3 expression `other%self`. """Create the Z3 expression `other%self`.
@ -2413,11 +2435,11 @@ class IntNumRef(ArithRef):
>>> v + 1 >>> v + 1
1 + 1 1 + 1
>>> v.as_long() + 1 >>> v.as_long() + 1
2L 2
""" """
if __debug__: if __debug__:
_z3_assert(self.is_int(), "Integer value expected") _z3_assert(self.is_int(), "Integer value expected")
return long(self.as_string()) return int(self.as_string())
def as_string(self): def as_string(self):
"""Return a Z3 integer numeral as a Python string. """Return a Z3 integer numeral as a Python string.
@ -2465,7 +2487,7 @@ class RatNumRef(ArithRef):
>>> v + 1 >>> v + 1
10000000000 + 1 10000000000 + 1
>>> v.numerator_as_long() + 1 >>> v.numerator_as_long() + 1
10000000001L 10000000001
""" """
return self.numerator().as_long() return self.numerator().as_long()
@ -2476,7 +2498,7 @@ class RatNumRef(ArithRef):
>>> v >>> v
1/3 1/3
>>> v.denominator_as_long() >>> v.denominator_as_long()
3L 3
""" """
return self.denominator().as_long() return self.denominator().as_long()
@ -2529,7 +2551,7 @@ class AlgebraicNumRef(ArithRef):
def _py2expr(a, ctx=None): def _py2expr(a, ctx=None):
if isinstance(a, bool): if isinstance(a, bool):
return BoolVal(a, ctx) return BoolVal(a, ctx)
if isinstance(a, int) or isinstance(a, long): if _is_int(a):
return IntVal(a, ctx) return IntVal(a, ctx)
if isinstance(a, float): if isinstance(a, float):
return RealVal(a, ctx) return RealVal(a, ctx)
@ -2576,9 +2598,7 @@ def _to_int_str(val):
return "1" return "1"
else: else:
return "0" return "0"
elif isinstance(val, int): elif _is_int(val):
return str(val)
elif isinstance(val, long):
return str(val) return str(val)
elif isinstance(val, str): elif isinstance(val, str):
return val return val
@ -2625,8 +2645,8 @@ def RatVal(a, b, ctx=None):
Real Real
""" """
if __debug__: 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(_is_int(a) or isinstance(a, str), "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(b) or isinstance(b, str), "Second argument cannot be converted into an integer")
return simplify(RealVal(a, ctx)/RealVal(b, ctx)) return simplify(RealVal(a, ctx)/RealVal(b, ctx))
def Q(a, b, ctx=None): def Q(a, b, ctx=None):
@ -3078,7 +3098,7 @@ class BitVecRef(ExprRef):
def __truediv__(self, other): def __truediv__(self, other):
"""Create the Z3 expression (signed) division `self / other`.""" """Create the Z3 expression (signed) division `self / other`."""
self.__div__(other) return self.__div__(other)
def __rdiv__(self, other): def __rdiv__(self, other):
"""Create the Z3 expression (signed) division `other / self`. """Create the Z3 expression (signed) division `other / self`.
@ -3098,7 +3118,7 @@ class BitVecRef(ExprRef):
def __rtruediv__(self, other): def __rtruediv__(self, other):
"""Create the Z3 expression (signed) division `other / self`.""" """Create the Z3 expression (signed) division `other / self`."""
self.__rdiv__(other) return self.__rdiv__(other)
def __mod__(self, other): def __mod__(self, other):
"""Create the Z3 expression (signed) mod `self % other`. """Create the Z3 expression (signed) mod `self % other`.
@ -3218,9 +3238,9 @@ class BitVecRef(ExprRef):
>>> BitVecVal(4, 3) >>> BitVecVal(4, 3)
4 4
>>> BitVecVal(4, 3).as_signed_long() >>> BitVecVal(4, 3).as_signed_long()
-4L -4
>>> simplify(BitVecVal(4, 3) >> 1).as_signed_long() >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
-2L -2
>>> simplify(BitVecVal(4, 3) >> 1) >>> simplify(BitVecVal(4, 3) >> 1)
6 6
>>> simplify(LShR(BitVecVal(4, 3), 1)) >>> simplify(LShR(BitVecVal(4, 3), 1))
@ -3284,32 +3304,32 @@ class BitVecNumRef(BitVecRef):
>>> v = BitVecVal(0xbadc0de, 32) >>> v = BitVecVal(0xbadc0de, 32)
>>> v >>> v
195936478 195936478
>>> print "0x%.8x" % v.as_long() >>> print("0x%.8x" % v.as_long())
0x0badc0de 0x0badc0de
""" """
return long(self.as_string()) return int(self.as_string())
def as_signed_long(self): 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. """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() >>> BitVecVal(4, 3).as_signed_long()
-4L -4
>>> BitVecVal(7, 3).as_signed_long() >>> BitVecVal(7, 3).as_signed_long()
-1L -1
>>> BitVecVal(3, 3).as_signed_long() >>> BitVecVal(3, 3).as_signed_long()
3L 3
>>> BitVecVal(2L**32 - 1, 32).as_signed_long() >>> BitVecVal(2**32 - 1, 32).as_signed_long()
-1L -1
>>> BitVecVal(2L**64 - 1, 64).as_signed_long() >>> BitVecVal(2**64 - 1, 64).as_signed_long()
-1L -1
""" """
sz = long(self.size()) sz = self.size()
val = self.as_long() val = self.as_long()
if val >= 2L**(sz - 1): if val >= 2**(sz - 1):
val = val - 2L**sz val = val - 2**sz
if val < -2L**(sz - 1): if val < -2**(sz - 1):
val = val + 2L**sz val = val + 2**sz
return val return int(val)
def as_string(self): def as_string(self):
return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) 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 = BitVecVal(10, 32)
>>> v >>> v
10 10
>>> print "0x%.8x" % v.as_long() >>> print("0x%.8x" % v.as_long())
0x0000000a 0x0000000a
""" """
if is_bv_sort(bv): if is_bv_sort(bv):
@ -3440,12 +3460,12 @@ def Concat(*args):
Concat(Concat(1, 1 + 1), 1) Concat(Concat(1, 1 + 1), 1)
>>> simplify(Concat(v, v+1, v)) >>> simplify(Concat(v, v+1, v))
289 289
>>> print "%.3x" % simplify(Concat(v, v+1, v)).as_long() >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
121 121
""" """
args = _get_args(args) args = _get_args(args)
if __debug__: 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.") _z3_assert(len(args) >= 2, "At least two arguments expected.")
ctx = args[0].ctx ctx = args[0].ctx
r = args[0] r = args[0]
@ -3615,9 +3635,9 @@ def LShR(a, b):
>>> BitVecVal(4, 3) >>> BitVecVal(4, 3)
4 4
>>> BitVecVal(4, 3).as_signed_long() >>> BitVecVal(4, 3).as_signed_long()
-4L -4
>>> simplify(BitVecVal(4, 3) >> 1).as_signed_long() >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
-2L -2
>>> simplify(BitVecVal(4, 3) >> 1) >>> simplify(BitVecVal(4, 3) >> 1)
6 6
>>> simplify(LShR(BitVecVal(4, 3), 1)) >>> simplify(LShR(BitVecVal(4, 3), 1))
@ -3682,7 +3702,7 @@ def SignExt(n, a):
254 254
>>> v.size() >>> v.size()
8 8
>>> print "%.x" % v.as_long() >>> print("%.x" % v.as_long())
fe fe
""" """
if __debug__: if __debug__:
@ -3727,12 +3747,12 @@ def RepeatBitVec(n, a):
>>> n.size() >>> n.size()
32 32
>>> v0 = BitVecVal(10, 4) >>> v0 = BitVecVal(10, 4)
>>> print "%.x" % v0.as_long() >>> print("%.x" % v0.as_long())
a a
>>> v = simplify(RepeatBitVec(4, v0)) >>> v = simplify(RepeatBitVec(4, v0))
>>> v.size() >>> v.size()
16 16
>>> print "%.x" % v.as_long() >>> print("%.x" % v.as_long())
aaaa aaaa
""" """
if __debug__: if __debug__:
@ -4006,7 +4026,7 @@ def Map(f, *args):
if __debug__: if __debug__:
_z3_assert(len(args) > 0, "At least one Z3 array expression expected") _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(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") _z3_assert(len(args) == f.arity(), "Number of arguments mismatch")
_args, sz = _to_ast_array(args) _args, sz = _to_ast_array(args)
ctx = f.ctx ctx = f.ctx
@ -4100,7 +4120,7 @@ class Datatype:
if __debug__: if __debug__:
_z3_assert(isinstance(name, str), "String expected") _z3_assert(isinstance(name, str), "String expected")
_z3_assert(isinstance(rec_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)) self.constructors.append((name, rec_name, args))
def declare(self, name, *args): def declare(self, name, *args):
@ -4187,9 +4207,9 @@ def CreateDatatypes(*ds):
ds = _get_args(ds) ds = _get_args(ds)
if __debug__: if __debug__:
_z3_assert(len(ds) > 0, "At least one Datatype must be specified") _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([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes")
_z3_assert(all(map(lambda d: d.ctx == ds[0].ctx, ds)), "Context mismatch") _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch")
_z3_assert(all(map(lambda d: d.constructors != [], ds)), "Non-empty Datatypes expected") _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected")
ctx = ds[0].ctx ctx = ds[0].ctx
num = len(ds) num = len(ds)
names = (Symbol * num)() names = (Symbol * num)()
@ -4355,7 +4375,7 @@ def EnumSort(name, values, ctx=None):
""" """
if __debug__: if __debug__:
_z3_assert(isinstance(name, str), "Name must be a string") _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") _z3_assert(len(values) > 0, "At least one value expected")
ctx = _get_ctx(ctx) ctx = _get_ctx(ctx)
num = len(values) num = len(values)
@ -4369,7 +4389,7 @@ def EnumSort(name, values, ctx=None):
V = [] V = []
for i in range(num): for i in range(num):
V.append(FuncDeclRef(_values[i], ctx)) V.append(FuncDeclRef(_values[i], ctx))
V = map(lambda a: a(), V) V = [a() for a in V]
return S, V return S, V
######################################### #########################################
@ -4432,7 +4452,8 @@ def args2params(arguments, keywords, ctx=None):
else: else:
r.set(prev, a) r.set(prev, a)
prev = None prev = None
for k, v in keywords.iteritems(): for k in keywords:
v = keywords[k]
r.set(k, v) r.set(k, v)
return r return r
@ -4469,7 +4490,7 @@ class ParamDescrsRef:
return Z3_param_descrs_get_kind(self.ctx.ref(), self.descr, to_symbol(n, self.ctx)) return Z3_param_descrs_get_kind(self.ctx.ref(), self.descr, to_symbol(n, self.ctx))
def __getitem__(self, arg): def __getitem__(self, arg):
if isinstance(arg, int) or isinstance(arg, long): if _is_int(arg):
return self.get_name(arg) return self.get_name(arg)
else: else:
return self.get_kind(arg) return self.get_kind(arg)
@ -5057,7 +5078,7 @@ class FuncEntry:
>>> try: >>> try:
... e.arg_value(2) ... e.arg_value(2)
... except IndexError: ... except IndexError:
... print "index error" ... print("index error")
index error index error
""" """
if idx >= self.num_args(): if idx >= self.num_args():
@ -5435,7 +5456,7 @@ class ModelRef(Z3PPObject):
1 1
>>> m[f] >>> m[f]
[1 -> 0, else -> 0] [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 x -> 1
f -> [1 -> 0, else -> 0] f -> [1 -> 0, else -> 0]
""" """
@ -5506,16 +5527,16 @@ class Statistics:
if in_html_mode(): if in_html_mode():
out = io.StringIO() out = io.StringIO()
even = True even = True
out.write(u'<table border="1" cellpadding="2" cellspacing="0">') out.write(u('<table border="1" cellpadding="2" cellspacing="0">'))
for k, v in self: for k, v in self:
if even: if even:
out.write(u'<tr style="background-color:#CFCFCF">') out.write(u('<tr style="background-color:#CFCFCF">'))
even = False even = False
else: else:
out.write(u'<tr>') out.write(u('<tr>'))
even = True even = True
out.write(u'<td>%s</td><td>%s</td></tr>' % (k, v)) out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v)))
out.write(u'</table>') out.write(u('</table>'))
return out.getvalue() return out.getvalue()
else: else:
return Z3_stats_to_string(self.ctx.ref(), self.stats) 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 > 0, 'p1')
>>> s.assert_and_track(x != 1, 'p2') >>> s.assert_and_track(x != 1, 'p2')
>>> s.assert_and_track(x < 0, p3) >>> s.assert_and_track(x < 0, p3)
>>> print s.check() >>> print(s.check())
unsat unsat
>>> c = s.unsat_core() >>> c = s.unsat_core()
>>> len(c) >>> len(c)
@ -5961,7 +5982,7 @@ class Solver(Z3PPObject):
def help(self): def help(self):
"""Display a string describing all available options.""" """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): def param_descrs(self):
"""Return the parameter description set.""" """Return the parameter description set."""
@ -6032,7 +6053,7 @@ class Fixedpoint(Z3PPObject):
else: else:
self.fixedpoint = fixedpoint self.fixedpoint = fixedpoint
Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint) Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint)
self.vars = [] self.vars = []
def __del__(self): def __del__(self):
if self.fixedpoint != None: if self.fixedpoint != None:
@ -6046,8 +6067,8 @@ class Fixedpoint(Z3PPObject):
def help(self): def help(self):
"""Display a string describing all available options.""" """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): def param_descrs(self):
"""Return the parameter description set.""" """Return the parameter description set."""
return ParamDescrsRef(Z3_fixedpoint_get_param_descrs(self.ctx.ref(), self.fixedpoint), self.ctx) 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: for arg in args:
if isinstance(arg, Goal) or isinstance(arg, AstVector): if isinstance(arg, Goal) or isinstance(arg, AstVector):
for f in arg: for f in arg:
f = self.abstract(f) f = self.abstract(f)
Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, f.as_ast()) Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, f.as_ast())
else: else:
arg = s.cast(arg) arg = s.cast(arg)
arg = self.abstract(arg) arg = self.abstract(arg)
Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, arg.as_ast()) Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, arg.as_ast())
def add(self, *args): def add(self, *args):
@ -6079,38 +6100,38 @@ class Fixedpoint(Z3PPObject):
self.assert_exprs(*args) self.assert_exprs(*args)
def add_rule(self, head, body = None, name = None): 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') >>> a = Bool('a')
>>> b = Bool('b') >>> b = Bool('b')
>>> s = Fixedpoint() >>> s = Fixedpoint()
>>> s.register_relation(a.decl()) >>> s.register_relation(a.decl())
>>> s.register_relation(b.decl()) >>> s.register_relation(b.decl())
>>> s.fact(a) >>> s.fact(a)
>>> s.rule(b, a) >>> s.rule(b, a)
>>> s.query(b) >>> s.query(b)
sat sat
""" """
if name == None: if name == None:
name = "" name = ""
name = to_symbol(name, self.ctx) name = to_symbol(name, self.ctx)
if body == None: if body == None:
head = self.abstract(head) head = self.abstract(head)
Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name) Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)
else: else:
body = _get_args(body) body = _get_args(body)
f = self.abstract(Implies(And(body),head)) f = self.abstract(Implies(And(body),head))
Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name) Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
def rule(self, head, body = None, name = None): def rule(self, head, body = None, name = None):
"""Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
self.add_rule(head, body, name) self.add_rule(head, body, name)
def fact(self, head, name = None): def fact(self, head, name = None):
"""Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.""" """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
self.add_rule(head, None, name) self.add_rule(head, None, name)
def query(self, *query): 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. You can also pass an tuple or list of recursive predicates.
""" """
query = _get_args(query) query = _get_args(query)
@ -6141,17 +6162,17 @@ class Fixedpoint(Z3PPObject):
def update_rule(self, head, body, name): def update_rule(self, head, body, name):
"""update rule""" """update rule"""
if name == None: if name == None:
name = "" name = ""
name = to_symbol(name, self.ctx) name = to_symbol(name, self.ctx)
body = _get_args(body) body = _get_args(body)
f = self.abstract(Implies(And(body),head)) 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): def get_answer(self):
"""Retrieve answer from last query call.""" """Retrieve answer from last query call."""
r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint) r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint)
return _to_expr_ref(r, self.ctx) return _to_expr_ref(r, self.ctx)
def get_num_levels(self, predicate): def get_num_levels(self, predicate):
"""Retrieve number of levels used for predicate in PDR engine""" """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) Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast)
def register_relation(self, *relations): def register_relation(self, *relations):
"""Register relation as recursive""" """Register relation as recursive"""
relations = _get_args(relations) relations = _get_args(relations)
for f in relations: for f in relations:
Z3_fixedpoint_register_relation(self.ctx.ref(), self.fixedpoint, f.ast) Z3_fixedpoint_register_relation(self.ctx.ref(), self.fixedpoint, f.ast)
def set_predicate_representation(self, f, *representations): def set_predicate_representation(self, f, *representations):
"""Control how relation is represented""" """Control how relation is represented"""
representations = _get_args(representations) representations = _get_args(representations)
representations = map(to_symbol, representations) representations = [to_symbol(s) for s in representations]
sz = len(representations) sz = len(representations)
args = (Symbol * sz)() args = (Symbol * sz)()
for i in range(sz): for i in range(sz):
args[i] = representations[i] args[i] = representations[i]
Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args) Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args)
def parse_string(self, s): def parse_string(self, s):
"""Parse rules and queries from a string""" """Parse rules and queries from a string"""
return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx) return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
def parse_file(self, f): def parse_file(self, f):
"""Parse rules and queries from a file""" """Parse rules and queries from a file"""
return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx) return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
def get_rules(self): def get_rules(self):
"""retrieve rules that have been added to fixedpoint context""" """retrieve rules that have been added to fixedpoint context"""
return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx) return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
def get_assertions(self): def get_assertions(self):
"""retrieve assertions that have been added to fixedpoint context""" """retrieve assertions that have been added to fixedpoint context"""
return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx) return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx)
def __repr__(self): def __repr__(self):
"""Return a formatted string with all added rules and constraints.""" """Return a formatted string with all added rules and constraints."""
return self.sexpr() return self.sexpr()
def sexpr(self): def sexpr(self):
"""Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format. """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)()) return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
def to_string(self, queries): 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. 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) return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
def statistics(self): def statistics(self):
"""Return statistics for the last `query()`. """Return statistics for the last `query()`.
""" """
return Statistics(Z3_fixedpoint_get_statistics(self.ctx.ref(), self.fixedpoint), self.ctx) return Statistics(Z3_fixedpoint_get_statistics(self.ctx.ref(), self.fixedpoint), self.ctx)
def reason_unknown(self): def reason_unknown(self):
@ -6226,21 +6247,21 @@ class Fixedpoint(Z3PPObject):
return Z3_fixedpoint_get_reason_unknown(self.ctx.ref(), self.fixedpoint) return Z3_fixedpoint_get_reason_unknown(self.ctx.ref(), self.fixedpoint)
def declare_var(self, *vars): def declare_var(self, *vars):
"""Add variable or several variables. """Add variable or several variables.
The added variable or variables will be bound in the rules The added variable or variables will be bound in the rules
and queries and queries
""" """
vars = _get_args(vars) vars = _get_args(vars)
for v in vars: for v in vars:
self.vars += [v] self.vars += [v]
def abstract(self, fml, is_forall=True): def abstract(self, fml, is_forall=True):
if self.vars == []: if self.vars == []:
return fml return fml
if is_forall: if is_forall:
return ForAll(self.vars, fml) return ForAll(self.vars, fml)
else: else:
return Exists(self.vars, fml) return Exists(self.vars, fml)
######################################### #########################################
# #
@ -6432,7 +6453,7 @@ class Tactic:
def help(self): def help(self):
"""Display a string containing a description of the available options for the `self` tactic.""" """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): def param_descrs(self):
"""Return the parameter description set.""" """Return the parameter description set."""
@ -6528,7 +6549,7 @@ def ParOr(*ts, **ks):
if __debug__: if __debug__:
_z3_assert(len(ts) >= 2, "At least two arguments expected") _z3_assert(len(ts) >= 2, "At least two arguments expected")
ctx = _get_ctx(ks.get('ctx', None)) 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) sz = len(ts)
_args = (TacticObj * sz)() _args = (TacticObj * sz)()
for i in range(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) >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
>>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip'))) >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
>>> r = t(c) >>> r = t(c)
>>> for subgoal in r: print subgoal >>> for subgoal in r: print(subgoal)
[x == 0, y == 0, x > y] [x == 0, y == 0, x > y]
[x == 0, y == 1, x > y] [x == 0, y == 1, x > y]
[x == 1, y == 0, 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.""" """Display a (tabular) description of all available tactics in Z3."""
if in_html_mode(): if in_html_mode():
even = True even = True
print '<table border="1" cellpadding="2" cellspacing="0">' print('<table border="1" cellpadding="2" cellspacing="0">')
for t in tactics(): for t in tactics():
if even: if even:
print '<tr style="background-color:#CFCFCF">' print('<tr style="background-color:#CFCFCF">')
even = False even = False
else: else:
print '<tr>' print('<tr>')
even = True even = True
print '<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(tactic_description(t), 40)) print('<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(tactic_description(t), 40)))
print '</table>' print('</table>')
else: else:
for t in tactics(): for t in tactics():
print '%s : %s' % (t, tactic_description(t)) print('%s : %s' % (t, tactic_description(t)))
class Probe: 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.""" """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 self.probe = probe
elif isinstance(probe, float): elif isinstance(probe, float):
self.probe = Z3_probe_const(self.ctx.ref(), probe) 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)) self.probe = Z3_probe_const(self.ctx.ref(), float(probe))
elif isinstance(probe, bool): elif isinstance(probe, bool):
if probe: if probe:
@ -6803,19 +6824,19 @@ def describe_probes():
"""Display a (tabular) description of all available probes in Z3.""" """Display a (tabular) description of all available probes in Z3."""
if in_html_mode(): if in_html_mode():
even = True even = True
print '<table border="1" cellpadding="2" cellspacing="0">' print('<table border="1" cellpadding="2" cellspacing="0">')
for p in probes(): for p in probes():
if even: if even:
print '<tr style="background-color:#CFCFCF">' print('<tr style="background-color:#CFCFCF">')
even = False even = False
else: else:
print '<tr>' print('<tr>')
even = True even = True
print '<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(probe_description(p), 40)) print('<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(probe_description(p), 40)))
print '</table>' print('</table>')
else: else:
for p in probes(): for p in probes():
print '%s : %s' % (p, probe_description(p)) print('%s : %s' % (p, probe_description(p)))
def _probe_nary(f, args, ctx): def _probe_nary(f, args, ctx):
if __debug__: if __debug__:
@ -6911,7 +6932,7 @@ def simplify(a, *arguments, **keywords):
def help_simplify(): def help_simplify():
"""Return a string describing all options available for Z3 `simplify` procedure.""" """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(): def simplify_param_descrs():
"""Return the set of parameter descriptions for Z3 `simplify` procedure.""" """Return the set of parameter descriptions for Z3 `simplify` procedure."""
@ -6934,7 +6955,7 @@ def substitute(t, *m):
m = _get_args(m1) m = _get_args(m1)
if __debug__: if __debug__:
_z3_assert(is_expr(t), "Z3 expression expected") _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) num = len(m)
_from = (Ast * num)() _from = (Ast * num)()
_to = (Ast * num)() _to = (Ast * num)()
@ -6956,7 +6977,7 @@ def substitute_vars(t, *m):
""" """
if __debug__: if __debug__:
_z3_assert(is_expr(t), "Z3 expression expected") _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) num = len(m)
_to = (Ast * num)() _to = (Ast * num)()
for i in range(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") _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
args = _coerce_expr_list(args, ctx) args = _coerce_expr_list(args, ctx)
if is_bv(args[0]): if is_bv(args[0]):
return reduce(lambda a, b: a + b, args, 0) return _reduce(lambda a, b: a + b, args, 0)
else: else:
_args, sz = _to_ast_array(args) _args, sz = _to_ast_array(args)
return ArithRef(Z3_mk_add(ctx.ref(), sz, _args), ctx) 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") _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression")
args = _coerce_expr_list(args, ctx) args = _coerce_expr_list(args, ctx)
if is_bv(args[0]): if is_bv(args[0]):
return reduce(lambda a, b: a * b, args, 1) return _reduce(lambda a, b: a * b, args, 1)
else: else:
_args, sz = _to_ast_array(args) _args, sz = _to_ast_array(args)
return ArithRef(Z3_mk_mul(ctx.ref(), sz, _args), ctx) return ArithRef(Z3_mk_mul(ctx.ref(), sz, _args), ctx)
@ -7028,18 +7049,18 @@ def solve(*args, **keywords):
s.set(**keywords) s.set(**keywords)
s.add(*args) s.add(*args)
if keywords.get('show', False): if keywords.get('show', False):
print s print(s)
r = s.check() r = s.check()
if r == unsat: if r == unsat:
print "no solution" print("no solution")
elif r == unknown: elif r == unknown:
print "failed to solve" print("failed to solve")
try: try:
print s.model() print(s.model())
except Z3Exception: except Z3Exception:
return return
else: else:
print s.model() print(s.model())
def solve_using(s, *args, **keywords): def solve_using(s, *args, **keywords):
"""Solve the constraints `*args` using solver `s`. """Solve the constraints `*args` using solver `s`.
@ -7054,21 +7075,21 @@ def solve_using(s, *args, **keywords):
s.set(**keywords) s.set(**keywords)
s.add(*args) s.add(*args)
if keywords.get('show', False): if keywords.get('show', False):
print "Problem:" print("Problem:")
print s print(s)
r = s.check() r = s.check()
if r == unsat: if r == unsat:
print "no solution" print("no solution")
elif r == unknown: elif r == unknown:
print "failed to solve" print("failed to solve")
try: try:
print s.model() print(s.model())
except Z3Exception: except Z3Exception:
return return
else: else:
if keywords.get('show', False): if keywords.get('show', False):
print "Solution:" print("Solution:")
print s.model() print(s.model())
def prove(claim, **keywords): def prove(claim, **keywords):
"""Try to prove the given claim. """Try to prove the given claim.
@ -7086,16 +7107,16 @@ def prove(claim, **keywords):
s.set(**keywords) s.set(**keywords)
s.add(Not(claim)) s.add(Not(claim))
if keywords.get('show', False): if keywords.get('show', False):
print s print(s)
r = s.check() r = s.check()
if r == unsat: if r == unsat:
print "proved" print("proved")
elif r == unknown: elif r == unknown:
print "failed to prove" print("failed to prove")
print s.model() print(s.model())
else: else:
print "counterexample" print("counterexample")
print s.model() print(s.model())
def _solve_html(*args, **keywords): def _solve_html(*args, **keywords):
"""Version of funcion `solve` used in RiSE4Fun.""" """Version of funcion `solve` used in RiSE4Fun."""
@ -7103,21 +7124,21 @@ def _solve_html(*args, **keywords):
s.set(**keywords) s.set(**keywords)
s.add(*args) s.add(*args)
if keywords.get('show', False): if keywords.get('show', False):
print "<b>Problem:</b>" print("<b>Problem:</b>")
print s print(s)
r = s.check() r = s.check()
if r == unsat: if r == unsat:
print "<b>no solution</b>" print("<b>no solution</b>")
elif r == unknown: elif r == unknown:
print "<b>failed to solve</b>" print("<b>failed to solve</b>")
try: try:
print s.model() print(s.model())
except Z3Exception: except Z3Exception:
return return
else: else:
if keywords.get('show', False): if keywords.get('show', False):
print "<b>Solution:</b>" print("<b>Solution:</b>")
print s.model() print(s.model())
def _solve_using_html(s, *args, **keywords): def _solve_using_html(s, *args, **keywords):
"""Version of funcion `solve_using` used in RiSE4Fun.""" """Version of funcion `solve_using` used in RiSE4Fun."""
@ -7126,21 +7147,21 @@ def _solve_using_html(s, *args, **keywords):
s.set(**keywords) s.set(**keywords)
s.add(*args) s.add(*args)
if keywords.get('show', False): if keywords.get('show', False):
print "<b>Problem:</b>" print("<b>Problem:</b>")
print s print(s)
r = s.check() r = s.check()
if r == unsat: if r == unsat:
print "<b>no solution</b>" print("<b>no solution</b>")
elif r == unknown: elif r == unknown:
print "<b>failed to solve</b>" print("<b>failed to solve</b>")
try: try:
print s.model() print(s.model())
except Z3Exception: except Z3Exception:
return return
else: else:
if keywords.get('show', False): if keywords.get('show', False):
print "<b>Solution:</b>" print("<b>Solution:</b>")
print s.model() print(s.model())
def _prove_html(claim, **keywords): def _prove_html(claim, **keywords):
"""Version of funcion `prove` used in RiSE4Fun.""" """Version of funcion `prove` used in RiSE4Fun."""
@ -7150,23 +7171,24 @@ def _prove_html(claim, **keywords):
s.set(**keywords) s.set(**keywords)
s.add(Not(claim)) s.add(Not(claim))
if keywords.get('show', False): if keywords.get('show', False):
print s print(s)
r = s.check() r = s.check()
if r == unsat: if r == unsat:
print "<b>proved</b>" print("<b>proved</b>")
elif r == unknown: elif r == unknown:
print "<b>failed to prove</b>" print("<b>failed to prove</b>")
print s.model() print(s.model())
else: else:
print "<b>counterexample</b>" print("<b>counterexample</b>")
print s.model() print(s.model())
def _dict2sarray(sorts, ctx): def _dict2sarray(sorts, ctx):
sz = len(sorts) sz = len(sorts)
_names = (Symbol * sz)() _names = (Symbol * sz)()
_sorts = (Sort * sz) () _sorts = (Sort * sz) ()
i = 0 i = 0
for k, v in sorts.iteritems(): for k in sorts:
v = sorts[k]
if __debug__: if __debug__:
_z3_assert(isinstance(k, str), "String expected") _z3_assert(isinstance(k, str), "String expected")
_z3_assert(is_sort(v), "Z3 sort expected") _z3_assert(is_sort(v), "Z3 sort expected")
@ -7180,7 +7202,8 @@ def _dict2darray(decls, ctx):
_names = (Symbol * sz)() _names = (Symbol * sz)()
_decls = (FuncDecl * sz) () _decls = (FuncDecl * sz) ()
i = 0 i = 0
for k, v in decls.iteritems(): for k in decls:
v = decls[k]
if __debug__: if __debug__:
_z3_assert(isinstance(k, str), "String expected") _z3_assert(isinstance(k, str), "String expected")
_z3_assert(is_func_decl(v) or is_const(v), "Z3 declaration or constant expected") _z3_assert(is_func_decl(v) or is_const(v), "Z3 declaration or constant expected")

59
src/api/python/z3printer.py
View file

@ -74,6 +74,15 @@ def _is_add(k):
def _is_sub(k): def _is_sub(k):
return k == Z3_OP_SUB or k == Z3_OP_BSUB 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 ] _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 = '...' _ellipses = '...'
@ -161,15 +170,19 @@ def _get_precedence(k):
return _z3_precedence.get(k, 100000) return _z3_precedence.get(k, 100000)
_z3_html_op_to_str = {} _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 _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_op_to_str[_k] = _v
_z3_html_precedence = {} _z3_html_precedence = {}
for _k, _v in _z3_precedence.iteritems(): for _k in _z3_precedence:
_v = _z3_precedence[_k]
_z3_html_precedence[_k] = _v _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 _z3_html_precedence[_k] = _v
_html_infix_map = {} _html_infix_map = {}
@ -237,7 +250,7 @@ class FormatObject:
class NAryFormatObject(FormatObject): class NAryFormatObject(FormatObject):
def __init__(self, fs): 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 self.children = fs
def children(self): def children(self):
return self.children return self.children
@ -246,7 +259,7 @@ class ComposeFormatObject(NAryFormatObject):
def is_compose(sef): def is_compose(sef):
return True return True
def as_tuple(self): 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): def space_upto_nl(self):
r = 0 r = 0
for child in self.children: for child in self.children:
@ -256,13 +269,13 @@ class ComposeFormatObject(NAryFormatObject):
return (r, True) return (r, True)
return (r, False) return (r, False)
def flat(self): def flat(self):
return compose(map(lambda a: a.flat(), self.children)) return compose([a.flat() for a in self.children ])
class ChoiceFormatObject(NAryFormatObject): class ChoiceFormatObject(NAryFormatObject):
def is_choice(sef): def is_choice(sef):
return True return True
def as_tuple(self): 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): def space_upto_nl(self):
return self.children[0].space_upto_nl() return self.children[0].space_upto_nl()
def flat(self): def flat(self):
@ -388,11 +401,11 @@ class PP:
if not self.bounded or self.pos <= self.max_width: if not self.bounded or self.pos <= self.max_width:
sz = _len(f) sz = _len(f)
if self.bounded and self.pos + sz > self.max_width: if self.bounded and self.pos + sz > self.max_width:
self.out.write(_ellipses) self.out.write(u(_ellipses))
else: else:
self.pos = self.pos + sz self.pos = self.pos + sz
self.ribbon_pos = self.ribbon_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): def pp_compose(self, f, indent):
for c in f.children: for c in f.children:
@ -410,11 +423,11 @@ class PP:
self.ribbon_pos = 0 self.ribbon_pos = 0
self.line = self.line + 1 self.line = self.line + 1
if self.line < self.max_lines: if self.line < self.max_lines:
self.out.write(unicode('\n')) self.out.write(u('\n'))
for i in range(indent): for i in range(indent):
self.out.write(unicode(' ')) self.out.write(u(' '))
else: else:
self.out.write(unicode('\n...')) self.out.write(u('\n...'))
raise StopPPException() raise StopPPException()
def pp(self, f, indent): def pp(self, f, indent):
@ -957,23 +970,23 @@ def in_html_mode():
def pp(a): def pp(a):
if _support_pp(a): if _support_pp(a):
print obj_to_string(a) print(obj_to_string(a))
else: else:
print a print(a)
def print_matrix(m): def print_matrix(m):
z3._z3_assert(isinstance(m, list) or isinstance(m, tuple), "matrix expected") z3._z3_assert(isinstance(m, list) or isinstance(m, tuple), "matrix expected")
if not in_html_mode(): if not in_html_mode():
print obj_to_string(m) print(obj_to_string(m))
else: else:
print '<table cellpadding="2", cellspacing="0", border="1">' print('<table cellpadding="2", cellspacing="0", border="1">')
for r in m: for r in m:
z3._z3_assert(isinstance(r, list) or isinstance(r, tuple), "matrix expected") z3._z3_assert(isinstance(r, list) or isinstance(r, tuple), "matrix expected")
print '<tr>' print('<tr>')
for c in r: for c in r:
print '<td>%s</td>' % c print('<td>%s</td>' % c)
print '</tr>' print('</tr>')
print '</table>' print('</table>')
def insert_line_breaks(s, width): def insert_line_breaks(s, width):
"""Break s in lines of size width (approx)""" """Break s in lines of size width (approx)"""
@ -984,9 +997,9 @@ def insert_line_breaks(s, width):
w = 0 w = 0
for i in range(sz): for i in range(sz):
if w > width and s[i] == ' ': if w > width and s[i] == ' ':
new_str.write(u'<br />') new_str.write(u('<br />'))
w = 0 w = 0
else: else:
new_str.write(unicode(s[i])) new_str.write(u(s[i]))
w = w + 1 w = w + 1
return new_str.getvalue() return new_str.getvalue()