From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Feb 2022 23:10:55 +0000 (-0600)
Subject: Fix rewrite for eliminating constant factors of PI from argument to sine (#8031)
X-Git-Tag: cvc5-1.0.0~470
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=59e8eb3e946e183999fd8584dfb31e21cc436e74;p=cvc5.git

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 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>();
         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