diff options
author | Tim King <taking@cs.nyu.edu> | 2012-04-17 16:07:22 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-04-17 16:07:22 +0000 |
commit | ccd77233892ace44fd4852999e66534d1c2283ea (patch) | |
tree | a856cacd24508a5839fcdbe728583ff055b64e34 /src/theory/arith/constraint.cpp | |
parent | 9644b6e12fbd3b649daafa43c5400d272e27bfb4 (diff) |
Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Below is a highlight of the changes:
- This introduces a new normal form to arithmetic.
-- Equalities and disequalities are in solved form.
Roughly speaking this means: (= x (+ y z)) is in normal form.
(See the comments in normal_form.h for what this formally requires.)
-- The normal form for inequality atoms always uses GEQ and GT instead of GEQ and LEQ.
Integer atoms always use GEQ.
- Constraint was added to TheoryArith.
-- A constraint is a triple of (k x v) where:
--- k is the type of the constraint (either LowerBound, UpperBound, Equality or Disequality),
--- x is an ArithVar, and
--- v is a DeltaRational value.
-- Constraints are always attached to a ConstraintDatabase.
-- A Constraint has its negation in the ConstraintDatabase [at least for now].
-- Every constraint belongs to a set of constraints for each ArithVar sorted by the delta rational values.
-- This set can be iterated over and provides efficient access to other constraints for this variable.
-- A literal may be attached to a constraint.
-- Constraints with attached literals may be marked as being asserted to the theory (sat context dependent).
-- Constraints can be propagated.
-- Every constraint has a proof (sat context dependent).
-- Proofs can be explained for either conflicts or propagations (if the node was propagated). (These proofs may be different.)
-- Equalities and disequalities can be marked as being split (user context dependent)
- This removes and replaces:
-- src/theory/arith/arith_prop_manager.*
-- src/theory/arith/atom_database.*
-- src/theory/arith/ordered_set.h
- Added isZero(), isOne() and isNegativeOne() to Rational and Integer.
- Added operator+ to CDList::const_iterator.
- Added const_iterator to CDQueue.
- Changes to regression tests.
Diffstat (limited to 'src/theory/arith/constraint.cpp')
-rw-r--r-- | src/theory/arith/constraint.cpp | 1130 |
1 files changed, 1130 insertions, 0 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp new file mode 100644 index 000000000..f78ecdddf --- /dev/null +++ b/src/theory/arith/constraint.cpp @@ -0,0 +1,1130 @@ + +#include "cvc4_private.h" +#include "theory/arith/constraint.h" +#include "theory/arith/arith_utilities.h" +#include "theory/arith/normal_form.h" + +#include <ostream> +#include <algorithm> + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace arith { + +/** Given a simplifiedKind this returns the corresponding ConstraintType. */ +//ConstraintType constraintTypeOfLiteral(Kind k); +ConstraintType constraintTypeOfComparison(const Comparison& cmp){ + Kind k = cmp.comparisonKind(); + switch(k){ + case LT: + case LEQ: + { + Polynomial l = cmp.getLeft(); + if(l.leadingCoefficientIsPositive()){ // (< x c) + return UpperBound; + }else{ + return LowerBound; // (< (-x) c) + } + } + case GT: + case GEQ: + { + Polynomial l = cmp.getLeft(); + if(l.leadingCoefficientIsPositive()){ + return LowerBound; // (> x c) + }else{ + return UpperBound; // (> (-x) c) + } + } + case EQUAL: + return Equality; + case DISTINCT: + return Disequality; + default: + Unhandled(k); + } +} + +ConstraintValue::ConstraintValue(ArithVar x, ConstraintType t, const DeltaRational& v) + : d_variable(x), + d_type(t), + d_value(v), + d_database(NULL), + d_literal(Node::null()), + d_negation(NullConstraint), + d_canBePropagated(false), + d_assertionOrder(AssertionOrderSentinel), + d_proof(ProofIdSentinel), + d_split(false), + d_variablePosition() +{ + Assert(!initialized()); +} + + +std::ostream& operator<<(std::ostream& o, const Constraint c){ + return o << *c; +} + +std::ostream& operator<<(std::ostream& o, const ConstraintType t){ + switch(t){ + case LowerBound: + return o << ">="; + case UpperBound: + return o << "<="; + case Equality: + return o << "="; + case Disequality: + return o << "!="; + default: + Unreachable(); + } +} + +std::ostream& operator<<(std::ostream& o, const ConstraintValue& c){ + o << c.getVariable() << ' ' << c.getType() << ' ' << c.getValue(); + if(c.hasLiteral()){ + o << "(node " << c.getLiteral() << ')'; + } + return o; +} + +std::ostream& operator<<(std::ostream& o, const ValueCollection& vc){ + o << "{"; + bool pending = false; + if(vc.hasEquality()){ + o << "eq: " << vc.getEquality(); + pending = true; + } + if(vc.hasLowerBound()){ + if(pending){ + o << ", "; + } + o << "lb: " << vc.getLowerBound(); + pending = true; + } + if(vc.hasUpperBound()){ + if(pending){ + o << ", "; + } + o << "ub: " << vc.getUpperBound(); + pending = true; + } + if(vc.hasDisequality()){ + if(pending){ + o << ", "; + } + o << "de: " << vc.getDisequality(); + } + return o << "}"; +} + +void ConstraintValue::debugPrint() const { + cout << *this << endl; +} + +void ValueCollection::push_into(std::vector<Constraint>& vec) const { + Debug("arith::constraint") << "push_into " << *this << endl; + if(hasEquality()){ + vec.push_back(d_equality); + } + if(hasLowerBound()){ + vec.push_back(d_lowerBound); + } + if(hasUpperBound()){ + vec.push_back(d_upperBound); + } + if(hasDisequality()){ + vec.push_back(d_disequality); + } +} + +ValueCollection ValueCollection::mkFromConstraint(Constraint c){ + ValueCollection ret; + Assert(ret.empty()); + switch(c->getType()){ + case LowerBound: + ret.d_lowerBound = c; + break; + case UpperBound: + ret.d_upperBound = c; + break; + case Equality: + ret.d_equality = c; + break; + case Disequality: + ret.d_disequality = c; + break; + default: + Unreachable(); + } + return ret; +} + +bool ValueCollection::hasConstraintOfType(ConstraintType t) const{ + switch(t){ + case LowerBound: + return hasLowerBound(); + case UpperBound: + return hasUpperBound(); + case Equality: + return hasEquality(); + case Disequality: + return hasDisequality(); + default: + Unreachable(); + } +} + +ArithVar ValueCollection::getVariable() const{ + Assert(!empty()); + return nonNull()->getVariable(); +} + +const DeltaRational& ValueCollection::getValue() const{ + Assert(!empty()); + return nonNull()->getValue(); +} + +void ValueCollection::add(Constraint c){ + Assert(c != NullConstraint); + + Assert(empty() || getVariable() == c->getVariable()); + Assert(empty() || getValue() == c->getValue()); + + switch(c->getType()){ + case LowerBound: + Assert(!hasLowerBound()); + d_lowerBound = c; + break; + case Equality: + Assert(!hasEquality()); + d_equality = c; + break; + case UpperBound: + Assert(!hasUpperBound()); + d_upperBound = c; + break; + case Disequality: + Assert(!hasDisequality()); + d_disequality = c; + break; + default: + Unreachable(); + } +} + +Constraint ValueCollection::getConstraintOfType(ConstraintType t) const{ + switch(t){ + case LowerBound: + Assert(hasLowerBound()); + return d_lowerBound; + case Equality: + Assert(hasEquality()); + return d_equality; + case UpperBound: + Assert(hasUpperBound()); + return d_upperBound; + case Disequality: + Assert(hasDisequality()); + return d_disequality; + default: + Unreachable(); + } +} + +void ValueCollection::remove(ConstraintType t){ + switch(t){ + case LowerBound: + Assert(hasLowerBound()); + d_lowerBound = NullConstraint; + break; + case Equality: + Assert(hasEquality()); + d_equality = NullConstraint; + break; + case UpperBound: + Assert(hasUpperBound()); + d_upperBound = NullConstraint; + break; + case Disequality: + Assert(hasDisequality()); + d_disequality = NullConstraint; + break; + default: + Unreachable(); + } +} + +bool ValueCollection::empty() const{ + return + !(hasLowerBound() || + hasUpperBound() || + hasEquality() || + hasDisequality()); +} + +Constraint 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()){ + return d_lowerBound; + }else if(hasUpperBound()){ + return d_upperBound; + }else if(hasEquality()){ + return d_equality; + }else if(hasDisequality()){ + return d_disequality; + }else{ + return NullConstraint; + } +} + +bool ConstraintValue::initialized() const { + return d_database != NULL; +} + +void ConstraintValue::initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, Constraint negation){ + Assert(!initialized()); + d_database = db; + d_variablePosition = v; + d_negation = negation; +} + +ConstraintValue::~ConstraintValue() { + Assert(safeToGarbageCollect()); + + if(initialized()){ + ValueCollection& vc = d_variablePosition->second; + Debug("arith::constraint") << "removing" << vc << endl; + + vc.remove(getType()); + + if(vc.empty()){ + Debug("arith::constraint") << "erasing" << vc << endl; + SortedConstraintMap& perVariable = d_database->getVariableSCM(getVariable()); + perVariable.erase(d_variablePosition); + } + + if(hasLiteral()){ + d_database->d_nodetoConstraintMap.erase(getLiteral()); + } + } +} + +const ValueCollection& ConstraintValue::getValueCollection() const{ + return d_variablePosition->second; +} + +Constraint ConstraintValue::getCeiling() { + Debug("getCeiling") << "ConstraintValue::getCeiling on " << *this << endl; + Assert(getValue().getInfinitesimalPart().sgn() > 0); + + DeltaRational ceiling(getValue().ceiling()); + +#warning "Optimize via the iterator" + return d_database->getConstraint(getVariable(), getType(), ceiling); +} + +Constraint ConstraintValue::getFloor() { + Assert(getValue().getInfinitesimalPart().sgn() < 0); + + DeltaRational floor(Rational(getValue().floor())); + +#warning "Optimize via the iterator" + return d_database->getConstraint(getVariable(), getType(), floor); +} + +void ConstraintValue::setCanBePropagated() { + Assert(!canBePropagated()); + d_database->pushCanBePropagatedWatch(this); +} + +void ConstraintValue::setAssertedToTheTheory() { + Assert(hasLiteral()); + Assert(!assertedToTheTheory()); + Assert(!d_negation->assertedToTheTheory()); + d_database->pushAssertionOrderWatch(this); +} + +bool ConstraintValue::isSelfExplaining() const { + return d_proof == d_database->d_selfExplainingProof; +} + +bool ConstraintValue::hasEqualityEngineProof() const { + return d_proof == d_database->d_equalityEngineProof; +} + +bool ConstraintValue::sanityChecking(Node n) const { + Comparison cmp = Comparison::parseNormalForm(n); + Kind k = cmp.comparisonKind(); + Polynomial pleft = cmp.normalizedVariablePart(); + Assert(k == EQUAL || k == DISTINCT || pleft.leadingCoefficientIsPositive()); + Assert(k != EQUAL || Monomial::isMember(n[0])); + Assert(k != DISTINCT || Monomial::isMember(n[0][0])); + + TNode left = pleft.getNode(); + DeltaRational right = cmp.normalizedDeltaRational(); + + const ArithVarNodeMap& av2node = d_database->getArithVarNodeMap(); + + Debug("nf::tmp") << cmp.getNode() << endl; + Debug("nf::tmp") << k << endl; + Debug("nf::tmp") << pleft.getNode() << endl; + Debug("nf::tmp") << left << endl; + Debug("nf::tmp") << right << endl; + Debug("nf::tmp") << getValue() << endl; + Debug("nf::tmp") << av2node.hasArithVar(left) << endl; + Debug("nf::tmp") << av2node.asArithVar(left) << endl; + Debug("nf::tmp") << getVariable() << endl; + + + if(av2node.hasArithVar(left) && + av2node.asArithVar(left) == getVariable() && + getValue() == right){ + switch(getType()){ + case LowerBound: + case UpperBound: + //Be overapproximate + return k == GT || k == GEQ ||k == LT || k == LEQ; + case Equality: + return k == EQUAL; + case Disequality: + return k == DISTINCT; + default: + Unreachable(); + } + }else{ + return false; + } +} + +Constraint ConstraintValue::makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r){ + switch(t){ + case LowerBound: + { + Assert(r.infinitesimalSgn() >= 0); + if(r.infinitesimalSgn() > 0){ + Assert(r.getInfinitesimalPart() == 1); + // make (not (v > r)), which is (v <= r) + DeltaRational dropInf(r.getNoninfinitesimalPart(), 0); + return new ConstraintValue(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); + } + } + case UpperBound: + { + Assert(r.infinitesimalSgn() <= 0); + if(r.infinitesimalSgn() < 0){ + Assert(r.getInfinitesimalPart() == -1); + // make (not (v < r)), which is (v >= r) + DeltaRational dropInf(r.getNoninfinitesimalPart(), 0); + return new ConstraintValue(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); + } + } + case Equality: + return new ConstraintValue(v, Disequality, r); + case Disequality: + return new ConstraintValue(v, Equality, r); + default: + Unreachable(); + return NullConstraint; + } +} + +ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext, const ArithVarNodeMap& av2nodeMap, + DifferenceManager& dm) + : d_varDatabases(), + d_toPropagate(satContext), + d_proofs(satContext, false), + d_watches(new Watches(satContext, userContext)), + d_av2nodeMap(av2nodeMap), + d_differenceManager(dm), + d_satContext(satContext), + d_satAllocationLevel(d_satContext->getLevel()) +{ + d_selfExplainingProof = d_proofs.size(); + d_proofs.push_back(NullConstraint); + + d_equalityEngineProof = d_proofs.size(); + d_proofs.push_back(NullConstraint); +} + +Constraint ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r){ + //This must always return a constraint. + + SortedConstraintMap& scm = getVariableSCM(v); + pair<SortedConstraintMapIterator, bool> insertAttempt; + insertAttempt = scm.insert(make_pair(r, ValueCollection())); + + SortedConstraintMapIterator pos = insertAttempt.first; + ValueCollection& vc = pos->second; + if(vc.hasConstraintOfType(t)){ + return vc.getConstraintOfType(t); + }else{ + Constraint c = new ConstraintValue(v, t, r); + Constraint negC = ConstraintValue::makeNegation(v, t, r); + + SortedConstraintMapIterator negPos; + if(t == Equality || t == Disequality){ + negPos = pos; + }else{ + pair<SortedConstraintMapIterator, bool> negInsertAttempt; + negInsertAttempt = scm.insert(make_pair(negC->getValue(), ValueCollection())); + Assert(negInsertAttempt.second); + negPos = negInsertAttempt.first; + } + + c->initialize(this, pos, negC); + negC->initialize(this, negPos, c); + + vc.add(c); + negPos->second.add(negC); + + return c; + } +} +bool ConstraintDatabase::emptyDatabase(const std::vector<PerVariableDatabase>& vec){ + std::vector<PerVariableDatabase>::const_iterator first = vec.begin(); + std::vector<PerVariableDatabase>::const_iterator last = vec.end(); + return std::find_if(first, last, PerVariableDatabase::IsEmpty) == last; +} + +ConstraintDatabase::~ConstraintDatabase(){ + Assert(d_satAllocationLevel <= d_satContext->getLevel()); + + delete d_watches; + + std::vector<Constraint> constraintList; + + while(!d_varDatabases.empty()){ + PerVariableDatabase* back = d_varDatabases.back(); + + SortedConstraintMap& scm = back->d_constraints; + SortedConstraintMapIterator i = scm.begin(), i_end = scm.end(); + for(; i != i_end; ++i){ + (i->second).push_into(constraintList); + } + while(!constraintList.empty()){ + Constraint c = constraintList.back(); + constraintList.pop_back(); + delete c; + } + Assert(scm.empty()); + d_varDatabases.pop_back(); + delete back; + } + + Assert(d_nodetoConstraintMap.empty()); +} + +void ConstraintDatabase::addVariable(ArithVar v){ + Assert(v == d_varDatabases.size()); + d_varDatabases.push_back(new PerVariableDatabase(v)); +} + +bool ConstraintValue::safeToGarbageCollect() const{ + return !isSplit() + && !canBePropagated() + && !hasProof() + && !assertedToTheTheory(); +} + +Node ConstraintValue::split(){ + Assert(isEquality() || isDisequality()); + + bool isEq = isEquality(); + + Constraint eq = isEq ? this : d_negation; + Constraint diseq = isEq ? d_negation : this; + + TNode eqNode = eq->getLiteral(); + Assert(eqNode.getKind() == kind::EQUAL); + TNode lhs = eqNode[0]; + TNode rhs = eqNode[1]; + + Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs; + Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs; + + Node lemma = NodeBuilder<3>(OR) << eqNode << ltNode << gtNode; + + + eq->d_database->pushSplitWatch(eq); + diseq->d_database->pushSplitWatch(diseq); + + return lemma; +} + +bool ConstraintDatabase::hasLiteral(TNode literal) const { + return lookup(literal) != NullConstraint; +} + +// Constraint ConstraintDatabase::addLiteral(TNode literal){ +// Assert(!hasLiteral(literal)); +// bool isNot = (literal.getKind() == NOT); +// TNode atom = isNot ? literal[0] : literal; + +// Constraint atomC = addAtom(atom); + +// return isNot ? atomC->d_negation : atomC; +// } + +// Constraint 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); +// } + +Constraint ConstraintDatabase::addLiteral(TNode literal){ + Assert(!hasLiteral(literal)); + bool isNot = (literal.getKind() == NOT); + Node atomNode = (isNot ? literal[0] : literal); + Node negationNode = atomNode.notNode(); + + Assert(!hasLiteral(atomNode)); + Assert(!hasLiteral(negationNode)); + Comparison posCmp = Comparison::parseNormalForm(atomNode); + + ConstraintType posType = constraintTypeOfComparison(posCmp); + + Polynomial nvp = posCmp.normalizedVariablePart(); + Debug("nf::tmp") << "here " << nvp.getNode() << " " << endl; + ArithVar v = d_av2nodeMap.asArithVar(nvp.getNode()); + + DeltaRational posDR = posCmp.normalizedDeltaRational(); + + Constraint posC = new ConstraintValue(v, posType, posDR); + + Debug("arith::constraint") << "addliteral( literal ->" << literal << ")" << endl; + Debug("arith::constraint") << "addliteral( posC ->" << posC << ")" << endl; + + SortedConstraintMap& scm = getVariableSCM(posC->getVariable()); + pair<SortedConstraintMapIterator, bool> insertAttempt; + insertAttempt = scm.insert(make_pair(posC->getValue(), ValueCollection())); + + SortedConstraintMapIterator posI = insertAttempt.first; + // If the attempt succeeds, i points to a new empty ValueCollection + // 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 + //the literal has not been associated with it. + Constraint hit = posI->second.getConstraintOfType(posC->getType()); + Debug("arith::constraint") << "hit " << hit << endl; + Debug("arith::constraint") << "posC " << posC << endl; + + delete posC; + + hit->setLiteral(atomNode); + hit->getNegation()->setLiteral(negationNode); + return isNot ? hit->getNegation(): hit; + }else{ + Comparison negCmp = Comparison::parseNormalForm(negationNode); + + ConstraintType negType = constraintTypeOfComparison(negCmp); + DeltaRational negDR = negCmp.normalizedDeltaRational(); + + Constraint negC = new ConstraintValue(v, negType, negDR); + + SortedConstraintMapIterator negI; + + if(posC->isEquality()){ + negI = posI; + }else{ + Assert(posC->isLowerBound() || posC->isUpperBound()); + + pair<SortedConstraintMapIterator, bool> negInsertAttempt; + negInsertAttempt = scm.insert(make_pair(negC->getValue(), ValueCollection())); + + Debug("nf::tmp") << "sdhjfgdhjkldfgljkhdfg" << endl; + Debug("nf::tmp") << negC << endl; + Debug("nf::tmp") << negC->getValue() << endl; + + //This should always succeed as the DeltaRational for the negation is unique! + Assert(negInsertAttempt.second); + + negI = negInsertAttempt.first; + } + + (posI->second).add(posC); + (negI->second).add(negC); + + posC->initialize(this, posI, negC); + negC->initialize(this, negI, posC); + + posC->setLiteral(atomNode); + negC->setLiteral(negationNode); + + return isNot ? negC : posC; + } +} + +// ConstraintType constraintTypeOfLiteral(Kind k){ +// switch(k){ +// case LT: +// case LEQ: +// return UpperBound; +// case GT: +// case GEQ: +// return LowerBound; +// case EQUAL: +// return Equality; +// case DISTINCT: +// return Disequality; +// default: +// Unreachable(); +// } +// } + +Constraint ConstraintDatabase::lookup(TNode literal) const{ + NodetoConstraintMap::const_iterator iter = d_nodetoConstraintMap.find(literal); + if(iter == d_nodetoConstraintMap.end()){ + return NullConstraint; + }else{ + return iter->second; + } +} + +void ConstraintValue::selfExplaining(){ + markAsTrue(); +} + +void ConstraintValue::propagate(){ + Assert(hasProof()); + Assert(canBePropagated()); + Assert(!assertedToTheTheory()); + Assert(!isSelfExplaining()); + + d_database->d_toPropagate.push(this); +} + +void ConstraintValue::propagate(Constraint a){ + Assert(!hasProof()); + Assert(canBePropagated()); + + markAsTrue(a); + propagate(); +} + +void ConstraintValue::propagate(Constraint a, Constraint b){ + Assert(!hasProof()); + Assert(canBePropagated()); + + markAsTrue(a, b); + propagate(); +} + +void ConstraintValue::propagate(const std::vector<Constraint>& b){ + Assert(!hasProof()); + Assert(canBePropagated()); + + markAsTrue(b); + propagate(); +} + +void ConstraintValue::impliedBy(Constraint a){ + Assert(!isTrue()); + Assert(!getNegation()->isTrue()); + + markAsTrue(a); + if(canBePropagated()){ + propagate(); + } +} + +void ConstraintValue::impliedBy(Constraint a, Constraint b){ + Assert(!isTrue()); + Assert(!getNegation()->isTrue()); + + markAsTrue(a, b); + if(canBePropagated()){ + propagate(); + } +} + +void ConstraintValue::impliedBy(const std::vector<Constraint>& b){ + Assert(!isTrue()); + Assert(!getNegation()->isTrue()); + + markAsTrue(b); + if(canBePropagated()){ + propagate(); + } +} + +void ConstraintValue::setEqualityEngineProof(){ + Assert(truthIsUnknown()); + Assert(hasLiteral()); + d_database->pushProofWatch(this, d_database->d_equalityEngineProof); +} + +void ConstraintValue::markAsTrue(){ + Assert(truthIsUnknown()); + Assert(hasLiteral()); + Assert(assertedToTheTheory()); + d_database->pushProofWatch(this, d_database->d_selfExplainingProof); +} + +void ConstraintValue::markAsTrue(Constraint imp){ + Assert(truthIsUnknown()); + Assert(imp->hasProof()); + + d_database->d_proofs.push_back(NullConstraint); + d_database->d_proofs.push_back(imp); + ProofId proof = d_database->d_proofs.size() - 1; + d_database->pushProofWatch(this, proof); +} + +void ConstraintValue::markAsTrue(Constraint impA, Constraint impB){ + Assert(truthIsUnknown()); + Assert(impA->hasProof()); + Assert(impB->hasProof()); + + d_database->d_proofs.push_back(NullConstraint); + d_database->d_proofs.push_back(impA); + d_database->d_proofs.push_back(impB); + ProofId proof = d_database->d_proofs.size() - 1; + + d_database->pushProofWatch(this, proof); +} + +void ConstraintValue::markAsTrue(const vector<Constraint>& a){ + Assert(truthIsUnknown()); + Assert(a.size() >= 1); + d_database->d_proofs.push_back(NullConstraint); + for(vector<Constraint>::const_iterator i = a.begin(), end = a.end(); i != end; ++i){ + Constraint c_i = *i; + Assert(c_i->hasProof()); + d_database->d_proofs.push_back(c_i); + } + + ProofId proof = d_database->d_proofs.size() - 1; + + d_database->pushProofWatch(this, proof); +} + +SortedConstraintMap& ConstraintValue::constraintSet() const{ + Assert(d_database->variableDatabaseIsSetup(d_variable)); + return (d_database->d_varDatabases[d_variable])->d_constraints; +} + +bool ConstraintValue::proofIsEmpty() const{ + Assert(hasProof()); + bool result = d_database->d_proofs[d_proof] == NullConstraint; + Assert((!result) || isSelfExplaining() || hasEqualityEngineProof()); + return result; +} + +void ConstraintValue::explainBefore(NodeBuilder<>& nb, AssertionOrder order) const{ + Assert(hasProof()); + Assert(!isSelfExplaining() || assertedToTheTheory()); + + if(assertedBefore(order)){ + nb << getLiteral(); + }else if(hasEqualityEngineProof()){ + d_database->eeExplain(this, nb); + }else{ + 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); + } + } +} +Node ConstraintValue::explainBefore(AssertionOrder order) const{ + Assert(hasProof()); + Assert(!isSelfExplaining() || assertedBefore(order)); + if(assertedBefore(order)){ + return getLiteral(); + }else if(hasEqualityEngineProof()){ + return d_database->eeExplain(this); + }else{ + Assert(!proofIsEmpty()); + //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); + }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); + } + return nb; + } + } +} + +Node ConstraintValue::explainConflict(Constraint a, Constraint b){ + NodeBuilder<> nb(kind::AND); + a->explainForConflict(nb); + b->explainForConflict(nb); + return nb; +} + +Node ConstraintValue::explainConflict(Constraint a, Constraint b, Constraint c){ + NodeBuilder<> nb(kind::AND); + a->explainForConflict(nb); + b->explainForConflict(nb); + c->explainForConflict(nb); + return nb; +} + +Constraint ConstraintValue::getStrictlyWeakerLowerBound(bool hasLiteral, bool asserted) const { + Assert(initialized()); + Assert(!asserted || hasLiteral); + + SortedConstraintMapConstIterator i = d_variablePosition; + const SortedConstraintMap& scm = constraintSet(); + SortedConstraintMapConstIterator i_begin = scm.begin(); + while(i != i_begin){ + --i; + const ValueCollection& vc = i->second; + if(vc.hasLowerBound()){ + Constraint weaker = vc.getLowerBound(); + + // asserted -> hasLiteral + // hasLiteral -> weaker->hasLiteral() + // asserted -> weaker->assertedToTheTheory() + if((!hasLiteral || (weaker->hasLiteral())) && + (!asserted || ( weaker->assertedToTheTheory()))){ + return weaker; + } + } + } + return NullConstraint; +} + +Constraint ConstraintValue::getStrictlyWeakerUpperBound(bool hasLiteral, bool asserted) const { + SortedConstraintMapConstIterator i = d_variablePosition; + const SortedConstraintMap& scm = constraintSet(); + SortedConstraintMapConstIterator i_end = scm.end(); + + ++i; + for(; i != i_end; ++i){ + const ValueCollection& vc = i->second; + if(vc.hasUpperBound()){ + Constraint weaker = vc.getUpperBound(); + if((!hasLiteral || (weaker->hasLiteral())) && + (!asserted || ( weaker->assertedToTheTheory()))){ + return weaker; + } + } + } + + return NullConstraint; +} + +Constraint ConstraintDatabase::getBestImpliedBound(ArithVar v, ConstraintType t, const DeltaRational& r) const { + Assert(variableDatabaseIsSetup(v)); + Assert(t == UpperBound || t == LowerBound); + + SortedConstraintMap& scm = getVariableSCM(v); + if(t == UpperBound){ + SortedConstraintMapConstIterator i = scm.lower_bound(r); + SortedConstraintMapConstIterator i_end = scm.end(); + Assert(i == i_end || r <= i->first); + for(; i != i_end; i++){ + Assert(r <= i->first); + const ValueCollection& vc = i->second; + if(vc.hasUpperBound()){ + return vc.getUpperBound(); + } + } + return NullConstraint; + }else{ + Assert(t == LowerBound); + if(scm.empty()){ + return NullConstraint; + }else{ + SortedConstraintMapConstIterator i = scm.lower_bound(r); + SortedConstraintMapConstIterator i_begin = scm.begin(); + SortedConstraintMapConstIterator i_end = scm.end(); + Assert(i == i_end || r <= i->first); + + int fdj = 0; + + if(i == i_end){ + --i; + Debug("getBestImpliedBound") << fdj++ << " " << r << " " << i->first << endl; + }else if( (i->first) > r){ + if(i == i_begin){ + return NullConstraint; + }else{ + --i; + Debug("getBestImpliedBound") << fdj++ << " " << r << " " << i->first << endl; + } + } + + do{ + Debug("getBestImpliedBound") << fdj++ << " " << r << " " << i->first << endl; + Assert(r >= i->first); + const ValueCollection& vc = i->second; + + if(vc.hasLowerBound()){ + return vc.getLowerBound(); + } + + if(i == i_begin){ + break; + }else{ + --i; + } + }while(true); + return NullConstraint; + } + } +} +Node ConstraintDatabase::eeExplain(const ConstraintValue* const c) const{ + Assert(c->hasLiteral()); + return d_differenceManager.explain(c->getLiteral()); +} + +void ConstraintDatabase::eeExplain(const ConstraintValue* const c, NodeBuilder<>& nb) const{ + Assert(c->hasLiteral()); + d_differenceManager.explain(c->getLiteral(), nb); +} + +bool ConstraintDatabase::variableDatabaseIsSetup(ArithVar v) const { + return v < d_varDatabases.size(); +} + + +ConstraintDatabase::Watches::Watches(context::Context* satContext, context::Context* userContext): + d_proofWatches(satContext), + d_canBePropagatedWatches(satContext), + d_assertionOrderWatches(satContext), + d_splitWatches(userContext) +{} + + +void ConstraintValue::setLiteral(Node n) { + Assert(!hasLiteral()); + Assert(sanityChecking(n)); + d_literal = n; + NodetoConstraintMap& map = d_database->d_nodetoConstraintMap; + Assert(map.find(n) == map.end()); + map.insert(make_pair(d_literal, this)); +} + +void implies(std::vector<Node>& out, Constraint a, Constraint b){ + Node la = a->getLiteral(); + Node lb = b->getLiteral(); + + Node neg_la = (la.getKind() == kind::NOT)? la[0] : la.notNode(); + + Assert(lb != neg_la); + Node orderOr = (lb < neg_la) ? lb.orNode(neg_la) : neg_la.orNode(lb); + out.push_back(orderOr); +} + +void mutuallyExclusive(std::vector<Node>& out, Constraint a, Constraint b){ + Node la = a->getLiteral(); + Node lb = b->getLiteral(); + + Node neg_la = (la.getKind() == kind::NOT)? la[0] : la.notNode(); + Node neg_lb = (lb.getKind() == kind::NOT)? lb[0] : lb.notNode(); + + Assert(neg_la != neg_lb); + Node orderOr = (neg_la < neg_lb) ? neg_la.orNode(neg_lb) : neg_lb.orNode(neg_la); + out.push_back(orderOr); +} + +void ConstraintDatabase::outputAllUnateLemmas(std::vector<Node>& out, ArithVar v) const{ + SortedConstraintMap& scm = getVariableSCM(v); + + SortedConstraintMapConstIterator outer; + SortedConstraintMapConstIterator scm_end = scm.end(); + + vector<Constraint> equalities; + for(outer = scm.begin(); outer != scm_end; ++outer){ + const ValueCollection& vc = outer->second; + if(vc.hasEquality()){ + Constraint eq = vc.getEquality(); + if(eq->hasLiteral()){ + equalities.push_back(eq); + } + } + } + + Constraint prev = NullConstraint; + //get transitive unates + //Only lower bounds or upperbounds should be done. + for(outer = scm.begin(); outer != scm_end; ++outer){ + const ValueCollection& vc = outer->second; + + if(vc.hasUpperBound()){ + Constraint ub = vc.getUpperBound(); + if(ub->hasLiteral()){ + if(prev != NullConstraint){ + implies(out, prev, ub); + } + prev = ub; + } + } + } + vector<Constraint>::const_iterator i, j, eq_end = equalities.end(); + for(i = equalities.begin(); i != eq_end; ++i){ + Constraint at_i = *i; + for(j= i + 1; j != eq_end; ++j){ + Constraint at_j = *j; + + mutuallyExclusive(out, at_i, at_j); + } + } + + for(i = equalities.begin(); i != eq_end; ++i){ + Constraint 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 ? + vc.getLowerBound() : eq->getStrictlyWeakerLowerBound(true, false); + Constraint ub = hasUB ? + vc.getUpperBound() : eq->getStrictlyWeakerUpperBound(true, false); + + if(hasUB && hasLB && !eq->isSplit()){ + out.push_back(eq->split()); + } + if(lb != NullConstraint){ + implies(out, eq, lb); + } + if(ub != NullConstraint){ + implies(out, eq, ub); + } + } + } + +void ConstraintDatabase::outputAllUnateLemmas(std::vector<Node>& lemmas) const{ + for(ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v){ + outputAllUnateLemmas(lemmas, v); + } +} + + +}/* arith namespace */ +}/* theory namespace */ +}/* CVC4 namespace */ |