From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Mon, 21 Dec 2020 19:49:24 +0000 (+0100)
Subject: Add proof for pi bound lemma (#5709)
X-Git-Tag: cvc5-1.0.0~2413
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c9747ae3a0577498073a04de97a978e1d9464d5d;p=cvc5.git

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 24cfa0091..a8b0c8b3d 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_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 e92e09a9b..9b7a54a09 100644
--- 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 c4f06a136..b5fccac85 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_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 67db4f2cc..b4f2e4cf6 100644
--- 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,