From 59e8eb3e946e183999fd8584dfb31e21cc436e74 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 Feb 2022 17:10:55 -0600 Subject: [PATCH] Fix rewrite for eliminating constant factors of PI from argument to sine (#8031) Fixes cvc5/cvc5-projects#441. Fixes cvc5/cvc5-projects#414. --- src/theory/arith/arith_rewriter.cpp | 13 ++++--------- test/unit/api/cpp/solver_black.cpp | 11 +++++++++++ 2 files changed, 15 insertions(+), 9 deletions(-) diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 49907450a..82cc5878f 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -844,22 +844,17 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { Rational r = pi_factor.getConst(); Rational r_abs = r.abs(); Rational rone = Rational(1); - Node ntwo = nm->mkConstInt(Rational(2)); + Rational rtwo = Rational(2); if (r_abs > rone) { //add/substract 2*pi beyond scope - Node ra_div_two = nm->mkNode( - kind::INTS_DIVISION, mkRationalNode(r_abs + rone), ntwo); + Rational ra_div_two = (r_abs + rone) / rtwo; Node new_pi_factor; if( r.sgn()==1 ){ - new_pi_factor = nm->mkNode( - kind::SUB, pi_factor, nm->mkNode(kind::MULT, ntwo, ra_div_two)); + new_pi_factor = nm->mkConstReal(r - rtwo * ra_div_two.floor()); }else{ Assert(r.sgn() == -1); - new_pi_factor = - nm->mkNode(kind::PLUS, - pi_factor, - nm->mkNode(kind::MULT, ntwo, ra_div_two)); + new_pi_factor = nm->mkConstReal(r + rtwo * ra_div_two.floor()); } Node new_arg = nm->mkNode(kind::MULT, new_pi_factor, pi); if (!rem.isNull()) diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index f644c3367..0fa3048ae 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -2994,5 +2994,16 @@ TEST_F(TestApiBlackSolver, proj_issue386) ASSERT_THROW(s2.instantiate({s1}), CVC5ApiException); } +TEST_F(TestApiBlackSolver, proj_issue414) +{ + Solver slv; + Sort s2 = slv.getRealSort(); + Term t1 = slv.mkConst(s2, "_x0"); + Term t16 = slv.mkTerm(Kind::PI); + Term t53 = slv.mkTerm(Kind::MINUS, {t1, t16}); + Term t54 = slv.mkTerm(Kind::SECANT, {t53}); + ASSERT_NO_THROW(slv.simplify(t54)); +} + } // namespace test } // namespace cvc5 -- 2.30.2