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, 43 insertions, 64 deletions

diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 7e2211595..fc8423e36 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -19,16 +19,18 @@
 
 #include "cvc4_private.h"
 
+#include "expr/node.h"
+
 #include "context/context.h"
 #include "context/cdvector.h"
+#include "context/cdo.h"
+
 #include "theory/arith/arithvar.h"
 #include "theory/arith/delta_rational.h"
-#include "expr/attribute.h"
-#include "expr/node.h"
+#include "theory/arith/constraint_forward.h"
 
-#include "theory/arith/difference_manager.h"
 
-#include <deque>
+#include <vector>
 
 #ifndef __CVC4__THEORY__ARITH__PARTIAL_MODEL_H
 #define __CVC4__THEORY__ARITH__PARTIAL_MODEL_H
@@ -41,19 +43,14 @@ class ArithPartialModel {
 private:
 
   unsigned d_mapSize;
-  //Maps from ArithVar -> T
-
-  std::vector<bool> d_hasHadABound;
 
+  //Maps from ArithVar -> T
   std::vector<bool> d_hasSafeAssignment;
   std::vector<DeltaRational> d_assignment;
   std::vector<DeltaRational> d_safeAssignment;
 
-  context::CDVector<DeltaRational> d_upperBound;
-  context::CDVector<DeltaRational> d_lowerBound;
-  context::CDVector<Node> d_upperConstraint;
-  context::CDVector<Node> d_lowerConstraint;
-
+  context::CDVector<Constraint> d_ubc;
+  context::CDVector<Constraint> d_lbc;
 
   bool d_deltaIsSafe;
   Rational d_delta;
@@ -64,30 +61,20 @@ private:
   typedef std::vector<ArithVar> HistoryList;
   HistoryList d_history;
 
-  DifferenceManager& d_dm;
 
 public:
 
-  ArithPartialModel(context::Context* c, DifferenceManager& dm):
-    d_mapSize(0),
-    d_hasHadABound(),
-    d_hasSafeAssignment(),
-    d_assignment(),
-    d_safeAssignment(),
-    d_upperBound(c),
-    d_lowerBound(c),
-    d_upperConstraint(c),
-    d_lowerConstraint(c),
-    d_deltaIsSafe(false),
-    d_delta(-1,1),
-    d_history(),
-    d_dm(dm)
-  { }
-
-  void setLowerConstraint(ArithVar x, TNode constraint);
-  void setUpperConstraint(ArithVar x, TNode constraint);
-  TNode getLowerConstraint(ArithVar x);
-  TNode getUpperConstraint(ArithVar x);
+  ArithPartialModel(context::Context* c);
+
+  void setLowerBoundConstraint(Constraint lb);
+  void setUpperBoundConstraint(Constraint ub);
+
+  inline Constraint getUpperBoundConstraint(ArithVar x) const{
+    return d_ubc[x];
+  }
+  inline Constraint getLowerBoundConstraint(ArithVar x) const{
+    return d_lbc[x];
+  }
 
 
   /* Initializes a variable to a safe value.*/
@@ -112,14 +99,7 @@ public:
     return hasUpperBound(x) && getUpperBound(x).sgn() == 0;
   }
 
-private:
-  void zeroDifferenceDetected(ArithVar x);
-
-public:
-  bool boundsAreEqual(ArithVar x);
-
-  void setUpperBound(ArithVar x, const DeltaRational& r);
-  void setLowerBound(ArithVar x, const DeltaRational& r);
+  bool boundsAreEqual(ArithVar x) const;
 
   /* Sets an unsafe variable assignment */
   void setAssignment(ArithVar x, const DeltaRational& r);
@@ -127,8 +107,8 @@ public:
 
 
   /** Must know that the bound exists before calling this! */
-  const DeltaRational& getUpperBound(ArithVar x);
-  const DeltaRational& getLowerBound(ArithVar x);
+  const DeltaRational& getUpperBound(ArithVar x) const;
+  const DeltaRational& getLowerBound(ArithVar x) const;
   const DeltaRational& getAssignment(ArithVar x) const;
 
 
