mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 11:55:51 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2012-11-17 18:03:46 -08:00
commit 39e6453f4a
31 changed files with 272 additions and 749 deletions
Download patch file Download diff file Expand all files Collapse all files

2
README
View file

@ -40,7 +40,7 @@ Remark: clang does not support OpenMP yet.
autoconf
./configure CXX=clang++
python scripts/mk_make.py --noomp
python scripts/mk_make.py
cd build
make

7
RELEASE_NOTES
View file

@ -1,10 +1,17 @@
RELEASE NOTES
Version 4.3.2
=============
- Added get_version() and get_version_string() to Z3Py
Version 4.3.1
=============
- Added support for compiling Z3 using clang++ on Linux and OSX
- Added missing compilation option (-D _EXTERNAL_RELEASE) in release mode.
Version 4.3.0
=============

48
configure.ac
View file

@ -83,7 +83,7 @@ fi
###################
# Sets CXX
AC_LANG([C++])
AC_PROG_CXX(g++ false)
AC_PROG_CXX(g++ clang++ false)
AC_PROG_CC
if test $CXX = "false"; then
AC_MSG_ERROR([C++ compiler was not found])
@ -99,8 +99,21 @@ AC_PROG_GREP
# Sets SED
AC_PROG_SED
# Sets OPENMP_CFLAGS
m4_ifdef([AC_OPENMP], [AC_OPENMP])
AS_IF([test "$CXX" = "g++"], [
# Enable OpenMP
CXXFLAGS+=" -fopenmp"
LDFLAGS+=" -fopenmp"
SLIBEXTRAFLAGS+=" -fopenmp"
# Use -mfpmath=sse
CXXFLAGS+=" -mfpmath=sse"
],
[test "$CXX" = "clang++"], [
# OpenMP is not supported in clang++
CXXFLAGS+=" -D _NO_OMP_"
],
[
AC_MSG_ERROR([Unsupported compiler: $CXX])
])
AR=ar
AC_SUBST(AR)
@ -115,30 +128,26 @@ host_os=`uname -s`
AS_IF([test "$host_os" = "Darwin"], [
PLATFORM=osx
SO_EXT=.dylib
LDFLAGS=
SLIBFLAGS="-dynamiclib"
SLIBEXTRAFLAGS=""
SLIBFLAGS+="-dynamiclib"
COMP_VERSIONS="-compatibility_version \$(Z3_VERSION) -current_version \$(Z3_VERSION)"
STATIC_FLAGS=
], [test "$host_os" = "Linux"], [
PLATFORM=linux
SO_EXT=.so
LDFLAGS=-lrt
SLIBFLAGS="-shared"
SLIBEXTRAFLAGS=
LDFLAGS+=" -lrt"
SLIBFLAGS+=" -shared"
COMP_VERSIONS=
STATIC_FLAGS=-static
CXXFLAGS+=" -fno-strict-aliasing"
if test "$CXX" = "clang++"; then
# More flags for clang++ for Linux
CXXFLAGS+=" -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value"
SLIBEXTRAFLAGS+=" -lrt"
fi
SLIBEXTRAFLAGS+=" -lrt"
], [test "${host_os:0:6}" = "CYGWIN"], [
PLATFORM=win
SO_EXT=.dll
LDFLAGS=
SLIBFLAGS="-shared"
SLIBEXTRAFLAGS=
SLIBFLAGS+="-shared"
COMP_VERSIONS=
CXXFLAGS+=" -D_CYGWIN -fno-strict-aliasing"
],
@ -146,11 +155,6 @@ AS_IF([test "$host_os" = "Darwin"], [
AC_MSG_ERROR([Unknown host platform: $host_os])
])
# Only add -mfpmath=sse if g++
if test "$CXX" = "g++"; then
CXXFLAGS+=" -mfpmath=sse"
fi
AC_SUBST(SLIBFLAGS)
AC_SUBST(LDFLAGS)
AC_SUBST(SLIBEXTRAFLAGS)
@ -189,22 +193,18 @@ AC_OUTPUT(scripts/config-debug.mk scripts/config-release.mk)
#
###################
MKMAKE_OPT=
if test "$CXX" = "clang++"; then
MKMAKE_OPT="--noomp"
fi
# Python is available, give user the option to generate the make files wherever they want
cat <<EOF
Z3 was configured with success.
Host platform: $PLATFORM
Compiler: $CXX
Arithmetic: $ARITH
Python: $PYTHON
Prefix: $prefix
64-bit: $IS_X64
To build and install Z3, execute:
python scripts/mk_make.py $MKMAKE_OPT
python scripts/mk_make.py
cd build
make
sudo make install

2
scripts/config-release.mk.in
View file

@ -1,7 +1,7 @@
CC=@CC@
PREFIX=@prefix@
CXX=@CXX@
CXXFLAGS=@CPPFLAGS@ @CXXFLAGS@ -c -O3 -fomit-frame-pointer -msse -msse2
CXXFLAGS=@CPPFLAGS@ @CXXFLAGS@ -c -O3 -D _EXTERNAL_RELEASE -fomit-frame-pointer -msse -msse2
CXX_OUT_FLAG=-o
OBJ_EXT=.o
LIB_EXT=.a

2
scripts/config-vs-debug-x64.mk
View file

@ -1,6 +1,6 @@
CC=cl
CXX=cl
CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-
CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-
CXX_OUT_FLAG=/Fo
OBJ_EXT=.obj
LIB_EXT=.lib

2
scripts/config-vs-debug.mk
View file

@ -1,6 +1,6 @@
CC=cl
CXX=cl
CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2
CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2
CXX_OUT_FLAG=/Fo
OBJ_EXT=.obj
LIB_EXT=.lib

2
scripts/config-vs-release-x64.mk
View file

@ -1,6 +1,6 @@
CC=cl
CXX=cl
CXXFLAGS=/c /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP
CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP
CXX_OUT_FLAG=/Fo
OBJ_EXT=.obj
LIB_EXT=.lib

2
scripts/config-vs-release.mk
View file

@ -1,6 +1,6 @@
CC=cl
CXX=cl
CXXFLAGS=/nologo /c /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2
CXXFLAGS=/nologo /c /Zi /openmp /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2
CXX_OUT_FLAG=/Fo
OBJ_EXT=.obj
LIB_EXT=.lib

3
scripts/mk_project.py
View file

@ -9,7 +9,7 @@ from mk_util import *
# Z3 Project definition
def init_project_def():
set_version(4, 3, 1, 0)
set_version(4, 3, 2, 0)
add_lib('util', [])
add_lib('polynomial', ['util'], 'math/polynomial')
add_lib('sat', ['util'])
@ -68,6 +68,7 @@ def init_project_def():
add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll',
reexports=['api'],
dll_name='libz3',
static=build_static_lib(),
export_files=API_files)
add_dot_net_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties')
add_hlib('cpp', 'api/c++', includes2install=['z3++.h'])

