diff options
Diffstat (limited to 'src/theory/arith/constraint.cpp')
-rw-r--r-- | src/theory/arith/constraint.cpp | 28 |
1 files changed, 2 insertions, 26 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 56703c12a..20405d359 100644 --- 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()! |