Add function for tightening literals (#3732)

* Add function for tightening literals

The function tightens a literal if it can be tightened, and prints a
proof of the result.

* Include a #include

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>

2 files changed, 88 insertions, 0 deletions

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index 3ff0ff539..f1d7c0e43 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -23,6 +23,7 @@
 #include "proof/proof_manager.h"
 #include "proof/theory_proof.h"
 #include "theory/arith/constraint_forward.h"
+#include "theory/arith/normal_form.h"
 #include "theory/arith/theory_arith.h"
 
 #define CVC4_ARITH_VAR_TERM_PREFIX "term."
@@ -1055,6 +1056,80 @@ void LFSCArithProof::printLinearPolynomialPredicateNormalizer(std::ostream& o,
   o << ")))";
 }
 
+std::pair<Node, std::string> LFSCArithProof::printProofAndMaybeTighten(
+    const Node& bound)
+{
+  const Node & nonNegBound = bound.getKind() == kind::NOT ? bound[0] : bound;
+  std::ostringstream pfOfPossiblyTightenedPredicate;
+  if (nonNegBound[0].getType().isInteger()) {
+    switch(bound.getKind())
+    {
+      case kind::NOT:
+      {
+        // Tighten ~[i >= r] to [i < r] to [i <= {r}] to [-i >= -{r}]
+        // where
+        //    * i is an integer
+        //    * r is a real
+        //    * {r} denotes the greatest int less than r
+        //      it is equivalent to (ceil(r) - 1)
+        Assert(nonNegBound[1].getKind() == kind::CONST_RATIONAL);
+        Rational oldBound = nonNegBound[1].getConst<Rational>();
+        Integer newBound = -(oldBound.ceiling() - 1);
+        pfOfPossiblyTightenedPredicate
+            << "("
+            << (oldBound.isIntegral() ? "tighten_not_>=_IntInt"
+                                      : "tighten_not_>=_IntReal")
+            << " _ _ _ _ ("
+            << (oldBound.isIntegral()
+                    ? "check_neg_of_greatest_integer_below_int "
+                    : "check_neg_of_greatest_integer_below ");
+        printInteger(pfOfPossiblyTightenedPredicate, newBound);
+        pfOfPossiblyTightenedPredicate << " ";
+        if (oldBound.isIntegral())
+        {
+          printInteger(pfOfPossiblyTightenedPredicate, oldBound.ceiling());
+        }
+        else
+        {
+          printRational(pfOfPossiblyTightenedPredicate, oldBound);
+        }
+        pfOfPossiblyTightenedPredicate << ") " << ProofManager::getLitName(bound.negate(), "") << ")";
+        Node newLeft = (theory::arith::Polynomial::parsePolynomial(nonNegBound[0]) * -1).getNode();
+        Node newRight = NodeManager::currentNM()->mkConst(Rational(newBound));
+        Node newTerm = NodeManager::currentNM()->mkNode(kind::GEQ, newLeft, newRight);
+        return std::make_pair(newTerm, pfOfPossiblyTightenedPredicate.str());
+      }
+      case kind::GEQ:
+      {
+        // Tighten [i >= r] to [i >= ceil(r)]
+        // where
+        //    * i is an integer
+        //    * r is a real
+        Assert(nonNegBound[1].getKind() == kind::CONST_RATIONAL);
+
+        Rational oldBound = nonNegBound[1].getConst<Rational>();
+        if (oldBound.isIntegral()) {
+          pfOfPossiblyTightenedPredicate << ProofManager::getLitName(bound.negate(), "");
+          return std::make_pair(bound, pfOfPossiblyTightenedPredicate.str());
+        } else {
+          Integer newBound = oldBound.ceiling();
+          pfOfPossiblyTightenedPredicate << "(tighten_>=_IntReal _ _ " <<
+            newBound << " " << ProofManager::getLitName(bound.negate(), "") << ")";
+          Node newRight = NodeManager::currentNM()->mkConst(Rational(newBound));
+          Node newTerm = NodeManager::currentNM()->mkNode(kind::GEQ, nonNegBound[0], newRight);
+          return std::make_pair(newTerm, pfOfPossiblyTightenedPredicate.str());
+        }
+        break;
+      }
+      default: Unreachable();
+    }
+  } else {
+    return std::make_pair(bound, ProofManager::getLitName(bound.negate(), ""));
+  }
+  // Silence compiler warnings about missing a return.
+  Unreachable();
+}
+
 void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
                                            std::ostream& os,
                                            std::ostream& paren,
diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index 5522b4eb4..44e99cb76 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -192,6 +192,19 @@ public:
                                  const ProofLetMap& globalLetMap) override;
 
   /**
+   * Given a node that is an arith literal (an arith comparison or negation
+   * thereof), prints a proof of that literal.
+   *
+   * If the node represents a tightenable bound (e.g. [Int] < 3) then it prints
+   * a proof of the tightening instead. (e.g. [Int] <= 2).
+   *
+   * @return a pair comprising:
+   *            * the new node (after tightening) and
+   *            * a string proving it.
+   */
+  std::pair<Node, std::string> printProofAndMaybeTighten(const Node& bound);
+
+  /**
    * Return whether this node, when serialized to LFSC, has sort `Bool`. Otherwise, the sort is `formula`.
    */
   bool printsAsBool(const Node& n) override;