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.

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 22459edd49baf94f962f1ea1b2782f4200f97b5e..24cfa0091f1a326f9393e0b2faf1695fe0805389 100644 (file)
--- 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 b5899af665e59d91d89f050292ebf67aa0237e86..e92e09a9b40c1ba40de593a0f940472f34b6f581 100644 (file)
--- 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 d407621e97e1a5359bf7e27c8d60e02f7481a2ea..c4f06a136e2718ab41dc4493d74ea8f8bb2f9e32 100644 (file)
--- 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 1747077bd88611b23c4b1683e93fd73c823e3552..40137095cb5531e5b8e9ad8372115b28d9faebdd 100644 (file)
--- 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);
 }