From cfbe16639f9fd1445ab6595fc68bbb895011dc69 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 13 Jul 2016 15:35:14 +0100 Subject: [PATCH 1/6] Bugfix for fpa2bv translation --- src/ast/fpa/fpa2bv_converter.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index e89664216..d3257ac55 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3641,11 +3641,11 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref // the maximum shift is `sbits', because after that the mantissa // would be zero anyways. So we can safely cut the shift variable down, // as long as we check the higher bits. - expr_ref sh(m), is_sh_zero(m), sl(m), sbits_s(m), short_shift(m); - zero_s = m_bv_util.mk_numeral(0, sbits-1); + expr_ref zero_ems(m), sh(m), is_sh_zero(m), sl(m), sbits_s(m), short_shift(m); + zero_ems = m_bv_util.mk_numeral(0, ebits - sbits); sbits_s = m_bv_util.mk_numeral(sbits, sbits); sh = m_bv_util.mk_extract(ebits-1, sbits, shift); - m_simp.mk_eq(zero_s, sh, is_sh_zero); + m_simp.mk_eq(zero_ems, sh, is_sh_zero); short_shift = m_bv_util.mk_extract(sbits-1, 0, shift); m_simp.mk_ite(is_sh_zero, short_shift, sbits_s, sl); denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, sl); From 3bea00efe3dc3d62a4cf16077cb7e825ad123ea1 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 13 Jul 2016 15:35:29 +0100 Subject: [PATCH 2/6] added smt_params trace --- src/smt/smt_quantifier.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index ad2c25e63..a5e15a201 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -147,6 +147,7 @@ namespace smt { } m_qi_queue.init_search_eh(); m_plugin->init_search_eh(); + TRACE("smt_params", m_params.display(tout); ); } void assign_eh(quantifier * q) { From a21d701fa1066d34d906b06d0bcd2f5b8d975f0f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 13 Jul 2016 15:36:21 +0100 Subject: [PATCH 3/6] tabs --- src/tactic/ufbv/ufbv_tactic.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/tactic/ufbv/ufbv_tactic.cpp b/src/tactic/ufbv/ufbv_tactic.cpp index 9d16d7f9a..b5a4ca3a3 100644 --- a/src/tactic/ufbv/ufbv_tactic.cpp +++ b/src/tactic/ufbv/ufbv_tactic.cpp @@ -40,12 +40,12 @@ tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) { no_elim_and.set_bool("elim_and", false); return and_then( - mk_trace_tactic("ufbv_pre"), + mk_trace_tactic("ufbv_pre"), and_then(mk_simplify_tactic(m, p), mk_propagate_values_tactic(m, p), and_then(using_params(mk_macro_finder_tactic(m, no_elim_and), no_elim_and), - mk_simplify_tactic(m, p)), - and_then(mk_snf_tactic(m, p), mk_simplify_tactic(m, p)), + mk_simplify_tactic(m, p)), + and_then(mk_snf_tactic(m, p), mk_simplify_tactic(m, p)), mk_elim_and_tactic(m, p), mk_solve_eqs_tactic(m, p), and_then(mk_der_fp_tactic(m, p), mk_simplify_tactic(m, p)), @@ -56,7 +56,7 @@ tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) { and_then(mk_quasi_macros_tactic(m, p), mk_simplify_tactic(m, p)), and_then(mk_der_fp_tactic(m, p), mk_simplify_tactic(m, p)), mk_simplify_tactic(m, p)), - mk_trace_tactic("ufbv_post")); + mk_trace_tactic("ufbv_post")); } tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p) { From 9f99482f076c8c1b9a9f006b7225a9e824ce7534 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Jul 2016 10:29:31 -0700 Subject: [PATCH 4/6] fix model generation for cos/sin transformation. Issue #680 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/purify_arith_tactic.cpp | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index f41eb017b..9e06a42d1 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -170,8 +170,8 @@ struct purify_arith_proc { } std::pair pair; if (!m_sin_cos.find(to_app(theta), pair)) { - pair.first = m().mk_fresh_const(0, m_util.mk_real()); - pair.second = m().mk_fresh_const(0, m_util.mk_real()); + pair.first = m().mk_fresh_const(0, u().mk_real()); + pair.second = m().mk_fresh_const(0, u().mk_real()); m_sin_cos.insert(to_app(theta), pair); m_pinned.push_back(pair.first); m_pinned.push_back(pair.second); @@ -680,6 +680,8 @@ struct purify_arith_proc { } }; + expr * mk_real_zero() { return u().mk_numeral(rational(0), false); } + struct rw : public rewriter_tpl { rw_cfg m_cfg; rw(purify_arith_proc & o): @@ -779,13 +781,15 @@ struct purify_arith_proc { mc = concat(mc.get(), emc); obj_map >::iterator it = m_sin_cos.begin(), end = m_sin_cos.end(); for (; it != end; ++it) { - emc->insert(it->m_key->get_decl(), m_util.mk_asin(it->m_value.first)); + emc->insert(it->m_key->get_decl(), + u().mk_add(u().mk_asin(it->m_value.first), + m().mk_ite(u().mk_ge(it->m_value.second, mk_real_zero()), mk_real_zero(), u().mk_pi()))); } } - // given values for x, y find value for theta - // x, y are rational } + + }; class purify_arith_tactic : public tactic { From 247e94a7c04dc651c4cba5d8a0b214f37435492b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Jul 2016 10:34:12 -0700 Subject: [PATCH 5/6] fix model generation for cos/sin transformation. Issue #680 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/purify_arith_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 9e06a42d1..346153adb 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -782,8 +782,8 @@ struct purify_arith_proc { obj_map >::iterator it = m_sin_cos.begin(), end = m_sin_cos.end(); for (; it != end; ++it) { emc->insert(it->m_key->get_decl(), - u().mk_add(u().mk_asin(it->m_value.first), - m().mk_ite(u().mk_ge(it->m_value.second, mk_real_zero()), mk_real_zero(), u().mk_pi()))); + u().mk_add(u().mk_acos(it->m_value.second), + m().mk_ite(u().mk_ge(it->m_value.first, mk_real_zero()), mk_real_zero(), u().mk_pi()))); } } From 3a70b6aab46ef640be396b3c2a74a718389d380f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Jul 2016 11:12:27 -0700 Subject: [PATCH 6/6] fix model generation, add rewrite rules for sin(acos(x)) reduction to help model validation. Issue #680 Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.h | 14 ++++++++++++-- src/ast/rewriter/arith_rewriter.cpp | 19 ++++++++++++++----- src/tactic/arith/purify_arith_tactic.cpp | 4 ++-- 3 files changed, 28 insertions(+), 9 deletions(-) diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 71e54c0a3..9ccf02d0d 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -290,6 +290,8 @@ public: bool is_asin(expr const* n) const { return is_app_of(n, m_afid, OP_ASIN); } bool is_acos(expr const* n) const { return is_app_of(n, m_afid, OP_ACOS); } bool is_atan(expr const* n) const { return is_app_of(n, m_afid, OP_ATAN); } + bool is_pi(expr * arg) { return is_app_of(arg, m_afid, OP_PI); } + bool is_e(expr * arg) { return is_app_of(arg, m_afid, OP_E); } MATCH_UNARY(is_uminus); MATCH_UNARY(is_to_real); @@ -307,8 +309,13 @@ public: MATCH_BINARY(is_idiv); MATCH_BINARY(is_power); - bool is_pi(expr * arg) { return is_app_of(arg, m_afid, OP_PI); } - bool is_e(expr * arg) { return is_app_of(arg, m_afid, OP_E); } + MATCH_UNARY(is_sin); + MATCH_UNARY(is_asin); + MATCH_UNARY(is_cos); + MATCH_UNARY(is_acos); + MATCH_UNARY(is_tan); + MATCH_UNARY(is_atan); + }; class arith_util : public arith_recognizers { @@ -355,6 +362,9 @@ public: app * mk_int(int i) { return mk_numeral(rational(i), true); } + app * mk_real(int i) { + return mk_numeral(rational(i), false); + } app * mk_le(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LE, arg1, arg2); } app * mk_ge(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_GE, arg1, arg2); } app * mk_lt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LT, arg1, arg2); } diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index c9a2d2379..8f8c9a2bc 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1196,11 +1196,17 @@ expr * arith_rewriter::mk_sin_value(rational const & k) { } br_status arith_rewriter::mk_sin_core(expr * arg, expr_ref & result) { - if (is_app_of(arg, get_fid(), OP_ASIN)) { + expr * m, *x; + if (m_util.is_asin(arg, x)) { // sin(asin(x)) == x - result = to_app(arg)->get_arg(0); + result = x; return BR_DONE; } + if (m_util.is_acos(arg, x)) { + // sin(acos(x)) == sqrt(1 - x^2) + result = m_util.mk_power(m_util.mk_sub(m_util.mk_real(1), m_util.mk_mul(x,x)), m_util.mk_numeral(rational(1,2), false)); + return BR_REWRITE_FULL; + } rational k; if (is_numeral(arg, k) && k.is_zero()) { // sin(0) == 0 @@ -1214,7 +1220,6 @@ br_status arith_rewriter::mk_sin_core(expr * arg, expr_ref & result) { return BR_REWRITE_FULL; } - expr * m; if (is_pi_offset(arg, k, m)) { rational k_prime = mod(floor(k), rational(2)) + k - floor(k); SASSERT(k_prime >= rational(0) && k_prime < rational(2)); @@ -1250,11 +1255,15 @@ br_status arith_rewriter::mk_sin_core(expr * arg, expr_ref & result) { } br_status arith_rewriter::mk_cos_core(expr * arg, expr_ref & result) { - if (is_app_of(arg, get_fid(), OP_ACOS)) { + expr* x; + if (m_util.is_acos(arg, x)) { // cos(acos(x)) == x - result = to_app(arg)->get_arg(0); + result = x; return BR_DONE; } + if (m_util.is_asin(arg, x)) { + // cos(asin(x)) == ... + } rational k; if (is_numeral(arg, k) && k.is_zero()) { diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 346153adb..d0891b28b 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -782,8 +782,8 @@ struct purify_arith_proc { obj_map >::iterator it = m_sin_cos.begin(), end = m_sin_cos.end(); for (; it != end; ++it) { emc->insert(it->m_key->get_decl(), - u().mk_add(u().mk_acos(it->m_value.second), - m().mk_ite(u().mk_ge(it->m_value.first, mk_real_zero()), mk_real_zero(), u().mk_pi()))); + m().mk_ite(u().mk_ge(it->m_value.first, mk_real_zero()), u().mk_acos(it->m_value.second), + u().mk_add(u().mk_acos(u().mk_uminus(it->m_value.second)), u().mk_pi()))); } }