From c360b3af4371cf871935a8bae96be5f8fecf741b Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 5 Mar 2020 14:59:20 -0800 Subject: [PATCH] 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. --- src/theory/arith/constraint.cpp | 28 +++++++++++++++++++++-- src/theory/arith/constraint.h | 19 +++++++++++++-- src/theory/arith/theory_arith_private.cpp | 4 ++-- 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); -- 2.30.2