diff options
| author | Gereon Kremer <gkremer@stanford.edu> | 2021-12-09 12:37:19 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-09 14:37:19 -0600 |
| commit | e20a8b4ea58f77a2d8a21b15d639d5a2a6a7b48d (patch) | |
| tree | 913a9bc49726b45a14a99372076c97e969b95c0b | |
| parent | 74f7773cda304b78417ecee22e8b9430725673c5 (diff) | |
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.
| -rw-r--r-- | src/theory/arith/nl/transcendental/sine_solver.cpp | 12 |
1 files changed, 11 insertions, 1 deletions
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); |