@@ -141,61 +121,60 @@ public:
    * If lowerbound = - \infty:
    *   return 1
    */
-  int cmpToLowerBound(ArithVar x, const DeltaRational& c);
+  int cmpToLowerBound(ArithVar x, const DeltaRational& c) const;
 
-  inline bool strictlyLessThanLowerBound(ArithVar x, const DeltaRational& c){
+  inline bool strictlyLessThanLowerBound(ArithVar x, const DeltaRational& c) const{
     return cmpToLowerBound(x, c) < 0;
   }
-  inline bool lessThanLowerBound(ArithVar x, const DeltaRational& c){
+  inline bool lessThanLowerBound(ArithVar x, const DeltaRational& c) const{
     return cmpToLowerBound(x, c) <= 0;
   }
 
-  inline bool strictlyGreaterThanLowerBound(ArithVar x, const DeltaRational& c){
+  inline bool strictlyGreaterThanLowerBound(ArithVar x, const DeltaRational& c) const{
     return cmpToLowerBound(x, c) > 0;
   }
 
+  inline bool greaterThanLowerBound(ArithVar x, const DeltaRational& c) const{
+    return cmpToLowerBound(x, c) >= 0;
+  }
   /**
    * If upperbound < \infty:
    *   return getAssignment(x).cmp(getUpperBound(x))
    * If upperbound = \infty:
    *   return -1
    */
-  int cmpToUpperBound(ArithVar x, const DeltaRational& c);
+  int cmpToUpperBound(ArithVar x, const DeltaRational& c) const;
 
-  inline bool strictlyLessThanUpperBound(ArithVar x, const DeltaRational& c){
+  inline bool strictlyLessThanUpperBound(ArithVar x, const DeltaRational& c) const{
     return cmpToUpperBound(x, c) < 0;
   }
 
-  inline bool lessThanUpperBound(ArithVar x, const DeltaRational& c){
+  inline bool lessThanUpperBound(ArithVar x, const DeltaRational& c) const{
     return cmpToUpperBound(x, c) <= 0;
   }
 
-  inline bool strictlyGreaterThanUpperBound(ArithVar x, const DeltaRational& c){
+  inline bool strictlyGreaterThanUpperBound(ArithVar x, const DeltaRational& c) const{
     return cmpToUpperBound(x, c) > 0;
   }
 
-  inline bool greaterThanUpperBound(ArithVar x, const DeltaRational& c){
+  inline bool greaterThanUpperBound(ArithVar x, const DeltaRational& c) const{
     return cmpToUpperBound(x, c) >= 0;
   }
 
 
-  bool strictlyBelowUpperBound(ArithVar x);
-  bool strictlyAboveLowerBound(ArithVar x);
-  bool assignmentIsConsistent(ArithVar x);
+  bool strictlyBelowUpperBound(ArithVar x) const;
+  bool strictlyAboveLowerBound(ArithVar x) const;
+  bool assignmentIsConsistent(ArithVar x) const;
 
   void printModel(ArithVar x);
 
   /** returns true iff x has both a lower and upper bound. */
-  bool hasEitherBound(ArithVar x);
-  inline bool hasLowerBound(ArithVar x){
-    return !d_lowerConstraint[x].isNull();
+  bool hasEitherBound(ArithVar x) const;
+  inline bool hasLowerBound(ArithVar x) const{
+    return d_lbc[x] != NullConstraint;
   }
-  inline bool hasUpperBound(ArithVar x){
-    return !d_upperConstraint[x].isNull();
-  }
-
-  bool hasEverHadABound(ArithVar var){
-    return d_hasHadABound[var];
+  inline bool hasUpperBound(ArithVar x) const{
+    return d_ubc[x] != NullConstraint;
   }
 
   const Rational& getDelta(){