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.

1 files changed, 73 insertions, 54 deletions

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index a5d94ec40..af32c3f87 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -168,17 +168,17 @@ inline int deltaCoeff(Kind k){
  * - (NOT (GT left right))    -> LEQ
  * If none of these match, it returns UNDEFINED_KIND.
  */
- inline Kind simplifiedKind(TNode assertion){
-  switch(assertion.getKind()){
+ inline Kind oldSimplifiedKind(TNode literal){
+  switch(literal.getKind()){
   case kind::LT:
   case kind::GT:
   case kind::LEQ:
   case kind::GEQ:
   case kind::EQUAL:
-    return assertion.getKind();
+    return literal.getKind();
   case  kind::NOT:
     {
-      TNode atom = assertion[0];
+      TNode atom = literal[0];
       switch(atom.getKind()){
       case  kind::LEQ: //(not (LEQ x c)) <=> (GT x c)
         return  kind::GT;
@@ -201,57 +201,58 @@ inline int deltaCoeff(Kind k){
   }
 }
 
-template <bool selectLeft>
-inline TNode getSide(TNode assertion, Kind simpleKind){
-  switch(simpleKind){
-  case kind::LT:
-  case kind::GT:
-  case kind::DISTINCT:
-    return selectLeft ? (assertion[0])[0] : (assertion[0])[1];
-  case kind::LEQ:
-  case kind::GEQ:
-  case kind::EQUAL:
-    return selectLeft ? assertion[0] : assertion[1];
-  default:
-    Unreachable();
-    return TNode::null();
-  }
-}
-
-inline DeltaRational determineRightConstant(TNode assertion, Kind simpleKind){
-  TNode right = getSide<false>(assertion, simpleKind);
-
-  Assert(right.getKind() == kind::CONST_RATIONAL);
-  const Rational& noninf = right.getConst<Rational>();
 
-  Rational inf = Rational(Integer(deltaCoeff(simpleKind)));
-  return DeltaRational(noninf, inf);
-}
-
-inline DeltaRational asDeltaRational(TNode n){
-  Kind simp = simplifiedKind(n);
-  return determineRightConstant(n, simp);
-}
-
- /**
-  * 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;
-  }
-};
+// template <bool selectLeft>
+// inline TNode getSide(TNode assertion, Kind simpleKind){
+//   switch(simpleKind){
+//   case kind::LT:
+//   case kind::GT:
+//   case kind::DISTINCT:
+//     return selectLeft ? (assertion[0])[0] : (assertion[0])[1];
+//   case kind::LEQ:
+//   case kind::GEQ:
+//   case kind::EQUAL:
+//     return selectLeft ? assertion[0] : assertion[1];
+//   default:
+//     Unreachable();
+//     return TNode::null();
+//   }
+// }
+
+// inline DeltaRational determineRightConstant(TNode assertion, Kind simpleKind){
+//   TNode right = getSide<false>(assertion, simpleKind);
+
+//   Assert(right.getKind() == kind::CONST_RATIONAL);
+//   const Rational& noninf = right.getConst<Rational>();
+
+//   Rational inf = Rational(Integer(deltaCoeff(simpleKind)));
+//   return DeltaRational(noninf, inf);
+// }
+
+// inline DeltaRational asDeltaRational(TNode n){
+//   Kind simp = simplifiedKind(n);
+//   return determineRightConstant(n, simp);
+// }
+
+//  /**
+//   * 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;
+//   }
+// };
 
 inline Node negateConjunctionAsClause(TNode conjunction){
   Assert(conjunction.getKind() == kind::AND);
@@ -278,6 +279,24 @@ inline Node maybeUnaryConvert(NodeBuilder<>& builder){
   }
 }
 
+inline void flattenAnd(Node n, std::vector<TNode>& out){
+  Assert(n.getKind() == kind::AND);
+  for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){
+    Node curr = *i;
+    if(curr.getKind() == kind::AND){
+      flattenAnd(curr, out);
+    }else{
+      out.push_back(curr);
+    }
+  }
+}
+
+inline Node flattenAnd(Node n){
+  std::vector<TNode> out;
+  flattenAnd(n, out);
+  return NodeManager::currentNM()->mkNode(kind::AND, out);
+}
+
 }; /* namesapce arith */
 }; /* namespace theory */
 }; /* namespace CVC4 */