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

This reverts commit c360b3af4371cf871935a8bae96be5f8fecf741b.

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 56703c12a16c43d3ea418f0538e057490fbcc860..20405d359c7cbfd9f5468b90f95fdacc3c961402 100644 (file)
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -93,7 +93,6 @@ 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;
   }
@@ -519,10 +518,6 @@ bool Constraint::hasSimpleFarkasProof() const
   return true;
 }
 
-bool Constraint::hasIntTightenProof() const {
-  return getProofType() == IntTightenAP;
-}
-
 bool Constraint::hasIntHoleProof() const {
   return getProofType() == IntHoleAP;
 }
@@ -1252,25 +1247,6 @@ 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());
@@ -1463,7 +1439,7 @@ void Constraint::assertionFringe(ConstraintCPVec& v){
           writePos++;
         }else{
           Assert(vi->hasTrichotomyProof() || vi->hasFarkasProof()
-                 || vi->hasIntHoleProof() || vi->hasIntTightenProof());
+                 || vi->hasIntHoleProof());
           AntecedentId p = vi->getEndAntecedent();
 
           ConstraintCP antecedent = antecedents[p];
@@ -1533,7 +1509,7 @@ Node Constraint::externalExplain(AssertionOrder order) const{
   }else if(hasEqualityEngineProof()){
     return d_database->eeExplain(this);
   }else{
-    Assert(hasFarkasProof() || hasIntHoleProof() || hasIntTightenProof() || hasTrichotomyProof());
+    Assert(hasFarkasProof() || hasIntHoleProof() || 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 225bf555e1e12ae6dfe0c98c71e6b92666f0616e..61b999a259369e1ff02917bbb30484049de0ec06 100644 (file)
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -124,8 +124,6 @@ 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
@@ -135,7 +133,6 @@ enum ArithProofType
     FarkasAP,
     TrichotomyAP,
     EqualityEngineAP,
-    IntTightenAP,
     IntHoleAP};
 
 /**
@@ -514,9 +511,6 @@ 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;
 
@@ -665,16 +659,7 @@ class Constraint {
 
   /**
    * Marks a the constraint c as being entailed by a.
-   * 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.
+   * The reason has to do with integer rounding.
    *
    * After calling impliedByIntHole(), the caller should either raise a conflict
    * or try call tryToPropagate().
@@ -683,7 +668,7 @@ class Constraint {
 
   /**
    * Marks a the constraint c as being entailed by a.
-   * The reason has to do with integer reasoning.
+   * The reason has to do with integer rounding.
    *
    * 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 786296b156012d56bc34de582aa2165594b5f6f8..037f0892a13daba7256678b5ea6891a424596d47 100644 (file)
--- 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->impliedByIntTighten(constraint, inConflict);
+        floorConstraint->impliedByIntHole(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->impliedByIntTighten(constraint, inConflict);
+        ceilingConstraint->impliedByIntHole(constraint, inConflict);
         ceilingConstraint->tryToPropagate();
         if(inConflict){
           raiseConflict(ceilingConstraint);