Add a new arith constraint proof rule: IntTightenAP (#3818)

This rule is used when a bound on an integer expression is tightened
because of integer reasoning.

Before this rule was subsumed by IntHoleAP, a catch-all rule for integer
reasoning. We are now articulating IntTightenAP separately, because we
can produce proofs for it.

For IntHoleAP, we will have to omit a hole.

3 files changed, 45 insertions, 6 deletions

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 20405d359..56703c12a 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -93,6 +93,7 @@ std::ostream& operator<<(std::ostream& o, const ArithProofType apt){
   case FarkasAP:  o << "FarkasAP"; break;
   case TrichotomyAP:  o << "TrichotomyAP"; break;
   case EqualityEngineAP:  o << "EqualityEngineAP"; break;
+  case IntTightenAP: o << "IntTightenAP"; break;
   case IntHoleAP: o << "IntHoleAP"; break;
   default: break;
   }
@@ -518,6 +519,10 @@ bool Constraint::hasSimpleFarkasProof() const
   return true;
 }
 
+bool Constraint::hasIntTightenProof() const {
+  return getProofType() == IntTightenAP;
+}
+
 bool Constraint::hasIntHoleProof() const {
   return getProofType() == IntHoleAP;
 }
@@ -1247,6 +1252,25 @@ bool Constraint::allHaveProof(const ConstraintCPVec& b){
   return true;
 }
 
+void Constraint::impliedByIntTighten(ConstraintCP a, bool nowInConflict){
+  Debug("constraints::pf") << "impliedByIntTighten(" << this << ", " << *a << ")" << std::endl;
+  Assert(!hasProof());
+  Assert(negationHasProof() == nowInConflict);
+  Assert(a->hasProof());
+  Debug("pf::arith") << "impliedByIntTighten(" << this << ", " << a << ")"
+                     << std::endl;
+
+  d_database->d_antecedents.push_back(NullConstraint);
+  d_database->d_antecedents.push_back(a);
+  AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
+  d_database->pushConstraintRule(ConstraintRule(this, IntTightenAP, antecedentEnd));
+
+  Assert(inConflict() == nowInConflict);
+  if(inConflict()){
+    Debug("constraint::conflictCommit") << "inConflict impliedByIntTighten" << this << std::endl;
+  }
+}
+
 void Constraint::impliedByIntHole(ConstraintCP a, bool nowInConflict){
   Debug("constraints::pf") << "impliedByIntHole(" << this << ", " << *a << ")" << std::endl;
   Assert(!hasProof());
@@ -1439,7 +1463,7 @@ void Constraint::assertionFringe(ConstraintCPVec& v){
           writePos++;
         }else{
           Assert(vi->hasTrichotomyProof() || vi->hasFarkasProof()
-                 || vi->hasIntHoleProof());
+                 || vi->hasIntHoleProof() || vi->hasIntTightenProof());
           AntecedentId p = vi->getEndAntecedent();
 
           ConstraintCP antecedent = antecedents[p];
@@ -1509,7 +1533,7 @@ Node Constraint::externalExplain(AssertionOrder order) const{
   }else if(hasEqualityEngineProof()){
     return d_database->eeExplain(this);
   }else{
-    Assert(hasFarkasProof() || hasIntHoleProof() || hasTrichotomyProof());
+    Assert(hasFarkasProof() || hasIntHoleProof() || hasIntTightenProof() || hasTrichotomyProof());
     Assert(!antecentListIsEmpty());
     //Force the selection of the layer above if the node is
     // assertedToTheTheory()!
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 61b999a25..225bf555e 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -124,6 +124,8 @@ namespace arith {
  *                    :   !(x > a) and !(x < a) => x = a
  * - EqualityEngineAP : This is propagated by the equality engine.
  *                    : Consult this for the proof.
+ * - IntTightenAP     : This is indicates that a bound involving integers was tightened.
+ *                    : e.g. i < 5.5 became i <= 5, when i is an integer.
  * - IntHoleAP        : This is currently a catch-all for all integer specific reason.
  */
 enum ArithProofType
@@ -133,6 +135,7 @@ enum ArithProofType
     FarkasAP,
     TrichotomyAP,
     EqualityEngineAP,
+    IntTightenAP,
     IntHoleAP};
 
 /**
@@ -511,6 +514,9 @@ class Constraint {
    */
   bool hasSimpleFarkasProof() const;
 
+  /** Returns true if the node has a int bound tightening proof. */
+  bool hasIntTightenProof() const;
+
   /** Returns true if the node has a int hole proof. */
   bool hasIntHoleProof() const;
 
@@ -659,7 +665,16 @@ class Constraint {
 
   /**
    * Marks a the constraint c as being entailed by a.
-   * The reason has to do with integer rounding.
+   * The reason has to do with integer bound tightening.
+   *
+   * After calling impliedByIntTighten(), the caller should either raise a conflict
+   * or try call tryToPropagate().
+   */
+  void impliedByIntTighten(ConstraintCP a, bool inConflict);
+
+  /**
+   * Marks a the constraint c as being entailed by a.
+   * The reason has to do with integer reasoning.
    *
    * After calling impliedByIntHole(), the caller should either raise a conflict
    * or try call tryToPropagate().
@@ -668,7 +683,7 @@ class Constraint {
 
   /**
    * Marks a the constraint c as being entailed by a.
-   * The reason has to do with integer rounding.
+   * The reason has to do with integer reasoning.
    *
    * After calling impliedByIntHole(), the caller should either raise a conflict
    * or try call tryToPropagate().
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 037f0892a..786296b15 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -2020,7 +2020,7 @@ bool TheoryArithPrivate::assertionCases(ConstraintP constraint){
           Debug("arith::intbound") << "literal, before: " << constraint->getLiteral() << std::endl;
           Debug("arith::intbound") << "constraint, after: " << floorConstraint << std::endl;
         }
-        floorConstraint->impliedByIntHole(constraint, inConflict);
+        floorConstraint->impliedByIntTighten(constraint, inConflict);
         floorConstraint->tryToPropagate();
         if(inConflict){
           raiseConflict(floorConstraint);
@@ -2040,7 +2040,7 @@ bool TheoryArithPrivate::assertionCases(ConstraintP constraint){
           Debug("arith::intbound") << "literal, before: " << constraint->getLiteral() << std::endl;
           Debug("arith::intbound") << "constraint, after: " << ceilingConstraint << std::endl;
         }
-        ceilingConstraint->impliedByIntHole(constraint, inConflict);
+        ceilingConstraint->impliedByIntTighten(constraint, inConflict);
         ceilingConstraint->tryToPropagate();
         if(inConflict){
           raiseConflict(ceilingConstraint);