Updates based on the group code review of arithmetic on 2011-02-15. The only substantive change is that UnatePropagator no longer uses attributes. The rest is comments and other beatification.

1 files changed, 36 insertions, 53 deletions

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 452d54fae..c8532f1a2 100644
--- 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 */