169
scripts/mk_util.py
View file

@ -40,7 +40,7 @@ Z3PY_SRC_DIR=None
VS_PROJ = False
TRACE = False
DOTNET_ENABLED=False
OMP = True
STATIC_LIB=False
VER_MAJOR=None
VER_MINOR=None
@ -57,6 +57,9 @@ def set_version(major, minor, build, revision):
def get_version():
return (VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION)
def build_static_lib():
return STATIC_LIB
def is_cr_lf(fname):
# Check whether text files use cr/lf
f = open(fname, 'r')
@ -121,12 +124,12 @@ def display_help():
print " -v, --vsproj generate Visual Studio Project Files."
print " -t, --trace enable tracing in release mode."
print " -n, --nodotnet do not generate Microsoft.Z3.dll make rules."
print " --noomp disable support for openmp."
print " --staticlib build Z3 static library."
exit(0)
# Parse configuration option for mk_make script
def parse_options():
global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, DOTNET_ENABLED, OMP
global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, DOTNET_ENABLED, STATIC_LIB
options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:dsxhmcvtn', ['build=',
'debug',
'silent',
@ -137,7 +140,7 @@ def parse_options():
'vsproj',
'trace',
'nodotnet',
'noomp'
'staticlib'
])
for opt, arg in options:
if opt in ('-b', '--build'):
@ -164,8 +167,8 @@ def parse_options():
TRACE = True
elif opt in ('-n', '--nodotnet'):
DOTNET_ENABLED = False
elif opt in ('--noomp'):
OMP = False
elif opt in ('--staticlib'):
STATIC_LIB = True
else:
raise MKException("Invalid command line option '%s'" % opt)
@ -347,17 +350,6 @@ class Component:
extra_opt = '/D _TRACE'
else:
extra_opt = '-D _TRACE'
if not OMP:
if IS_WINDOWS:
extra_opt = '%s /D _NO_OMP_' % extra_opt
else:
extra_opt = '%s -D _NO_OMP_' % extra_opt
else:
if IS_WINDOWS:
extra_opt = '%s /openmp' % extra_opt
else:
extra_opt = '%s -fopenmp' % extra_opt
out.write('\t@$(CXX) $(CXXFLAGS) %s $(%s) $(CXX_OUT_FLAG)%s %s\n' % (extra_opt, include_defs, objfile, srcfile))
def mk_makefile(self, out):
@ -386,6 +378,10 @@ class Component:
def require_def_file(self):
return False
# Return true if the component needs builder to generate a mem_initializer.cpp file with mem_initialize() and mem_finalize() functions.
def require_mem_initializer(self):
return False
def mk_install(self, out):
return
@ -492,15 +488,15 @@ class ExeComponent(Component):
for dep in deps:
c_dep = get_component(dep)
out.write(' %s/%s$(LIB_EXT)' % (c_dep.build_dir, c_dep.name))
extra_flags = ''
if OMP and not IS_WINDOWS:
extra_flags = '-fopenmp'
out.write(' $(LINK_EXTRA_FLAGS) %s\n' % extra_flags)
out.write(' $(LINK_EXTRA_FLAGS)\n')
out.write('%s: %s\n\n' % (self.name, exefile))
def require_install_tactics(self):
return ('tactic' in self.deps) and ('cmd_context' in self.deps)
def require_mem_initializer(self):
return True
# All executables are included in the all: rule
def main_component(self):
return True
@ -511,9 +507,8 @@ class ExeComponent(Component):
out.write('\t@cp %s $(PREFIX)/bin/%s\n' % (exefile, exefile))
def mk_uninstall(self, out):
if self.install:
exefile = '%s$(EXE_EXT)' % self.exe_name
out.write('\t@rm -f $(PREFIX)/bin/%s\n' % exefile)
exefile = '%s$(EXE_EXT)' % self.exe_name
out.write('\t@rm -f $(PREFIX)/bin/%s\n' % exefile)
def mk_win_dist(self, build_path, dist_path):
if self.install:
@ -530,7 +525,7 @@ class ExtraExeComponent(ExeComponent):
return False
class DLLComponent(Component):
def __init__(self, name, dll_name, path, deps, export_files, reexports, install):
def __init__(self, name, dll_name, path, deps, export_files, reexports, install, static):
Component.__init__(self, name, path, deps)
if dll_name == None:
dll_name = name
@ -538,6 +533,7 @@ class DLLComponent(Component):
self.export_files = export_files
self.reexports = reexports
self.install = install
self.static = static
def mk_makefile(self, out):
Component.mk_makefile(self, out)
@ -571,22 +567,50 @@ class DLLComponent(Component):
if not dep in self.reexports:
c_dep = get_component(dep)
out.write(' %s/%s$(LIB_EXT)' % (c_dep.build_dir, c_dep.name))
extra_flags= ''
if OMP and not IS_WINDOWS:
extra_flags = '-fopenmp'
out.write(' $(SLINK_EXTRA_FLAGS) %s' % extra_flags)
out.write(' $(SLINK_EXTRA_FLAGS)')
if IS_WINDOWS:
out.write(' /DEF:%s/%s.def' % (self.to_src_dir, self.name))
out.write('\n')
out.write('%s: %s\n\n' % (self.name, dllfile))
if self.static:
self.mk_static(out)
libfile = '%s$(LIB_EXT)' % self.dll_name
out.write('%s: %s %s\n\n' % (self.name, dllfile, libfile))
else:
out.write('%s: %s\n\n' % (self.name, dllfile))
# All DLLs are included in the all: rule
def mk_static(self, out):
# generate rule for lib
objs = []
for cppfile in get_cpp_files(self.src_dir):
objfile = '%s/%s$(OBJ_EXT)' % (self.build_dir, os.path.splitext(cppfile)[0])
objs.append(objfile)
# we have to "reexport" all object files
for dep in self.deps:
dep = get_component(dep)
for cppfile in get_cpp_files(dep.src_dir):
objfile = '%s/%s$(OBJ_EXT)' % (dep.build_dir, os.path.splitext(cppfile)[0])
objs.append(objfile)
libfile = '%s$(LIB_EXT)' % self.dll_name
out.write('%s:' % libfile)
for obj in objs:
out.write(' ')
out.write(obj)
out.write('\n')
out.write('\t@$(AR) $(AR_FLAGS) $(AR_OUTFLAG)%s' % libfile)
for obj in objs:
out.write(' ')
out.write(obj)
out.write('\n')
def main_component(self):
return True
return self.install
def require_install_tactics(self):
return ('tactic' in self.deps) and ('cmd_context' in self.deps)
def require_mem_initializer(self):
return True
def require_def_file(self):
return IS_WINDOWS and self.export_files
@ -595,18 +619,27 @@ class DLLComponent(Component):
dllfile = '%s$(SO_EXT)' % self.dll_name
out.write('\t@cp %s $(PREFIX)/lib/%s\n' % (dllfile, dllfile))
out.write('\t@cp %s %s/%s\n' % (dllfile, PYTHON_PACKAGE_DIR, dllfile))
if self.static:
libfile = '%s$(LIB_EXT)' % self.dll_name
out.write('\t@cp %s $(PREFIX)/lib/%s\n' % (libfile, libfile))
def mk_uninstall(self, out):
if self.install:
dllfile = '%s$(SO_EXT)' % self.dll_name
out.write('\t@rm -f $(PREFIX)/lib/%s\n' % dllfile)
out.write('\t@rm -f %s/%s\n' % (PYTHON_PACKAGE_DIR, dllfile))
dllfile = '%s$(SO_EXT)' % self.dll_name
out.write('\t@rm -f $(PREFIX)/lib/%s\n' % dllfile)
out.write('\t@rm -f %s/%s\n' % (PYTHON_PACKAGE_DIR, dllfile))
libfile = '%s$(LIB_EXT)' % self.dll_name
out.write('\t@rm -f $(PREFIX)/lib/%s\n' % libfile)
def mk_win_dist(self, build_path, dist_path):
if self.install:
mk_dir('%s/bin' % dist_path)
shutil.copy('%s/%s.dll' % (build_path, self.dll_name),
'%s/bin/%s.dll' % (dist_path, self.dll_name))
if self.static:
mk_dir('%s/bin' % dist_path)
shutil.copy('%s/%s.lib' % (build_path, self.dll_name),
'%s/bin/%s.lib' % (dist_path, self.dll_name))
class DotNetDLLComponent(Component):
def __init__(self, name, dll_name, path, deps, assembly_info_dir):
@ -701,10 +734,7 @@ class CppExampleComponent(ExampleComponent):
out.write('%s.lib' % dll_name)
else:
out.write(dll)
extra_flags = ''
if OMP and not IS_WINDOWS:
extra_flags = '-fopenmp'
out.write(' $(LINK_EXTRA_FLAGS) %s\n' % extra_flags)
out.write(' $(LINK_EXTRA_FLAGS)\n')
out.write('_ex_%s: %s\n\n' % (self.name, exefile))
class CExampleComponent(CppExampleComponent):
@ -788,8 +818,8 @@ def add_extra_exe(name, deps=[], path=None, exe_name=None, install=True):
c = ExtraExeComponent(name, exe_name, path, deps, install)
reg_component(name, c)
def add_dll(name, deps=[], path=None, dll_name=None, export_files=[], reexports=[], install=True):
c = DLLComponent(name, dll_name, path, deps, export_files, reexports, install)
def add_dll(name, deps=[], path=None, dll_name=None, export_files=[], reexports=[], install=True, static=False):
c = DLLComponent(name, dll_name, path, deps, export_files, reexports, install, static)
reg_component(name, c)
def add_dot_net_dll(name, deps=[], path=None, dll_name=None, assembly_info_dir=None):
@ -907,6 +937,7 @@ def mk_auto_src():
if not ONLY_MAKEFILES:
mk_pat_db()
mk_all_install_tactic_cpps()
mk_all_mem_initializer_cpps()
# TODO: delete after src/ast/pattern/expr_pattern_match
# database.smt ==> database.h
@ -1079,6 +1110,60 @@ def mk_all_install_tactic_cpps():
cnames.append(c.name)
mk_install_tactic_cpp(cnames, c.src_dir)
# Generate an mem_initializer.cpp at path.
# This file implements the procedures
# void mem_initialize()
# void mem_finalize()
# This procedures are invoked by the Z3 memory_manager
def mk_mem_initializer_cpp(cnames, path):
initializer_cmds = []
finalizer_cmds = []
fullname = '%s/mem_initializer.cpp' % path
fout = open(fullname, 'w')
fout.write('// Automatically generated file.\n')
initializer_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)')
finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)')
for cname in cnames:
c = get_component(cname)
h_files = filter(lambda f: f.endswith('.h'), os.listdir(c.src_dir))
for h_file in h_files:
added_include = False
fin = open("%s/%s" % (c.src_dir, h_file), 'r')
for line in fin:
m = initializer_pat.match(line)
if m:
if not added_include:
added_include = True
fout.write('#include"%s"\n' % h_file)
initializer_cmds.append(m.group(1))
m = finalizer_pat.match(line)
if m:
if not added_include:
added_include = True
fout.write('#include"%s"\n' % h_file)
finalizer_cmds.append(m.group(1))
fout.write('void mem_initialize() {\n')
for cmd in initializer_cmds:
fout.write(cmd)
fout.write('\n')
fout.write('}\n')
fout.write('void mem_finalize() {\n')
for cmd in finalizer_cmds:
fout.write(cmd)
fout.write('\n')
fout.write('}\n')
if VERBOSE:
print "Generated '%s'" % fullname
def mk_all_mem_initializer_cpps():
if not ONLY_MAKEFILES:
for c in get_components():
if c.require_mem_initializer():
cnames = []
cnames.extend(c.deps)
cnames.append(c.name)
mk_mem_initializer_cpp(cnames, c.src_dir)
# Generate a .def based on the files at c.export_files slot.
def mk_def_file(c):
pat1 = re.compile(".*Z3_API.*")

