From 274f2b7a5d40051c4af4791e157544bfc9a74926 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 Mar 2015 11:22:09 -0700 Subject: [PATCH 01/12] Move to MIT License --- LICENSE.txt | 46 ++++++---------------------------------------- 1 file changed, 6 insertions(+), 40 deletions(-) diff --git a/LICENSE.txt b/LICENSE.txt index 72d85818f..91c8070d0 100644 --- a/LICENSE.txt +++ b/LICENSE.txt @@ -1,41 +1,7 @@ -Microsoft Research License Agreement -Non-Commercial Use Only Z3 -_____________________________________________________________________ -This Microsoft Research License Agreement, including all exhibits ("MSR-LA") is a legal agreement between you and Microsoft Corporation ("Microsoft" or "we") for the data identified above, which may include associated materials, text or speech files, associated media and "online" or electronic documentation and any updates we provide in our discretion (together, the "Software"). - -By installing, copying, or otherwise using this Software, you agree to be bound by the terms of this MSR-LA. If you do not agree, do not install copy or use the Software. The Software is protected by copyright and other intellectual property laws and is licensed, not sold. - -SCOPE OF RIGHTS: -You may use, copy, reproduce, and distribute this Software for any non-commercial purpose, subject to the restrictions in this MSR-LA. Some purposes which can be non-commercial are teaching, academic research, public demonstrations and personal experimentation. You may also distribute this Software with books or other teaching materials, or publish the Software on websites, that are intended to teach the use of the Software for academic or other non-commercial purposes. - -You may not use or distribute this Software or any derivative works in any form for commercial purposes. Examples of commercial purposes would be running business operations, licensing, leasing, or selling the Software, distributing the Software for use with commercial products, using the Software in the creation or use of commercial products or any other activity which purpose is to procure a commercial gain to you or others. - -You may create derivative works of the Software source code and distribute the modified Software solely for non-commercial academic purposes, as provided herein. If you distribute the Software or any derivative works of the Software, you will distribute them under the same terms and conditions as in this license, and you will not grant other rights to the Software or derivative works that are different from those provided by this MSR-LA. - -If you have created derivative works of the Software, and distribute such derivative works, you will cause the modified files to carry prominent notices so that recipients know that they are not receiving the original Software. Such notices must state: (i) that you have changed the Software; and (ii) the date of any changes. -In return, we simply require that you agree: - -1. That you will not remove any copyright or other notices from the Software. - -2. That if any of the Software is in binary format, you will not attempt to modify such portions of the Software, or to reverse engineer or decompile them, except and only to the extent authorized by applicable law. - -3. That Microsoft is granted back, without any restrictions or limitations, a non-exclusive, perpetual, irrevocable, royalty-free, assignable and sub-licensable license, to reproduce, publicly perform or display, install, use, modify, post, distribute, make and have made, sell and transfer your modifications to and/or derivative works of the Software source code or data, for any purpose. - -4. That any feedback about the Software provided by you to us is voluntarily given, and Microsoft shall be free to use the feedback as it sees fit without obligation or restriction of any kind, even if the feedback is designated by you as confidential. - -5. THAT THE SOFTWARE COMES "AS IS", WITH NO WARRANTIES. THIS MEANS NO EXPRESS, IMPLIED OR STATUTORY WARRANTY, INCLUDING WITHOUT LIMITATION, WARRANTIES OF MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE, ANY WARRANTY AGAINST INTERFERENCE WITH YOUR ENJOYMENT OF THE SOFTWARE OR ANY WARRANTY OF TITLE OR NON-INFRINGEMENT. THERE IS NO WARRANTY THAT THIS SOFTWARE WILL FULFILL ANY OF YOUR PARTICULAR PURPOSES OR NEEDS. ALSO, YOU MUST PASS THIS DISCLAIMER ON WHENEVER YOU DISTRIBUTE THE SOFTWARE OR DERIVATIVE WORKS. - -6. THAT NEITHER MICROSOFT NOR ANY CONTRIBUTOR TO THE SOFTWARE WILL BE LIABLE FOR ANY DAMAGES RELATED TO THE SOFTWARE OR THIS MSR-LA, INCLUDING DIRECT, INDIRECT, SPECIAL, CONSEQUENTIAL OR INCIDENTAL DAMAGES, TO THE MAXIMUM EXTENT THE LAW PERMITS, NO MATTER WHAT LEGAL THEORY IT IS BASED ON. ALSO, YOU MUST PASS THIS LIMITATION OF LIABILITY ON WHENEVER YOU DISTRIBUTE THE SOFTWARE OR DERIVATIVE WORKS. - -7. That we have no duty of reasonable care or lack of negligence, and we are not obligated to (and will not) provide technical support for the Software. - -8. That if you breach this MSR-LA or if you sue anyone over patents that you think may apply to or read on the Software or anyone's use of the Software, this MSR-LA (and your license and rights obtained herein) terminate automatically. Upon any such termination, you shall destroy all of your copies of the Software immediately. Sections 3, 4, 5, 6, 7, 8, 11 and 12 of this MSR-LA shall survive any termination of this MSR-LA. - -9. That the patent rights, if any, granted to you in this MSR-LA only apply to the Software, not to any derivative works you make. - -10. That the Software may be subject to U.S. export jurisdiction at the time it is licensed to you, and it may be subject to additional export or import laws in other places. You agree to comply with all such laws and regulations that may apply to the Software after delivery of the Software to you. - -11. That all rights not expressly granted to you in this MSR-LA are reserved. - -12. That this MSR-LA shall be construed and controlled by the laws of the State of Washington, USA, without regard to conflicts of law. If any provision of this MSR-LA shall be deemed unenforceable or contrary to law, the rest of this MSR-LA shall remain in full effect and interpreted in an enforceable manner that most nearly captures the intent of the original language. +Copyright (c) Microsoft Corporation +All rights reserved. +MIT License +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the ""Software""), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: +The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. +THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. From 3b16cfbd4449bb5fd3becb527d4545ef98757e09 Mon Sep 17 00:00:00 2001 From: NikolajBjorner Date: Thu, 26 Mar 2015 11:31:34 -0700 Subject: [PATCH 02/12] Update README change reference to license --- README | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/README b/README index 074abd2a3..d7f441d64 100644 --- a/README +++ b/README @@ -1,6 +1,5 @@ Z3 is a theorem prover from Microsoft Research. -Z3 is licensed under MSR-LA (Microsoft Research License Agreement). -See http://z3.codeplex.com/license for more information about this license. +Z3 is licensed under the MIT license. Z3 can be built using Visual Studio Command Prompt and make/g++. 1) Building Z3 on Windows using Visual Studio Command Prompt @@ -42,4 +41,4 @@ Remark: clang does not support OpenMP yet. make -To clean Z3 you can delete the build directory and run the mk_make.py script again. \ No newline at end of file +To clean Z3 you can delete the build directory and run the mk_make.py script again. From e456af142e5e51ab80e5cf8f49a1f09a32368a5d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Mar 2015 02:42:08 -0700 Subject: [PATCH 03/12] fix complex.py example with power prompted by suggestion of smilliken Signed-off-by: Nikolaj Bjorner --- examples/python/complex/complex.py | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/examples/python/complex/complex.py b/examples/python/complex/complex.py index a2de4a6cc..5d6283745 100644 --- a/examples/python/complex/complex.py +++ b/examples/python/complex/complex.py @@ -46,6 +46,15 @@ class ComplexExpr: other = _to_complex(other) return ComplexExpr(other.r*self.r - other.i*self.i, other.i*self.r + other.r*self.i) + def __pow__(self, k): + if k == 0: + return ComplexExpr(1, 0) + if k == 1: + return self + if k < 0: + return (self ** (-k)).inv() + return reduce(lambda x, y: x * y, [self for _ in xrange(k)], ComplexExpr(1, 0)) + def inv(self): den = self.r*self.r + self.i*self.i return ComplexExpr(self.r/den, -self.i/den) @@ -104,4 +113,5 @@ print(s.model()) s.add(x.i != 1) print(s.check()) # print(s.model()) -print (3 + I)^2/(5 - I) +print ((3 + I) ** 2)/(5 - I) +print ((3 + I) ** -3)/(5 - I) From 4bfe20647bd17092179dbed8f9390017456652ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Mar 2015 02:43:21 -0700 Subject: [PATCH 04/12] remove tab in mk_util.py Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 0f4fdb216..e13bbada3 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -565,7 +565,7 @@ def parse_options(): if not IS_WINDOWS: raise MKException('x64 compilation mode can only be specified when using Visual Studio') VS_X64 = True - elif opt in ('--x86'): + elif opt in ('--x86'): LINUX_X64=False elif opt in ('-h', '--help'): display_help(0) From 690eb8eaca3e7d79d5379cf6ab5ab4682e480c00 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 29 Mar 2015 13:31:44 +0100 Subject: [PATCH 05/12] Bugfix for fp.isSubnormal. Fixes #10 --- src/ast/fpa/fpa2bv_converter.cpp | 9 +++++++-- src/util/mpf.cpp | 2 +- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 89072a795..738422b89 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2952,11 +2952,16 @@ void fpa2bv_converter::mk_is_pzero(expr * e, expr_ref & result) { } void fpa2bv_converter::mk_is_denormal(expr * e, expr_ref & result) { - expr * sgn, * sig, * exp; + expr * sgn, *sig, *exp; split_fp(e, sgn, exp, sig); - expr_ref zero(m); + + expr_ref zero(m), zexp(m), is_zero(m), n_is_zero(m); zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(exp)); m_simp.mk_eq(exp, zero, result); + m_simp.mk_eq(exp, zero, zexp); + mk_is_zero(e, is_zero); + m_simp.mk_not(is_zero, n_is_zero); + m_simp.mk_and(n_is_zero, zexp, result); } void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) { diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 4e452b1e8..d28395195 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1350,7 +1350,7 @@ bool mpf_manager::is_ninf(mpf const & x) { } bool mpf_manager::is_normal(mpf const & x) { - return !has_bot_exp(x) && !has_top_exp(x); + return !is_zero(x) && has_bot_exp(x); } bool mpf_manager::is_denormal(mpf const & x) { From 0ed16c09f9dbfed1c80ae08f7303a9d67ffa12bd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 29 Mar 2015 13:57:11 +0100 Subject: [PATCH 06/12] Bugfix for fp.isNegative. Fixes #13 --- src/ast/fpa/fpa2bv_converter.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 738422b89..f049750c3 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1837,7 +1837,10 @@ void fpa2bv_converter::mk_is_subnormal(func_decl * f, unsigned num, expr * const void fpa2bv_converter::mk_is_negative(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); - mk_is_neg(args[0], result); + expr_ref t1(m), t2(m); + mk_is_nan(args[0], t1); + mk_is_neg(args[0], t2); + result = m.mk_and(m.mk_not(t1), t2); TRACE("fpa2bv_is_negative", tout << "result = " << mk_ismt2_pp(result, m) << std::endl;); } From 5911f788c3eba23e3d1f1aba28c64af218cdd028 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 29 Mar 2015 14:39:47 +0100 Subject: [PATCH 07/12] Improved translation from reals to floats (fp.to_real). Fixes #14 --- src/ast/fpa/fpa2bv_converter.cpp | 58 ++++++++++++++++++++++++++++++++ 1 file changed, 58 insertions(+) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index f049750c3..06662e205 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2107,6 +2107,64 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * mk_fp(sgn, e, s, result); } + else if (m_util.au().is_numeral(x)) { + rational q; + bool is_int; + m_util.au().is_numeral(x, q, is_int); + + expr_ref rm_nta(m), rm_nte(m), rm_tp(m), rm_tn(m), rm_tz(m); + mk_is_rm(rm, BV_RM_TIES_TO_AWAY, rm_nta); + mk_is_rm(rm, BV_RM_TIES_TO_EVEN, rm_nte); + mk_is_rm(rm, BV_RM_TO_POSITIVE, rm_tp); + mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_tn); + mk_is_rm(rm, BV_RM_TO_ZERO, rm_tz); + + scoped_mpf v_nta(m_mpf_manager), v_nte(m_mpf_manager), v_tp(m_mpf_manager); + scoped_mpf v_tn(m_mpf_manager), v_tz(m_mpf_manager); + m_util.fm().set(v_nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, q.to_mpq()); + m_util.fm().set(v_nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, q.to_mpq()); + m_util.fm().set(v_tp, ebits, sbits, MPF_ROUND_TOWARD_POSITIVE, q.to_mpq()); + m_util.fm().set(v_tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, q.to_mpq()); + m_util.fm().set(v_tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, q.to_mpq()); + + expr_ref v1(m), v2(m), v3(m), v4(m); + + expr_ref sgn(m), s(m), e(m), unbiased_exp(m); + sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nta)) ? 1 : 0, 1); + s = m_bv_util.mk_numeral(m_util.fm().sig(v_nta), sbits - 1); + unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nta), ebits); + mk_bias(unbiased_exp, e); + mk_fp(sgn, e, s, v1); + + sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nte)) ? 1 : 0, 1); + s = m_bv_util.mk_numeral(m_util.fm().sig(v_nte), sbits - 1); + unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nte), ebits); + mk_bias(unbiased_exp, e); + mk_fp(sgn, e, s, v2); + + sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1); + s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1); + unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits); + mk_bias(unbiased_exp, e); + mk_fp(sgn, e, s, v3); + + sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tn)) ? 1 : 0, 1); + s = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1); + unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tn), ebits); + mk_bias(unbiased_exp, e); + mk_fp(sgn, e, s, v4); + + sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1); + s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1); + unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits); + mk_bias(unbiased_exp, e); + + mk_fp(sgn, e, s, result); + mk_ite(rm_tn, v4, result, result); + mk_ite(rm_tp, v3, result, result); + mk_ite(rm_nte, v2, result, result); + mk_ite(rm_nta, v1, result, result); + } else { bv_util & bu = m_bv_util; arith_util & au = m_arith_util; From 0f03cd2ae0ccc1ec96f4b51a398cfd69d163cd2d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 29 Mar 2015 15:49:03 +0100 Subject: [PATCH 08/12] Enabled test for OpenMP in Windows (for old and express versions of visual studio). Fixes #8 --- scripts/mk_util.py | 25 +++++++++++++++++-------- 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index e13bbada3..99df6aa4d 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -226,7 +226,10 @@ def test_openmp(cc): t = TempFile('tstomp.cpp') t.add('#include\nint main() { return omp_in_parallel() ? 1 : 0; }\n') t.commit() - return exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '-fopenmp']) == 0 + if IS_WINDOWS: + return exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '/openmp']) == 0 + else: + return exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '-fopenmp']) == 0 def find_jni_h(path): for root, dirs, files in os.walk(path): @@ -1706,21 +1709,26 @@ def mk_config(): 'SLINK_OUT_FLAG=/Fe\n' 'OS_DEFINES=/D _WINDOWS\n') extra_opt = '' + HAS_OMP = test_openmp('cl') + if HAS_OMP: + extra_opt = ' /openmp' + else: + extra_opt = ' -D_NO_OMP_' if GIT_HASH: - extra_opt = '%s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH) + extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH) if DEBUG_MODE: config.write( 'LINK_FLAGS=/nologo /MDd\n' 'SLINK_FLAGS=/nologo /LDd\n') if not VS_X64: config.write( - 'CXXFLAGS=/c /GL /Zi /nologo /openmp /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 /GL /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) config.write( 'LINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'SLINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') else: config.write( - 'CXXFLAGS=/c /GL /Zi /nologo /openmp /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 /GL /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) config.write( 'LINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'SLINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') @@ -1730,16 +1738,16 @@ def mk_config(): 'LINK_FLAGS=/nologo /MD\n' 'SLINK_FLAGS=/nologo /LD\n') if TRACE: - extra_opt = '%s /D _TRACE' % extra_opt + extra_opt = '%s /D _TRACE ' % extra_opt if not VS_X64: config.write( - 'CXXFLAGS=/nologo /c /GL /Zi /openmp /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' % extra_opt) + 'CXXFLAGS=/nologo /c /GL /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' % extra_opt) config.write( 'LINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'SLINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') else: config.write( - 'CXXFLAGS=/c /GL /Zi /nologo /openmp /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' % extra_opt) + 'CXXFLAGS=/c /GL /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' % extra_opt) config.write( 'LINK_EXTRA_FLAGS=/link /LTCG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n' 'SLINK_EXTRA_FLAGS=/link /LTCG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n') @@ -1747,7 +1755,8 @@ def mk_config(): # End of Windows VS config.mk if is_verbose(): print('64-bit: %s' % is64()) - if is_java_enabled(): + print('OpenMP: %s' % HAS_OMP) + if is_java_enabled(): print('JNI Bindings: %s' % JNI_HOME) print('Java Compiler: %s' % JAVAC) if is_ml_enabled(): From 99ea0a8c19e04c7daf0f2649cd1e4826f64dd722 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 30 Mar 2015 08:02:57 +0100 Subject: [PATCH 09/12] Bugfix for mpf is_normal. Fixes #17 --- src/util/mpf.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index d28395195..c96ba594e 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1350,11 +1350,11 @@ bool mpf_manager::is_ninf(mpf const & x) { } bool mpf_manager::is_normal(mpf const & x) { - return !is_zero(x) && has_bot_exp(x); + return !(has_top_exp(x) || is_denormal(x)); } bool mpf_manager::is_denormal(mpf const & x) { - return has_bot_exp(x); + return !is_zero(x) && has_bot_exp(x); } bool mpf_manager::is_int(mpf const & x) { From 1d9c9bcf7ac074b965bb862cc8d23c6f6ed7b92a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 31 Mar 2015 19:51:42 +0200 Subject: [PATCH 10/12] Made the InterpolationContext public. Fixes #20 --- src/api/dotnet/InterpolationContext.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/dotnet/InterpolationContext.cs b/src/api/dotnet/InterpolationContext.cs index b5ada1bbd..0f516c0b0 100644 --- a/src/api/dotnet/InterpolationContext.cs +++ b/src/api/dotnet/InterpolationContext.cs @@ -13,7 +13,7 @@ namespace Microsoft.Z3 /// For more information on interpolation please refer /// too the C/C++ API, which is well documented. [ContractVerification(true)] - class InterpolationContext : Context + public class InterpolationContext : Context { /// From b47851d7da0965e24e33c5c1d532776618e0698d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 2 Apr 2015 16:51:30 +0100 Subject: [PATCH 11/12] Made GetInterpolant and ComputeInterpolant public in Java and .NET. Fixes Codeplex discussion #616450 --- src/api/dotnet/ASTVector.cs | 2 +- src/api/dotnet/InterpolationContext.cs | 4 ++-- src/api/java/ASTVector.java | 2 +- src/api/java/InterpolationContext.java | 4 ++-- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/api/dotnet/ASTVector.cs b/src/api/dotnet/ASTVector.cs index 597b1decc..b70ff13b6 100644 --- a/src/api/dotnet/ASTVector.cs +++ b/src/api/dotnet/ASTVector.cs @@ -25,7 +25,7 @@ namespace Microsoft.Z3 /// /// Vectors of ASTs. /// - internal class ASTVector : Z3Object + public class ASTVector : Z3Object { /// /// The size of the vector diff --git a/src/api/dotnet/InterpolationContext.cs b/src/api/dotnet/InterpolationContext.cs index 0f516c0b0..d54c8f634 100644 --- a/src/api/dotnet/InterpolationContext.cs +++ b/src/api/dotnet/InterpolationContext.cs @@ -47,7 +47,7 @@ namespace Microsoft.Z3 /// For more information on interpolation please refer /// too the function Z3_get_interpolant in the C/C++ API, which is /// well documented. - Expr[] GetInterpolant(Expr pf, Expr pat, Params p) + public Expr[] GetInterpolant(Expr pf, Expr pat, Params p) { Contract.Requires(pf != null); Contract.Requires(pat != null); @@ -72,7 +72,7 @@ namespace Microsoft.Z3 /// For more information on interpolation please refer /// too the function Z3_compute_interpolant in the C/C++ API, which is /// well documented. - Z3_lbool ComputeInterpolant(Expr pat, Params p, out ASTVector interp, out Model model) + public Z3_lbool ComputeInterpolant(Expr pat, Params p, out ASTVector interp, out Model model) { Contract.Requires(pat != null); Contract.Requires(p != null); diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java index 48c079ecc..03e1b0a98 100644 --- a/src/api/java/ASTVector.java +++ b/src/api/java/ASTVector.java @@ -20,7 +20,7 @@ package com.microsoft.z3; /** * Vectors of ASTs. **/ -class ASTVector extends Z3Object +public class ASTVector extends Z3Object { /** * The size of the vector diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 4c20ec6ae..91aac7f93 100644 --- a/src/api/java/InterpolationContext.java +++ b/src/api/java/InterpolationContext.java @@ -73,7 +73,7 @@ public class InterpolationContext extends Context * well documented. * @throws Z3Exception **/ - Expr[] GetInterpolant(Expr pf, Expr pat, Params p) throws Z3Exception + public Expr[] GetInterpolant(Expr pf, Expr pat, Params p) throws Z3Exception { checkContextMatch(pf); checkContextMatch(pat); @@ -94,7 +94,7 @@ public class InterpolationContext extends Context * well documented. * @throws Z3Exception **/ - Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model) throws Z3Exception + public Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model) throws Z3Exception { checkContextMatch(pat); checkContextMatch(p); From d01c3491a67d4a06ea1f6e57d385f04914529317 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Apr 2015 10:28:30 -0700 Subject: [PATCH 12/12] simplify with caching, but without expanding number of asserted formulas. Bug reported by Heizmann, codeplex issue 197 Signed-off-by: Nikolaj Bjorner --- src/smt/asserted_formulas.cpp | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index faf5ce0ef..c02c6760a 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -603,11 +603,11 @@ void asserted_formulas::propagate_values() { proof_ref_vector new_prs1(m_manager); expr_ref_vector new_exprs2(m_manager); proof_ref_vector new_prs2(m_manager); - unsigned i = 0; unsigned sz = m_asserted_formulas.size(); - for (; i < sz; i++) { + for (unsigned i = 0; i < sz; i++) { expr * n = m_asserted_formulas.get(i); proof * pr = m_asserted_formula_prs.get(i, 0); + TRACE("simplifier", tout << mk_pp(n, m_manager) << "\n";); if (m_manager.is_eq(n)) { expr * lhs = to_app(n)->get_arg(0); expr * rhs = to_app(n)->get_arg(1); @@ -615,9 +615,11 @@ void asserted_formulas::propagate_values() { if (m_manager.is_value(lhs)) std::swap(lhs, rhs); if (!m_manager.is_value(lhs) && !m_simplifier.is_cached(lhs)) { - new_exprs1.push_back(n); - if (m_manager.proofs_enabled()) - new_prs1.push_back(pr); + if (i >= m_asserted_qhead) { + new_exprs1.push_back(n); + if (m_manager.proofs_enabled()) + new_prs1.push_back(pr); + } TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\n";); m_simplifier.cache_result(lhs, rhs, pr); found = true; @@ -625,9 +627,11 @@ void asserted_formulas::propagate_values() { } } } - new_exprs2.push_back(n); - if (m_manager.proofs_enabled()) - new_prs2.push_back(pr); + if (i >= m_asserted_qhead) { + new_exprs2.push_back(n); + if (m_manager.proofs_enabled()) + new_prs2.push_back(pr); + } } TRACE("propagate_values", tout << "found: " << found << "\n";); // If C is not empty, then reduce R using the updated simplifier cache with entries