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.

1 files changed, 17 insertions, 2 deletions

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().