From 0c2a43ab616c3670f3077758defcaa1f61cbe291 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Mon, 21 Dec 2020 18:16:53 +0100
Subject: [PATCH] Add proof for sine shift lemmas. (#5710)

This PR adds proofs for the sine shift lemmas that add equivalent instances of the sine function where the argument is in its "main phase" between minus pi and pi.
---
 src/expr/proof_rule.cpp                       |  1 +
 src/expr/proof_rule.h                         | 14 +++++++++++
 .../arith/nl/transcendental/proof_checker.cpp | 25 +++++++++++++++++++
 .../arith/nl/transcendental/sine_solver.cpp   |  8 +++++-
 4 files changed, 47 insertions(+), 1 deletion(-)

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 22459edd4..24cfa0091 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -160,6 +160,7 @@ const char* toString(PfRule id)
     case PfRule::INT_TRUST: return "INT_TRUST";
     case PfRule::ARITH_MULT_TANGENT: return "ARITH_MULT_TANGENT";
     case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM";
+    case PfRule::ARITH_TRANS_SINE_SHIFT: return "ARITH_TRANS_SINE_SHIFT";
     //================================================= Unknown rule
     case PfRule::UNKNOWN: return "UNKNOWN";
     default: return "?";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index b5899af66..e92e09a9b 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -1104,6 +1104,20 @@ enum class PfRule : uint32_t
   // or 1. tplane is the tangent plane of x*y at (a,b): b*x + a*y - a*b
   ARITH_MULT_TANGENT,
 
+  //======== Sine arg shifted to -pi..pi
+  // Children: none
+  // Arguments: (x, y, s)
+  // ---------------------
+  // Conclusion: (and
+  //   (<= -pi y pi)
+  //   (= (sin y) (sin x))
+  //   (ite (<= -pi x pi) (= x y) (= x (+ y (* 2 pi s))))
+  // )
+  // Where x is the argument to sine, y is a new real skolem that is x shifted
+  // into -pi..pi and s is a new integer skolem that is the number of phases y
+  // is shifted.
+  ARITH_TRANS_SINE_SHIFT,
+
   //================================================= Unknown rule
   UNKNOWN,
 };
diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp
index d407621e9..c4f06a136 100644
--- a/src/theory/arith/nl/transcendental/proof_checker.cpp
+++ b/src/theory/arith/nl/transcendental/proof_checker.cpp
@@ -29,6 +29,7 @@ namespace transcendental {
 
 void TranscendentalProofRuleChecker::registerTo(ProofChecker* pc)
 {
+  pc->registerChecker(PfRule::ARITH_TRANS_SINE_SHIFT, this);
 }
 
 Node TranscendentalProofRuleChecker::checkInternal(
@@ -45,6 +46,30 @@ Node TranscendentalProofRuleChecker::checkInternal(
   {
     Trace("nl-trans-checker") << "\t" << c << std::endl;
   }
+  if (id == PfRule::ARITH_TRANS_SINE_SHIFT)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 3);
+    const auto& x = args[0];
+    const auto& y = args[1];
+    const auto& s = args[2];
+    return nm->mkAnd(std::vector<Node>{
+        nm->mkAnd(std::vector<Node>{
+            nm->mkNode(Kind::GEQ, y, nm->mkNode(Kind::MULT, mone, pi)),
+            nm->mkNode(Kind::LEQ, y, pi)}),
+        nm->mkNode(
+            Kind::ITE,
+            nm->mkAnd(std::vector<Node>{
+                nm->mkNode(Kind::GEQ, x, nm->mkNode(Kind::MULT, mone, pi)),
+                nm->mkNode(Kind::LEQ, x, pi),
+            }),
+            x.eqNode(y),
+            x.eqNode(nm->mkNode(
+                Kind::PLUS,
+                y,
+                nm->mkNode(Kind::MULT, nm->mkConst<Rational>(2), s, pi)))),
+        nm->mkNode(Kind::SINE, y).eqNode(nm->mkNode(Kind::SINE, x))});
+  }
   return Node::null();
 }
 
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index 1747077bd..40137095c 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -70,11 +70,17 @@ void SineSolver::doPhaseShift(TNode a, TNode new_a, TNode y)
                                                    shift,
                                                    d_data->d_pi)))),
       new_a.eqNode(a));
+  CDProof* proof = nullptr;
+  if (d_data->isProofEnabled())
+  {
+    proof = d_data->getProof();
+    proof->addStep(lem, PfRule::ARITH_TRANS_SINE_SHIFT, {}, {a[0], y, shift});
+  }
   // note we must do preprocess on this lemma
   Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem
                         << std::endl;
   NlLemma nlem(
-      lem, LemmaProperty::PREPROCESS, nullptr, InferenceId::NL_T_PURIFY_ARG);
+      lem, LemmaProperty::PREPROCESS, proof, InferenceId::NL_T_PURIFY_ARG);
   d_data->d_im.addPendingArithLemma(nlem);
 }
 
-- 
2.30.2