mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
fixed problem reported by Dejan
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
60b9207485
commit
44ae1a2d70
5
README
5
README
|
@ -20,9 +20,10 @@ Execute:
|
||||||
It will install z3 executable at /usr/bin, libraries at /usr/lib, and include files at /usr/include.
|
It will install z3 executable at /usr/bin, libraries at /usr/lib, and include files at /usr/include.
|
||||||
You can change the installation p
|
You can change the installation p
|
||||||
|
|
||||||
Use the following commands to install in a different prefix (e.g., /home/leo).
|
Use the following commands to install in a different prefix (e.g., /home/leo), and the Z3 python
|
||||||
|
bindings in a different python package directory.
|
||||||
|
|
||||||
python scripts/mk_make.py --prefix=/home/leo
|
python scripts/mk_make.py --prefix=/home/leo --pydir=/home/leo/python
|
||||||
cd build
|
cd build
|
||||||
make
|
make
|
||||||
sudo make install
|
sudo make install
|
||||||
|
|
|
@ -3,6 +3,8 @@ RELEASE NOTES
|
||||||
Version 4.3.2
|
Version 4.3.2
|
||||||
=============
|
=============
|
||||||
|
|
||||||
|
- New parameter setting infrastructure. Now, it is possible to set parameter for Z3 internal modules. Several parameter names changed. Execute `z3 -p` for the new parameter list.
|
||||||
|
|
||||||
- Added get_version() and get_version_string() to Z3Py
|
- Added get_version() and get_version_string() to Z3Py
|
||||||
|
|
||||||
- Added support for FreeBSD. Z3 can be compiled on FreeBSD using g++.
|
- Added support for FreeBSD. Z3 can be compiled on FreeBSD using g++.
|
||||||
|
@ -20,6 +22,8 @@ Version 4.3.2
|
||||||
|
|
||||||
- Fixed crash when parsing incorrect formulas. The crash was introduced when support for "arithmetic coercions" was added in Z3 4.3.0.
|
- Fixed crash when parsing incorrect formulas. The crash was introduced when support for "arithmetic coercions" was added in Z3 4.3.0.
|
||||||
|
|
||||||
|
- Added new option to mk_make to allow users to specify where python bindings (Z3Py) will be installed. (Thanks to Dejan Jovanovic for reporting the problem).
|
||||||
|
|
||||||
Version 4.3.1
|
Version 4.3.1
|
||||||
=============
|
=============
|
||||||
|
|
||||||
|
|
|
@ -341,6 +341,7 @@ def display_help(exit_code):
|
||||||
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 " -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."
|
||||||
|
@ -371,52 +372,56 @@ def display_help(exit_code):
|
||||||
# Parse configuration option for mk_make script
|
# Parse configuration option for mk_make script
|
||||||
def parse_options():
|
def parse_options():
|
||||||
global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE
|
global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE
|
||||||
global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP
|
global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, PYTHON_PACKAGE_DIR
|
||||||
try:
|
try:
|
||||||
options, remainder = getopt.gnu_getopt(sys.argv[1:],
|
options, remainder = getopt.gnu_getopt(sys.argv[1:],
|
||||||
'b:dsxhmcvtnp:gj',
|
'b:dsxhmcvtnp:gjy:',
|
||||||
['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
|
['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
|
||||||
'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'java'])
|
'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'java', 'pydir='])
|
||||||
for opt, arg in options:
|
|
||||||
if opt in ('-b', '--build'):
|
|
||||||
if arg == 'src':
|
|
||||||
raise MKException('The src directory should not be used to host the Makefile')
|
|
||||||
set_build_dir(arg)
|
|
||||||
elif opt in ('-s', '--silent'):
|
|
||||||
VERBOSE = False
|
|
||||||
elif opt in ('-d', '--debug'):
|
|
||||||
DEBUG_MODE = True
|
|
||||||
elif opt in ('-x', '--x64'):
|
|
||||||
if not IS_WINDOWS:
|
|
||||||
raise MKException('x64 compilation mode can only be specified when using Visual Studio')
|
|
||||||
VS_X64 = True
|
|
||||||
elif opt in ('-h', '--help'):
|
|
||||||
display_help(0)
|
|
||||||
elif opt in ('-m', '--onlymakefiles'):
|
|
||||||
ONLY_MAKEFILES = True
|
|
||||||
elif opt in ('-c', '--showcpp'):
|
|
||||||
SHOW_CPPS = True
|
|
||||||
elif opt in ('-v', '--vsproj'):
|
|
||||||
VS_PROJ = True
|
|
||||||
elif opt in ('-t', '--trace'):
|
|
||||||
TRACE = True
|
|
||||||
elif opt in ('-n', '--nodotnet'):
|
|
||||||
DOTNET_ENABLED = False
|
|
||||||
elif opt in ('--staticlib'):
|
|
||||||
STATIC_LIB = True
|
|
||||||
elif opt in ('-p', '--prefix'):
|
|
||||||
PREFIX = arg
|
|
||||||
elif opt in ('-g', '--gmp'):
|
|
||||||
GMP = True
|
|
||||||
elif opt in ('-j', '--java'):
|
|
||||||
JAVA_ENABLED = True
|
|
||||||
else:
|
|
||||||
print "ERROR: Invalid command line option '%s'" % opt
|
|
||||||
display_help(1)
|
|
||||||
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:
|
||||||
|
if opt in ('-b', '--build'):
|
||||||
|
if arg == 'src':
|
||||||
|
raise MKException('The src directory should not be used to host the Makefile')
|
||||||
|
set_build_dir(arg)
|
||||||
|
elif opt in ('-s', '--silent'):
|
||||||
|
VERBOSE = False
|
||||||
|
elif opt in ('-d', '--debug'):
|
||||||
|
DEBUG_MODE = True
|
||||||
|
elif opt in ('-x', '--x64'):
|
||||||
|
if not IS_WINDOWS:
|
||||||
|
raise MKException('x64 compilation mode can only be specified when using Visual Studio')
|
||||||
|
VS_X64 = True
|
||||||
|
elif opt in ('-h', '--help'):
|
||||||
|
display_help(0)
|
||||||
|
elif opt in ('-m', '--onlymakefiles'):
|
||||||
|
ONLY_MAKEFILES = True
|
||||||
|
elif opt in ('-c', '--showcpp'):
|
||||||
|
SHOW_CPPS = True
|
||||||
|
elif opt in ('-v', '--vsproj'):
|
||||||
|
VS_PROJ = True
|
||||||
|
elif opt in ('-t', '--trace'):
|
||||||
|
TRACE = True
|
||||||
|
elif opt in ('-n', '--nodotnet'):
|
||||||
|
DOTNET_ENABLED = False
|
||||||
|
elif opt in ('--staticlib'):
|
||||||
|
STATIC_LIB = True
|
||||||
|
elif opt in ('-p', '--prefix'):
|
||||||
|
PREFIX = arg
|
||||||
|
elif opt in ('-y', '--pydir'):
|
||||||
|
PYTHON_PACKAGE_DIR = arg
|
||||||
|
mk_dir(PYTHON_PACKAGE_DIR)
|
||||||
|
elif opt in ('-g', '--gmp'):
|
||||||
|
GMP = True
|
||||||
|
elif opt in ('-j', '--java'):
|
||||||
|
JAVA_ENABLED = True
|
||||||
|
else:
|
||||||
|
print "ERROR: Invalid command line option '%s'" % opt
|
||||||
|
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
|
||||||
# the given C/C++ file named fname.
|
# the given C/C++ file named fname.
|
||||||
def extract_c_includes(fname):
|
def extract_c_includes(fname):
|
||||||
|
|
Loading…
Reference in a new issue