Add proof for pi bound lemma (#5709)

This PR adds proofs for lemmas that introduce bounds on the constant representing pi.

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 24cfa0091f1a326f9393e0b2faf1695fe0805389..a8b0c8b3db667e3f4b6d9eaf06d7067f537dad6e 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_PI: return "ARITH_TRANS_PI";
     case PfRule::ARITH_TRANS_SINE_SHIFT: return "ARITH_TRANS_SINE_SHIFT";
     //================================================= Unknown rule
     case PfRule::UNKNOWN: return "UNKNOWN";

diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index e92e09a9b40c1ba40de593a0f940472f34b6f581..9b7a54a09d040a9d7baa3af2a1a47b13c1712765 100644 (file)
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -1104,6 +1104,14 @@ 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,
 
+  // ================ Lemmas for transcendentals
+  //======== Assert bounds on PI
+  // Children: none
+  // Arguments: (l, u)
+  // ---------------------
+  // Conclusion: (and (>= real.pi l) (<= real.pi u))
+  // Where l (u) is a valid lower (upper) bound on pi.
+  ARITH_TRANS_PI,
   //======== Sine arg shifted to -pi..pi
   // Children: none
   // Arguments: (x, y, s)

diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp
index c4f06a136e2718ab41dc4493d74ea8f8bb2f9e32..b5fccac850f51792bae2e8feafaaba9cad77c755 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_PI, this);
   pc->registerChecker(PfRule::ARITH_TRANS_SINE_SHIFT, this);
 }
 
@@ -46,7 +47,13 @@ Node TranscendentalProofRuleChecker::checkInternal(
   {
     Trace("nl-trans-checker") << "\t" << c << std::endl;
   }
-  if (id == PfRule::ARITH_TRANS_SINE_SHIFT)
+  if (id == PfRule::ARITH_TRANS_PI)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 2);
+    return nm->mkAnd(std::vector<Node>{nm->mkNode(Kind::GEQ, pi, args[0]),
+                                       nm->mkNode(Kind::LEQ, pi, args[1])});
+  } else if (id == PfRule::ARITH_TRANS_SINE_SHIFT)
   {
     Assert(children.empty());
     Assert(args.size() == 3);

diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index 67db4f2cc875428719dfef81f692310ba9d1ffe2..b4f2e4cf6affc5eb34d3613edf4357a6abd577b9 100644 (file)
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -215,7 +215,14 @@ void TranscendentalState::getCurrentPiBounds()
   Node pi_lem = nm->mkNode(Kind::AND,
                            nm->mkNode(Kind::GEQ, d_pi, d_pi_bound[0]),
                            nm->mkNode(Kind::LEQ, d_pi, d_pi_bound[1]));
-  d_im.addPendingArithLemma(pi_lem, InferenceId::NL_T_PI_BOUND);
+  CDProof* proof = nullptr;
+  if (isProofEnabled())
+  {
+    proof = getProof();
+    proof->addStep(
+        pi_lem, PfRule::ARITH_TRANS_PI, {}, {d_pi_bound[0], d_pi_bound[1]});
+  }
+  d_im.addPendingArithLemma(pi_lem, InferenceId::NL_T_PI_BOUND, proof);
 }
 
 std::pair<Node, Node> TranscendentalState::getClosestSecantPoints(TNode e,