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.

1 files changed, 317 insertions, 155 deletions

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<Constraint>& 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<ConstraintP>& 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<Constraint>& 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<PerVariableDatabase>& vec){
   std::vector<PerVariableDatabase>::const_iterator first = vec.begin();
   std::vector<PerVariableDatabase>::const_iterator last = vec.end();
@@ -550,7 +653,7 @@ ConstraintDatabase::~ConstraintDatabase(){
 
   delete d_watches;
 
-  std::vector<Constraint> constraintList;
+  std::vector<ConstraintP> 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<Constraint> constraintList;
+    std::vector<ConstraintP> 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<Constraint>& b){
+void Constraint_::propagate(const ConstraintCPVec& b){
   Assert(!hasProof());
   Assert(canBePropagated());
 
@@ -817,9 +937,8 @@ void ConstraintValue::propagate(const std::vector<Constraint>& 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<Constraint>& 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<Constraint>& 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<Constraint>& a){
+void Constraint_::markAsTrue(const ConstraintCPVec& 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;
+  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<Constraint>& 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<Constraint>& 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<Constraint>& b){
-  NodeBuilder<> nb(kind::AND);
-  for(vector<Constraint>::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<ConstraintCP, ConstraintCPHash> 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<Node>& out, Constraint a, Constraint b){
+void implies(std::vector<Node>& out, ConstraintP a, ConstraintP b){
   Node la = a->getLiteral();
   Node lb = b->getLiteral();
 
@@ -1153,7 +1316,7 @@ void implies(std::vector<Node>& out, Constraint a, Constraint b){
   out.push_back(orderOr);
 }
 
-void mutuallyExclusive(std::vector<Node>& out, Constraint a, Constraint b){
+void mutuallyExclusive(std::vector<Node>& out, ConstraintP a, ConstraintP b){
   Node la = a->getLiteral();
   Node lb = b->getLiteral();
 
@@ -1169,13 +1332,13 @@ void ConstraintDatabase::outputUnateInequalityLemmas(std::vector<Node>& 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<Node>& out, Ari
 
 void ConstraintDatabase::outputUnateEqualityLemmas(std::vector<Node>& out, ArithVar v) const{
 
-  vector<Constraint> equalities;
+  vector<ConstraintP> equalities;
 
   SortedConstraintMap& scm = getVariableSCM(v);
   SortedConstraintMapConstIterator scm_iter = scm.begin();
@@ -1197,34 +1360,34 @@ void ConstraintDatabase::outputUnateEqualityLemmas(std::vector<Node>& 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<Constraint>::const_iterator i, j, eq_end = equalities.end();
+  vector<ConstraintP>::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<Node>& 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;