4
src/api/dotnet/Properties/AssemblyInfo.cs
View file

@ -34,6 +34,6 @@ using System.Security.Permissions;
// You can specify all the values or you can default the Build and Revision Numbers
// by using the '*' as shown below:
// [assembly: AssemblyVersion("4.2.0.0")]
[assembly: AssemblyVersion("4.3.1.0")]
[assembly: AssemblyFileVersion("4.3.1.0")]
[assembly: AssemblyVersion("4.3.2.0")]
[assembly: AssemblyFileVersion("4.3.2.0")]

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

@ -49,6 +49,22 @@ def enable_trace(msg):
def disable_trace(msg):
Z3_disable_trace(msg)
def get_version_string():
major = ctypes.c_uint(0)
minor = ctypes.c_uint(0)
build = ctypes.c_uint(0)
rev = ctypes.c_uint(0)
Z3_get_version(major, minor, build, rev)
return "%s.%s.%s" % (major.value, minor.value, build.value)
def get_version():
major = ctypes.c_uint(0)
minor = ctypes.c_uint(0)
build = ctypes.c_uint(0)
rev = ctypes.c_uint(0)
Z3_get_version(major, minor, build, rev)
return (major.value, minor.value, build.value, rev.value)
# We use _z3_assert instead of the assert command because we want to
# produce nice error messages in Z3Py at rise4fun.com
def _z3_assert(cond, msg):

