From: Gereon Kremer <gkremer@stanford.edu>
Date: Thu, 9 Dec 2021 20:37:19 +0000 (-0800)
Subject: Fix sine symmetry proof (#7783)
X-Git-Tag: cvc5-1.0.0~692
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e20a8b4ea58f77a2d8a21b15d639d5a2a6a7b48d;p=cvc5.git

Fix sine symmetry proof (#7783)

This PR fixes an issue in proofs for sine symmetry arising from the proof checker no longer using the rewriter.
---

diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index 583a54a51..338e37baa 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -143,7 +143,17 @@ void SineSolver::checkInitialRefine()
           if (d_data->isProofEnabled())
           {
             proof = d_data->getProof();
-            proof->addStep(lem, PfRule::ARITH_TRANS_SINE_SYMMETRY, {}, {t[0]});
+            Node tmplem =
+                nm->mkNode(Kind::PLUS,
+                           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);