Fix rewrite for eliminating constant factors of PI from argument to sine (#8031)

Fixes cvc5/cvc5-projects#441.
Fixes cvc5/cvc5-projects#414.

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 49907450aa93fc415642511dd3cfa5c9e87bc2d5..82cc5878f588712c4d76d872230cc6a0c4cb829c 100644 (file)
--- 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>();
         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 f644c3367c096c6da302e175a5901db209f30ac4..0fa3048aeec3090e0cbfcda7cfce314a469f83f9 100644 (file)
--- 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