516
src/ast/ast_pp.cpp
View file

@ -1,516 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
ast_pp.cpp
Abstract:
Expression DAG pretty printer
Author:
Leonardo de Moura 2008-01-20.
Revision History:
--*/
#include"ast_pp.h"
#include"pp.h"
#include"obj_pair_hashtable.h"
#include"ast_ll_pp.h"
#include"arith_decl_plugin.h"
#include"bv_decl_plugin.h"
#include"datatype_decl_plugin.h"
#include"dl_decl_plugin.h"
#include"ast_list.h"
#include<sstream>
using namespace format_ns;
mk_pp::mk_pp(ast * a, ast_manager & m, pp_params const & p, unsigned indent, unsigned num_var_names, char const * const * var_names):
m_ast(a),
m_manager(m),
m_params(p),
m_indent(indent),
m_num_var_names(num_var_names),
m_var_names(var_names) {
}
mk_pp::mk_pp(ast * a, ast_manager & m, unsigned indent, unsigned num_var_names, char const * const * var_names):
m_ast(a),
m_manager(m),
m_params(get_pp_default_params()),
m_indent(indent),
m_num_var_names(num_var_names),
m_var_names(var_names) {
}
std::ostream & ast_pp(std::ostream & strm, ast * n, ast_manager & m) {
return ast_pp(strm, n, m, get_pp_default_params());
}
struct pp_cache {
typedef obj_pair_map<ast, quantifier_list, format *> cache;
ast_manager & m_manager;
cache m_cache;
pp_cache(ast_manager & m):
m_manager(m) {
}
~pp_cache() {
reset();
}
bool contains(ast * k1, quantifier_list * k2) const { return m_cache.contains(k1, k2); }
void get(ast * k1, quantifier_list * k2, format * & r) const { m_cache.find(k1, k2, r); }
void insert(ast * k1, quantifier_list * k2, format * f) {
SASSERT(!m_cache.contains(k1, k2));
fm(m_manager).inc_ref(f);
m_cache.insert(k1, k2, f);
}
void reset() {
cache::iterator it = m_cache.begin();
cache::iterator end = m_cache.end();
for (; it != end; ++it) {
format * f = (*it).get_value();
fm(m_manager).dec_ref(f);
}
m_cache.reset();
}
};
class formatter {
typedef quantifier_list_manager qlist_manager;
typedef quantifier_list_ref qlist_ref;
typedef quantifier_list_ref_vector qlist_ref_vector;
pp_params const & m_params;
ast_manager & m_manager;
qlist_manager m_qlist_manager;
pp_cache m_cache;
typedef std::pair<ast*, quantifier_list*> pp_entry;
svector<pp_entry> m_todo;
qlist_ref_vector m_qlists;
app_ref m_nil;
arith_util m_autil;
bv_util m_bvutil;
datatype_util m_datatype_util;
datalog::dl_decl_util m_dl_util;
ptr_vector<sort> m_datatypes;
app_ref_vector m_format_trail;
ast_mark m_visited_datatypes;
unsigned m_num_var_names;
char const * const * m_var_names;
struct symbol2format {
ast_manager & m_manager;
symbol2format(ast_manager & m):m_manager(m) {}
format * operator()(symbol const & s) {
std::string str = s.str();
return mk_string(m_manager, str.c_str());
}
};
format * get_cached(ast * n, quantifier_list * qlist) {
format * f = 0;
if (is_sort(n)) {
qlist = m_qlist_manager.mk_nil();
}
m_cache.get(n, qlist, f);
SASSERT(f);
return f;
}
void visit(ast * n, quantifier_list * qlist, bool & visited) {
if (is_sort(n)) {
qlist = m_qlist_manager.mk_nil();
}
if (!m_cache.contains(n, qlist)) {
m_todo.push_back(pp_entry(n, qlist));
visited = false;
}
}
bool visit_children(ast * n, quantifier_list * qlist) {
unsigned j;
bool visited = true;
switch (n->get_kind()) {
case AST_FUNC_DECL: {
func_decl* f = to_func_decl(n);
j = f->get_arity();
while (j > 0) {
--j;
visit(f->get_domain(j), qlist, visited);
}
visit(f->get_range(), qlist, visited);
j = f->get_num_parameters();
while (j > 0) {
--j;
parameter p(f->get_parameter(j));
if (p.is_ast()) {
visit(p.get_ast(), qlist, visited);
}
}
break;
}
case AST_SORT: {
sort* s = to_sort(n);
j = s->get_num_parameters();
while (j > 0) {
--j;
parameter p(s->get_parameter(j));
if (p.is_ast()) {
visit(p.get_ast(), qlist, visited);
}
}
break;
}
case AST_APP: {
app* a = to_app(n);
j = a->get_num_args();
while (j > 0) {
--j;
visit(a->get_arg(j), qlist, visited);
}
visit(a->get_decl(), qlist, visited);
break;
}
case AST_QUANTIFIER:
j = to_quantifier(n)->get_num_patterns();
qlist = m_qlist_manager.mk_cons(to_quantifier(n), qlist);
m_qlists.push_back(qlist);
while (j > 0) {
--j;
visit(to_quantifier(n)->get_pattern(j), qlist, visited);
}
j = to_quantifier(n)->get_num_no_patterns();
while (j > 0) {
--j;
visit(to_quantifier(n)->get_no_pattern(j), qlist, visited);
}
j = to_quantifier(n)->get_num_decls();
while (j > 0) {
--j;
visit(to_quantifier(n)->get_decl_sort(j), qlist, visited);
visit_sort(to_quantifier(n)->get_decl_sort(j));
}
visit(to_quantifier(n)->get_expr(), qlist, visited);
break;
default:
break;
}
return visited;
}
void reduce1(ast * n, quantifier_list * qlist) {
format * r;
switch(n->get_kind()) {
case AST_APP:
r = reduce1_app(to_app(n), qlist);
break;
case AST_VAR:
r = reduce1_var(to_var(n), qlist);
break;
case AST_QUANTIFIER:
r = reduce1_quantifier(to_quantifier(n), qlist);
break;
case AST_SORT:
r = reduce1_sort(to_sort(n), qlist);
break;
case AST_FUNC_DECL:
r = reduce1_func_decl(to_func_decl(n), qlist);
break;
}
m_cache.insert(n, qlist, r);
}
format * mk_parameter(parameter const & p, quantifier_list * qlist) {
if (p.is_int()) {
return mk_int(m_manager, p.get_int());
}
else if (p.is_symbol()) {
return mk_string(m_manager, p.get_symbol().str().c_str());
}
else if (p.is_ast()) {
ast * n = p.get_ast();
if (is_func_decl(n)) {
return mk_string(m_manager, to_func_decl(n)->get_name().str().c_str());
}
else {
return get_cached(p.get_ast(), qlist);
}
}
else if (p.is_rational()) {
return mk_string(m_manager, p.get_rational().to_string().c_str());
}
else {
return 0;
}
}
void mk_parameters(unsigned num_params, parameter const * p, quantifier_list * qlist, ptr_buffer<format> & result, bool add_separator) {
bool first = true;
for (unsigned i = 0; i < num_params; i++) {
if (!first && add_separator) {
result.push_back(mk_string(m_manager, ":"));
}
format * pp = mk_parameter(p[i], qlist);
if (pp) {
result.push_back(pp);
first = false;
}
}
}
format * mk_parameters(unsigned num_params, parameter const * p, quantifier_list * qlist) {
if (num_params == 0)
return m_nil;
ptr_buffer<format> buffer;
buffer.push_back(mk_string(m_manager, "["));
mk_parameters(num_params, p, qlist, buffer, true);
buffer.push_back(mk_string(m_manager, "]"));
return mk_compose(m_manager, buffer.size(), buffer.c_ptr());
}
void visit_sort(sort* s) {
if (m_datatype_util.is_datatype(s) &&
!m_visited_datatypes.is_marked(s)) {
m_datatypes.push_back(s);
m_visited_datatypes.mark(s, true);
}
}
format * reduce1_sort(sort * s, quantifier_list * qlist) {
if (m_datatype_util.is_datatype(s)) {
return mk_string(m_manager, s->get_name().str().c_str());
}
ptr_buffer<format> pps;
mk_parameters(s->get_num_parameters(), s->get_parameters(), qlist, pps, false);
std::string name = s->get_name().str();
if (pps.empty())
return mk_string(m_manager, name.c_str());
return mk_seq1(m_manager, pps.c_ptr(), pps.c_ptr() + pps.size(),
f2f(), name.c_str());
}
format * reduce1_func_decl(func_decl * f, quantifier_list * qlist) {
ptr_buffer<format> children;
children.push_back(mk_compose(m_manager,
mk_string(m_manager, f->get_name().str().c_str()),
mk_parameters(f->get_num_parameters(), f->get_parameters(), qlist)));
for (unsigned i = 0; i < f->get_arity(); i++)
children.push_back(get_cached(f->get_domain(i), qlist));
children.push_back(get_cached(f->get_range(), qlist));
return mk_seq1(m_manager, children.begin(), children.end(), f2f(), "define");
}
void get_children(app * n, quantifier_list * qlist, ptr_buffer<format> & result) {
for (unsigned i = 0; i < n->get_num_args(); i++)
result.push_back(get_cached(n->get_arg(i), qlist));
}
format * reduce1_app(app * n, quantifier_list * qlist) {
rational val;
bool is_int;
bool pos;
unsigned bv_size;
uint64 uval;
buffer<symbol> names;
ptr_buffer<format> children;
if (m_autil.is_numeral(n, val, is_int)) {
std::string str;
if (val.is_neg()) {
str = "(- " + (-val).to_string() + ")";
}
else {
str = val.to_string();
}
return mk_string(m_manager, str.c_str());
}
else if (m_bvutil.is_numeral(n, val, bv_size)) {
std::string str = val.to_string();
return mk_compose(m_manager,
mk_string(m_manager, "bv"),
mk_string(m_manager, str.c_str()),
mk_compose(m_manager, mk_string(m_manager, "["), mk_unsigned(m_manager, bv_size), mk_string(m_manager, "]")));
}
else if (m_dl_util.is_finite_sort(n) &&
m_dl_util.is_numeral_ext(n, uval)) {
return mk_string(m_manager, rational(uval,rational::ui64()).to_string().c_str());
}
else if (m_manager.is_label(n, pos, names)) {
get_children(n, qlist, children);
symbol2format f(m_manager);
format * lbl = names.size() > 1 ? mk_seq5(m_manager, names.begin(), names.end(), f) : f(names[0]);
format * args[2] = { lbl, children[0] };
format ** begin = args;
return mk_seq1(m_manager, begin, begin+2, f2f(), pos ? "lblpos" : "lblneg");
}
else if (m_manager.is_pattern(n)) {
get_children(n, qlist, children);
return mk_seq5(m_manager, children.begin(), children.end(), f2f(), "{", "}");
}
else if (m_manager.is_proof(n)) {
get_children(n, qlist, children);
return mk_seq2(m_manager, children.begin(), children.end(), f2f(), n->get_decl()->get_name().str().c_str(),
FORMAT_DEFAULT_INDENT, "[", "]");
}
else if (m_params.m_pp_fixed_indent || (n->get_decl()->get_num_parameters() > 0 && !n->get_decl()->private_parameters())) {
format * head = mk_compose(m_manager,
mk_string(m_manager, n->get_decl()->get_name().str().c_str()),
mk_parameters(n->get_decl()->get_num_parameters(), n->get_decl()->get_parameters(), qlist));
if (n->get_num_args() == 0)
return head;
children.push_back(head);
get_children(n, qlist, children);
return mk_seq4(m_manager, children.begin(), children.end(), f2f());
}
else if (n->get_num_args() == 0)
return mk_string(m_manager, n->get_decl()->get_name().str().c_str());
else {
get_children(n, qlist, children);
return mk_seq1(m_manager, children.begin(), children.end(), f2f(), n->get_decl()->get_name().str().c_str());
}
}
format * reduce1_var(var * v, quantifier_list * qlist) {
unsigned idx = v->get_idx();
unsigned i = idx;
while (!is_nil(qlist)) {
quantifier * q = head(qlist);
if (i < q->get_num_decls())
return mk_string(m_manager, q->get_decl_name(q->get_num_decls() - i - 1).str().c_str());
i -= q->get_num_decls();
qlist = tail(qlist);
}
if (i < m_num_var_names) {
return mk_string(m_manager, m_var_names[m_num_var_names - i - 1]);
}
else {
return mk_compose(m_manager, mk_string(m_manager, "#"), mk_unsigned(m_manager, idx));
}
}
format * reduce1_quantifier(quantifier * q, quantifier_list * qlist) {
qlist = m_qlist_manager.mk_cons(q, qlist);
ptr_buffer<format> buffer;
unsigned num = q->get_num_decls();
for (unsigned j = 0; j < num; j++) {
format * d[2];
d[0] = mk_string(m_manager, q->get_decl_name(j).str().c_str());
d[1] = get_cached(q->get_decl_sort(j), qlist);
format ** it = d;
buffer.push_back(mk_seq5(m_manager, it, it+2, f2f()));
}
buffer.push_back(get_cached(q->get_expr(), qlist));
num = q->get_num_patterns();
char const * pat = ":pat ";
unsigned pat_indent = static_cast<unsigned>(strlen(pat));
for (unsigned i = 0; i < num; i++)
buffer.push_back(mk_compose(m_manager, mk_string(m_manager, pat), mk_indent(m_manager, pat_indent, get_cached(q->get_pattern(i), qlist))));
num = q->get_num_no_patterns();
for (unsigned i = 0; i < num; i++)
buffer.push_back(mk_compose(m_manager, mk_string(m_manager, ":nopat {"), get_cached(q->get_no_pattern(i), qlist), mk_string(m_manager, "}")));
if (q->get_qid() != symbol::null)
buffer.push_back(mk_compose(m_manager, mk_string(m_manager, ":qid {"), mk_string(m_manager, q->get_qid().str().c_str()), mk_string(m_manager, "}")));
return mk_seq3(m_manager, buffer.begin(), buffer.end(), f2f(), q->is_forall() ? "forall" : "exists",
q->get_num_decls());
}
public:
formatter(ast_manager & m, pp_params const & p, unsigned num_var_names, char const * const * var_names):
m_params(p),
m_manager(m),
m_qlist_manager(m),
m_cache(m),
m_qlists(m_qlist_manager),
m_nil(mk_nil(m), fm(m)),
m_autil(m),
m_bvutil(m),
m_datatype_util(m),
m_dl_util(m),
m_format_trail(fm(m)),
m_num_var_names(num_var_names),
m_var_names(var_names) {
}
~formatter() {
}
format * operator()(ast * n) {
m_todo.push_back(pp_entry(n, m_qlist_manager.mk_nil()));
while (!m_todo.empty()) {
pp_entry k = m_todo.back();
if (m_cache.contains(k.first, k.second))
m_todo.pop_back();
else if (visit_children(k.first, k.second)) {
m_todo.pop_back();
reduce1(k.first, k.second);
}
}
format* f1 = get_cached(n, m_qlist_manager.mk_nil());
if (m_datatypes.empty()) {
return f1;
}
ptr_buffer<format> formats;
formats.push_back(f1);
for (unsigned i = 0; i < m_datatypes.size(); ++i) {
sort* s = m_datatypes[i];
std::ostringstream buffer;
m_datatype_util.display_datatype(s, buffer);
format* f2 = mk_string(m_manager, buffer.str().c_str());
formats.push_back(mk_line_break(m_manager));
formats.push_back(f2);
}
f1 = mk_compose(m_manager, formats.size(), formats.c_ptr());
//
// Ensure that reference count is live.
//
m_format_trail.push_back(f1);
return f1;
}
};
std::ostream & ast_pp(std::ostream & out, ast * n, ast_manager & m, pp_params const & p, unsigned indent,
unsigned num_vars, char const * const * names) {
formatter f(m, p, num_vars, names);
app_ref fmt(fm(m));
fmt = f(n);
if (indent > 0)
fmt = format_ns::mk_indent(m, indent, fmt);
pp(out, fmt, m, p);
return out;
}
std::string & ast_pp(std::string & out, ast * n, ast_manager & m, pp_params const & p, unsigned indent) {
std::ostringstream buffer;
buffer << mk_pp(n, m, p, indent);
out += buffer.str();
return out;
}
std::string ast_pp(ast * n, ast_manager & m, pp_params const & p, unsigned indent) {
std::string out;
return ast_pp(out, n, m, p, indent);
}
std::string & ast_pp(std::string & out, ast * n, ast_manager & m) {
return ast_pp(out, n, m, get_pp_default_params());
}
std::string ast_pp(ast * n, ast_manager & m) {
return ast_pp(n, m, get_pp_default_params());
}

