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, 0 insertions, 116 deletions

diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h
deleted file mode 100644
index 8887daa8d..000000000
--- a/src/theory/arith/ordered_set.h
+++ /dev/null
@@ -1,116 +0,0 @@
-/*********************                                                        */
-/*! \file ordered_set.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__ARITH__ORDERED_SET_H
-#define __CVC4__THEORY__ARITH__ORDERED_SET_H
-
-#include <map>
-#include <set>
-#include "expr/kind.h"
-#include "expr/node.h"
-#include "util/Assert.h"
-#include "theory/arith/arith_utilities.h"
-
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-inline const Rational& rightHandRational(TNode ineq){
-  Assert(ineq.getKind() == kind::LEQ
-         || ineq.getKind() == kind::GEQ
-         || ineq.getKind() == kind::EQUAL);
-  TNode righthand = ineq[1];
-  Assert(righthand.getKind() == kind::CONST_RATIONAL);
-  return righthand.getConst<Rational>();
-}
-
-class BoundValueEntry {
-private:
-  const Rational& value;
-  TNode d_leq, d_geq;
-
-  BoundValueEntry(const Rational& v, TNode l, TNode g):
-    value(v),
-    d_leq(l),
-    d_geq(g)
-  {}
-
-public:
-  Node getLeq() const{
-    Assert(hasLeq());
-    return d_leq;
-  }
-  Node getGeq() const{
-    Assert(hasGeq());
-    return d_geq;
-  }
-
-  static BoundValueEntry mkFromLeq(TNode leq){
-    Assert(leq.getKind() == kind::LEQ);
-    return BoundValueEntry(rightHandRational(leq), leq, TNode::null());
-  }
-
-  static BoundValueEntry mkFromGeq(TNode geq){
-    Assert(geq.getKind() == kind::GEQ);
-    return BoundValueEntry(rightHandRational(geq), TNode::null(), geq);
-  }
-
-  void addLeq(TNode leq){
-    Assert(leq.getKind() == kind::LEQ);
-    Assert(rightHandRational(leq) == getValue());
-    // [MGD] With context-dependent pre-registration, we could get the
-    // same one twice
-    Assert(!hasLeq() || d_leq == leq);
-    d_leq = leq;
-  }
-
-  void addGeq(TNode geq){
-    Assert(geq.getKind() == kind::GEQ);
-    Assert(rightHandRational(geq) == getValue());
-    // [MGD] With context-dependent pre-registration, we could get the
-    // same one twice
-    Assert(!hasGeq() || d_geq == geq);
-    d_geq = geq;
-  }
-
-  bool hasGeq() const { return d_geq != TNode::null(); }
-  bool hasLeq() const { return d_leq != TNode::null(); }
-
-
-  const Rational& getValue() const{
-    return value;
-  }
-
-  bool operator<(const BoundValueEntry& other){
-    return value < other.value;
-  }
-};
-
-typedef std::map<Rational, BoundValueEntry> BoundValueSet;
-
-typedef std::set<TNode, RightHandRationalLT> EqualValueSet;
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__ARITH__ORDERED_SET_H */