From 52b4282d2002178f5076d341565c37235fc45327 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 22 Feb 2022 12:14:06 -0600
Subject: [PATCH] Change inference scheme in transcendentals to rewrite rule
 (#8115)

Avoids introducing new sine terms.
---
 src/theory/arith/arith_rewriter.cpp           | 15 ++++++++++++-
 .../arith/nl/transcendental/sine_solver.cpp   | 22 -------------------
 2 files changed, 14 insertions(+), 23 deletions(-)

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index abef4eec3..ffd7427af 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -807,7 +807,20 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) {
                               nm->mkNode(kind::SINE, nm->mkConstReal(-rat)));
         return RewriteResponse(REWRITE_AGAIN_FULL, ret);
       }
-    }else{
+    }
+    else if ((t[0].getKind() == MULT || t[0].getKind() == NONLINEAR_MULT)
+             && t[0][0].isConst() && t[0][0].getConst<Rational>().sgn() == -1)
+    {
+      // sin(-n*x) ---> -sin(n*x)
+      std::vector<Node> mchildren(t[0].begin(), t[0].end());
+      mchildren[0] = nm->mkConstReal(-t[0][0].getConst<Rational>());
+      Node ret = nm->mkNode(
+          kind::NEG,
+          nm->mkNode(kind::SINE, nm->mkNode(t[0].getKind(), mchildren)));
+      return RewriteResponse(REWRITE_AGAIN_FULL, ret);
+    }
+    else
+    {
       // get the factor of PI in the argument
       Node pi_factor;
       Node pi;
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index d6a357b56..926894a49 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -134,28 +134,6 @@ void SineSolver::checkInitialRefine()
           d_data->d_im.addPendingLemma(
               lem, InferenceId::ARITH_NL_T_INIT_REFINE, proof);
         }
-        {
-          // sine symmetry: sin(t) - sin(-t) = 0
-          Node lem = nm->mkNode(Kind::ADD, t, symn).eqNode(d_data->d_zero);
-          CDProof* proof = nullptr;
-          if (d_data->isProofEnabled())
-          {
-            proof = d_data->getProof();
-            Node tmplem =
-                nm->mkNode(Kind::ADD,
-                           t,
-                           nm->mkNode(
-                               Kind::SINE,
-                               nm->mkNode(Kind::MULT, d_data->d_neg_one, t[0])))
-                    .eqNode(d_data->d_zero);
-            proof->addStep(
-                tmplem, PfRule::ARITH_TRANS_SINE_SYMMETRY, {}, {t[0]});
-            proof->addStep(
-                lem, PfRule::MACRO_SR_PRED_TRANSFORM, {tmplem}, {lem});
-          }
-          d_data->d_im.addPendingLemma(
-              lem, InferenceId::ARITH_NL_T_INIT_REFINE, proof);
-        }
         {
           // sine zero tangent:
           //   t > 0  =>  sin(t) < t
-- 
2.30.2