From 8ad12a7dd4994327b9fac1571d648e18e1258108 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Nov 2012 09:14:02 -0800 Subject: [PATCH 01/15] Missing config option Signed-off-by: Leonardo de Moura --- scripts/config-release.mk.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/config-release.mk.in b/scripts/config-release.mk.in index 5936c6135..0ba4c8222 100644 --- a/scripts/config-release.mk.in +++ b/scripts/config-release.mk.in @@ -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 From f9ec1f2a637030edcb68bc329f311f9e19f993e8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Nov 2012 09:14:36 -0800 Subject: [PATCH 02/15] making sure par-or and par-then combinators work correctly even when OpenMP is not available Signed-off-by: Leonardo de Moura --- src/tactic/tactical.cpp | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index ae9c73a00..d13eab75e 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -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; From 50e00b615fac6db0b6e1e935c4832f94c98bf164 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Nov 2012 09:16:51 -0800 Subject: [PATCH 03/15] updated release notes Signed-off-by: Leonardo de Moura --- RELEASE_NOTES | 2 ++ 1 file changed, 2 insertions(+) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 6c652874e..e146be973 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -5,6 +5,8 @@ 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 ============= From 3e8d3db290f252be03e9cb30b719005b6c7e2a16 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Nov 2012 09:26:01 -0800 Subject: [PATCH 04/15] fixed gcc compilation error Signed-off-by: Leonardo de Moura --- src/muz_qe/pdr_context.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 13c2c0f6d..d3c87985b 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -383,7 +383,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); } From ad3aa96726cbb07f28cf92eb3d0f94d410091a86 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Nov 2012 21:26:28 -0800 Subject: [PATCH 05/15] improving clang++ support Signed-off-by: Leonardo de Moura --- README | 2 +- configure.ac | 47 ++++++++++++++++---------------- scripts/config-vs-debug-x64.mk | 2 +- scripts/config-vs-debug.mk | 2 +- scripts/config-vs-release-x64.mk | 2 +- scripts/config-vs-release.mk | 2 +- scripts/mk_util.py | 35 ++++-------------------- 7 files changed, 33 insertions(+), 59 deletions(-) diff --git a/README b/README index 26753e26d..a85d13726 100644 --- a/README +++ b/README @@ -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 diff --git a/configure.ac b/configure.ac index 49431f500..f0314e7c0 100644 --- a/configure.ac +++ b/configure.ac @@ -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,25 @@ 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= + 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 +154,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 +192,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 < Date: Tue, 13 Nov 2012 21:49:37 -0800 Subject: [PATCH 06/15] fixed clang++ for linux Signed-off-by: Leonardo de Moura --- configure.ac | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/configure.ac b/configure.ac index f0314e7c0..a02915ff4 100644 --- a/configure.ac +++ b/configure.ac @@ -134,7 +134,8 @@ AS_IF([test "$host_os" = "Darwin"], [ ], [test "$host_os" = "Linux"], [ PLATFORM=linux SO_EXT=.so - SLIBFLAGS+="-shared" + LDFLAGS+=" -lrt" + SLIBFLAGS+=" -shared" COMP_VERSIONS= STATIC_FLAGS=-static CXXFLAGS+=" -fno-strict-aliasing" From 79eca95a95f685fc057732ac1cb30ee673a36d5d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Nov 2012 22:46:57 -0800 Subject: [PATCH 07/15] bumped version number Signed-off-by: Leonardo de Moura --- scripts/mk_project.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index cb1dae205..deef749c0 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -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']) From ead762e0d03d24d31777b48883592a29a659a3e4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 14 Nov 2012 09:02:53 -0800 Subject: [PATCH 08/15] bumped version number Signed-off-by: Leonardo de Moura --- src/api/dotnet/Properties/AssemblyInfo.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/dotnet/Properties/AssemblyInfo.cs b/src/api/dotnet/Properties/AssemblyInfo.cs index cdec553fb..1ac6cb520 100644 --- a/src/api/dotnet/Properties/AssemblyInfo.cs +++ b/src/api/dotnet/Properties/AssemblyInfo.cs @@ -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")] From b472a36b42822870785abaa45fe7a4d534639a1a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 14 Nov 2012 09:03:13 -0800 Subject: [PATCH 09/15] added --staticlib option to mk_make.py Signed-off-by: Leonardo de Moura --- scripts/mk_project.py | 1 + scripts/mk_util.py | 75 ++++++++++++++++++++++++++++++++++--------- 2 files changed, 61 insertions(+), 15 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index deef749c0..b197c5131 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -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']) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 54f1931e5..5af927f5f 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -40,6 +40,7 @@ Z3PY_SRC_DIR=None VS_PROJ = False TRACE = False DOTNET_ENABLED=False +STATIC_LIB=False VER_MAJOR=None VER_MINOR=None @@ -56,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') @@ -120,11 +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 " --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 + 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', @@ -134,7 +139,8 @@ def parse_options(): 'showcpp', 'vsproj', 'trace', - 'nodotnet' + 'nodotnet', + 'staticlib' ]) for opt, arg in options: if opt in ('-b', '--build'): @@ -161,6 +167,8 @@ def parse_options(): TRACE = True elif opt in ('-n', '--nodotnet'): DOTNET_ENABLED = False + elif opt in ('--staticlib'): + STATIC_LIB = True else: raise MKException("Invalid command line option '%s'" % opt) @@ -492,9 +500,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: @@ -511,7 +518,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 @@ -519,6 +526,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) @@ -556,11 +564,39 @@ class DLLComponent(Component): 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) @@ -573,18 +609,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): @@ -763,8 +808,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): From 1ec0d02ead6d4ad48a39de5610aca53d24c8b268 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 14 Nov 2012 11:14:09 -0800 Subject: [PATCH 10/15] added get_version to z3py Signed-off-by: Leonardo de Moura --- src/api/python/z3.py | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index f3de4258a..f6c152d5e 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -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): From 3f52f30f9cb8c838e41e25e38a702f579c85efcf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 14 Nov 2012 11:15:12 -0800 Subject: [PATCH 11/15] updated RELEASE_NOTES Signed-off-by: Leonardo de Moura --- RELEASE_NOTES | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index e146be973..3282fa2ba 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -1,5 +1,10 @@ RELEASE NOTES +Version 4.3.2 +============= + +- Added get_version() and get_version_string() to Z3Py + Version 4.3.1 ============= From 1645f61d859685e3bd807f1db9782d2be4df0f49 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 17 Nov 2012 09:32:01 -0800 Subject: [PATCH 12/15] added READMEs Signed-off-by: Leonardo de Moura --- src/math/euclid/README | 2 ++ src/math/interval/README | 2 ++ src/math/polynomial/README | 3 +++ 3 files changed, 7 insertions(+) create mode 100644 src/math/euclid/README create mode 100644 src/math/interval/README create mode 100644 src/math/polynomial/README diff --git a/src/math/euclid/README b/src/math/euclid/README new file mode 100644 index 000000000..7235cd76f --- /dev/null +++ b/src/math/euclid/README @@ -0,0 +1,2 @@ +Basic Euclidean solver for linear integer equations. +This solver generates "explanations". \ No newline at end of file diff --git a/src/math/interval/README b/src/math/interval/README new file mode 100644 index 000000000..75aa2e9c6 --- /dev/null +++ b/src/math/interval/README @@ -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. \ No newline at end of file diff --git a/src/math/polynomial/README b/src/math/polynomial/README new file mode 100644 index 000000000..5d079eea0 --- /dev/null +++ b/src/math/polynomial/README @@ -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. \ No newline at end of file From 93bfcaa4047162996139bf8a11602262cb11ec7c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 17 Nov 2012 10:20:08 -0800 Subject: [PATCH 13/15] Making ast_smt2_pp the default pretty printer. Now, mk_pp is just an alias for mk_ismt2_pp Signed-off-by: Leonardo de Moura --- src/ast/ast_pp.cpp | 516 --------------------- src/ast/ast_pp.h | 39 +- src/ast/pattern/expr_pattern_match.cpp | 39 +- src/ast/substitution/substitution_tree.cpp | 2 +- src/muz_qe/dl_base.cpp | 2 +- src/test/quant_elim.cpp | 4 +- 6 files changed, 27 insertions(+), 575 deletions(-) delete mode 100644 src/ast/ast_pp.cpp diff --git a/src/ast/ast_pp.cpp b/src/ast/ast_pp.cpp deleted file mode 100644 index 842f05408..000000000 --- a/src/ast/ast_pp.cpp +++ /dev/null @@ -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 - -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 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 pp_entry; - svector 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 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 & 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 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 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 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 & 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 names; - ptr_buffer 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 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(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 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()); -} - diff --git a/src/ast/ast_pp.h b/src/ast/ast_pp.h index eeee29d44..d99fb7670 100644 --- a/src/ast/ast_pp.h +++ b/src/ast/ast_pp.h @@ -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 + diff --git a/src/ast/pattern/expr_pattern_match.cpp b/src/ast/pattern/expr_pattern_match.cpp index aca739949..25be8dbf0 100644 --- a/src/ast/pattern/expr_pattern_match.cpp +++ b/src/ast/pattern/expr_pattern_match.cpp @@ -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: diff --git a/src/ast/substitution/substitution_tree.cpp b/src/ast/substitution/substitution_tree.cpp index 6e44c68f2..81b2f7be6 100644 --- a/src/ast/substitution/substitution_tree.cpp +++ b/src/ast/substitution/substitution_tree.cpp @@ -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 { diff --git a/src/muz_qe/dl_base.cpp b/src/muz_qe/dl_base.cpp index 5556920f0..89ebc7e4e 100644 --- a/src/muz_qe/dl_base.cpp +++ b/src/muz_qe/dl_base.cpp @@ -47,7 +47,7 @@ namespace datalog { out<<"("; for(unsigned i=0; i " << 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); } } From 570147e326b4213f4bbe70e813a2d3d61560aa7b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 17 Nov 2012 10:33:09 -0800 Subject: [PATCH 14/15] removed dead code Signed-off-by: Leonardo de Moura --- src/util/mem_stat.cpp | 56 ------------------------------------------- src/util/mem_stat.h | 25 ------------------- 2 files changed, 81 deletions(-) delete mode 100644 src/util/mem_stat.cpp delete mode 100644 src/util/mem_stat.h diff --git a/src/util/mem_stat.cpp b/src/util/mem_stat.cpp deleted file mode 100644 index c0753dea9..000000000 --- a/src/util/mem_stat.cpp +++ /dev/null @@ -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 -#include -#include - -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(pmc.PeakWorkingSetSize) / static_cast(1024*1024); - } - - CloseHandle( hProcess ); - - return result; -} - -#else - -double get_max_heap_size() { - // not available in this platform - return -1.0; -} - -#endif - diff --git a/src/util/mem_stat.h b/src/util/mem_stat.h deleted file mode 100644 index 84c7d0096..000000000 --- a/src/util/mem_stat.h +++ /dev/null @@ -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_ */ - From ed5d154f78532acc81a2c75e728b6f0cfe268191 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 17 Nov 2012 11:30:25 -0800 Subject: [PATCH 15/15] broke dependency between components that need initialization and memory_manager Signed-off-by: Leonardo de Moura --- scripts/mk_util.py | 65 +++++++++++++++++++++++++++++++++++++ src/util/debug.h | 3 ++ src/util/memory_manager.cpp | 34 +++++++++++-------- src/util/prime_generator.h | 3 ++ src/util/rational.h | 5 ++- src/util/symbol.h | 4 +++ src/util/trace.h | 3 ++ 7 files changed, 103 insertions(+), 14 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 5af927f5f..6828dd8f9 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -378,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 @@ -490,6 +494,9 @@ class ExeComponent(Component): 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 @@ -601,6 +608,9 @@ class DLLComponent(Component): 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 @@ -927,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 @@ -1099,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.*") diff --git a/src/util/debug.h b/src/util/debug.h index ab9fdd57b..64cc35fcf 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -98,6 +98,9 @@ private: }; void finalize_debug(); +/* + ADD_FINALIZER('finalize_debug();') +*/ #endif /* _DEBUG_H_ */ diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 3aeb65d3b..b6eb648d9 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -1,13 +1,27 @@ +#include #include +#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) diff --git a/src/util/prime_generator.h b/src/util/prime_generator.h index efb675737..d63fdb224 100644 --- a/src/util/prime_generator.h +++ b/src/util/prime_generator.h @@ -48,6 +48,9 @@ public: prime_iterator(prime_generator * g = 0); uint64 next(); static void finalize(); + /* + ADD_FINALIZER('prime_iterator::finalize();') + */ }; #endif diff --git a/src/util/rational.h b/src/util/rational.h index 4aa2f5fc6..f0406f30a 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -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); } diff --git a/src/util/symbol.h b/src/util/symbol.h index e32eeb55b..65325b461 100644 --- a/src/util/symbol.h +++ b/src/util/symbol.h @@ -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. diff --git a/src/util/trace.h b/src/util/trace.h index 941520f87..0c8c2e5b6 100644 --- a/src/util/trace.h +++ b/src/util/trace.h @@ -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(); })