From 58b9fc437d95c1f1c0fa3442ebc13d0b49d60fbe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 13 Dec 2018 16:09:08 -0600 Subject: [PATCH] add sin/cos axiom regardless of whether sin/cos can be eliminated. fix #2037 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/purify_arith_tactic.cpp | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 67dadd34b..14b6c6b41 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -509,6 +509,9 @@ struct purify_arith_proc { return BR_DONE; } else { + expr_ref s(u().mk_sin(theta), m()); + expr_ref c(u().mk_cos(theta), m()); + push_cnstr(EQ(mk_real_one(), u().mk_add(u().mk_mul(s, s), u().mk_mul(c, c)))); return BR_FAILED; } } @@ -777,11 +780,10 @@ struct purify_arith_proc { if (produce_models && !m_sin_cos.empty()) { generic_model_converter* emc = alloc(generic_model_converter, m(), "purify_sin_cos"); mc = concat(mc.get(), emc); - obj_map >::iterator it = m_sin_cos.begin(), end = m_sin_cos.end(); - for (; it != end; ++it) { - emc->add(it->m_key->get_decl(), - 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()))); + for (auto const& kv : m_sin_cos) { + emc->add(kv.m_key->get_decl(), + m().mk_ite(u().mk_ge(kv.m_value.first, mk_real_zero()), u().mk_acos(kv.m_value.second), + u().mk_add(u().mk_acos(u().mk_uminus(kv.m_value.second)), u().mk_pi()))); } }