Updates based on the group code review of arithmetic on 2011-02-15. The only substan...

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 31867c4cf2c76bb1cb52e9e6dc6311820842c9da..139a533509b7307bc4dc5e074d242b7b44baa8d2 100644 (file)
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -17,9 +17,7 @@ libarith_la_SOURCES = \
        delta_rational.cpp \
        partial_model.h \
        partial_model.cpp \
-       ordered_bounds_list.h \
        ordered_set.h \
-       arithvar_dense_set.h \
        arithvar_set.h \
        tableau.h \
        tableau.cpp \

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 452d54fae8809e64868b4615d29d86736c4be848..c8532f1a26c49a59c559b75ba4d0dee4ecde4ff4 100644 (file)
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -119,16 +119,22 @@ inline bool isRelationOperator(Kind k){
   }
 }
 
-/** is k \in {LT, LEQ, EQ, GEQ, GT} */
+/**
+ * Given a relational kind, k, return the kind k' s.t.
+ * swapping the lefthand and righthand side is equivalent.
+ *
+ * The following equivalence should hold, 
+ *   (k l r) <=> (k' r l)
+ */
 inline Kind reverseRelationKind(Kind k){
   using namespace kind;
 
   switch(k){
-  case LT: return GT;
-  case LEQ: return GEQ;
+  case LT:    return GT;
+  case LEQ:   return GEQ;
   case EQUAL: return EQUAL;
-  case GEQ: return LEQ;
-  case GT: return LT;
+  case GEQ:   return LEQ;
+  case GT:    return LT;
 
   default:
     Unreachable();
@@ -150,56 +156,13 @@ inline bool evaluateConstantPredicate(Kind k, const Rational& left, const Ration
   }
 }
 
-
-
-inline Node pushInNegation(Node assertion){
-  using namespace CVC4::kind;
-  Assert(assertion.getKind() == NOT);
-
-  Node p = assertion[0];
-
-  Kind k;
-
-  switch(p.getKind()){
-  case EQUAL:
-    return assertion;
-  case GT:
-    k = LEQ;
-    break;
-  case GEQ:
-    k = LT;
-    break;
-  case LEQ:
-    k = GT;
-    break;
-  case LT:
-    k = GEQ;
-    break;
-  default:
-    Unreachable();
-  }
-
-  return NodeManager::currentNM()->mkNode(k, p[0],p[1]);
-}
-
 /**
- * Validates that a node constraint has the following form:
- *   constraint: x |><| c
- * where |><| is either <, <=, ==, >=, LT,
- * x is of metakind a variabale,
- * and c is a constant rational.
+ * Returns the appropraite coefficient for the infinitesimal given the kind
+ * for an arithmetic atom inorder to represent strict inequalities as inequalities.
+ *   x < c  becomes  x <= c + (-1) * \delta
+ *   x > c  becomes  x >= x + ( 1) * \delta
+ * Non-strict inequalities have a coefficient of zero.
  */
-inline bool validateConstraint(TNode constraint){
-  using namespace CVC4::kind;
-  switch(constraint.getKind()){
-  case LT:case LEQ: case EQUAL: case GEQ: case GT: break;
-  default: return false;
-  }
-
-  if(constraint[0].getMetaKind() != metakind::VARIABLE) return false;
-  return constraint[1].getKind() == CONST_RATIONAL;
-}
-
 inline int deltaCoeff(Kind k){
   switch(k){
   case kind::LT:
@@ -256,6 +219,26 @@ inline int deltaCoeff(Kind k){
   }
 }
 
+ /**
+  * Takes two nodes with exactly 2 children,
+  * the second child of both are of kind CONST_RATIONAL,
+  * and compares value of the two children.
+  * This is for comparing inequality nodes.
+  *   RightHandRationalLT((<= x 50), (< x 75)) == true
+  */
+struct RightHandRationalLT
+{
+  bool operator()(TNode s1, TNode s2) const
+  {
+    TNode rh1 = s1[1];
+    TNode rh2 = s2[1];
+    const Rational& c1 = rh1.getConst<Rational>();
+    const Rational& c2 = rh2.getConst<Rational>();
+    int cmpRes = c1.cmp(c2);
+    return cmpRes < 0;
+  }
+};
+
 }; /* namesapce arith */
 }; /* namespace theory */
 }; /* namespace CVC4 */

diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h
index fa606188a09bb1985d37f513c0a081643c8761bb..68c5e18c9140929e0e928379ceb22ca57e8d8a2f 100644 (file)
--- a/src/theory/arith/ordered_set.h
+++ b/src/theory/arith/ordered_set.h
@@ -2,26 +2,15 @@
 #include "expr/kind.h"
 #include "expr/node.h"
 #include "util/Assert.h"
+#include "theory/arith/arith_utilities.h"
 
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
-struct RightHandRationalLT
-{
-  bool operator()(TNode s1, TNode s2) const
-  {
-    TNode rh1 = s1[1];
-    TNode rh2 = s2[1];
-    const Rational& c1 = rh1.getConst<Rational>();
-    const Rational& c2 = rh2.getConst<Rational>();
-    int cmpRes = c1.cmp(c2);
-    return cmpRes < 0;
-  }
-};
 
-typedef std::set<Node, RightHandRationalLT> OrderedSet;
+typedef std::set<TNode, RightHandRationalLT> OrderedSet;
 
 struct SetCleanupStrategy{
   static void cleanup(OrderedSet* l){

diff --git a/src/theory/arith/unate_propagator.cpp b/src/theory/arith/unate_propagator.cpp
index e042e2320fe3f39901e33bbea54888d3aaa6c252..069f4f0f33a974e0c872c02e4097126cebbf7716 100644 (file)
--- a/src/theory/arith/unate_propagator.cpp
+++ b/src/theory/arith/unate_propagator.cpp
@@ -30,28 +30,37 @@ using namespace CVC4::kind;
 
 using namespace std;
 
-struct PropagatorLeqSetID {};
-typedef expr::Attribute<PropagatorLeqSetID, OrderedSet*, SetCleanupStrategy> PropagatorLeqSet;
-
-struct PropagatorEqSetID {};
-typedef expr::Attribute<PropagatorEqSetID, OrderedSet*, SetCleanupStrategy> PropagatorEqSet;
-
-struct PropagatorGeqSetID {};
-typedef expr::Attribute<PropagatorGeqSetID, OrderedSet*, SetCleanupStrategy> PropagatorGeqSet;
-
 ArithUnatePropagator::ArithUnatePropagator(context::Context* cxt, OutputChannel& out) :
-  d_arithOut(out)
+  d_arithOut(out), d_orderedListMap()
 { }
 
 bool ArithUnatePropagator::leftIsSetup(TNode left){
-  return left.hasAttribute(PropagatorEqSet());
+  return d_orderedListMap.find(left) != d_orderedListMap.end();
+}
+
+ArithUnatePropagator::OrderedSetTriple& ArithUnatePropagator::getOrderedSetTriple(TNode left){
+  Assert(leftIsSetup(left));
+  return d_orderedListMap[left];
+}
+
+OrderedSet& ArithUnatePropagator::getEqSet(TNode left){
+  Assert(leftIsSetup(left));
+  return getOrderedSetTriple(left).d_eqSet;
+}
+OrderedSet& ArithUnatePropagator::getLeqSet(TNode left){
+  Assert(leftIsSetup(left));
+  return getOrderedSetTriple(left).d_leqSet;
+}
+OrderedSet& ArithUnatePropagator::getGeqSet(TNode left){
+  Assert(leftIsSetup(left));
+  return getOrderedSetTriple(left).d_geqSet;
 }
 
 bool ArithUnatePropagator::hasAnyAtoms(TNode v){
   Assert(!leftIsSetup(v)
-         || !v.getAttribute(PropagatorEqSet())->empty()
-         || !v.getAttribute(PropagatorLeqSet())->empty()
-         || !v.getAttribute(PropagatorGeqSet())->empty());
+         || !(getEqSet(v)).empty()
+         || !(getLeqSet(v)).empty()
+         || !(getGeqSet(v)).empty());
 
   return leftIsSetup(v);
 }
@@ -59,13 +68,7 @@ bool ArithUnatePropagator::hasAnyAtoms(TNode v){
 void ArithUnatePropagator::setupLefthand(TNode left){
   Assert(!leftIsSetup(left));
 
-  OrderedSet* eqList = new OrderedSet();
-  OrderedSet* leqList = new OrderedSet();
-  OrderedSet* geqList = new OrderedSet();
-
-  left.setAttribute(PropagatorEqSet(), eqList);
-  left.setAttribute(PropagatorLeqSet(), geqList);
-  left.setAttribute(PropagatorGeqSet(), leqList);
+  d_orderedListMap[left] = OrderedSetTriple();
 }
 
 void ArithUnatePropagator::addAtom(TNode atom){
@@ -76,38 +79,38 @@ void ArithUnatePropagator::addAtom(TNode atom){
     setupLefthand(left);
   }
 
-  OrderedSet* eqSet = left.getAttribute(PropagatorEqSet());
-  OrderedSet* leqSet = left.getAttribute(PropagatorLeqSet());
-  OrderedSet* geqSet = left.getAttribute(PropagatorGeqSet());
+  OrderedSet& eqSet = getEqSet(left);
+  OrderedSet& leqSet = getLeqSet(left);
+  OrderedSet& geqSet = getGeqSet(left);
 
   switch(atom.getKind()){
   case EQUAL:
     {
-      pair<OrderedSet::iterator, bool> res = eqSet->insert(atom);
+      pair<OrderedSet::iterator, bool> res = eqSet.insert(atom);
       Assert(res.second);
-      addEqualityToEqualities(atom, eqSet, res.first);
-      addEqualityToLeqs(atom, leqSet);
-      addEqualityToGeqs(atom, geqSet);
+      addImplicationsUsingEqualityAndEqualityList(atom, eqSet);
+      addImplicationsUsingEqualityAndLeqList(atom, leqSet);
+      addImplicationsUsingEqualityAndGeqList(atom, geqSet);
       break;
     }
   case LEQ:
     {
-      pair<OrderedSet::iterator, bool> res = leqSet->insert(atom);
+      pair<OrderedSet::iterator, bool> res = leqSet.insert(atom);
       Assert(res.second);
 
-      addLeqToLeqs(atom, leqSet, res.first);
-      addLeqToEqualities(atom, eqSet);
-      addLeqToGeqs(atom, geqSet);
+      addImplicationsUsingLeqAndEqualityList(atom, eqSet);
+      addImplicationsUsingLeqAndLeqList(atom, leqSet);
+      addImplicationsUsingLeqAndGeqList(atom, geqSet);
       break;
     }
   case GEQ:
     {
-      pair<OrderedSet::iterator, bool> res = geqSet->insert(atom);
+      pair<OrderedSet::iterator, bool> res = geqSet.insert(atom);
       Assert(res.second);
 
-      addGeqToGeqs(atom, geqSet, res.first);
-      addGeqToEqualities(atom, eqSet);
-      addGeqToLeqs(atom, leqSet);
+      addImplicationsUsingGeqAndEqualityList(atom, eqSet);
+      addImplicationsUsingGeqAndLeqList(atom, leqSet);
+      addImplicationsUsingGeqAndGeqList(atom, geqSet);
 
       break;
     }
@@ -125,23 +128,24 @@ bool rightHandRationalIsEqual(TNode a, TNode b){
 
   return qA == qB;
 }
-bool rightHandRationalIsLT(TNode a, TNode b){
-  TNode secondA = a[1];
-  TNode secondB = b[1];
 
-  const Rational& qA = secondA.getConst<Rational>();
-  const Rational& qB = secondB.getConst<Rational>();
 
-  return qA < qB;
+bool rightHandRationalIsLT(TNode a, TNode b){
+  //This version is sticking around because it is easier to read!
+  return RightHandRationalLT()(a,b);
 }
 
-void ArithUnatePropagator::addEqualityToEqualities(TNode atom,
-                                                   OrderedSet* eqSet,
-                                                   OrderedSet::iterator eqPos){
+//void addImplicationsUsingEqualityAndEqualityList(TNode eq, OrderedSet* eqSet);
+
+void ArithUnatePropagator::addImplicationsUsingEqualityAndEqualityList(TNode atom, OrderedSet& eqSet){
   Assert(atom.getKind() == EQUAL);
+  OrderedSet::iterator eqPos = eqSet.find(atom);
+  Assert(eqPos != eqSet.end());
+  Assert(*eqPos == atom);
+
   Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
-  for(OrderedSet::iterator eqIter = eqSet->begin();
-      eqIter != eqSet->end(); ++eqIter){
+  for(OrderedSet::iterator eqIter = eqSet.begin();
+      eqIter != eqSet.end(); ++eqIter){
     if(eqIter == eqPos) continue;
     TNode eq = *eqIter;
     Assert(!rightHandRationalIsEqual(eq, atom));
@@ -149,17 +153,17 @@ void ArithUnatePropagator::addEqualityToEqualities(TNode atom,
   }
 }
 
-void ArithUnatePropagator::addEqualityToLeqs(TNode atom, OrderedSet* leqSet)
-{
+void ArithUnatePropagator::addImplicationsUsingEqualityAndLeqList(TNode atom, OrderedSet& leqSet){
+
   Assert(atom.getKind() == EQUAL);
   Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
 
-  OrderedSet::iterator leqIter = leqSet->lower_bound(atom);
-  if(leqIter != leqSet->end()){
+  OrderedSet::iterator leqIter = leqSet.lower_bound(atom);
+  if(leqIter != leqSet.end()){
     TNode lowerBound = *leqIter;
     if(rightHandRationalIsEqual(atom, lowerBound)){
       addImplication(atom, lowerBound);  // x=b /\ b = b' => x <= b'
-      if(leqIter != leqSet->begin()){
+      if(leqIter != leqSet.begin()){
         --leqIter;
         Assert(rightHandRationalIsLT(*leqIter, atom));
         addImplication(*leqIter, negation); // x=b /\ b > b' => x > b'
@@ -169,34 +173,34 @@ void ArithUnatePropagator::addEqualityToLeqs(TNode atom, OrderedSet* leqSet)
       Assert(rightHandRationalIsLT(atom, lowerBound));
       addImplication(atom, lowerBound);// x=b /\ b < b' => x <= b'
 
-      if(leqIter != leqSet->begin()){
+      if(leqIter != leqSet.begin()){
         --leqIter;
         Assert(rightHandRationalIsLT(*leqIter, atom));
         addImplication(*leqIter, negation);// x=b /\ b > b' => x > b'
       }
     }
-  }else if(leqIter != leqSet->begin()){
+  }else if(leqIter != leqSet.begin()){
     --leqIter;
     TNode strictlyLessThan = *leqIter;
     Assert(rightHandRationalIsLT(strictlyLessThan, atom));
     addImplication(*leqIter, negation); // x=b /\ b < b' => x <= b'
   }else{
-    Assert(leqSet->empty());
+    Assert(leqSet.empty());
   }
 }
 
-void ArithUnatePropagator::addEqualityToGeqs(TNode atom, OrderedSet* geqSet){
+void ArithUnatePropagator::addImplicationsUsingEqualityAndGeqList(TNode atom, OrderedSet& geqSet){
 
   Assert(atom.getKind() == EQUAL);
   Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
 
-  OrderedSet::iterator geqIter = geqSet->lower_bound(atom);
-  if(geqIter != geqSet->end()){
+  OrderedSet::iterator geqIter = geqSet.lower_bound(atom);
+  if(geqIter != geqSet.end()){
     TNode lowerBound = *geqIter;
     if(rightHandRationalIsEqual(atom, lowerBound)){
       addImplication(atom, lowerBound);  // x=b /\ b = b' => x >= b'
       ++geqIter;
-      if(geqIter != geqSet->end()){ // x=b /\ b < b' => x < b'
+      if(geqIter != geqSet.end()){ // x=b /\ b < b' => x < b'
         TNode strictlyGt = *geqIter;
         Assert(rightHandRationalIsLT( atom, strictlyGt ));
         addImplication(strictlyGt, negation);
@@ -204,32 +208,33 @@ void ArithUnatePropagator::addEqualityToGeqs(TNode atom, OrderedSet* geqSet){
     }else{
       Assert(rightHandRationalIsLT(atom, lowerBound));
       addImplication(lowerBound, negation);// x=b /\ b < b' => x < b'
-      if(geqIter != geqSet->begin()){
+      if(geqIter != geqSet.begin()){
         --geqIter;
         TNode strictlyLessThan = *geqIter;
         Assert(rightHandRationalIsLT(strictlyLessThan, atom));
         addImplication(atom, strictlyLessThan);// x=b /\ b > b' => x >= b'
       }
     }
-  }else if(geqIter != geqSet->begin()){
+  }else if(geqIter != geqSet.begin()){
     --geqIter;
     TNode strictlyLT = *geqIter;
     Assert(rightHandRationalIsLT(strictlyLT, atom));
     addImplication(atom, strictlyLT);// x=b /\ b > b' => x >= b'
   }else{
-    Assert(geqSet->empty());
+    Assert(geqSet.empty());
   }
 }
 
-void ArithUnatePropagator::addLeqToLeqs
-(TNode atom,
- OrderedSet* leqSet,
- OrderedSet::iterator atomPos)
+void ArithUnatePropagator::addImplicationsUsingLeqAndLeqList(TNode atom, OrderedSet& leqSet)
 {
   Assert(atom.getKind() == LEQ);
   Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
 
-  if(atomPos != leqSet->begin()){
+  OrderedSet::iterator atomPos = leqSet.find(atom);
+  Assert(atomPos != leqSet.end());
+  Assert(*atomPos == atom);
+
+  if(atomPos != leqSet.begin()){
     --atomPos;
     TNode beforeLeq = *atomPos;
     Assert(rightHandRationalIsLT(beforeLeq, atom));
@@ -237,25 +242,25 @@ void ArithUnatePropagator::addLeqToLeqs
     ++atomPos;
   }
   ++atomPos;
-  if(atomPos != leqSet->end()){
+  if(atomPos != leqSet.end()){
     TNode afterLeq = *atomPos;
     Assert(rightHandRationalIsLT(atom, afterLeq));
     addImplication(atom, afterLeq);// x<=b /\ b < b' => x <= b'
   }
 }
-void ArithUnatePropagator::addLeqToGeqs(TNode atom, OrderedSet* geqSet) {
+void ArithUnatePropagator::addImplicationsUsingLeqAndGeqList(TNode atom, OrderedSet& geqSet) {
 
   Assert(atom.getKind() == LEQ);
   Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
 
-  OrderedSet::iterator geqIter = geqSet->lower_bound(atom);
-  if(geqIter != geqSet->end()){
+  OrderedSet::iterator geqIter = geqSet.lower_bound(atom);
+  if(geqIter != geqSet.end()){
     TNode lowerBound = *geqIter;
     if(rightHandRationalIsEqual(atom, lowerBound)){
       Assert(rightHandRationalIsEqual(atom, lowerBound));
       addImplication(negation, lowerBound);// (x > b) => (x >= b)
       ++geqIter;
-      if(geqIter != geqSet->end()){
+      if(geqIter != geqSet.end()){
         TNode next = *geqIter;
         Assert(rightHandRationalIsLT(atom, next));
         addImplication(next, negation);// x>=b' /\ b' > b => x > b
@@ -263,29 +268,29 @@ void ArithUnatePropagator::addLeqToGeqs(TNode atom, OrderedSet* geqSet) {
     }else{
       Assert(rightHandRationalIsLT(atom, lowerBound));
       addImplication(lowerBound, negation);// x>=b' /\ b' > b => x > b
-      if(geqIter != geqSet->begin()){
+      if(geqIter != geqSet.begin()){
         --geqIter;
         TNode prev = *geqIter;
         Assert(rightHandRationalIsLT(prev, atom));
         addImplication(negation, prev);// (x>b /\ b > b') => x >= b'
       }
     }
-  }else if(geqIter != geqSet->begin()){
+  }else if(geqIter != geqSet.begin()){
     --geqIter;
     TNode strictlyLT = *geqIter;
     Assert(rightHandRationalIsLT(strictlyLT, atom));
     addImplication(negation, strictlyLT);// (x>b /\ b > b') => x >= b'
   }else{
-    Assert(geqSet->empty());
+    Assert(geqSet.empty());
   }
 }
 
-void ArithUnatePropagator::addLeqToEqualities(TNode atom, OrderedSet* eqSet) {
+void ArithUnatePropagator::addImplicationsUsingLeqAndEqualityList(TNode atom, OrderedSet& eqSet) {
   Assert(atom.getKind() == LEQ);
   Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
 
   //TODO Improve this later
-  for(OrderedSet::iterator eqIter = eqSet->begin(); eqIter != eqSet->end(); ++eqIter){
+  for(OrderedSet::iterator eqIter = eqSet.begin(); eqIter != eqSet.end(); ++eqIter){
     TNode eq = *eqIter;
     if(rightHandRationalIsEqual(atom, eq)){
       // (x = b' /\ b = b') =>  x <= b
@@ -301,13 +306,15 @@ void ArithUnatePropagator::addLeqToEqualities(TNode atom, OrderedSet* eqSet) {
 }
 
 
-void ArithUnatePropagator::addGeqToGeqs
-(TNode atom, OrderedSet* geqSet, OrderedSet::iterator atomPos)
-{
+void ArithUnatePropagator::addImplicationsUsingGeqAndGeqList(TNode atom, OrderedSet& geqSet){
   Assert(atom.getKind() == GEQ);
   Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
 
-  if(atomPos != geqSet->begin()){
+  OrderedSet::iterator atomPos = geqSet.find(atom);
+  Assert(atomPos != geqSet.end());
+  Assert(*atomPos == atom);
+
+  if(atomPos != geqSet.begin()){
     --atomPos;
     TNode beforeGeq = *atomPos;
     Assert(rightHandRationalIsLT(beforeGeq, atom));
@@ -315,26 +322,26 @@ void ArithUnatePropagator::addGeqToGeqs
     ++atomPos;
   }
   ++atomPos;
-  if(atomPos != geqSet->end()){
+  if(atomPos != geqSet.end()){
     TNode afterGeq = *atomPos;
     Assert(rightHandRationalIsLT(atom, afterGeq));
     addImplication(afterGeq, atom);// x>=b' /\ b' > b => x >= b
   }
 }
 
-void ArithUnatePropagator::addGeqToLeqs(TNode atom, OrderedSet* leqSet){
+void ArithUnatePropagator::addImplicationsUsingGeqAndLeqList(TNode atom, OrderedSet& leqSet){
 
   Assert(atom.getKind() == GEQ);
   Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
 
-  OrderedSet::iterator leqIter = leqSet->lower_bound(atom);
-  if(leqIter != leqSet->end()){
+  OrderedSet::iterator leqIter = leqSet.lower_bound(atom);
+  if(leqIter != leqSet.end()){
     TNode lowerBound = *leqIter;
     if(rightHandRationalIsEqual(atom, lowerBound)){
       Assert(rightHandRationalIsEqual(atom, lowerBound));
       addImplication(negation, lowerBound);// (x < b) => (x <= b)
 
-      if(leqIter != leqSet->begin()){
+      if(leqIter != leqSet.begin()){
         --leqIter;
         TNode prev = *leqIter;
         Assert(rightHandRationalIsLT(prev, atom));
@@ -344,28 +351,28 @@ void ArithUnatePropagator::addGeqToLeqs(TNode atom, OrderedSet* leqSet){
       Assert(rightHandRationalIsLT(atom, lowerBound));
       addImplication(negation, lowerBound);// (x < b /\ b < b') => x <= b'
       ++leqIter;
-      if(leqIter != leqSet->end()){
+      if(leqIter != leqSet.end()){
         TNode next = *leqIter;
         Assert(rightHandRationalIsLT(atom, next));
         addImplication(negation, next);// (x < b /\ b < b') => x <= b'
       }
     }
-  }else if(leqIter != leqSet->begin()){
+  }else if(leqIter != leqSet.begin()){
     --leqIter;
     TNode strictlyLT = *leqIter;
     Assert(rightHandRationalIsLT(strictlyLT, atom));
     addImplication(strictlyLT, negation);// (x <= b' /\ b' < b) => x < b
   }else{
-    Assert(leqSet->empty());
+    Assert(leqSet.empty());
   }
 }
-void ArithUnatePropagator::addGeqToEqualities(TNode atom, OrderedSet* eqSet){
+void ArithUnatePropagator::addImplicationsUsingGeqAndEqualityList(TNode atom, OrderedSet& eqSet){
 
   Assert(atom.getKind() == GEQ);
   Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
 
   //TODO Improve this later
-  for(OrderedSet::iterator eqIter = eqSet->begin(); eqIter != eqSet->end(); ++eqIter){
+  for(OrderedSet::iterator eqIter = eqSet.begin(); eqIter != eqSet.end(); ++eqIter){
     TNode eq = *eqIter;
     if(rightHandRationalIsEqual(atom, eq)){
       // (x = b' /\ b = b') =>  x >= b

diff --git a/src/theory/arith/unate_propagator.h b/src/theory/arith/unate_propagator.h
index ca2135cf34e4a4772a04d5277022cbc553f90c27..383b9f8e82eb71159b78ef65353314510fb4c791 100644 (file)
--- a/src/theory/arith/unate_propagator.h
+++ b/src/theory/arith/unate_propagator.h
@@ -49,13 +49,13 @@
 #define __CVC4__THEORY__ARITH__ARITH_PROPAGATOR_H
 
 #include "expr/node.h"
-#include "context/cdlist.h"
 #include "context/context.h"
-#include "context/cdo.h"
 
 #include "theory/output_channel.h"
 #include "theory/arith/ordered_set.h"
 
+#include <ext/hash_map>
+
 namespace CVC4 {
 namespace theory {
 namespace arith {
@@ -68,6 +68,16 @@ private:
    */
   OutputChannel& d_arithOut;
 
+  struct OrderedSetTriple {
+    OrderedSet d_leqSet;
+    OrderedSet d_eqSet;
+    OrderedSet d_geqSet;
+  };
+
+  /** TODO: justify making this a TNode. */
+  typedef __gnu_cxx::hash_map<Node, OrderedSetTriple, NodeHashFunction> NodeToOrderedSetMap;
+  NodeToOrderedSetMap d_orderedListMap;
+
 public:
   ArithUnatePropagator(context::Context* cxt, OutputChannel& arith);
 
@@ -81,6 +91,12 @@ public:
   bool hasAnyAtoms(TNode v);
 
 private:
+  OrderedSetTriple& getOrderedSetTriple(TNode left);
+  OrderedSet& getEqSet(TNode left);
+  OrderedSet& getLeqSet(TNode left);
+  OrderedSet& getGeqSet(TNode left);
+
+
   /** Sends an implication (=> a b) to the PropEngine via d_arithOut. */
   void addImplication(TNode a, TNode b);
 
@@ -92,32 +108,32 @@ private:
 
 
   /**
-   * The addKtoJs(...) functions are the work horses of ArithUnatePropagator.
+   * The addImplicationsUsingKAndJList(...)
+   * functions are the work horses of ArithUnatePropagator.
    * These take an atom of the kind K that has just been added
-   * to its associated list, and the list of Js associated with the lhs,
+   * to its associated list, and the ordered list of Js associated with the lhs,
    * and uses these to deduce unate implications.
    * (K and J vary over EQUAL, LEQ, and GEQ.)
    *
    * Input:
-   * atom - the atom being inserted
-   * Kset - the list of atoms of kind K associated with the lhs.
-   * atomPos - the atoms Position in its own list after being inserted.
+   * atom - the atom being inserted of kind K
+   * Jset - the list of atoms of kind J associated with the lhs.
    *
    * Unfortunately, these tend to be an absolute bear to read because
    * of all of the special casing and C++ iterator manipulation required.
    */
 
-  void addEqualityToEqualities(TNode eq, OrderedSet* eqSet, OrderedSet::iterator eqPos);
-  void addEqualityToLeqs(TNode eq, OrderedSet* leqSet);
-  void addEqualityToGeqs(TNode eq, OrderedSet* geqSet);
+  void addImplicationsUsingEqualityAndEqualityList(TNode eq, OrderedSet& eqSet);
+  void addImplicationsUsingEqualityAndLeqList(TNode eq, OrderedSet& leqSet);
+  void addImplicationsUsingEqualityAndGeqList(TNode eq, OrderedSet& geqSet);
 
-  void addLeqToLeqs(TNode leq, OrderedSet* leqSet, OrderedSet::iterator leqPos);
-  void addLeqToGeqs(TNode leq, OrderedSet* geqSet);
-  void addLeqToEqualities(TNode leq, OrderedSet* eqSet);
+  void addImplicationsUsingLeqAndEqualityList(TNode leq, OrderedSet& eqSet);
+  void addImplicationsUsingLeqAndLeqList(TNode leq, OrderedSet& leqSet);
+  void addImplicationsUsingLeqAndGeqList(TNode leq, OrderedSet& geqSet);
 
-  void addGeqToGeqs(TNode geq, OrderedSet* geqSet, OrderedSet::iterator geqPos);
-  void addGeqToLeqs(TNode geq, OrderedSet* leqSet);
-  void addGeqToEqualities(TNode geq, OrderedSet* eqSet);
+  void addImplicationsUsingGeqAndEqualityList(TNode geq, OrderedSet& eqSet);
+  void addImplicationsUsingGeqAndLeqList(TNode geq, OrderedSet& leqSet);
+  void addImplicationsUsingGeqAndGeqList(TNode geq, OrderedSet& geqSet);
 
 };