diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-03-05 14:59:20 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-05 15:59:17 -0800 |
commit | e1845f92742854a35c294541bd931b898b0211d2 (patch) | |
tree | 39bbe132003a16610d7dbe2a576e0d70873ff856 /src/theory/arith/constraint.h | |
parent | 1caa321893805c826a18e68aa5a3c86ce5304a9f (diff) |
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.
Diffstat (limited to 'src/theory/arith/constraint.h')
-rw-r--r-- | src/theory/arith/constraint.h | 19 |
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(). |