From e20a8b4ea58f77a2d8a21b15d639d5a2a6a7b48d Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 9 Dec 2021 12:37:19 -0800 Subject: [PATCH] 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. --- src/theory/arith/nl/transcendental/sine_solver.cpp | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) 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); -- 2.30.2