From c422b48bf43f9a1e2b29c4803c646de0617e32b4 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 21 May 2015 15:06:47 +0100 Subject: [PATCH 01/15] Bugfix for hwf_manager::round_to_integral --- src/util/hwf.cpp | 35 +++++++++++++++++++++++++++++++++-- 1 file changed, 33 insertions(+), 2 deletions(-) diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index 40d20b644..b159cbdb6 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -338,8 +338,39 @@ void hwf_manager::sqrt(mpf_rounding_mode rm, hwf const & x, hwf & o) { void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o) { set_rounding_mode(rm); - modf(x.value, &o.value); - // Note: on x64, this sometimes produces an SNAN instead of a QNAN? + // CMW: modf is not the right function here. + // modf(x.value, &o.value); + + // According to the Intel Architecture manual, the x87-instrunction FRNDINT is the + // same in 32-bit and 64-bit mode. The _mm_round_* intrinsics are SSE4 extensions. + +#ifdef USE_INTRINSICS + switch (rm) { + case 0: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_NEAREST_INT)); break; + case 2: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_POS_INF)); break; + case 3: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_NEG_INF)); break; + case 4: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_ZERO)); break; + case 1: + UNREACHABLE(); // Note: MPF_ROUND_NEAREST_TAWAY is not supported by the hardware! + break; + default: + UNREACHABLE(); // Unknown rounding mode. + } +#else + NOT_IMPLEMENTED_YET(); +#endif + +#if 0 + double xv = x.value; + double & ov = o.value; + + __asm { + fld xv + frndint + fstp ov // Store result away. + } + +#endif } void hwf_manager::rem(hwf const & x, hwf const & y, hwf & o) { From 8c18bdcca9e72ce71ac4de47816c351c3dbfb84f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 21 May 2015 18:12:14 +0100 Subject: [PATCH 02/15] Bugfix for fp.roundToIntegral. Fixes #69 --- src/ast/fpa/fpa2bv_converter.cpp | 13 +++++++++---- src/util/mpf.cpp | 28 ++++++++++++++++------------ 2 files changed, 25 insertions(+), 16 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 83ba843ac..f69f27214 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1586,9 +1586,10 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * mk_nzero(f, nzero); mk_pzero(f, pzero); - expr_ref x_is_zero(m), x_is_pos(m); + expr_ref x_is_zero(m), x_is_pos(m), x_is_neg(m); mk_is_zero(x, x_is_zero); mk_is_pos(x, x_is_pos); + mk_is_neg(x, x_is_neg); dbg_decouple("fpa2bv_r2i_x_is_zero", x_is_zero); dbg_decouple("fpa2bv_r2i_x_is_pos", x_is_pos); @@ -1655,9 +1656,13 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * mk_ite(c422, xone, v42, v42); mk_ite(c421, xzero, v42, v42); - mk_ite(m.mk_eq(a_sgn, one_1), nzero, pone, v4); - mk_ite(m.mk_or(rm_is_rte, rm_is_rta), v42, v4, v4); - mk_ite(m.mk_or(rm_is_rtz, rm_is_rtn), xzero, v4, v4); + expr_ref v4_rtn(m), v4_rtp(m); + mk_ite(x_is_neg, nzero, pone, v4_rtp); + mk_ite(x_is_neg, none, pzero, v4_rtn); + + mk_ite(rm_is_rtp, v4_rtp, v42, v4); + mk_ite(rm_is_rtn, v4_rtn, v4, v4); + mk_ite(rm_is_rtz, xzero, v4, v4); SASSERT(is_well_sorted(m, v4)); diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 1dab7b995..e66f6d270 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1006,11 +1006,22 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o else if (is_zero(x)) mk_zero(x.ebits, x.sbits, x.sign, o); // -0.0 -> -0.0, says IEEE754, Sec 5.9. else if (x.exponent < 0) { - if (rm == MPF_ROUND_TOWARD_ZERO || - rm == MPF_ROUND_TOWARD_NEGATIVE) + if (rm == MPF_ROUND_TOWARD_ZERO) mk_zero(x.ebits, x.sbits, x.sign, o); - else if (rm == MPF_ROUND_NEAREST_TEVEN || - rm == MPF_ROUND_NEAREST_TAWAY) { + else if (rm == MPF_ROUND_TOWARD_NEGATIVE) { + if (x.sign) + mk_one(x.ebits, x.sbits, true, o); + else + mk_zero(x.ebits, x.sbits, false, o); + } + else if (rm == MPF_ROUND_TOWARD_POSITIVE) { + if (x.sign) + mk_zero(x.ebits, x.sbits, true, o); + else + mk_one(x.ebits, x.sbits, false, o); + } + else { + SASSERT(rm == MPF_ROUND_NEAREST_TEVEN || rm == MPF_ROUND_NEAREST_TAWAY); bool tie = m_mpz_manager.is_zero(x.significand) && x.exponent == -1; TRACE("mpf_dbg", tout << "tie = " << tie << std::endl;); if (tie && rm == MPF_ROUND_NEAREST_TEVEN) @@ -1019,15 +1030,8 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o mk_one(x.ebits, x.sbits, x.sign, o); else if (x.exponent < -1) mk_zero(x.ebits, x.sbits, x.sign, o); - else - mk_one(x.ebits, x.sbits, x.sign, o); - } - else { - SASSERT(rm == MPF_ROUND_TOWARD_POSITIVE); - if (x.sign) - mk_nzero(x.ebits, x.sbits, o); else - mk_one(x.ebits, x.sbits, false, o); + mk_one(x.ebits, x.sbits, x.sign, o); } } else if (x.exponent >= x.sbits - 1) From eee076b9f8b5d2f3347dfa4f83b64851cb2372a0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 21 May 2015 18:16:02 +0100 Subject: [PATCH 03/15] Bugfixes for fp.min, fp.max. Fixes the fix for #68 --- src/ast/fpa/fpa2bv_converter.cpp | 4 ++-- src/ast/rewriter/fpa_rewriter.cpp | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index f69f27214..1d794c898 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1072,7 +1072,7 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, result = y; mk_ite(lt, x, result, result); - mk_ite(both_zero, pzero, result, result); + mk_ite(both_zero, y, result, result); mk_ite(y_is_nan, x, result, result); mk_ite(x_is_nan, y, result, result); @@ -1102,7 +1102,7 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, result = y; mk_ite(gt, x, result, result); - mk_ite(both_zero, pzero, result, result); + mk_ite(both_zero, y, result, result); mk_ite(y_is_nan, x, result, result); mk_ite(x_is_nan, y, result, result); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 40021e330..37c42b494 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -412,7 +412,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { return BR_DONE; } if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) { - result = m_util.mk_pzero(m().get_sort(arg1)); + result = arg2; return BR_DONE; } @@ -421,7 +421,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { m().mk_ite(mk_eq_nan(arg2), arg1, m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), - m_util.mk_pzero(m().get_sort(arg1)), + arg2, m().mk_ite(m_util.mk_lt(arg1, arg2), arg1, arg2)))); @@ -438,7 +438,7 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { return BR_DONE; } if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) { - result = m_util.mk_pzero(m().get_sort(arg1)); + result = arg2; return BR_DONE; } @@ -447,7 +447,7 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { m().mk_ite(mk_eq_nan(arg2), arg1, m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), - m_util.mk_pzero(m().get_sort(arg1)), + arg2, m().mk_ite(m_util.mk_gt(arg1, arg2), arg1, arg2)))); From 6f575689b190740a78f8073816046f5efd4c4eab Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 21 May 2015 19:02:09 +0100 Subject: [PATCH 04/15] Added injection of auxiliary lemmas for fp.isNaN, so that the value propagation can pick up these values and propagate them. Fixes #96. --- src/ast/fpa/fpa2bv_converter.cpp | 7 +++++++ src/tactic/fpa/qffp_tactic.cpp | 1 + 2 files changed, 8 insertions(+) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 1d794c898..cc0fef3c3 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3044,6 +3044,13 @@ void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) { m_simp.mk_not(sig_is_zero, sig_is_not_zero); m_simp.mk_eq(exp, top_exp, exp_is_top); m_simp.mk_and(exp_is_top, sig_is_not_zero, result); + + // Inject auxiliary lemmas that fix e to the one and only NaN value, + // that is (= e (fp #b0 #b1...1 #b0...01)), so that the value propagation + // has a value to propagate. + m_extra_assertions.push_back(m.mk_eq(sgn, m_bv_util.mk_numeral(0, 1))); + m_extra_assertions.push_back(m.mk_eq(exp, top_exp)); + m_extra_assertions.push_back(m.mk_eq(sig, m_bv_util.mk_numeral(1, m_bv_util.get_bv_size(sig)))); } void fpa2bv_converter::mk_is_inf(expr * e, expr_ref & result) { diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp index c45898cc7..4854b3c07 100644 --- a/src/tactic/fpa/qffp_tactic.cpp +++ b/src/tactic/fpa/qffp_tactic.cpp @@ -37,6 +37,7 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) { mk_smt_tactic(), and_then( mk_fpa2bv_tactic(m, p), + mk_propagate_values_tactic(m, p), using_params(mk_simplify_tactic(m, p), simp_p), mk_bit_blaster_tactic(m, p), using_params(mk_simplify_tactic(m, p), simp_p), From f100d4feda71e78af653c76fae52b7427e26f2ce Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 21 May 2015 11:10:42 -0700 Subject: [PATCH 05/15] hoist out basic union find Signed-off-by: Nikolaj Bjorner --- .../dl_mk_quantifier_instantiation.h | 70 ++----------------- src/util/union_find.h | 66 +++++++++++++++++ 2 files changed, 70 insertions(+), 66 deletions(-) diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.h b/src/muz/transforms/dl_mk_quantifier_instantiation.h index 138d5abee..37a5b8a6c 100644 --- a/src/muz/transforms/dl_mk_quantifier_instantiation.h +++ b/src/muz/transforms/dl_mk_quantifier_instantiation.h @@ -26,8 +26,9 @@ Revision History: #define _DL_MK_QUANTIFIER_INSTANTIATION_H_ -#include"dl_rule_transformer.h" -#include"expr_safe_replace.h" +#include "dl_rule_transformer.h" +#include "expr_safe_replace.h" +#include "union_find.h" namespace datalog { @@ -37,75 +38,12 @@ namespace datalog { class mk_quantifier_instantiation : public rule_transformer::plugin { typedef svector > term_pairs; - class union_find { - unsigned_vector m_find; - unsigned_vector m_size; - unsigned_vector m_next; - - void ensure_size(unsigned v) { - while (v >= get_num_vars()) { - mk_var(); - } - } - public: - unsigned mk_var() { - unsigned r = m_find.size(); - m_find.push_back(r); - m_size.push_back(1); - m_next.push_back(r); - return r; - } - unsigned get_num_vars() const { return m_find.size(); } - - unsigned find(unsigned v) const { - if (v >= get_num_vars()) { - return v; - } - while (true) { - unsigned new_v = m_find[v]; - if (new_v == v) - return v; - v = new_v; - } - } - - unsigned next(unsigned v) const { - if (v >= get_num_vars()) { - return v; - } - return m_next[v]; - } - - bool is_root(unsigned v) const { - return v >= get_num_vars() || m_find[v] == v; - } - - void merge(unsigned v1, unsigned v2) { - unsigned r1 = find(v1); - unsigned r2 = find(v2); - if (r1 == r2) - return; - ensure_size(v1); - ensure_size(v2); - if (m_size[r1] > m_size[r2]) - std::swap(r1, r2); - m_find[r1] = r2; - m_size[r2] += m_size[r1]; - std::swap(m_next[r1], m_next[r2]); - } - - void reset() { - m_find.reset(); - m_next.reset(); - m_size.reset(); - } - }; ast_manager& m; context& m_ctx; expr_safe_replace m_var2cnst; expr_safe_replace m_cnst2var; - union_find m_uf; + basic_union_find m_uf; ptr_vector m_todo; ptr_vector m_terms; ptr_vector m_binding; diff --git a/src/util/union_find.h b/src/util/union_find.h index 32de6846a..23d33a442 100644 --- a/src/util/union_find.h +++ b/src/util/union_find.h @@ -173,5 +173,71 @@ public: #endif }; + +class basic_union_find { + unsigned_vector m_find; + unsigned_vector m_size; + unsigned_vector m_next; + + void ensure_size(unsigned v) { + while (v >= get_num_vars()) { + mk_var(); + } + } + public: + unsigned mk_var() { + unsigned r = m_find.size(); + m_find.push_back(r); + m_size.push_back(1); + m_next.push_back(r); + return r; + } + unsigned get_num_vars() const { return m_find.size(); } + + unsigned find(unsigned v) const { + if (v >= get_num_vars()) { + return v; + } + while (true) { + unsigned new_v = m_find[v]; + if (new_v == v) + return v; + v = new_v; + } + } + + unsigned next(unsigned v) const { + if (v >= get_num_vars()) { + return v; + } + return m_next[v]; + } + + bool is_root(unsigned v) const { + return v >= get_num_vars() || m_find[v] == v; + } + + void merge(unsigned v1, unsigned v2) { + unsigned r1 = find(v1); + unsigned r2 = find(v2); + if (r1 == r2) + return; + ensure_size(v1); + ensure_size(v2); + if (m_size[r1] > m_size[r2]) + std::swap(r1, r2); + m_find[r1] = r2; + m_size[r2] += m_size[r1]; + std::swap(m_next[r1], m_next[r2]); + } + + void reset() { + m_find.reset(); + m_next.reset(); + m_size.reset(); + } +}; + + #endif /* _UNION_FIND_H_ */ From c969d7804235292fc919fbfd5061a0b3b918da15 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 21 May 2015 15:07:01 -0700 Subject: [PATCH 06/15] throw exception instead of debug mode assertion in ast_manager on malformed input Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 10 +++++++++- src/math/euclid/euclidean_solver.cpp | 2 +- src/smt/theory_arith_int.h | 4 ++-- 3 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 86c23a799..4ae6b6106 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2043,7 +2043,15 @@ inline app * ast_manager::mk_app_core(func_decl * decl, expr * arg1, expr * arg2 } app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * args) { - SASSERT(decl->get_arity() == num_args || decl->is_right_associative() || decl->is_left_associative() || decl->is_chainable()); + if (decl->get_arity() != num_args && + !decl->is_right_associative() && + !decl->is_left_associative() && + !decl->is_chainable()) { + std::ostringstream buffer; + buffer << "Wrong number of arguments (" << num_args + << ") passed to function " << mk_pp(decl, *this); + throw ast_exception(buffer.str().c_str()); + } app * r = 0; if (num_args > 2 && !decl->is_flat_associative()) { if (decl->is_right_associative()) { diff --git a/src/math/euclid/euclidean_solver.cpp b/src/math/euclid/euclidean_solver.cpp index 718dbb052..02ff1591e 100644 --- a/src/math/euclid/euclidean_solver.cpp +++ b/src/math/euclid/euclidean_solver.cpp @@ -717,7 +717,7 @@ struct euclidean_solver::imp { elim_unit(); else decompose_and_elim(); - TRACE("euclidean_solver_step", display(tout);); + TRACE("euclidean_solver", display(tout);); if (inconsistent()) return false; } return true; diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index b600dd3c0..45c615e0c 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -1041,8 +1041,8 @@ namespace smt { num_args = 1; args = &n; } - for (unsigned j = 0; j < num_args; j++) { - expr * arg = args[j]; + for (unsigned i = 0; i < num_args; i++) { + expr * arg = args[i]; expr * pp; rational a_val; get_monomial(arg, a_val, pp); From 8a34bd2bf1c8d2b686f65f059c236884cab10d3f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 21 May 2015 15:08:39 -0700 Subject: [PATCH 07/15] fixes issue #88 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 4ae6b6106..d56bb73ff 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2043,10 +2043,8 @@ inline app * ast_manager::mk_app_core(func_decl * decl, expr * arg1, expr * arg2 } app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * args) { - if (decl->get_arity() != num_args && - !decl->is_right_associative() && - !decl->is_left_associative() && - !decl->is_chainable()) { + if (decl->get_arity() != num_args && !decl->is_right_associative() && + !decl->is_left_associative() && !decl->is_chainable()) { std::ostringstream buffer; buffer << "Wrong number of arguments (" << num_args << ") passed to function " << mk_pp(decl, *this); From 705ace6f0a6722dff15dd7edfc77e162dd295b58 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 22 May 2015 11:39:08 +0100 Subject: [PATCH 08/15] Naming consistency --- src/util/hwf.cpp | 2 +- src/util/hwf.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index b159cbdb6..ff92d57d0 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -306,7 +306,7 @@ void hwf_manager::div(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf & #pragma fp_contract(on) #endif -void hwf_manager::fused_mul_add(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf const &z, hwf & o) { +void hwf_manager::fma(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf const &z, hwf & o) { // CMW: fused_mul_add is not available on most CPUs. As of 2012, only Itanium, // Intel Sandybridge and AMD Bulldozers support that (via AVX). diff --git a/src/util/hwf.h b/src/util/hwf.h index 9059869a0..97b4133f7 100644 --- a/src/util/hwf.h +++ b/src/util/hwf.h @@ -105,7 +105,7 @@ public: void mul(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf & o); void div(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf & o); - void fused_mul_add(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf const &z, hwf & o); + void fma(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf const &z, hwf & o); void sqrt(mpf_rounding_mode rm, hwf const & x, hwf & o); From 759d9f2ddadfe2ce51bf356589fa372afa8485de Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 22 May 2015 11:39:28 +0100 Subject: [PATCH 09/15] bugfix for hwf::fma --- src/util/hwf.cpp | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index ff92d57d0..3cbda74cd 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -315,11 +315,8 @@ void hwf_manager::fma(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf co set_rounding_mode(rm); o.value = x.value * y.value + z.value; #else - // NOT_IMPLEMENTED_YET(); - // Just a dummy for now: - hwf t; - mul(rm, x, y, t); - add(rm, t, z, o); + set_rounding_mode(rm); + o.value = ::fma(x.value, y.value, z.value); #endif } From 54cde7cabb1e66e706de440dffa6ee34d7e833dd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 22 May 2015 11:39:58 +0100 Subject: [PATCH 10/15] Bugfix for hwf::round_to_integral --- src/util/hwf.cpp | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index 3cbda74cd..5a41ac86c 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -340,7 +340,7 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o // According to the Intel Architecture manual, the x87-instrunction FRNDINT is the // same in 32-bit and 64-bit mode. The _mm_round_* intrinsics are SSE4 extensions. - +#ifdef _WINDOWS #ifdef USE_INTRINSICS switch (rm) { case 0: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_NEAREST_INT)); break; @@ -354,10 +354,6 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o UNREACHABLE(); // Unknown rounding mode. } #else - NOT_IMPLEMENTED_YET(); -#endif - -#if 0 double xv = x.value; double & ov = o.value; @@ -366,7 +362,10 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o frndint fstp ov // Store result away. } - +#endif +#else + // Linux, OSX. + o.value = nearbyint(x.value); #endif } From ffbbf08d201cd7b6412328af901deaba05521aae Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 22 May 2015 11:59:31 +0100 Subject: [PATCH 11/15] Fixed warning message about unused lock when OpenMP is not available. --- src/util/mpn.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/util/mpn.h b/src/util/mpn.h index 495ae135c..f8cec0301 100644 --- a/src/util/mpn.h +++ b/src/util/mpn.h @@ -27,7 +27,9 @@ Revision History: typedef unsigned int mpn_digit; class mpn_manager { +#ifndef _NO_OMP omp_nest_lock_t m_lock; +#endif #define MPN_BEGIN_CRITICAL() omp_set_nest_lock(&m_lock); #define MPN_END_CRITICAL() omp_unset_nest_lock(&m_lock); From 891073d3fe8ce0066102b9822b3b3ee12752f39a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 22 May 2015 12:01:10 +0100 Subject: [PATCH 12/15] typo --- src/util/mpn.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/mpn.h b/src/util/mpn.h index f8cec0301..c5566bf7e 100644 --- a/src/util/mpn.h +++ b/src/util/mpn.h @@ -27,7 +27,7 @@ Revision History: typedef unsigned int mpn_digit; class mpn_manager { -#ifndef _NO_OMP +#ifndef _NO_OMP_ omp_nest_lock_t m_lock; #endif #define MPN_BEGIN_CRITICAL() omp_set_nest_lock(&m_lock); From a229416a2bd12ec4beb9b638d8da65aecc9af645 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marcus=20V=C3=B6lker?= Date: Fri, 22 May 2015 15:55:09 +0200 Subject: [PATCH 13/15] Change ASTVector to Expr[] in interpolation result --- src/api/java/InterpolationContext.java | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 667c91a53..25f132fa7 100644 --- a/src/api/java/InterpolationContext.java +++ b/src/api/java/InterpolationContext.java @@ -90,7 +90,7 @@ public class InterpolationContext extends Context public class ComputeInterpolantResult { public Z3_lbool status = Z3_lbool.Z3_L_UNDEF; - public ASTVector interp = null; + public Expr[] interp = null; public Model model = null; }; @@ -110,7 +110,14 @@ public class InterpolationContext extends Context Native.LongPtr n_i = new Native.LongPtr(); Native.LongPtr n_m = new Native.LongPtr(); res.status =Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m)); - if (res.status == Z3_lbool.Z3_L_FALSE) res.interp = new ASTVector(this, n_i.value); + if (res.status == Z3_lbool.Z3_L_FALSE) + { + ASTVector seq = new ASTVector(this, n_i.value); + int n = seq.size(); + res.interp = new Expr[n]; + for (int i = 0; i < n; i++) + res.interp[i] = Expr.create(this, seq.get(i).getNativeObject()); + } if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value); return res; } From b4f72c81457712929405f397b89c02bd8ca264c3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 22 May 2015 08:24:45 -0700 Subject: [PATCH 14/15] Revert "Change ASTVector to Expr[] in interpolation result" --- src/api/java/InterpolationContext.java | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 25f132fa7..667c91a53 100644 --- a/src/api/java/InterpolationContext.java +++ b/src/api/java/InterpolationContext.java @@ -90,7 +90,7 @@ public class InterpolationContext extends Context public class ComputeInterpolantResult { public Z3_lbool status = Z3_lbool.Z3_L_UNDEF; - public Expr[] interp = null; + public ASTVector interp = null; public Model model = null; }; @@ -110,14 +110,7 @@ public class InterpolationContext extends Context Native.LongPtr n_i = new Native.LongPtr(); Native.LongPtr n_m = new Native.LongPtr(); res.status =Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m)); - if (res.status == Z3_lbool.Z3_L_FALSE) - { - ASTVector seq = new ASTVector(this, n_i.value); - int n = seq.size(); - res.interp = new Expr[n]; - for (int i = 0; i < n; i++) - res.interp[i] = Expr.create(this, seq.get(i).getNativeObject()); - } + if (res.status == Z3_lbool.Z3_L_FALSE) res.interp = new ASTVector(this, n_i.value); if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value); return res; } From 279ef05713462237e427dc96192d911a9cb18dbc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 22 May 2015 08:57:05 -0700 Subject: [PATCH 15/15] expose BoolExpr[] for ASTVector and merge common functionality Signed-off-by: Nikolaj Bjorner --- src/api/java/ASTVector.java | 8 ++++++++ src/api/java/Fixedpoint.java | 12 ++---------- src/api/java/InterpolationContext.java | 8 +++++--- src/api/java/Solver.java | 6 +----- 4 files changed, 16 insertions(+), 18 deletions(-) diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java index 9c6504493..e08a75e7f 100644 --- a/src/api/java/ASTVector.java +++ b/src/api/java/ASTVector.java @@ -119,4 +119,12 @@ public class ASTVector extends Z3Object getContext().getASTVectorDRQ().add(o); super.decRef(o); } + + BoolExpr[] ToBoolArray() { + int n = size(); + BoolExpr[] res = new BoolExpr[n]; + for (int i = 0; i < n; i++) + res[i] = new BoolExpr(getContext(), get(i).getNativeObject()); + return res; + } } diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index c9d14288b..daa0f4e3f 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -298,11 +298,7 @@ public class Fixedpoint extends Z3Object ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules( getContext().nCtx(), getNativeObject())); - int n = v.size(); - BoolExpr[] res = new BoolExpr[n]; - for (int i = 0; i < n; i++) - res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject()); - return res; + return v.ToBoolArray(); } /** @@ -315,11 +311,7 @@ public class Fixedpoint extends Z3Object ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions( getContext().nCtx(), getNativeObject())); - int n = v.size(); - BoolExpr[] res = new BoolExpr[n]; - for (int i = 0; i < n; i++) - res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject()); - return res; + return v.ToBoolArray(); } /** diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 667c91a53..50c6a223a 100644 --- a/src/api/java/InterpolationContext.java +++ b/src/api/java/InterpolationContext.java @@ -90,7 +90,7 @@ public class InterpolationContext extends Context public class ComputeInterpolantResult { public Z3_lbool status = Z3_lbool.Z3_L_UNDEF; - public ASTVector interp = null; + public BoolExpr[] interp = null; public Model model = null; }; @@ -109,8 +109,10 @@ public class InterpolationContext extends Context ComputeInterpolantResult res = new ComputeInterpolantResult(); Native.LongPtr n_i = new Native.LongPtr(); Native.LongPtr n_m = new Native.LongPtr(); - res.status =Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m)); - if (res.status == Z3_lbool.Z3_L_FALSE) res.interp = new ASTVector(this, n_i.value); + res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m)); + if (res.status == Z3_lbool.Z3_L_FALSE) { + res.interp = (new ASTVector(this, n_i.value)).ToBoolArray(); + } if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value); return res; } diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index e4ba9de42..7c4c1f4b9 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -190,11 +190,7 @@ public class Solver extends Z3Object { ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions( getContext().nCtx(), getNativeObject())); - int n = assrts.size(); - BoolExpr[] res = new BoolExpr[n]; - for (int i = 0; i < n; i++) - res[i] = new BoolExpr(getContext(), assrts.get(i).getNativeObject()); - return res; + return assrts.ToBoolArray(); } /**