From 8cc3ba5a8b8ced685669d43ec315bd282a13269d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 4 Mar 2016 13:09:42 +0000 Subject: [PATCH 01/12] fixed FP Python doctest examples --- src/api/python/z3.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 3a4276dfd..088cd0d4d 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -8524,11 +8524,11 @@ def FPVal(sig, exp=None, fps=None, ctx=None): >>> v = FPVal(-2.25, FPSort(8, 24)) >>> v -1.125*(2**1) - >>> v = FPVal(-0.0, FPSort(8, 24)) + >>> FPVal(-0.0, FPSort(8, 24)) -0.0 - >>> v = FPVal(0.0, FPSort(8, 24)) + >>> FPVal(0.0, FPSort(8, 24)) +0.0 - >>> v = FPVal(+0.0, FPSort(8, 24)) + >>> FPVal(+0.0, FPSort(8, 24)) +0.0 """ ctx = _get_ctx(ctx) @@ -8911,7 +8911,7 @@ def fpNEQ(a, b, ctx=None): >>> fpNEQ(x, y) Not(fpEQ(x, y)) >>> (x != y).sexpr() - '(not (fp.eq x y))' + '(distinct x y)' """ return Not(fpEQ(a, b, ctx)) From a51201298c2016fb4ed67372ccce84c26a797fd8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 4 Mar 2016 14:42:38 +0000 Subject: [PATCH 02/12] Bugfix for assumptions in inc_sat_solver --- src/sat/sat_solver/inc_sat_solver.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 1c156d83e..7feed9fb1 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -151,6 +151,7 @@ public: lbool r = internalize_formulas(); if (r != l_true) return r; r = internalize_assumptions(sz, assumptions, dep2asm); + SASSERT(sz == m_asms.size()); if (r != l_true) return r; r = m_solver.check(m_asms.size(), m_asms.c_ptr(), m_weights.c_ptr(), max_weight); @@ -300,6 +301,7 @@ private: lbool internalize_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) { if (sz == 0) { + m_asms.shrink(0); return l_true; } goal_ref g = alloc(goal, m, true, true); // models and cores are enabled. @@ -331,6 +333,7 @@ private: sat::literal lit; for (unsigned i = 0; i < sz; ++i) { if (dep2asm.find(asms[i], lit)) { + SASSERT(lit.var() <= m_solver.num_vars()); m_asms.push_back(lit); if (i != j && !m_weights.empty()) { m_weights[j] = m_weights[i]; From cf5910e041c42603a532c40cf69f9b0a1067eb81 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 4 Mar 2016 15:08:03 +0000 Subject: [PATCH 03/12] typos --- scripts/update_api.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index fc0f1c939..badd960cc 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -57,7 +57,7 @@ log_h.write('inline void SetR(void * obj) { *g_z3_log << "= " << obj << "\\n"; } log_h.write('#define RETURN_Z3(Z3RES) if (_LOG_CTX.enabled()) { SetR(Z3RES); } return Z3RES\n') log_h.write('void _Z3_append_log(char const * msg);\n') ## -exe_c.write('void Z3_replacer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg(ctx, c)); }\n') +exe_c.write('void Z3_replayer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg(ctx, c)); }\n') ## core_py.write('# Automatically generated file\n') core_py.write('import sys, os\n') @@ -1068,7 +1068,7 @@ def def_API(name, result, params): if is_obj(result): exe_c.write(" in.store_result(result);\n") if name == 'Z3_mk_context' or name == 'Z3_mk_context_rc': - exe_c.write(" Z3_set_error_handler(result, Z3_replacer_error_handler);") + exe_c.write(" Z3_set_error_handler(result, Z3_replayer_error_handler);") log_c.write('}\n') exe_c.write('}\n') mk_log_macro(log_h, name, params) From 40c5152075ae9a96aee4a0fdb08e65af96f25e1d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 4 Mar 2016 18:32:45 +0000 Subject: [PATCH 04/12] Added --staticbin option. Relates to #456 --- scripts/mk_util.py | 40 +++++++++++++++++++++++++++------------- 1 file changed, 27 insertions(+), 13 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index a02a9b40f..36f7b5ce3 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -82,6 +82,7 @@ JAVA_ENABLED=False ML_ENABLED=False PYTHON_INSTALL_ENABLED=False STATIC_LIB=False +STATIC_BIN=False VER_MAJOR=None VER_MINOR=None VER_BUILD=None @@ -532,6 +533,9 @@ def get_version(): def build_static_lib(): return STATIC_LIB +def build_static_bin(): + return STATIC_BIN + def is_cr_lf(fname): # Check whether text files use cr/lf f = open(fname, 'r') @@ -616,6 +620,7 @@ def display_help(exit_code): print(" --ml generate OCaml bindings.") print(" --python generate Python bindings.") print(" --staticlib build Z3 static library.") + print(" --staticbin build a statically linked Z3 binary.") if not IS_WINDOWS: print(" -g, --gmp use GMP.") print(" --gprof enable gprof") @@ -646,14 +651,14 @@ def display_help(exit_code): # 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, VS_PAR, VS_PAR_NUM - global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, PYTHON_INSTALL_ENABLED + global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, PYTHON_INSTALL_ENABLED global LINUX_X64, SLOW_OPTIMIZE, USE_OMP try: options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:df:sxhmcvtnp:gj', ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'trace', 'dotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof', - 'githash=', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python']) + 'githash=', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python', 'staticbin']) except: print("ERROR: Invalid command line option") display_help(1) @@ -688,6 +693,8 @@ def parse_options(): DOTNET_ENABLED = True elif opt in ('--staticlib'): STATIC_LIB = True + elif opt in ('--staticbin'): + STATIC_BIN = True elif opt in ('--optimize'): SLOW_OPTIMIZE = True elif not IS_WINDOWS and opt in ('-p', '--prefix'): @@ -2189,14 +2196,19 @@ def mk_config(): extra_opt = ' -D_NO_OMP_' if GIT_HASH: extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH) + if STATIC_BIN: + static_opt = '/MT' + else: + static_opt = '/MD' if DEBUG_MODE: + static_opt = static_opt + 'd' config.write( 'AR_FLAGS=/nologo\n' - 'LINK_FLAGS=/nologo /MDd\n' - 'SLINK_FLAGS=/nologo /LDd\n') + 'LINK_FLAGS=/nologo %s\n' + 'SLINK_FLAGS=/nologo /LDd\n' % static_opt) if VS_X64: config.write( - 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n' % extra_opt) + 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n' % extra_opt) config.write( 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') @@ -2205,7 +2217,7 @@ def mk_config(): exit(1) else: config.write( - 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt) + 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt) config.write( 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') @@ -2214,15 +2226,14 @@ def mk_config(): LTCG=' /LTCG' if SLOW_OPTIMIZE else '' GL = ' /GL' if SLOW_OPTIMIZE else '' config.write( - 'AR_FLAGS=/nologo%s\n' - 'LINK_FLAGS=/nologo /MD\n' - 'SLINK_FLAGS=/nologo /LD\n' - % LTCG) + 'AR_FLAGS=/nologo %s\n' + 'LINK_FLAGS=/nologo %s\n' + 'SLINK_FLAGS=/nologo /LD\n' % (LTCG, static_opt)) if TRACE: extra_opt = '%s /D _TRACE ' % extra_opt if VS_X64: config.write( - 'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP\n' % (GL, extra_opt)) + 'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP\n' % (GL, extra_opt)) config.write( 'LINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n' 'SLINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n' % (LTCG, LTCG)) @@ -2231,7 +2242,7 @@ def mk_config(): exit(1) else: config.write( - 'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % (GL, extra_opt)) + 'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % (GL, extra_opt)) config.write( 'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n' % (LTCG, LTCG)) @@ -2356,7 +2367,10 @@ def mk_config(): config.write('AR_OUTFLAG=\n') config.write('EXE_EXT=\n') config.write('LINK=%s\n' % CXX) - config.write('LINK_FLAGS=\n') + if STATIC_BIN: + config.write('LINK_FLAGS=-static\n') + else: + config.write('LINK_FLAGS=\n') config.write('LINK_OUT_FLAG=-o \n') config.write('LINK_EXTRA_FLAGS=-lpthread %s\n' % LDFLAGS) config.write('SO_EXT=%s\n' % SO_EXT) From b13db1e82ee7d34ab2bce009bc8752d5f55432f1 Mon Sep 17 00:00:00 2001 From: Zephyr Pellerin Date: Fri, 4 Mar 2016 18:26:00 -0800 Subject: [PATCH 05/12] Bugfix for arith_rewriter single operand division --- src/ast/rewriter/arith_rewriter.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index e48a4fd2a..d45a4b092 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -61,8 +61,10 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c case OP_ADD: st = mk_add_core(num_args, args, result); break; case OP_MUL: st = mk_mul_core(num_args, args, result); break; case OP_SUB: st = mk_sub(num_args, args, result); break; - case OP_DIV: SASSERT(num_args == 2); st = mk_div_core(args[0], args[1], result); break; - case OP_IDIV: SASSERT(num_args == 2); st = mk_idiv_core(args[0], args[1], result); break; + case OP_DIV: if (num_args == 1) { result = args[0]; st = BR_DONE; break; } + SASSERT(num_args == 2); st = mk_div_core(args[0], args[1], result); break; + case OP_IDIV: if (num_args == 1) { result = args[0]; st = BR_DONE; break; } + SASSERT(num_args == 2); st = mk_idiv_core(args[0], args[1], result); break; case OP_MOD: SASSERT(num_args == 2); st = mk_mod_core(args[0], args[1], result); break; case OP_REM: SASSERT(num_args == 2); st = mk_rem_core(args[0], args[1], result); break; case OP_UMINUS: SASSERT(num_args == 1); st = mk_uminus(args[0], result); break; @@ -292,7 +294,7 @@ expr * arith_rewriter::reduce_power(expr * arg, bool is_eq) { for (unsigned i = 0; i < sz; i++) { expr * arg = args[i]; expr * arg0, *arg1; - if (m_util.is_power(arg, arg0, arg1) && m_util.is_numeral(arg1, k) && k.is_int() && + if (m_util.is_power(arg, arg0, arg1) && m_util.is_numeral(arg1, k) && k.is_int() && ((is_eq && k > rational(1)) || (!is_eq && k > rational(2)))) { if (is_eq || !k.is_even()) { new_args.push_back(arg0); From fedc6d475489f73eaa3317a6344d5e5ae03d61bf Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 5 Mar 2016 12:54:36 +0000 Subject: [PATCH 06/12] Fixed memory leak in fpa2bv tactic. --- src/tactic/fpa/fpa2bv_tactic.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index cfedb66d7..aa9277e39 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -93,9 +93,9 @@ class fpa2bv_tactic : public tactic { expr * sgn, *sig, *exp; expr_ref top_exp(m); m_conv.split_fp(new_curr, sgn, exp, sig); - m.mk_eq(sgn, m_conv.bu().mk_numeral(0, 1)); - m.mk_eq(exp, m_conv.bu().mk_numeral(-1, m_conv.bu().get_bv_size(exp))); - m.mk_eq(sig, m_conv.bu().mk_numeral(1, m_conv.bu().get_bv_size(sig))); + result.back()->assert_expr(m.mk_eq(sgn, m_conv.bu().mk_numeral(0, 1))); + result.back()->assert_expr(m.mk_eq(exp, m_conv.bu().mk_numeral(-1, m_conv.bu().get_bv_size(exp)))); + result.back()->assert_expr(m.mk_eq(sig, m_conv.bu().mk_numeral(1, m_conv.bu().get_bv_size(sig)))); } } } @@ -155,7 +155,7 @@ public: virtual void cleanup() { imp * d = alloc(imp, m_imp->m, m_params); - std::swap(d, m_imp); + std::swap(d, m_imp); dealloc(d); } From 09832ca807bfbcf6f1d3ba5bea848b47a9d58135 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 5 Mar 2016 13:58:28 +0000 Subject: [PATCH 07/12] Fixed static Windows binary build. --- scripts/mk_util.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 36f7b5ce3..870c63845 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2208,7 +2208,7 @@ def mk_config(): 'SLINK_FLAGS=/nologo /LDd\n' % static_opt) if VS_X64: config.write( - 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n' % extra_opt) + '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 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- %s %s\n' % (extra_opt, static_opt)) config.write( 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') @@ -2217,7 +2217,7 @@ def mk_config(): exit(1) else: config.write( - 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt) + 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2 %s %s\n' % (extra_opt, static_opt)) config.write( 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') @@ -2233,7 +2233,7 @@ def mk_config(): extra_opt = '%s /D _TRACE ' % extra_opt if VS_X64: config.write( - 'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP\n' % (GL, extra_opt)) + 'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP %s %s\n' % (GL, extra_opt, static_opt)) config.write( 'LINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n' 'SLINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n' % (LTCG, LTCG)) @@ -2242,7 +2242,7 @@ def mk_config(): exit(1) else: config.write( - 'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % (GL, extra_opt)) + 'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2 %s %s\n' % (GL, extra_opt, static_opt)) config.write( 'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n' % (LTCG, LTCG)) From 9dfc2bc61e73ab6498ff63786a360dd8947ae37c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 5 Mar 2016 16:47:08 +0000 Subject: [PATCH 08/12] Fixed memory leaks in fpa2bv converter. Fixes #480 --- src/ast/fpa/fpa2bv_converter.cpp | 117 +++++++++++++++++-------------- src/ast/fpa/fpa2bv_converter.h | 13 ---- src/tactic/fpa/fpa2bv_tactic.cpp | 1 - 3 files changed, 65 insertions(+), 66 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 40bb7efe8..0d90e1c5a 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -81,7 +81,7 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) { SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_INTERNAL_RM)); TRACE("fpa2bv", tout << "mk_eq_rm a=" << mk_ismt2_pp(a, m) << std::endl; - tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;); + tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;); m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), result); } @@ -113,9 +113,10 @@ void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * a result = m.mk_true(); for (unsigned i = 0; i < num; i++) { for (unsigned j = i+1; j < num; j++) { - expr_ref eq(m); + expr_ref eq(m), neq(m); mk_eq(args[i], args[j], eq); - m_simp.mk_and(result, m.mk_not(eq), result); + neq = m.mk_not(eq); + m_simp.mk_and(result, neq, result); } } } @@ -422,10 +423,11 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, if (log2(sbits + 2) < ebits + 2) { // cap the delta - expr_ref cap(m), cap_le_delta(m); + expr_ref cap(m), cap_le_delta(m), exp_delta_ext(m); cap = m_bv_util.mk_numeral(sbits + 2, ebits + 2); cap_le_delta = m_bv_util.mk_ule(cap, m_bv_util.mk_zero_extend(2, exp_delta)); - m_simp.mk_ite(cap_le_delta, cap, m_bv_util.mk_zero_extend(2, exp_delta), exp_delta); + exp_delta_ext = m_bv_util.mk_zero_extend(2, exp_delta); + m_simp.mk_ite(cap_le_delta, cap, exp_delta_ext, exp_delta); exp_delta = m_bv_util.mk_extract(ebits - 1, 0, exp_delta); dbg_decouple("fpa2bv_add_exp_cap", cap); } @@ -465,7 +467,7 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref eq_sgn(m); m_simp.mk_eq(c_sgn, d_sgn, eq_sgn); - // dbg_decouple("fpa2bv_add_eq_sgn", eq_sgn); + dbg_decouple("fpa2bv_add_eq_sgn", eq_sgn); TRACE("fpa2bv_add_core", tout << "EQ_SGN = " << mk_ismt2_pp(eq_sgn, m) << std::endl; ); // two extra bits for catching the overflow. @@ -478,11 +480,10 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, dbg_decouple("fpa2bv_add_c_sig", c_sig); dbg_decouple("fpa2bv_add_shifted_d_sig", shifted_d_sig); - expr_ref sum(m); - m_simp.mk_ite(eq_sgn, - m_bv_util.mk_bv_add(c_sig, shifted_d_sig), - m_bv_util.mk_bv_sub(c_sig, shifted_d_sig), - sum); + expr_ref sum(m), c_plus_d(m), c_minus_d(m); + c_plus_d = m_bv_util.mk_bv_add(c_sig, shifted_d_sig); + c_minus_d = m_bv_util.mk_bv_sub(c_sig, shifted_d_sig); + m_simp.mk_ite(eq_sgn, c_plus_d, c_minus_d, sum); SASSERT(is_well_sorted(m, sum)); @@ -594,7 +595,7 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args, c6 = y_is_zero; v6 = x; - // Actual addition. + //// Actual addition. unsigned ebits = m_util.get_ebits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range()); @@ -949,8 +950,11 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_div_res_sig_shift_amount", res_sig_shift_amount); expr_ref shift_cond(m); shift_cond = m_bv_util.mk_ule(res_sig_lz, m_bv_util.mk_numeral(1, sbits + 4)); - m_simp.mk_ite(shift_cond, res_sig, m_bv_util.mk_bv_shl(res_sig, res_sig_shift_amount), res_sig); - m_simp.mk_ite(shift_cond, res_exp, m_bv_util.mk_bv_sub(res_exp, m_bv_util.mk_extract(ebits+1, 0, res_sig_shift_amount)), res_exp); + expr_ref res_sig_shifted(m), res_exp_shifted(m); + res_sig_shifted = m_bv_util.mk_bv_shl(res_sig, res_sig_shift_amount); + res_exp_shifted = m_bv_util.mk_bv_sub(res_exp, m_bv_util.mk_extract(ebits + 1, 0, res_sig_shift_amount)); + m_simp.mk_ite(shift_cond, res_sig, res_sig_shifted, res_sig); + m_simp.mk_ite(shift_cond, res_exp, res_exp_shifted, res_exp); round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, v8); @@ -1374,8 +1378,9 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, // (x is 0) || (y is 0) -> z m_simp.mk_or(x_is_zero, y_is_zero, c7); - expr_ref ite_c(m); - m_simp.mk_and(z_is_zero, m.mk_not(rm_is_to_neg), ite_c); + expr_ref ite_c(m), rm_is_not_to_neg(m); + rm_is_not_to_neg = m.mk_not(rm_is_to_neg); + m_simp.mk_and(z_is_zero, rm_is_not_to_neg, ite_c); mk_ite(ite_c, pzero, z, v7); // else comes the fused multiplication. @@ -1512,11 +1517,10 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_fma_add_e_sig", e_sig); dbg_decouple("fpa2bv_fma_add_shifted_f_sig", shifted_f_sig); - expr_ref sum(m); - m_simp.mk_ite(eq_sgn, - m_bv_util.mk_bv_add(e_sig, shifted_f_sig), - m_bv_util.mk_bv_sub(e_sig, shifted_f_sig), - sum); + expr_ref sum(m), e_plus_f(m), e_minus_f(m); + e_plus_f = m_bv_util.mk_bv_add(e_sig, shifted_f_sig); + e_minus_f = m_bv_util.mk_bv_sub(e_sig, shifted_f_sig), + m_simp.mk_ite(eq_sgn, e_plus_f, e_minus_f, sum); SASSERT(is_well_sorted(m, sum)); @@ -1664,10 +1668,10 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_sqrt_e_is_odd", e_is_odd); dbg_decouple("fpa2bv_sqrt_real_exp", real_exp); - expr_ref sig_prime(m); - m_simp.mk_ite(e_is_odd, m_bv_util.mk_concat(a_sig, zero1), - m_bv_util.mk_concat(zero1, a_sig), - sig_prime); + expr_ref sig_prime(m), a_z(m), z_a(m); + a_z = m_bv_util.mk_concat(a_sig, zero1); + z_a = m_bv_util.mk_concat(zero1, a_sig); + m_simp.mk_ite(e_is_odd, a_z, z_a, sig_prime); SASSERT(m_bv_util.get_bv_size(sig_prime) == sbits+1); dbg_decouple("fpa2bv_sqrt_sig_prime", sig_prime); @@ -1696,21 +1700,22 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, SASSERT(m_bv_util.get_bv_size(S) == sbits + 5); SASSERT(m_bv_util.get_bv_size(T) == sbits + 6); - expr_ref t_lt_0(m); - m_simp.mk_eq(m_bv_util.mk_extract(sbits+5, sbits+5, T), one1, t_lt_0); + expr_ref t_lt_0(m), T_lsds5(m); + T_lsds5 = m_bv_util.mk_extract(sbits + 5, sbits + 5, T); + m_simp.mk_eq(T_lsds5, one1, t_lt_0); expr * or_args[2] = { Q, S }; - - m_simp.mk_ite(t_lt_0, Q, - m_bv_util.mk_bv_or(2, or_args), - Q); - m_simp.mk_ite(t_lt_0, m_bv_util.mk_concat(m_bv_util.mk_extract(sbits+3, 0, R), zero1), - m_bv_util.mk_extract(sbits+4, 0, T), - R); + expr_ref Q_or_S(m), R_shftd(m), T_lsds4(m); + Q_or_S = m_bv_util.mk_bv_or(2, or_args); + m_simp.mk_ite(t_lt_0, Q, Q_or_S, Q); + R_shftd = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits + 3, 0, R), zero1); + T_lsds4 = m_bv_util.mk_extract(sbits + 4, 0, T); + m_simp.mk_ite(t_lt_0, R_shftd, T_lsds4, R); } - expr_ref is_exact(m); - m_simp.mk_eq(R, m_bv_util.mk_numeral(0, sbits+5), is_exact); + expr_ref is_exact(m), zero_sbits5(m); + zero_sbits5 = m_bv_util.mk_numeral(0, sbits + 5); + m_simp.mk_eq(R, zero_sbits5, is_exact); dbg_decouple("fpa2bv_sqrt_is_exact", is_exact); expr_ref rest(m), last(m), q_is_odd(m), rest_ext(m); @@ -1719,10 +1724,10 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_sqrt_last", last); dbg_decouple("fpa2bv_sqrt_rest", rest); rest_ext = m_bv_util.mk_zero_extend(1, rest); - expr_ref sticky(m); - m_simp.mk_ite(is_exact, m_bv_util.mk_zero_extend(sbits+3, last), - m_bv_util.mk_numeral(1, sbits+4), - sticky); + expr_ref sticky(m), last_ext(m), one_sbits4(m); + last_ext = m_bv_util.mk_zero_extend(sbits + 3, last); + one_sbits4 = m_bv_util.mk_numeral(1, sbits + 4); + m_simp.mk_ite(is_exact, last_ext, one_sbits4, sticky); expr * or_args[2] = { rest_ext, sticky }; res_sig = m_bv_util.mk_bv_or(2, or_args); @@ -1813,8 +1818,11 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * mk_one(f, one_1, none); mk_ite(m.mk_eq(a_sgn, one_1), none, pone, xone); - m_simp.mk_eq(a_sig, m_bv_util.mk_numeral(fu().fm().m_powers2(sbits-1), sbits), t1); - m_simp.mk_eq(a_exp, m_bv_util.mk_numeral(-1, ebits), t2); + expr_ref pow_2_sbitsm1(m), m1(m); + pow_2_sbitsm1 = m_bv_util.mk_numeral(fu().fm().m_powers2(sbits - 1), sbits); + m1 = m_bv_util.mk_numeral(-1, ebits); + m_simp.mk_eq(a_sig, pow_2_sbitsm1, t1); + m_simp.mk_eq(a_exp, m1, t2); m_simp.mk_and(t1, t2, tie); dbg_decouple("fpa2bv_r2i_c42_tie", tie); @@ -1896,14 +1904,17 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * SASSERT(is_well_sorted(m, tie2_c)); SASSERT(is_well_sorted(m, v51)); - expr_ref c521(m), v52(m); - m_simp.mk_not(m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits+1)), c521); - m_simp.mk_and(c521, m.mk_eq(res_sgn, zero_1), c521); + expr_ref c521(m), v52(m), rem_eq_0(m), sgn_eq_zero(m); + rem_eq_0 = m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits + 1)); + sgn_eq_zero = m.mk_eq(res_sgn, zero_1); + m_simp.mk_not(rem_eq_0, c521); + m_simp.mk_and(c521, sgn_eq_zero, c521); m_simp.mk_ite(c521, div_p1, div, v52); - expr_ref c531(m), v53(m); - m_simp.mk_not(m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits+1)), c531); - m_simp.mk_and(c531, m.mk_eq(res_sgn, one_1), c531); + expr_ref c531(m), v53(m), sgn_eq_one(m); + sgn_eq_one = m.mk_eq(res_sgn, one_1); + m_simp.mk_not(rem_eq_0, c531); + m_simp.mk_and(c531, sgn_eq_one, c531); m_simp.mk_ite(c531, div_p1, div, v53); expr_ref c51(m), c52(m), c53(m); @@ -3377,9 +3388,10 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref zero_s = m_bv_util.mk_numeral(0, sbits); m_simp.mk_eq(zero_s, denormal_sig, is_sig_zero); - expr_ref lz_d(m); + expr_ref lz_d(m), norm_or_zero(m); mk_leading_zeros(denormal_sig, ebits, lz_d); - m_simp.mk_ite(m.mk_or(is_normal, is_sig_zero), zero_e, lz_d, lz); + norm_or_zero = m.mk_or(is_normal, is_sig_zero); + m_simp.mk_ite(norm_or_zero, zero_e, lz_d, lz); dbg_decouple("fpa2bv_unpack_lz", lz); expr_ref shift(m); @@ -3770,8 +3782,9 @@ void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_re dbg_decouple("fpa2bv_rnd_rm_is_to_pos", rm_is_to_pos); - expr_ref sgn_is_zero(m); - m_simp.mk_eq(sgn, m_bv_util.mk_numeral(0, 1), sgn_is_zero); + expr_ref sgn_is_zero(m), zero1(m); + zero1 = m_bv_util.mk_numeral(0, 1); + m_simp.mk_eq(sgn, zero1, sgn_is_zero); dbg_decouple("fpa2bv_rnd_sgn_is_zero", sgn_is_zero); expr_ref max_sig(m), max_exp(m), inf_sig(m), inf_exp(m); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 65d99d2c8..8dc3dc019 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -26,19 +26,6 @@ Notes: #include"bv_decl_plugin.h" #include"basic_simplifier_plugin.h" -struct func_decl_triple { - func_decl_triple () { f_sgn = 0; f_sig = 0; f_exp = 0; } - func_decl_triple (func_decl * sgn, func_decl * sig, func_decl * exp) - { - f_sgn = sgn; - f_sig = sig; - f_exp = exp; - } - func_decl * f_sgn; - func_decl * f_sig; - func_decl * f_exp; - }; - class fpa2bv_converter { protected: ast_manager & m; diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index aa9277e39..28597c6ec 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -91,7 +91,6 @@ class fpa2bv_tactic : public tactic { // that is (= e (fp #b0 #b1...1 #b0...01)), so that the value propagation // has a value to propagate. expr * sgn, *sig, *exp; - expr_ref top_exp(m); m_conv.split_fp(new_curr, sgn, exp, sig); result.back()->assert_expr(m.mk_eq(sgn, m_conv.bu().mk_numeral(0, 1))); result.back()->assert_expr(m.mk_eq(exp, m_conv.bu().mk_numeral(-1, m_conv.bu().get_bv_size(exp)))); From f34e15f2891710c079a829f2dd7d98fd698b42aa Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 5 Mar 2016 16:47:39 +0000 Subject: [PATCH 09/12] whitespace --- src/ast/fpa/fpa2bv_rewriter.h | 56 +++++++++++++++++------------------ 1 file changed, 28 insertions(+), 28 deletions(-) diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h index c3720421c..3842e673e 100644 --- a/src/ast/fpa/fpa2bv_rewriter.h +++ b/src/ast/fpa/fpa2bv_rewriter.h @@ -27,8 +27,8 @@ Notes: #include"fpa2bv_rewriter_params.hpp" struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { - ast_manager & m_manager; - expr_ref_vector m_out; + ast_manager & m_manager; + expr_ref_vector m_out; fpa2bv_converter & m_conv; sort_ref_vector m_bindings; @@ -49,7 +49,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { m_manager.register_plugin(s_bv, alloc(bv_decl_plugin)); } - ~fpa2bv_rewriter_cfg() { + ~fpa2bv_rewriter_cfg() { } void cleanup_buffers() { @@ -71,7 +71,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { updt_local_params(p); } - bool max_steps_exceeded(unsigned num_steps) const { + bool max_steps_exceeded(unsigned num_steps) const { cooperate("fpa2bv"); return num_steps > m_max_steps; } @@ -91,9 +91,9 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { if (m().is_eq(f)) { SASSERT(num == 2); - TRACE("fpa2bv_rw", tout << "(= " << mk_ismt2_pp(args[0], m()) << " " << + TRACE("fpa2bv_rw", tout << "(= " << mk_ismt2_pp(args[0], m()) << " " << mk_ismt2_pp(args[1], m()) << ")" << std::endl;); - SASSERT(m().get_sort(args[0]) == m().get_sort(args[1])); + SASSERT(m().get_sort(args[0]) == m().get_sort(args[1])); sort * ds = f->get_domain()[0]; if (m_conv.is_float(ds)) { m_conv.mk_eq(args[0], args[1], result); @@ -121,7 +121,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { } return BR_FAILED; } - + if (m_conv.is_float_family(f)) { switch (f->get_decl_kind()) { case OP_FPA_RM_NEAREST_TIES_TO_AWAY: @@ -129,7 +129,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FPA_RM_TOWARD_NEGATIVE: case OP_FPA_RM_TOWARD_POSITIVE: case OP_FPA_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE; - case OP_FPA_NUM: m_conv.mk_numeral(f, num, args, result); return BR_DONE; + case OP_FPA_NUM: m_conv.mk_numeral(f, num, args, result); return BR_DONE; case OP_FPA_PLUS_INF: m_conv.mk_pinf(f, result); return BR_DONE; case OP_FPA_MINUS_INF: m_conv.mk_ninf(f, result); return BR_DONE; case OP_FPA_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE; @@ -141,7 +141,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FPA_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE; case OP_FPA_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE; case OP_FPA_REM: m_conv.mk_rem(f, num, args, result); return BR_DONE; - case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE; + case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE; case OP_FPA_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE; case OP_FPA_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE; case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE; @@ -150,7 +150,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FPA_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE; case OP_FPA_LE: m_conv.mk_float_le(f, num, args, result); return BR_DONE; case OP_FPA_GE: m_conv.mk_float_ge(f, num, args, result); return BR_DONE; - case OP_FPA_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE; + case OP_FPA_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE; case OP_FPA_IS_NAN: m_conv.mk_is_nan(f, num, args, result); return BR_DONE; case OP_FPA_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE; case OP_FPA_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE; @@ -164,7 +164,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; - + case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_REWRITE_FULL; case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_REWRITE_FULL; @@ -174,10 +174,10 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FPA_INTERNAL_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE; case OP_FPA_INTERNAL_RM: - case OP_FPA_INTERNAL_BVWRAP: - case OP_FPA_INTERNAL_BVUNWRAP: + case OP_FPA_INTERNAL_BVWRAP: + case OP_FPA_INTERNAL_BVUNWRAP: case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: - case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return BR_FAILED; default: TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; @@ -207,8 +207,8 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { { TRACE("fpa2bv", tout << "pre_visit: " << mk_ismt2_pp(t, m()) << std::endl;); - if (is_quantifier(t)) { - quantifier * q = to_quantifier(t); + if (is_quantifier(t)) { + quantifier * q = to_quantifier(t); TRACE("fpa2bv", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;); sort_ref_vector new_bindings(m_manager); for (unsigned i = 0 ; i < q->get_num_decls(); i++) @@ -219,9 +219,9 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { return true; } - bool reduce_quantifier(quantifier * old_q, - expr * new_body, - expr * const * new_patterns, + bool reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, expr * const * new_no_patterns, expr_ref & result, proof_ref & result_pr) { @@ -241,7 +241,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { name_buffer.reset(); name_buffer << n << ".bv"; new_decl_names.push_back(symbol(name_buffer.c_str())); - new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits+ebits)); + new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits+ebits)); } else { new_decl_sorts.push_back(s); @@ -252,18 +252,18 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(), old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns); result_pr = 0; - m_bindings.shrink(old_sz); - TRACE("fpa2bv", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " << + m_bindings.shrink(old_sz); + TRACE("fpa2bv", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " << mk_ismt2_pp(old_q->get_expr(), m()) << std::endl << " new body: " << mk_ismt2_pp(new_body, m()) << std::endl; - tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;); + tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;); return true; } - bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { + bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { if (t->get_idx() >= m_bindings.size()) return false; - // unsigned inx = m_bindings.size() - t->get_idx() - 1; + // unsigned inx = m_bindings.size() - t->get_idx() - 1; expr_ref new_exp(m()); sort * s = t->get_sort(); @@ -275,14 +275,14 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits)); m_conv.mk_fp(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var), m_conv.bu().mk_extract(ebits - 1, 0, new_var), - m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var), + m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var), new_exp); } else new_exp = m().mk_var(t->get_idx(), s); result = new_exp; - result_pr = 0; + result_pr = 0; TRACE("fpa2bv", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;); return true; } @@ -293,7 +293,7 @@ template class rewriter_tpl; struct fpa2bv_rewriter : public rewriter_tpl { fpa2bv_rewriter_cfg m_cfg; fpa2bv_rewriter(ast_manager & m, fpa2bv_converter & c, params_ref const & p): - rewriter_tpl(m, m.proofs_enabled(), m_cfg), + rewriter_tpl(m, m.proofs_enabled(), m_cfg), m_cfg(m, c, p) { } }; From 03a8ef27958e369a312c55a93fc8518a9f4a6805 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 5 Mar 2016 17:14:19 +0000 Subject: [PATCH 10/12] Fixed non-Windows preprocessor options. Fixes #463 --- scripts/mk_util.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 870c63845..f003dd12c 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2351,7 +2351,9 @@ def mk_config(): LDFLAGS = '%s -m32' % LDFLAGS SLIBFLAGS = '%s -m32' % SLIBFLAGS if DEBUG_MODE: - CPPFLAGS = '%s -DZ3DEBUG' % CPPFLAGS + CPPFLAGS = '%s -DZ3DEBUG -D_DEBUG' % CPPFLAGS + else: + CPPFLAGS = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS if TRACE or DEBUG_MODE: CPPFLAGS = '%s -D_TRACE' % CPPFLAGS config.write('PREFIX=%s\n' % PREFIX) @@ -3471,7 +3473,7 @@ def mk_vs_proj_cl_compile(f, name, components, debug): if debug: f.write(' WIN32;_DEBUG;Z3DEBUG;_TRACE;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)\n') else: - f.write(' WIN32;_NDEBUG;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)\n') + f.write(' WIN32;NDEBUG;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)\n') if VS_PAR: f.write(' false\n') f.write(' true\n') From 8abedbf389fc313ee856b339becf8b5398637444 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 5 Mar 2016 17:55:27 +0000 Subject: [PATCH 11/12] whitespace --- src/api/z3_api.h | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 55a1b93d9..15bcedcb0 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -62,7 +62,7 @@ DEFINE_TYPE(Z3_rcf_num); - \c Z3_constructor: type constructor for a (recursive) datatype. - \c Z3_constructor_list: list of constructors for a (recursive) datatype. - \c Z3_params: parameter set used to configure many components such as: simplifiers, tactics, solvers, etc. - - \c Z3_param_descrs: provides a collection of parameter names, their types, default values and documentation strings. Solvers, tactics, and other objects accept different collection of parameters. + - \c Z3_param_descrs: provides a collection of parameter names, their types, default values and documentation strings. Solvers, tactics, and other objects accept different collection of parameters. - \c Z3_model: model for the constraints asserted into the logical context. - \c Z3_func_interp: interpretation of a function in a model. - \c Z3_func_entry: representation of the value of a \c Z3_func_interp at a particular point. @@ -1129,7 +1129,7 @@ typedef enum { Z3_OP_SEQ_EXTRACT, Z3_OP_SEQ_REPLACE, Z3_OP_SEQ_AT, - Z3_OP_SEQ_LENGTH, + Z3_OP_SEQ_LENGTH, Z3_OP_SEQ_INDEX, Z3_OP_SEQ_TO_RE, Z3_OP_SEQ_IN_RE, @@ -3185,11 +3185,11 @@ extern "C" { def_API('Z3_is_string', BOOL, (_in(CONTEXT), _in(AST))) */ - Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s); + Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s); /** \brief Retrieve the string constant stored in \c s. - + \pre Z3_is_string(c, s) def_API('Z3_get_string' ,STRING ,(_in(CONTEXT), _in(AST))) @@ -3285,7 +3285,7 @@ extern "C" { def_API('Z3_mk_seq_index' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset); - + /** \brief Create a regular expression that accepts the sequence \c seq. @@ -4429,8 +4429,8 @@ extern "C" { Provides an interface to the AST simplifier used by Z3. It returns an AST object which is equal to the argument. - The returned AST is simplified using algebraic simplificaiton rules, - such as constant propagation (propagating true/false over logical connectives). + The returned AST is simplified using algebraic simplificaiton rules, + such as constant propagation (propagating true/false over logical connectives). def_API('Z3_simplify', AST, (_in(CONTEXT), _in(AST))) */ From a2ecb19d0384e20446138213c1ac7d27081efb94 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 5 Mar 2016 17:58:32 +0000 Subject: [PATCH 12/12] Added hash-consing remarks to mk_context and mk_context_rc. Fixes #452 --- src/api/z3_api.h | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 15bcedcb0..5c7a819da 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1457,7 +1457,7 @@ extern "C" { /*@{*/ /** - \deprecated + \deprecated \brief Create a context using the given configuration. After a context is created, the configuration cannot be changed, @@ -1474,6 +1474,11 @@ extern "C" { Z3_solver, Z3_func_interp have to be managed by the caller. Their reference counts are not handled by the context. + Further remarks: + - Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are Z3_ast's. + - Z3 uses hash-consing, i.e., when the same Z3_ast is created twice, + Z3 will return the same pointer twice. + \sa Z3_del_context def_API('Z3_mk_context', CONTEXT, (_in(CONFIG),)) @@ -1492,11 +1497,13 @@ extern "C" { anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD. - Remark: Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are - Z3_ast's. + Remarks: - After a context is created, the configuration cannot be changed. - All main interaction with Z3 happens in the context of a \c Z3_context. + - Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are Z3_ast's. + - After a context is created, the configuration cannot be changed. + - All main interaction with Z3 happens in the context of a \c Z3_context. + - Z3 uses hash-consing, i.e., when the same Z3_ast is created twice, + Z3 will return the same pointer twice. def_API('Z3_mk_context_rc', CONTEXT, (_in(CONFIG),)) */