From 44105b7aeb8ec6e85dfba23321eaa6838695d1f3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Sep 2015 08:32:57 -0700 Subject: [PATCH 1/4] reduce verbosity level of error message when equivalence checking fails Signed-off-by: Nikolaj Bjorner --- src/muz/rel/check_relation.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/muz/rel/check_relation.cpp b/src/muz/rel/check_relation.cpp index 534a66284..7c6dac5e4 100644 --- a/src/muz/rel/check_relation.cpp +++ b/src/muz/rel/check_relation.cpp @@ -430,12 +430,12 @@ namespace datalog { IF_VERBOSE(3, verbose_stream() << objective << " verified\n";); } else if (res == l_true) { - IF_VERBOSE(3, verbose_stream() << "NOT verified " << res << "\n"; + IF_VERBOSE(0, verbose_stream() << "NOT verified " << res << "\n"; verbose_stream() << mk_pp(fml1, m) << "\n"; verbose_stream() << mk_pp(fml2, m) << "\n"; verbose_stream().flush(); ); - throw 0; + throw default_exception("operation was not verified"); } } From 45cfb80d1403e6dd59c0cb86d5b293933ec1b1d2 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 10 Sep 2015 09:01:44 +0100 Subject: [PATCH 2/4] tentatively fix another issue with char signedness as reported in issue #210 Signed-off-by: Nuno Lopes --- src/smt/smt_context.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index fb20a81c6..231b73fe3 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -157,7 +157,7 @@ namespace smt { u_map m_expr2bool_var; #endif ptr_vector m_bool_var2expr; // bool_var -> expr - char_vector m_assignment; //!< mapping literal id -> assignment lbool + signed_char_vector m_assignment; //!< mapping literal id -> assignment lbool vector m_watches; //!< per literal vector m_lit_occs; //!< index for backward subsumption svector m_bdata; //!< mapping bool_var -> data From 980a0e97f8bea58b72a5cc064f406b9cfabfbee1 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 10 Sep 2015 09:32:45 +0100 Subject: [PATCH 3/4] Python 3 compat for z3.py; patch by Sarah Winkler Signed-off-by: Nuno Lopes --- src/api/python/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index e4394e9b2..f561f82d7 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -6495,7 +6495,7 @@ class Optimize(Z3PPObject): return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize)) def reason_unknown(self): - """Return a string that describes why the last `check()` returned `unknown`.""" + """Return a string that describes why the last `check()` returned `unknown`.""" return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize) def model(self): From 25f75b60fefd5c8be1f905bc3aa2f8c844732a3d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 10 Sep 2015 11:37:06 +0100 Subject: [PATCH 4/4] Bugfix for fp.mul and fp.fma for small numbers of e/s bits. Fixes #215. --- src/ast/rewriter/fpa_rewriter.cpp | 2 +- src/util/mpf.cpp | 19 ++++++++++++++----- src/util/mpf.h | 2 +- 3 files changed, 16 insertions(+), 7 deletions(-) diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 07a39bcae..1d12621cd 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -468,7 +468,7 @@ br_status fpa_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg scoped_mpf v2(m_fm), v3(m_fm), v4(m_fm); if (m_util.is_numeral(arg2, v2) && m_util.is_numeral(arg3, v3) && m_util.is_numeral(arg4, v4)) { scoped_mpf t(m_fm); - m_fm.fused_mul_add(rm, v2, v3, v4, t); + m_fm.fma(rm, v2, v3, v4, t); result = m_util.mk_value(t); return BR_DONE; } diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 57e5b56b5..36974519c 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -638,7 +638,11 @@ void mpf_manager::mul(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf & // Remove the extra bits, keeping a sticky bit. scoped_mpz sticky_rem(m_mpz_manager); - m_mpz_manager.machine_div_rem(o.significand, m_powers2(x.sbits-4), o.significand, sticky_rem); + if (o.sbits >= 4) + m_mpz_manager.machine_div_rem(o.significand, m_powers2(o.sbits - 4), o.significand, sticky_rem); + else + m_mpz_manager.mul2k(o.significand, 4-o.sbits, o.significand); + if (!m_mpz_manager.is_zero(sticky_rem) && m_mpz_manager.is_even(o.significand)) m_mpz_manager.inc(o.significand); @@ -728,7 +732,7 @@ void mpf_manager::div(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf & } } -void mpf_manager::fused_mul_add(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf const &z, mpf & o) { +void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf const &z, mpf & o) { SASSERT(x.sbits == y.sbits && x.ebits == y.ebits && x.sbits == y.sbits && z.ebits == z.ebits); @@ -861,7 +865,7 @@ void mpf_manager::fused_mul_add(mpf_rounding_mode rm, mpf const & x, mpf const & o.exponent = mul_res.exponent(); - unsigned extra = x.sbits-4; + unsigned extra = 0; // Result could overflow into 4.xxx ... SASSERT(m_mpz_manager.lt(o.significand, m_powers2(2 * x.sbits + 2))); if(m_mpz_manager.ge(o.significand, m_powers2(2 * x.sbits + 1))) @@ -871,8 +875,13 @@ void mpf_manager::fused_mul_add(mpf_rounding_mode rm, mpf const & x, mpf const & TRACE("mpf_dbg", tout << "Addition overflew!" << std::endl;); } - // Get rid of the extra bits. - m_mpz_manager.machine_div_rem(o.significand, m_powers2(extra), o.significand, sticky_rem); + // Remove the extra bits, keeping a sticky bit. + m_mpz_manager.set(sticky_rem, 0); + if (o.sbits >= (4+extra)) + m_mpz_manager.machine_div_rem(o.significand, m_powers2(4+extra), o.significand, sticky_rem); + else + m_mpz_manager.mul2k(o.significand, (4+extra) - o.sbits, o.significand); + if (!m_mpz_manager.is_zero(sticky_rem) && m_mpz_manager.is_even(o.significand)) m_mpz_manager.inc(o.significand); diff --git a/src/util/mpf.h b/src/util/mpf.h index b99f8ab08..059f2ab25 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -121,7 +121,7 @@ public: void mul(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf & o); void div(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf & o); - void fused_mul_add(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf const &z, mpf & o); + void fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf const &z, mpf & o); void sqrt(mpf_rounding_mode rm, mpf const & x, mpf & o);