From 9ccdea06edbc72e3ecd282e9e015f6fc4b2e7173 Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 7 Mar 2014 18:00:37 -0500 Subject: Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled. --- src/theory/arith/constraint.cpp | 472 +++++++++++++++++++++++++++------------- 1 file changed, 317 insertions(+), 155 deletions(-) (limited to 'src/theory/arith/constraint.cpp') diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 78b9d3494..acbd4a04b 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -64,7 +64,7 @@ ConstraintType constraintTypeOfComparison(const Comparison& cmp){ } } -ConstraintValue::ConstraintValue(ArithVar x, ConstraintType t, const DeltaRational& v) +Constraint_::Constraint_(ArithVar x, ConstraintType t, const DeltaRational& v) : d_variable(x), d_type(t), d_value(v), @@ -72,7 +72,7 @@ ConstraintValue::ConstraintValue(ArithVar x, ConstraintType t, const DeltaRatio d_literal(Node::null()), d_negation(NullConstraint), d_canBePropagated(false), - _d_assertionOrder(AssertionOrderSentinel), + d_assertionOrder(AssertionOrderSentinel), d_witness(TNode::null()), d_proof(ProofIdSentinel), d_split(false), @@ -82,7 +82,7 @@ ConstraintValue::ConstraintValue(ArithVar x, ConstraintType t, const DeltaRatio } -std::ostream& operator<<(std::ostream& o, const Constraint c){ +std::ostream& operator<<(std::ostream& o, const ConstraintP c){ if(c == NullConstraint){ return o << "NullConstraint"; }else{ @@ -105,7 +105,7 @@ std::ostream& operator<<(std::ostream& o, const ConstraintType t){ } } -std::ostream& operator<<(std::ostream& o, const ConstraintValue& c){ +std::ostream& operator<<(std::ostream& o, const Constraint_& c){ o << c.getVariable() << ' ' << c.getType() << ' ' << c.getValue(); if(c.hasLiteral()){ o << "(node " << c.getLiteral() << ')'; @@ -143,11 +143,67 @@ std::ostream& operator<<(std::ostream& o, const ValueCollection& vc){ return o << "}"; } -void ConstraintValue::debugPrint() const { +std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v){ + o << "[" << v.size() << "x"; + ConstraintCPVec::const_iterator i, end; + for(i=v.begin(), end=v.end(); i != end; ++i){ + ConstraintCP c = *i; + o << ", " << (*c); + } + o << "]"; + return o; +} + +void Constraint_::debugPrint() const { Message() << *this << endl; } -void ValueCollection::push_into(std::vector& vec) const { + +ValueCollection::ValueCollection() + : d_lowerBound(NullConstraint), + d_upperBound(NullConstraint), + d_equality(NullConstraint), + d_disequality(NullConstraint) +{} + +bool ValueCollection::hasLowerBound() const{ + return d_lowerBound != NullConstraint; +} + +bool ValueCollection::hasUpperBound() const{ + return d_upperBound != NullConstraint; +} + +bool ValueCollection::hasEquality() const{ + return d_equality != NullConstraint; +} + +bool ValueCollection::hasDisequality() const { + return d_disequality != NullConstraint; +} + +ConstraintP ValueCollection::getLowerBound() const { + Assert(hasLowerBound()); + return d_lowerBound; +} + +ConstraintP ValueCollection::getUpperBound() const { + Assert(hasUpperBound()); + return d_upperBound; +} + +ConstraintP ValueCollection::getEquality() const { + Assert(hasEquality()); + return d_equality; +} + +ConstraintP ValueCollection::getDisequality() const { + Assert(hasDisequality()); + return d_disequality; +} + + +void ValueCollection::push_into(std::vector& vec) const { Debug("arith::constraint") << "push_into " << *this << endl; if(hasEquality()){ vec.push_back(d_equality); @@ -163,7 +219,7 @@ void ValueCollection::push_into(std::vector& vec) const { } } -ValueCollection ValueCollection::mkFromConstraint(Constraint c){ +ValueCollection ValueCollection::mkFromConstraint(ConstraintP c){ ValueCollection ret; Assert(ret.empty()); switch(c->getType()){ @@ -210,7 +266,7 @@ const DeltaRational& ValueCollection::getValue() const{ return nonNull()->getValue(); } -void ValueCollection::add(Constraint c){ +void ValueCollection::add(ConstraintP c){ Assert(c != NullConstraint); Assert(empty() || getVariable() == c->getVariable()); @@ -238,7 +294,7 @@ void ValueCollection::add(Constraint c){ } } -Constraint ValueCollection::getConstraintOfType(ConstraintType t) const{ +ConstraintP ValueCollection::getConstraintOfType(ConstraintType t) const{ switch(t){ case LowerBound: Assert(hasLowerBound()); @@ -288,7 +344,7 @@ bool ValueCollection::empty() const{ hasDisequality()); } -Constraint ValueCollection::nonNull() const{ +ConstraintP ValueCollection::nonNull() const{ //This can be optimized by caching, but this is not necessary yet! /* "Premature optimization is the root of all evil." */ if(hasLowerBound()){ @@ -304,18 +360,18 @@ Constraint ValueCollection::nonNull() const{ } } -bool ConstraintValue::initialized() const { +bool Constraint_::initialized() const { return d_database != NULL; } -void ConstraintValue::initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, Constraint negation){ +void Constraint_::initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, ConstraintP negation){ Assert(!initialized()); d_database = db; d_variablePosition = v; d_negation = negation; } -ConstraintValue::~ConstraintValue() { +Constraint_::~Constraint_() { Assert(safeToGarbageCollect()); if(initialized()){ @@ -336,12 +392,12 @@ ConstraintValue::~ConstraintValue() { } } -const ValueCollection& ConstraintValue::getValueCollection() const{ +const ValueCollection& Constraint_::getValueCollection() const{ return d_variablePosition->second; } -Constraint ConstraintValue::getCeiling() { - Debug("getCeiling") << "ConstraintValue::getCeiling on " << *this << endl; +ConstraintP Constraint_::getCeiling() { + Debug("getCeiling") << "Constraint_::getCeiling on " << *this << endl; Assert(getValue().getInfinitesimalPart().sgn() > 0); DeltaRational ceiling(getValue().ceiling()); @@ -350,7 +406,7 @@ Constraint ConstraintValue::getCeiling() { return d_database->getConstraint(getVariable(), getType(), ceiling); } -Constraint ConstraintValue::getFloor() { +ConstraintP Constraint_::getFloor() { Assert(getValue().getInfinitesimalPart().sgn() < 0); DeltaRational floor(Rational(getValue().floor())); @@ -359,19 +415,26 @@ Constraint ConstraintValue::getFloor() { return d_database->getConstraint(getVariable(), getType(), floor); } -void ConstraintValue::setCanBePropagated() { +void Constraint_::setCanBePropagated() { Assert(!canBePropagated()); d_database->pushCanBePropagatedWatch(this); } -void ConstraintValue::setAssertedToTheTheory(TNode witness) { +void Constraint_::setAssertedToTheTheoryWithNegationTrue(TNode witness) { + Assert(hasLiteral()); + Assert(!assertedToTheTheory()); + Assert(d_negation->hasProof()); + d_database->pushAssertionOrderWatch(this, witness); +} + +void Constraint_::setAssertedToTheTheory(TNode witness) { Assert(hasLiteral()); Assert(!assertedToTheTheory()); Assert(!d_negation->assertedToTheTheory()); d_database->pushAssertionOrderWatch(this, witness); } -bool ConstraintValue::satisfiedBy(const DeltaRational& dr) const { +bool Constraint_::satisfiedBy(const DeltaRational& dr) const { switch(getType()){ case LowerBound: return getValue() <= dr; @@ -385,19 +448,19 @@ bool ConstraintValue::satisfiedBy(const DeltaRational& dr) const { Unreachable(); } -// bool ConstraintValue::isPsuedoConstraint() const { -// return d_proof == d_database->d_psuedoConstraintProof; -// } +bool Constraint_::isInternalDecision() const { + return d_proof == d_database->d_internalDecisionProof; +} -bool ConstraintValue::isSelfExplaining() const { +bool Constraint_::isSelfExplaining() const { return d_proof == d_database->d_selfExplainingProof; } -bool ConstraintValue::hasEqualityEngineProof() const { +bool Constraint_::hasEqualityEngineProof() const { return d_proof == d_database->d_equalityEngineProof; } -bool ConstraintValue::sanityChecking(Node n) const { +bool Constraint_::sanityChecking(Node n) const { Comparison cmp = Comparison::parseNormalForm(n); Kind k = cmp.comparisonKind(); Polynomial pleft = cmp.normalizedVariablePart(); @@ -441,7 +504,7 @@ bool ConstraintValue::sanityChecking(Node n) const { } } -Constraint ConstraintValue::makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r){ +ConstraintP Constraint_::makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r){ switch(t){ case LowerBound: { @@ -450,12 +513,12 @@ Constraint ConstraintValue::makeNegation(ArithVar v, ConstraintType t, const Del Assert(r.getInfinitesimalPart() == 1); // make (not (v > r)), which is (v <= r) DeltaRational dropInf(r.getNoninfinitesimalPart(), 0); - return new ConstraintValue(v, UpperBound, dropInf); + return new Constraint_(v, UpperBound, dropInf); }else{ Assert(r.infinitesimalSgn() == 0); // make (not (v >= r)), which is (v < r) DeltaRational addInf(r.getNoninfinitesimalPart(), -1); - return new ConstraintValue(v, UpperBound, addInf); + return new Constraint_(v, UpperBound, addInf); } } case UpperBound: @@ -465,18 +528,18 @@ Constraint ConstraintValue::makeNegation(ArithVar v, ConstraintType t, const Del Assert(r.getInfinitesimalPart() == -1); // make (not (v < r)), which is (v >= r) DeltaRational dropInf(r.getNoninfinitesimalPart(), 0); - return new ConstraintValue(v, LowerBound, dropInf); + return new Constraint_(v, LowerBound, dropInf); }else{ Assert(r.infinitesimalSgn() == 0); // make (not (v <= r)), which is (v > r) DeltaRational addInf(r.getNoninfinitesimalPart(), 1); - return new ConstraintValue(v, LowerBound, addInf); + return new Constraint_(v, LowerBound, addInf); } } case Equality: - return new ConstraintValue(v, Disequality, r); + return new Constraint_(v, Disequality, r); case Disequality: - return new ConstraintValue(v, Equality, r); + return new Constraint_(v, Equality, r); default: Unreachable(); return NullConstraint; @@ -500,11 +563,42 @@ ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Co d_equalityEngineProof = d_proofs.size(); d_proofs.push_back(NullConstraint); - // d_pseudoConstraintProof = d_proofs.size(); - // d_proofs.push_back(NullConstraint); + d_internalDecisionProof = d_proofs.size(); + d_proofs.push_back(NullConstraint); +} + +SortedConstraintMap& ConstraintDatabase::getVariableSCM(ArithVar v) const{ + Assert(variableDatabaseIsSetup(v)); + return d_varDatabases[v]->d_constraints; +} + +void ConstraintDatabase::pushSplitWatch(ConstraintP c){ + Assert(!c->d_split); + c->d_split = true; + d_watches->d_splitWatches.push_back(c); +} + + +void ConstraintDatabase::pushCanBePropagatedWatch(ConstraintP c){ + Assert(!c->d_canBePropagated); + c->d_canBePropagated = true; + d_watches->d_canBePropagatedWatches.push_back(c); +} + +void ConstraintDatabase::pushAssertionOrderWatch(ConstraintP c, TNode witness){ + Assert(!c->assertedToTheTheory()); + c->d_assertionOrder = d_watches->d_assertionOrderWatches.size(); + c->d_witness = witness; + d_watches->d_assertionOrderWatches.push_back(c); } -Constraint ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r){ +void ConstraintDatabase::pushProofWatch(ConstraintP c, ProofId pid){ + Assert(c->d_proof == ProofIdSentinel); + c->d_proof = pid; + d_watches->d_proofWatches.push_back(c); +} + +ConstraintP ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r){ //This must always return a constraint. SortedConstraintMap& scm = getVariableSCM(v); @@ -516,8 +610,8 @@ Constraint ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, const if(vc.hasConstraintOfType(t)){ return vc.getConstraintOfType(t); }else{ - Constraint c = new ConstraintValue(v, t, r); - Constraint negC = ConstraintValue::makeNegation(v, t, r); + ConstraintP c = new Constraint_(v, t, r); + ConstraintP negC = Constraint_::makeNegation(v, t, r); SortedConstraintMapIterator negPos; if(t == Equality || t == Disequality){ @@ -539,6 +633,15 @@ Constraint ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, const return c; } } + +ConstraintP ConstraintDatabase::ensureConstraint(ValueCollection& vc, ConstraintType t){ + if(vc.hasConstraintOfType(t)){ + return vc.getConstraintOfType(t); + }else{ + return getConstraint(vc.getVariable(), t, vc.getValue()); + } +} + bool ConstraintDatabase::emptyDatabase(const std::vector& vec){ std::vector::const_iterator first = vec.begin(); std::vector::const_iterator last = vec.end(); @@ -550,7 +653,7 @@ ConstraintDatabase::~ConstraintDatabase(){ delete d_watches; - std::vector constraintList; + std::vector constraintList; while(!d_varDatabases.empty()){ PerVariableDatabase* back = d_varDatabases.back(); @@ -561,7 +664,7 @@ ConstraintDatabase::~ConstraintDatabase(){ (i->second).push_into(constraintList); } while(!constraintList.empty()){ - Constraint c = constraintList.back(); + ConstraintP c = constraintList.back(); constraintList.pop_back(); delete c; } @@ -586,17 +689,25 @@ ConstraintDatabase::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_unatePropagateImplications); } +void ConstraintDatabase::deleteConstraintAndNegation(ConstraintP c){ + Assert(c->safeToGarbageCollect()); + ConstraintP neg = c->getNegation(); + Assert(neg->safeToGarbageCollect()); + delete c; + delete neg; +} + void ConstraintDatabase::addVariable(ArithVar v){ if(d_reclaimable.isMember(v)){ SortedConstraintMap& scm = getVariableSCM(v); - std::vector constraintList; + std::vector constraintList; for(SortedConstraintMapIterator i = scm.begin(), end = scm.end(); i != end; ++i){ (i->second).push_into(constraintList); } while(!constraintList.empty()){ - Constraint c = constraintList.back(); + ConstraintP c = constraintList.back(); constraintList.pop_back(); Assert(c->safeToGarbageCollect()); delete c; @@ -605,6 +716,7 @@ void ConstraintDatabase::addVariable(ArithVar v){ d_reclaimable.remove(v); }else{ + Debug("arith::constraint") << "about to fail" << v << " " << d_varDatabases.size() << endl; Assert(v == d_varDatabases.size()); d_varDatabases.push_back(new PerVariableDatabase(v)); } @@ -615,20 +727,20 @@ void ConstraintDatabase::removeVariable(ArithVar v){ d_reclaimable.add(v); } -bool ConstraintValue::safeToGarbageCollect() const{ +bool Constraint_::safeToGarbageCollect() const{ return !isSplit() && !canBePropagated() && !hasProof() && !assertedToTheTheory(); } -Node ConstraintValue::split(){ +Node Constraint_::split(){ Assert(isEquality() || isDisequality()); bool isEq = isEquality(); - Constraint eq = isEq ? this : d_negation; - Constraint diseq = isEq ? d_negation : this; + ConstraintP eq = isEq ? this : d_negation; + ConstraintP diseq = isEq ? d_negation : this; TNode eqNode = eq->getLiteral(); Assert(eqNode.getKind() == kind::EQUAL); @@ -651,26 +763,26 @@ bool ConstraintDatabase::hasLiteral(TNode literal) const { return lookup(literal) != NullConstraint; } -// Constraint ConstraintDatabase::addLiteral(TNode literal){ +// ConstraintP ConstraintDatabase::addLiteral(TNode literal){ // Assert(!hasLiteral(literal)); // bool isNot = (literal.getKind() == NOT); // TNode atom = isNot ? literal[0] : literal; -// Constraint atomC = addAtom(atom); +// ConstraintP atomC = addAtom(atom); // return isNot ? atomC->d_negation : atomC; // } -// Constraint ConstraintDatabase::allocateConstraintForComparison(ArithVar v, const Comparison cmp){ +// ConstraintP ConstraintDatabase::allocateConstraintForComparison(ArithVar v, const Comparison cmp){ // Debug("arith::constraint") << "allocateConstraintForLiteral(" << v << ", "<< cmp <<")" << endl; // Kind kind = cmp.comparisonKind(); // ConstraintType type = constraintTypeOfLiteral(kind); // DeltaRational dr = cmp.getDeltaRational(); -// return new ConstraintValue(v, type, dr); +// return new Constraint_(v, type, dr); // } -Constraint ConstraintDatabase::addLiteral(TNode literal){ +ConstraintP ConstraintDatabase::addLiteral(TNode literal){ Assert(!hasLiteral(literal)); bool isNot = (literal.getKind() == NOT); Node atomNode = (isNot ? literal[0] : literal); @@ -688,7 +800,7 @@ Constraint ConstraintDatabase::addLiteral(TNode literal){ DeltaRational posDR = posCmp.normalizedDeltaRational(); - Constraint posC = new ConstraintValue(v, posType, posDR); + ConstraintP posC = new Constraint_(v, posType, posDR); Debug("arith::constraint") << "addliteral( literal ->" << literal << ")" << endl; Debug("arith::constraint") << "addliteral( posC ->" << posC << ")" << endl; @@ -702,9 +814,9 @@ Constraint ConstraintDatabase::addLiteral(TNode literal){ // If the attempt fails, i points to a pre-existing ValueCollection if(posI->second.hasConstraintOfType(posC->getType())){ - //This is the situation where the Constraint exists, but + //This is the situation where the ConstraintP exists, but //the literal has not been associated with it. - Constraint hit = posI->second.getConstraintOfType(posC->getType()); + ConstraintP hit = posI->second.getConstraintOfType(posC->getType()); Debug("arith::constraint") << "hit " << hit << endl; Debug("arith::constraint") << "posC " << posC << endl; @@ -719,7 +831,7 @@ Constraint ConstraintDatabase::addLiteral(TNode literal){ ConstraintType negType = constraintTypeOfComparison(negCmp); DeltaRational negDR = negCmp.normalizedDeltaRational(); - Constraint negC = new ConstraintValue(v, negType, negDR); + ConstraintP negC = new Constraint_(v, negType, negDR); SortedConstraintMapIterator negI; @@ -771,7 +883,7 @@ Constraint ConstraintDatabase::addLiteral(TNode literal){ // } // } -Constraint ConstraintDatabase::lookup(TNode literal) const{ +ConstraintP ConstraintDatabase::lookup(TNode literal) const{ NodetoConstraintMap::const_iterator iter = d_nodetoConstraintMap.find(literal); if(iter == d_nodetoConstraintMap.end()){ return NullConstraint; @@ -780,11 +892,19 @@ Constraint ConstraintDatabase::lookup(TNode literal) const{ } } -void ConstraintValue::selfExplaining(){ +void Constraint_::selfExplainingWithNegationTrue(){ + Assert(!hasProof()); + Assert(getNegation()->hasProof()); + Assert(hasLiteral()); + Assert(assertedToTheTheory()); + d_database->pushProofWatch(this, d_database->d_selfExplainingProof); +} + +void Constraint_::selfExplaining(){ markAsTrue(); } -void ConstraintValue::propagate(){ +void Constraint_::propagate(){ Assert(hasProof()); Assert(canBePropagated()); Assert(!assertedToTheTheory()); @@ -793,7 +913,7 @@ void ConstraintValue::propagate(){ d_database->d_toPropagate.push(this); } -void ConstraintValue::propagate(Constraint a){ +void Constraint_::propagate(ConstraintCP a){ Assert(!hasProof()); Assert(canBePropagated()); @@ -801,7 +921,7 @@ void ConstraintValue::propagate(Constraint a){ propagate(); } -void ConstraintValue::propagate(Constraint a, Constraint b){ +void Constraint_::propagate(ConstraintCP a, ConstraintCP b){ Assert(!hasProof()); Assert(canBePropagated()); @@ -809,7 +929,7 @@ void ConstraintValue::propagate(Constraint a, Constraint b){ propagate(); } -void ConstraintValue::propagate(const std::vector& b){ +void Constraint_::propagate(const ConstraintCPVec& b){ Assert(!hasProof()); Assert(canBePropagated()); @@ -817,9 +937,8 @@ void ConstraintValue::propagate(const std::vector& b){ propagate(); } -void ConstraintValue::impliedBy(Constraint a){ - Assert(!isTrue()); - Assert(!getNegation()->isTrue()); +void Constraint_::impliedBy(ConstraintCP a){ + Assert(truthIsUnknown()); markAsTrue(a); if(canBePropagated()){ @@ -827,9 +946,8 @@ void ConstraintValue::impliedBy(Constraint a){ } } -void ConstraintValue::impliedBy(Constraint a, Constraint b){ - Assert(!isTrue()); - Assert(!getNegation()->isTrue()); +void Constraint_::impliedBy(ConstraintCP a, ConstraintCP b){ + Assert(truthIsUnknown()); markAsTrue(a, b); if(canBePropagated()){ @@ -837,9 +955,8 @@ void ConstraintValue::impliedBy(Constraint a, Constraint b){ } } -void ConstraintValue::impliedBy(const std::vector& b){ - Assert(!isTrue()); - Assert(!getNegation()->isTrue()); +void Constraint_::impliedBy(const ConstraintCPVec& b){ + Assert(truthIsUnknown()); markAsTrue(b); if(canBePropagated()){ @@ -847,30 +964,29 @@ void ConstraintValue::impliedBy(const std::vector& b){ } } -// void ConstraintValue::setPseudoConstraint(){ -// Assert(truthIsUnknown()); -// Assert(!hasLiteral()); +void Constraint_::setInternalDecision(){ + Assert(truthIsUnknown()); + Assert(!assertedToTheTheory()); -// d_database->pushProofWatch(this, d_database->d_pseudoConstraintProof); -// } + d_database->pushProofWatch(this, d_database->d_internalDecisionProof); +} -void ConstraintValue::setEqualityEngineProof(){ +void Constraint_::setEqualityEngineProof(){ Assert(truthIsUnknown()); Assert(hasLiteral()); d_database->pushProofWatch(this, d_database->d_equalityEngineProof); } -void ConstraintValue::markAsTrue(){ +void Constraint_::markAsTrue(){ Assert(truthIsUnknown()); Assert(hasLiteral()); Assert(assertedToTheTheory()); d_database->pushProofWatch(this, d_database->d_selfExplainingProof); } -void ConstraintValue::markAsTrue(Constraint imp){ +void Constraint_::markAsTrue(ConstraintCP imp){ Assert(truthIsUnknown()); Assert(imp->hasProof()); - //Assert(!imp->isPseudoConstraint()); d_database->d_proofs.push_back(NullConstraint); d_database->d_proofs.push_back(imp); @@ -878,12 +994,10 @@ void ConstraintValue::markAsTrue(Constraint imp){ d_database->pushProofWatch(this, proof); } -void ConstraintValue::markAsTrue(Constraint impA, Constraint impB){ +void Constraint_::markAsTrue(ConstraintCP impA, ConstraintCP impB){ Assert(truthIsUnknown()); Assert(impA->hasProof()); Assert(impB->hasProof()); - //Assert(!impA->isPseudoConstraint()); - //Assert(!impB->isPseudoConstraint()); d_database->d_proofs.push_back(NullConstraint); d_database->d_proofs.push_back(impA); @@ -893,12 +1007,12 @@ void ConstraintValue::markAsTrue(Constraint impA, Constraint impB){ d_database->pushProofWatch(this, proof); } -void ConstraintValue::markAsTrue(const vector& a){ +void Constraint_::markAsTrue(const ConstraintCPVec& a){ Assert(truthIsUnknown()); Assert(a.size() >= 1); d_database->d_proofs.push_back(NullConstraint); - for(vector::const_iterator i = a.begin(), end = a.end(); i != end; ++i){ - Constraint c_i = *i; + for(ConstraintCPVec::const_iterator i = a.begin(), end = a.end(); i != end; ++i){ + ConstraintCP c_i = *i; Assert(c_i->hasProof()); //Assert(!c_i->isPseudoConstraint()); d_database->d_proofs.push_back(c_i); @@ -909,12 +1023,12 @@ void ConstraintValue::markAsTrue(const vector& a){ d_database->pushProofWatch(this, proof); } -SortedConstraintMap& ConstraintValue::constraintSet() const{ +SortedConstraintMap& Constraint_::constraintSet() const{ Assert(d_database->variableDatabaseIsSetup(d_variable)); return (d_database->d_varDatabases[d_variable])->d_constraints; } -bool ConstraintValue::proofIsEmpty() const{ +bool Constraint_::proofIsEmpty() const{ Assert(hasProof()); bool result = d_database->d_proofs[d_proof] == NullConstraint; //Assert((!result) || isSelfExplaining() || hasEqualityEngineProof() || isPseudoConstraint()); @@ -922,32 +1036,76 @@ bool ConstraintValue::proofIsEmpty() const{ return result; } -Node ConstraintValue::makeImplication(const std::vector& b) const{ - Node antecedent = makeConjunction(b); +Node Constraint_::externalImplication(const ConstraintCPVec& b) const{ + Assert(hasLiteral()); + Node antecedent = externalExplainByAssertions(b); Node implied = getLiteral(); return antecedent.impNode(implied); } -Node ConstraintValue::makeConjunction(const std::vector& b){ - NodeBuilder<> nb(kind::AND); - for(vector::const_iterator i = b.begin(), end = b.end(); i != end; ++i){ - Constraint b_i = *i; - b_i->explainBefore(nb, AssertionOrderSentinel); +Node Constraint_::externalExplainByAssertions(const ConstraintCPVec& b){ + return externalExplain(b, AssertionOrderSentinel); +} + +struct ConstraintCPHash { + /* Todo replace with an id */ + size_t operator()(ConstraintCP c) const{ + Assert(sizeof(ConstraintCP) > 0); + return ((size_t)c)/sizeof(ConstraintCP); } - if(nb.getNumChildren() >= 2){ - return nb; - }else if(nb.getNumChildren() == 1){ - return nb[0]; - }else{ - return mkBoolNode(true); +}; + +void Constraint_::assertionFringe(ConstraintCPVec& v){ + hash_set visited; + size_t writePos = 0; + + if(!v.empty()){ + const ConstraintDatabase* db = v.back()->d_database; + const CDConstraintList& proofs = db->d_proofs; + for(size_t i = 0; i < v.size(); ++i){ + ConstraintCP vi = v[i]; + if(visited.find(vi) == visited.end()){ + Assert(vi->hasProof()); + visited.insert(vi); + if(vi->onFringe()){ + v[writePos] = vi; + writePos++; + }else{ + Assert(!vi->isSelfExplaining()); + ProofId p = vi->d_proof; + ConstraintCP antecedent = proofs[p]; + while(antecedent != NullConstraint){ + v.push_back(antecedent); + --p; + antecedent = proofs[p]; + } + } + } + } + v.resize(writePos); + } +} + +void Constraint_::assertionFringe(ConstraintCPVec& o, const ConstraintCPVec& i){ + o.insert(o.end(), i.begin(), i.end()); + assertionFringe(o); +} + +Node Constraint_::externalExplain(const ConstraintCPVec& v, AssertionOrder order){ + NodeBuilder<> nb(kind::AND); + ConstraintCPVec::const_iterator i, end; + for(i = v.begin(), end = v.end(); i != end; ++i){ + ConstraintCP v_i = *i; + v_i->externalExplain(nb, order); } + return safeConstructNary(nb); } -void ConstraintValue::explainBefore(NodeBuilder<>& nb, AssertionOrder order) const{ +void Constraint_::externalExplain(NodeBuilder<>& nb, AssertionOrder order) const{ Assert(hasProof()); Assert(!isSelfExplaining() || assertedToTheTheory()); - + Assert(!isInternalDecision()); if(assertedBefore(order)){ nb << getWitness(); @@ -956,56 +1114,61 @@ void ConstraintValue::explainBefore(NodeBuilder<>& nb, AssertionOrder order) con }else{ Assert(!isSelfExplaining()); ProofId p = d_proof; - Constraint antecedent = d_database->d_proofs[p]; + ConstraintCP antecedent = d_database->d_proofs[p]; for(; antecedent != NullConstraint; antecedent = d_database->d_proofs[--p] ){ - antecedent->explainBefore(nb, order); + antecedent->externalExplain(nb, order); } } } -Node ConstraintValue::explainBefore(AssertionOrder order) const{ + +Node Constraint_::externalExplain(AssertionOrder order) const{ Assert(hasProof()); Assert(!isSelfExplaining() || assertedBefore(order)); + Assert(!isInternalDecision()); if(assertedBefore(order)){ return getWitness(); }else if(hasEqualityEngineProof()){ return d_database->eeExplain(this); }else{ Assert(!proofIsEmpty()); - //Force the selection of the layer above if the node is assertedToTheTheory()! + //Force the selection of the layer above if the node is + // assertedToTheTheory()! if(d_database->d_proofs[d_proof-1] == NullConstraint){ - Constraint antecedent = d_database->d_proofs[d_proof]; - return antecedent->explainBefore(order); + ConstraintCP antecedent = d_database->d_proofs[d_proof]; + return antecedent->externalExplain(order); }else{ NodeBuilder<> nb(kind::AND); Assert(!isSelfExplaining()); ProofId p = d_proof; - Constraint antecedent = d_database->d_proofs[p]; - for(; antecedent != NullConstraint; antecedent = d_database->d_proofs[--p] ){ - antecedent->explainBefore(nb, order); + ConstraintCP antecedent = d_database->d_proofs[p]; + while(antecedent != NullConstraint){ + antecedent->externalExplain(nb, order); + --p; + antecedent = d_database->d_proofs[p]; } return nb; } } } -Node ConstraintValue::explainConflict(Constraint a, Constraint b){ +Node Constraint_::externalExplainByAssertions(ConstraintCP a, ConstraintCP b){ NodeBuilder<> nb(kind::AND); - a->explainForConflict(nb); - b->explainForConflict(nb); + a->externalExplainByAssertions(nb); + b->externalExplainByAssertions(nb); return nb; } -Node ConstraintValue::explainConflict(Constraint a, Constraint b, Constraint c){ +Node Constraint_::externalExplainByAssertions(ConstraintCP a, ConstraintCP b, ConstraintCP c){ NodeBuilder<> nb(kind::AND); - a->explainForConflict(nb); - b->explainForConflict(nb); - c->explainForConflict(nb); + a->externalExplainByAssertions(nb); + b->externalExplainByAssertions(nb); + c->externalExplainByAssertions(nb); return nb; } -Constraint ConstraintValue::getStrictlyWeakerLowerBound(bool hasLiteral, bool asserted) const { +ConstraintP Constraint_::getStrictlyWeakerLowerBound(bool hasLiteral, bool asserted) const { Assert(initialized()); Assert(!asserted || hasLiteral); @@ -1016,7 +1179,7 @@ Constraint ConstraintValue::getStrictlyWeakerLowerBound(bool hasLiteral, bool as --i; const ValueCollection& vc = i->second; if(vc.hasLowerBound()){ - Constraint weaker = vc.getLowerBound(); + ConstraintP weaker = vc.getLowerBound(); // asserted -> hasLiteral // hasLiteral -> weaker->hasLiteral() @@ -1030,7 +1193,7 @@ Constraint ConstraintValue::getStrictlyWeakerLowerBound(bool hasLiteral, bool as return NullConstraint; } -Constraint ConstraintValue::getStrictlyWeakerUpperBound(bool hasLiteral, bool asserted) const { +ConstraintP Constraint_::getStrictlyWeakerUpperBound(bool hasLiteral, bool asserted) const { SortedConstraintMapConstIterator i = d_variablePosition; const SortedConstraintMap& scm = constraintSet(); SortedConstraintMapConstIterator i_end = scm.end(); @@ -1039,7 +1202,7 @@ Constraint ConstraintValue::getStrictlyWeakerUpperBound(bool hasLiteral, bool as for(; i != i_end; ++i){ const ValueCollection& vc = i->second; if(vc.hasUpperBound()){ - Constraint weaker = vc.getUpperBound(); + ConstraintP weaker = vc.getUpperBound(); if((!hasLiteral || (weaker->hasLiteral())) && (!asserted || ( weaker->assertedToTheTheory()))){ return weaker; @@ -1050,7 +1213,7 @@ Constraint ConstraintValue::getStrictlyWeakerUpperBound(bool hasLiteral, bool as return NullConstraint; } -Constraint ConstraintDatabase::getBestImpliedBound(ArithVar v, ConstraintType t, const DeltaRational& r) const { +ConstraintP ConstraintDatabase::getBestImpliedBound(ArithVar v, ConstraintType t, const DeltaRational& r) const { Assert(variableDatabaseIsSetup(v)); Assert(t == UpperBound || t == LowerBound); @@ -1110,12 +1273,12 @@ Constraint ConstraintDatabase::getBestImpliedBound(ArithVar v, ConstraintType t, } } } -Node ConstraintDatabase::eeExplain(const ConstraintValue* const c) const{ +Node ConstraintDatabase::eeExplain(const Constraint_* const c) const{ Assert(c->hasLiteral()); return d_congruenceManager.explain(c->getLiteral()); } -void ConstraintDatabase::eeExplain(const ConstraintValue* const c, NodeBuilder<>& nb) const{ +void ConstraintDatabase::eeExplain(const Constraint_* const c, NodeBuilder<>& nb) const{ Assert(c->hasLiteral()); d_congruenceManager.explain(c->getLiteral(), nb); } @@ -1133,7 +1296,7 @@ ConstraintDatabase::Watches::Watches(context::Context* satContext, context::Cont {} -void ConstraintValue::setLiteral(Node n) { +void Constraint_::setLiteral(Node n) { Assert(!hasLiteral()); Assert(sanityChecking(n)); d_literal = n; @@ -1142,7 +1305,7 @@ void ConstraintValue::setLiteral(Node n) { map.insert(make_pair(d_literal, this)); } -void implies(std::vector& out, Constraint a, Constraint b){ +void implies(std::vector& out, ConstraintP a, ConstraintP b){ Node la = a->getLiteral(); Node lb = b->getLiteral(); @@ -1153,7 +1316,7 @@ void implies(std::vector& out, Constraint a, Constraint b){ out.push_back(orderOr); } -void mutuallyExclusive(std::vector& out, Constraint a, Constraint b){ +void mutuallyExclusive(std::vector& out, ConstraintP a, ConstraintP b){ Node la = a->getLiteral(); Node lb = b->getLiteral(); @@ -1169,13 +1332,13 @@ void ConstraintDatabase::outputUnateInequalityLemmas(std::vector& out, Ari SortedConstraintMap& scm = getVariableSCM(v); SortedConstraintMapConstIterator scm_iter = scm.begin(); SortedConstraintMapConstIterator scm_end = scm.end(); - Constraint prev = NullConstraint; + ConstraintP prev = NullConstraint; //get transitive unates //Only lower bounds or upperbounds should be done. for(; scm_iter != scm_end; ++scm_iter){ const ValueCollection& vc = scm_iter->second; if(vc.hasUpperBound()){ - Constraint ub = vc.getUpperBound(); + ConstraintP ub = vc.getUpperBound(); if(ub->hasLiteral()){ if(prev != NullConstraint){ implies(out, prev, ub); @@ -1188,7 +1351,7 @@ void ConstraintDatabase::outputUnateInequalityLemmas(std::vector& out, Ari void ConstraintDatabase::outputUnateEqualityLemmas(std::vector& out, ArithVar v) const{ - vector equalities; + vector equalities; SortedConstraintMap& scm = getVariableSCM(v); SortedConstraintMapConstIterator scm_iter = scm.begin(); @@ -1197,34 +1360,34 @@ void ConstraintDatabase::outputUnateEqualityLemmas(std::vector& out, Arith for(; scm_iter != scm_end; ++scm_iter){ const ValueCollection& vc = scm_iter->second; if(vc.hasEquality()){ - Constraint eq = vc.getEquality(); + ConstraintP eq = vc.getEquality(); if(eq->hasLiteral()){ equalities.push_back(eq); } } } - vector::const_iterator i, j, eq_end = equalities.end(); + vector::const_iterator i, j, eq_end = equalities.end(); for(i = equalities.begin(); i != eq_end; ++i){ - Constraint at_i = *i; + ConstraintP at_i = *i; for(j= i + 1; j != eq_end; ++j){ - Constraint at_j = *j; + ConstraintP at_j = *j; mutuallyExclusive(out, at_i, at_j); } } for(i = equalities.begin(); i != eq_end; ++i){ - Constraint eq = *i; + ConstraintP eq = *i; const ValueCollection& vc = eq->getValueCollection(); Assert(vc.hasEquality() && vc.getEquality()->hasLiteral()); bool hasLB = vc.hasLowerBound() && vc.getLowerBound()->hasLiteral(); bool hasUB = vc.hasUpperBound() && vc.getUpperBound()->hasLiteral(); - Constraint lb = hasLB ? + ConstraintP lb = hasLB ? vc.getLowerBound() : eq->getStrictlyWeakerLowerBound(true, false); - Constraint ub = hasUB ? + ConstraintP ub = hasUB ? vc.getUpperBound() : eq->getStrictlyWeakerUpperBound(true, false); if(hasUB && hasLB && !eq->isSplit()){ @@ -1251,21 +1414,20 @@ void ConstraintDatabase::outputUnateInequalityLemmas(std::vector& lemmas) } } -void ConstraintDatabase::raiseUnateConflict(Constraint ant, Constraint cons){ +void ConstraintDatabase::raiseUnateConflict(ConstraintP ant, ConstraintP cons){ Assert(ant->hasProof()); - Constraint negCons = cons->getNegation(); + ConstraintP negCons = cons->getNegation(); Assert(negCons->hasProof()); Debug("arith::unate::conf") << ant << "implies " << cons << endl; Debug("arith::unate::conf") << negCons << " is true." << endl; - - Node conf = ConstraintValue::explainConflict(ant, negCons); - Debug("arith::unate::conf") << conf << std::endl; - d_raiseConflict(conf); + d_raiseConflict.addConstraint(ant); + d_raiseConflict.addConstraint(negCons); + d_raiseConflict.commitConflict(); } -void ConstraintDatabase::unatePropLowerBound(Constraint curr, Constraint prev){ +void ConstraintDatabase::unatePropLowerBound(ConstraintP curr, ConstraintP prev){ Debug("arith::unate") << "unatePropLowerBound " << curr << " " << prev << endl; Assert(curr != prev); Assert(curr != NullConstraint); @@ -1297,7 +1459,7 @@ void ConstraintDatabase::unatePropLowerBound(Constraint curr, Constraint prev){ //Don't worry about implying the negation of upperbound. //These should all be handled by propagating the LowerBounds! if(vc.hasLowerBound()){ - Constraint lb = vc.getLowerBound(); + ConstraintP lb = vc.getLowerBound(); if(lb->negationHasProof()){ raiseUnateConflict(curr, lb); return; @@ -1309,7 +1471,7 @@ void ConstraintDatabase::unatePropLowerBound(Constraint curr, Constraint prev){ } } if(vc.hasDisequality()){ - Constraint dis = vc.getDisequality(); + ConstraintP dis = vc.getDisequality(); if(dis->negationHasProof()){ raiseUnateConflict(curr, dis); return; @@ -1323,7 +1485,7 @@ void ConstraintDatabase::unatePropLowerBound(Constraint curr, Constraint prev){ } } -void ConstraintDatabase::unatePropUpperBound(Constraint curr, Constraint prev){ +void ConstraintDatabase::unatePropUpperBound(ConstraintP curr, ConstraintP prev){ Debug("arith::unate") << "unatePropUpperBound " << curr << " " << prev << endl; Assert(curr != prev); Assert(curr != NullConstraint); @@ -1348,7 +1510,7 @@ void ConstraintDatabase::unatePropUpperBound(Constraint curr, Constraint prev){ //Don't worry about implying the negation of upperbound. //These should all be handled by propagating the UpperBounds! if(vc.hasUpperBound()){ - Constraint ub = vc.getUpperBound(); + ConstraintP ub = vc.getUpperBound(); if(ub->negationHasProof()){ raiseUnateConflict(curr, ub); return; @@ -1359,7 +1521,7 @@ void ConstraintDatabase::unatePropUpperBound(Constraint curr, Constraint prev){ } } if(vc.hasDisequality()){ - Constraint dis = vc.getDisequality(); + ConstraintP dis = vc.getDisequality(); if(dis->negationHasProof()){ raiseUnateConflict(curr, dis); return; @@ -1373,7 +1535,7 @@ void ConstraintDatabase::unatePropUpperBound(Constraint curr, Constraint prev){ } } -void ConstraintDatabase::unatePropEquality(Constraint curr, Constraint prevLB, Constraint prevUB){ +void ConstraintDatabase::unatePropEquality(ConstraintP curr, ConstraintP prevLB, ConstraintP prevUB){ Debug("arith::unate") << "unatePropEquality " << curr << " " << prevLB << " " << prevUB << endl; Assert(curr != prevLB); Assert(curr != prevUB); @@ -1405,7 +1567,7 @@ void ConstraintDatabase::unatePropEquality(Constraint curr, Constraint prevLB, C //Don't worry about implying the negation of upperbound. //These should all be handled by propagating the LowerBounds! if(vc.hasLowerBound()){ - Constraint lb = vc.getLowerBound(); + ConstraintP lb = vc.getLowerBound(); if(lb->negationHasProof()){ raiseUnateConflict(curr, lb); return; @@ -1416,7 +1578,7 @@ void ConstraintDatabase::unatePropEquality(Constraint curr, Constraint prevLB, C } } if(vc.hasDisequality()){ - Constraint dis = vc.getDisequality(); + ConstraintP dis = vc.getDisequality(); if(dis->negationHasProof()){ raiseUnateConflict(curr, dis); return; @@ -1440,7 +1602,7 @@ void ConstraintDatabase::unatePropEquality(Constraint curr, Constraint prevLB, C //Don't worry about implying the negation of upperbound. //These should all be handled by propagating the UpperBounds! if(vc.hasUpperBound()){ - Constraint ub = vc.getUpperBound(); + ConstraintP ub = vc.getUpperBound(); if(ub->negationHasProof()){ raiseUnateConflict(curr, ub); return; @@ -1452,7 +1614,7 @@ void ConstraintDatabase::unatePropEquality(Constraint curr, Constraint prevLB, C } } if(vc.hasDisequality()){ - Constraint dis = vc.getDisequality(); + ConstraintP dis = vc.getDisequality(); if(dis->negationHasProof()){ raiseUnateConflict(curr, dis); return; -- cgit v1.2.3