39
src/ast/ast_pp.h
View file

@ -15,39 +15,22 @@ Author:
Revision History:
2012-11-17 - ast_smt2_pp is the official pretty printer in Z3
--*/
#ifndef _AST_PP_H_
#define _AST_PP_H_
#include"ast.h"
#include"pp_params.h"
#include"ast_smt2_pp.h"
std::ostream & ast_pp(std::ostream & strm, ast * n, ast_manager & m, pp_params const & p, unsigned indent = 0,
unsigned num_vars = 0, char const * const * names = 0);
std::ostream & ast_pp(std::ostream & strm, ast * n, ast_manager & m);
std::string & ast_pp(std::string & s, ast * n, ast_manager & m, pp_params const & p, unsigned indent = 0);
std::string ast_pp(ast * n, ast_manager & m, pp_params const & p, unsigned indent = 0);
std::string & ast_pp(std::string & s, ast * n, ast_manager & m);
std::string ast_pp(ast * n, ast_manager & m);
struct mk_pp {
ast * m_ast;
ast_manager & m_manager;
pp_params const & m_params;
unsigned m_indent;
unsigned m_num_var_names;
char const * const * m_var_names;
mk_pp(ast * a, ast_manager & m, pp_params const & p, unsigned indent = 0, unsigned num_var_names = 0, char const * const * var_names = 0);
mk_pp(ast * a, ast_manager & m, unsigned indent = 0, unsigned num_var_names = 0, char const * const * var_names = 0);
struct mk_pp : public mk_ismt2_pp {
mk_pp(ast * t, ast_manager & m, pp_params const & p, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0):
mk_ismt2_pp(t, m, p, indent, num_vars, var_prefix) {
}
mk_pp(ast * t, ast_manager & m, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0):
mk_ismt2_pp(t, m, indent, num_vars, var_prefix) {
}
};
inline std::ostream& operator<<(std::ostream& out, const mk_pp & p) {
return ast_pp(out, p.m_ast, p.m_manager, p.m_params, p.m_indent, p.m_num_var_names, p.m_var_names);
}
inline std::string& operator+=(std::string& out, const mk_pp & p) {
return ast_pp(out, p.m_ast, p.m_manager, p.m_params, p.m_indent);
}
#endif

39
src/ast/pattern/expr_pattern_match.cpp
View file

@ -205,14 +205,10 @@ expr_pattern_match::match(expr* a, unsigned init, subst& s)
// substitution s contains registers with matching declarations.
return true;
case CHECK_TERM:
TRACE("expr_pattern_match", display(tout, pc);
ast_pp(tout, m_regs[pc.m_reg], m_manager) << "\n";);
ok = (pc.m_pat == m_regs[pc.m_reg]);
break;
case SET_VAR:
case CHECK_VAR: {
TRACE("expr_pattern_match", display(tout, pc);
ast_pp(tout, m_regs[pc.m_reg], m_manager) << "\n";);
app* app1 = to_app(pc.m_pat);
a = m_regs[pc.m_reg];
if (a->get_kind() != AST_APP) {
@ -237,8 +233,6 @@ expr_pattern_match::match(expr* a, unsigned init, subst& s)
break;
}
case SET_BOUND: {
TRACE("expr_pattern_match", display(tout, pc);
ast_pp(tout, m_regs[pc.m_reg], m_manager) << "\n";);
a = m_regs[pc.m_reg];
if (a->get_kind() != AST_VAR) {
break;
@ -329,15 +323,6 @@ expr_pattern_match::match(expr* a, unsigned init, subst& s)
if (k < fac*num_args) {
bstack.push_back(instr(CHOOSE_AC, pc.m_offset, pc.m_next, app2, k+1));
}
TRACE("expr_pattern_match",
{
tout << "fac: " << fac << " num_args:" << num_args << " k:" << k << "\n";
for (unsigned i = 0; i < num_args; ++i) {
ast_pp(tout, m_regs[pc.m_offset + i], m_manager);
tout << " ";
}
tout << "\n";
});
break;
}
case BACKTRACK:
@ -430,24 +415,24 @@ expr_pattern_match::display(std::ostream& out, instr const& pc) const {
break;
case BIND:
out << "bind ";
ast_pp(out, to_app(pc.m_pat)->get_decl(), m_manager) << " ";
ast_pp(out, pc.m_pat, m_manager) << "\n";
out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " ";
out << mk_pp(pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "offset: " << pc.m_offset << "\n";
out << "reg: " << pc.m_reg << "\n";
break;
case BIND_AC:
out << "bind_ac ";
ast_pp(out, to_app(pc.m_pat)->get_decl(), m_manager) << " ";
ast_pp(out, pc.m_pat, m_manager) << "\n";
out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " ";
out << mk_pp(pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "offset: " << pc.m_offset << "\n";
out << "reg: " << pc.m_reg << "\n";
break;
case BIND_C:
out << "bind_c ";
ast_pp(out, to_app(pc.m_pat)->get_decl(), m_manager) << " ";
ast_pp(out, pc.m_pat, m_manager) << "\n";
out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " ";
out << mk_pp(pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "offset: " << pc.m_offset << "\n";
out << "reg: " << pc.m_reg << "\n";
@ -464,23 +449,23 @@ expr_pattern_match::display(std::ostream& out, instr const& pc) const {
break;
case CHECK_VAR:
out << "check_var ";
ast_pp(out, pc.m_pat, m_manager) << "\n";
out << mk_pp(pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "reg: " << pc.m_reg << "\n";
out << "other_reg: " << pc.m_other_reg << "\n";
break;
case CHECK_TERM:
out << "check ";
ast_pp(out, pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "reg: " << pc.m_reg << "\n";
break;
out << mk_pp(pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "reg: " << pc.m_reg << "\n";
break;
case YIELD:
out << "yield\n";
break;
case SET_VAR:
out << "set_var ";
ast_pp(out, pc.m_pat, m_manager) << "\n";
out << mk_pp(pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
break;
default:

2
src/ast/substitution/substitution_tree.cpp
View file

@ -610,7 +610,7 @@ void substitution_tree::display(std::ostream & out, node * n, unsigned delta) co
pp_params p;
p.m_pp_single_line = true;
out << " ==> ";
ast_pp(out, n->m_expr, m_manager, p);
out << mk_pp(n->m_expr, m_manager, p);
out << "\n";
}
else {

2
src/math/euclid/README Normal file
View file

@ -0,0 +1,2 @@
Basic Euclidean solver for linear integer equations.
This solver generates "explanations".

2
src/math/interval/README Normal file
View file

@ -0,0 +1,2 @@
Template for interval arithmetic. The template can be instantiated using different numeral (integers/mpz, rationals/mpq, floating-point/mpf, etc) packages.
The class im_default_config defines a default configuration for the template that uses rationals. It also shows what is the expected signature used by the template.

3
src/math/polynomial/README Normal file
View file

@ -0,0 +1,3 @@
Polynomial manipulation package.
It contains support for univariate (upolynomial.*) and multivariate polynomials (polynomial.*).
Multivariate polynomial factorization does not work yet (polynomial_factorization.*), and it is disabled.

2
src/muz_qe/dl_base.cpp
View file

@ -47,7 +47,7 @@ namespace datalog {
out<<"(";
for(unsigned i=0; i<sz; i++) {
if(i) { out<<","; }
out<<ast_pp((*this)[i], m);
out << mk_pp((*this)[i], m);
}
out<<")";
}

3
src/muz_qe/pdr_context.cpp
View file

@ -386,7 +386,8 @@ namespace pdr {
fi->set_else(result);
md->register_decl(m_head, fi);
}
apply(ctx.get_model_converter(), md, 0);
model_converter_ref mc = ctx.get_model_converter();
apply(mc, md, 0);
if (p_orig->get_arity() == 0) {
result = md->get_const_interp(p_orig);
}

17
src/tactic/tactical.cpp
View file

@ -545,8 +545,13 @@ public:
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
if (omp_in_parallel()) {
bool use_seq;
#ifdef _NO_OMP_
use_seq = true;
#else
use_seq = omp_in_parallel();
#endif
if (use_seq) {
// execute tasks sequentially
or_else_tactical::operator()(in, result, mc, pc, core);
return;
@ -668,7 +673,13 @@ public:
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
if (omp_in_parallel()) {
bool use_seq;
#ifdef _NO_OMP_
use_seq = true;
#else
use_seq = omp_in_parallel();
#endif
if (use_seq) {
// execute tasks sequentially
and_then_tactical::operator()(in, result, mc, pc, core);
return;

4
src/test/quant_elim.cpp
View file

@ -42,11 +42,11 @@ static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char cons
qe(m.mk_true(), fml, result);
std::cout << " -> " << mk_pp(result, m) << " " << expected_outcome << "\n";
if (expected_outcome == l_true && !m.is_true(result)) {
std::cout << "ERROR: expected true, instead got " << ast_pp(result, m).c_str() << "\n";
std::cout << "ERROR: expected true, instead got " << mk_pp(result, m) << "\n";
//exit(-1);
}
if (expected_outcome == l_false && !m.is_false(result)) {
std::cout << "ERROR: expected false, instead got " << ast_pp(result, m).c_str() << "\n";
std::cout << "ERROR: expected false, instead got " << mk_pp(result, m) << "\n";
//exit(-1);
}
}

3
src/util/debug.h
View file

@ -98,6 +98,9 @@ private:
};
void finalize_debug();
/*
ADD_FINALIZER('finalize_debug();')
*/
#endif /* _DEBUG_H_ */

56
src/util/mem_stat.cpp
View file

@ -1,56 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
mem_stat.cpp
Abstract:
Memory usage statistics
Author:
Leonardo de Moura (leonardo) 2006-11-09.
Revision History:
--*/
#ifdef _WINDOWS
#include<windows.h>
#include<cstdio>
#include<psapi.h>
double get_max_heap_size() {
DWORD processID = GetCurrentProcessId();
HANDLE hProcess;
PROCESS_MEMORY_COUNTERS pmc;
hProcess = OpenProcess(PROCESS_QUERY_INFORMATION |
PROCESS_VM_READ,
FALSE, processID);
double result = -1.0;
if (NULL == hProcess) {
return -1.0;
}
if (GetProcessMemoryInfo( hProcess, &pmc, sizeof(pmc))) {
result = static_cast<double>(pmc.PeakWorkingSetSize) / static_cast<double>(1024*1024);
}
CloseHandle( hProcess );
return result;
}
#else
double get_max_heap_size() {
// not available in this platform
return -1.0;
}
#endif

25
src/util/mem_stat.h
View file

@ -1,25 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
mem_stat.h
Abstract:
Memory usage statistics
Author:
Leonardo de Moura (leonardo) 2006-11-09.
Revision History:
--*/
#ifndef _MEM_STAT_H_
#define _MEM_STAT_H_
double get_max_heap_size();
#endif /* _MEM_STAT_H_ */

34
src/util/memory_manager.cpp
View file

@ -1,13 +1,27 @@
#include<iostream>
#include<stdlib.h>
#include"trace.h"
#include"memory_manager.h"
#include"rational.h"
#include"prime_generator.h"
#include"debug.h"
#include"error_codes.h"
// The following two function are automatically generated by the mk_make.py script.
// The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files.
// For example, rational.h contains
// ADD_INITIALIZER('rational::initialize();')
// ADD_FINALIZER('rational::finalize();')
// Thus, any executable or shared object (DLL) that depends on rational.h
// will have an automalically generated file mem_initializer.cpp containing
// mem_initialize()
// mem_finalize()
// and these functions will include the statements:
// rational::initialize();
//
// rational::finalize();
void mem_initialize();
void mem_finalize();
// If PROFILE_MEMORY is defined, Z3 will display the amount of memory used, and the number of synchronization steps during finalization
// #define PROFILE_MEMORY
void initialize_symbols();
void finalize_symbols();
out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) {
}
@ -58,8 +72,7 @@ mem_usage_report g_info;
void memory::initialize(size_t max_size) {
g_memory_out_of_memory = false;
g_memory_max_size = max_size;
rational::initialize();
initialize_symbols();
mem_initialize();
}
bool memory::is_out_of_memory() {
@ -96,14 +109,9 @@ static bool g_finalizing = false;
void memory::finalize() {
g_finalizing = true;
finalize_debug();
finalize_trace();
finalize_symbols();
rational::finalize();
prime_iterator::finalize();
mem_finalize();
}
unsigned long long memory::get_allocation_size() {
long long r;
#pragma omp critical (z3_memory_manager)

3
src/util/prime_generator.h
View file

@ -48,6 +48,9 @@ public:
prime_iterator(prime_generator * g = 0);
uint64 next();
static void finalize();
/*
ADD_FINALIZER('prime_iterator::finalize();')
*/
};
#endif

5
src/util/rational.h
View file

@ -35,7 +35,10 @@ public:
static void initialize();
static void finalize();
/*
ADD_INITIALIZER('rational::initialize();')
ADD_FINALIZER('rational::finalize();')
*/
rational() {}
rational(rational const & r) { m().set(m_val, r.m_val); }

4
src/util/symbol.h
View file

@ -141,6 +141,10 @@ struct symbol_eq_proc {
void initialize_symbols();
void finalize_symbols();
/*
ADD_INITIALIZER('initialize_symbols();')
ADD_FINALIZER('finalize_symbols();')
*/
// total order on symbols... I did not overloaded '<' to avoid misunderstandings.
// numerical symbols are smaller than non numerical symbols.

3
src/util/trace.h
View file

@ -40,6 +40,9 @@ bool is_trace_enabled(const char * tag);
void close_trace();
void open_trace();
void finalize_trace();
/*
ADD_FINALIZER('finalize_trace();')
*/
#define TRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE tout << "------------------------------------------------\n"; tout.flush(); })