Change inference scheme in transcendentals to rewrite rule (#8115)

Avoids introducing new sine terms.

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index abef4eec33de48f706ec80d2819bd20cf2cb5101..ffd7427af668f7b647ace8518737909aea9d16b8 100644 (file)
--- 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 d6a357b56dec506fed8ead9c86e2b68df78ff76a..926894a49addee7adf0d72605ff66f35a6618416 100644 (file)
--- 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