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, 57 insertions, 151 deletions

diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 65b0083d9..32c9f6adc 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -20,6 +20,7 @@
 
 #include "theory/arith/partial_model.h"
 #include "util/output.h"
+#include "theory/arith/constraint.h"
 
 using namespace std;
 
@@ -27,62 +28,26 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-
-
-bool ArithPartialModel::boundsAreEqual(ArithVar x){
+ArithPartialModel::ArithPartialModel(context::Context* c)
+ : d_mapSize(0),
+   d_hasSafeAssignment(),
+   d_assignment(),
+   d_safeAssignment(),
+   d_ubc(c),
+   d_lbc(c),
+   d_deltaIsSafe(false),
+   d_delta(-1,1),
+   d_history()
+{ }
+
+bool ArithPartialModel::boundsAreEqual(ArithVar x) const{
   if(hasLowerBound(x) && hasUpperBound(x)){
-    return d_upperBound[x] == d_lowerBound[x];
+    return getUpperBound(x) == getLowerBound(x);
   }else{
     return false;
   }
 }
 
-void ArithPartialModel::zeroDifferenceDetected(ArithVar x){
-  Assert(d_dm.isDifferenceSlack(x));
-  Assert(upperBoundIsZero(x));
-  Assert(lowerBoundIsZero(x));
-
-  Node lb = getLowerConstraint(x);
-  Node ub = getUpperConstraint(x);
-  Node reason = lb != ub ? lb.andNode(ub) : lb;
-  d_dm.differenceIsZero(x, reason);
-}
-
-void ArithPartialModel::setUpperBound(ArithVar x, const DeltaRational& r){
-  d_deltaIsSafe = false;
-
-  Debug("partial_model") << "setUpperBound(" << x << "," << r << ")" << endl;
-  d_hasHadABound[x] = true;
-  d_upperBound.set(x,r);
-
-  if(d_dm.isDifferenceSlack(x)){
-    int sgn = r.sgn();
-    if(sgn < 0){
-      d_dm.differenceCannotBeZero(x, getUpperConstraint(x));
-    }else if(sgn == 0 && lowerBoundIsZero(x)){
-      zeroDifferenceDetected(x);
-    }
-  }
-}
-
-void ArithPartialModel::setLowerBound(ArithVar x, const DeltaRational& r){
-  d_deltaIsSafe = false;
-
-  Debug("partial_model") << "setLowerBound(" << x << "," << r << ")" << endl;
-  d_hasHadABound[x] = true;
-  d_lowerBound.set(x,r);
-
-
-  if(d_dm.isDifferenceSlack(x)){
-    int sgn = r.sgn();
-    if(sgn > 0){
-      d_dm.differenceCannotBeZero(x, getLowerConstraint(x));
-    }else if(sgn == 0 && upperBoundIsZero(x)){
-      zeroDifferenceDetected(x);
-    }
-  }
-}
-
 void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& r){
    Debug("partial_model") << "pm: updating the assignment to" << x
                           << " now " << r <<endl;
@@ -114,14 +79,12 @@ void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& safe, con
 }
 
 bool ArithPartialModel::equalSizes(){
-  return d_mapSize == d_hasHadABound.size() &&
+  return
     d_mapSize == d_hasSafeAssignment.size() &&
     d_mapSize == d_assignment.size() &&
     d_mapSize == d_safeAssignment.size() &&
-    d_mapSize == d_upperBound.size() &&
-    d_mapSize == d_lowerBound.size() &&
-    d_mapSize == d_upperConstraint.size() &&
-    d_mapSize == d_lowerConstraint.size();
+    d_mapSize == d_ubc.size() &&
+    d_mapSize == d_lbc.size();
 }
 
 void ArithPartialModel::initialize(ArithVar x, const DeltaRational& r){
@@ -129,33 +92,27 @@ void ArithPartialModel::initialize(ArithVar x, const DeltaRational& r){
   Assert(equalSizes());
   ++d_mapSize;
 
-
-  d_hasHadABound.push_back( false );
-
   d_hasSafeAssignment.push_back( false );
   d_assignment.push_back( r );
   d_safeAssignment.push_back( DeltaRational(0) );
 
-  d_upperBound.push_back( DeltaRational(0) );
-  d_lowerBound.push_back( DeltaRational(0) );
-
-  d_upperConstraint.push_back( TNode::null() );
-  d_lowerConstraint.push_back( TNode::null() );
+  d_ubc.push_back(NullConstraint);
+  d_lbc.push_back(NullConstraint);
 }
 
 /** Must know that the bound exists both calling this! */
-const DeltaRational& ArithPartialModel::getUpperBound(ArithVar x) {
+const DeltaRational& ArithPartialModel::getUpperBound(ArithVar x) const {
   Assert(inMaps(x));
   Assert(hasUpperBound(x));
 
-  return d_upperBound[x];
+  return getUpperBoundConstraint(x)->getValue();
 }
 
-const DeltaRational& ArithPartialModel::getLowerBound(ArithVar x) {
+const DeltaRational& ArithPartialModel::getLowerBound(ArithVar x) const {
   Assert(inMaps(x));
   Assert(hasLowerBound(x));
 
-  return d_lowerBound[x];
+  return getLowerBoundConstraint(x)->getValue();
 }
 
 const DeltaRational& ArithPartialModel::getSafeAssignment(ArithVar x) const{
@@ -182,144 +139,93 @@ const DeltaRational& ArithPartialModel::getAssignment(ArithVar x) const{
 }
 
 
-
-void ArithPartialModel::setLowerConstraint(ArithVar x, TNode constraint){
-  Debug("partial_model") << "setLowerConstraint("
-                         << x << ":" << constraint << ")" << endl;
+void ArithPartialModel::setLowerBoundConstraint(Constraint c){
+  AssertArgument(c != NullConstraint, "Cannot set a lower bound to NullConstraint.");
+  AssertArgument(c->isEquality() || c->isLowerBound(),
+                 "Constraint type must be set to an equality or UpperBound.");
+  ArithVar x = c->getVariable();
+  Debug("partial_model") << "setLowerBoundConstraint(" << x << ":" << c << ")" << endl;
   Assert(inMaps(x));
-  d_lowerConstraint.set(x,constraint);
+  Assert(greaterThanLowerBound(x, c->getValue()));
 
+  d_lbc.set(x, c);
 }
 
-void ArithPartialModel::setUpperConstraint(ArithVar x, TNode constraint){
-  Debug("partial_model") << "setUpperConstraint("
-                         << x << ":" << constraint << ")" << endl;
-  Assert(inMaps(x));
-  d_upperConstraint.set(x, constraint);
-}
+void ArithPartialModel::setUpperBoundConstraint(Constraint c){
+  AssertArgument(c != NullConstraint, "Cannot set a upper bound to NullConstraint.");
+  AssertArgument(c->isEquality() || c->isUpperBound(),
+                 "Constraint type must be set to an equality or UpperBound.");
 
-TNode ArithPartialModel::getLowerConstraint(ArithVar x){
+  ArithVar x = c->getVariable();
+  Debug("partial_model") << "setUpperBoundConstraint(" << x << ":" << c << ")" << endl;
   Assert(inMaps(x));
-  Assert(hasLowerBound(x));
-  return d_lowerConstraint[x];
-}
+  Assert(lessThanUpperBound(x, c->getValue()));
 
-TNode ArithPartialModel::getUpperConstraint(ArithVar x){
-  Assert(inMaps(x));
-  Assert(hasUpperBound(x));
-  return d_upperConstraint[x];
+  d_ubc.set(x, c);
 }
 
-int ArithPartialModel::cmpToLowerBound(ArithVar x, const DeltaRational& c){
+int ArithPartialModel::cmpToLowerBound(ArithVar x, const DeltaRational& c) const{
   if(!hasLowerBound(x)){
     // l = -\intfy
     // ? c < -\infty |-  _|_
     return 1;
   }else{
-    return c.cmp(d_lowerBound[x]);
+    return c.cmp(getLowerBound(x));
   }
 }
 
-int ArithPartialModel::cmpToUpperBound(ArithVar x, const DeltaRational& c){
+int ArithPartialModel::cmpToUpperBound(ArithVar x, const DeltaRational& c) const{
   if(!hasUpperBound(x)){
     //u = \intfy
     // ? c > \infty |-  _|_
     return -1;
   }else{
-    return c.cmp(d_upperBound[x]);
+    return c.cmp(getUpperBound(x));
   }
 }
 
-// bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool strict){
-//   if(!hasLowerBound(x)){
-//     // l = -\intfy
-//     // ? c < -\infty |-  _|_
-//     return false;
-//   }
-//   if(strict){
-//     return c < d_lowerBound[x];
-//   }else{
-//     return c <= d_lowerBound[x];
-//   }
-// }
-
-// bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){
-//   if(!hasUpperBound(x)){
-//     // u = \intfy
-//     // ? c > \infty |-  _|_
-//     return false;
-//   }
-//   if(strict){
-//     return c > d_upperBound[x];
-//   }else{
-//     return c >= d_upperBound[x];
-//   }
-// }
-
 bool ArithPartialModel::equalsLowerBound(ArithVar x, const DeltaRational& c){
   if(!hasLowerBound(x)){
     return false;
   }else{
-    return c == d_lowerBound[x];
+    return c == getLowerBound(x);
   }
 }
 bool ArithPartialModel::equalsUpperBound(ArithVar x, const DeltaRational& c){
   if(!hasUpperBound(x)){
     return false;
   }else{
-    return c == d_upperBound[x];
+    return c == getUpperBound(x);
   }
 }
 
-bool ArithPartialModel::hasEitherBound(ArithVar x){
+bool ArithPartialModel::hasEitherBound(ArithVar x) const{
   return hasLowerBound(x) || hasUpperBound(x);
 }
 
-bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x){
+bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x) const{
   Assert(inMaps(x));
   if(!hasUpperBound(x)){ // u = \infty
     return true;
+  }else{
+    return d_assignment[x] < getUpperBound(x);
   }
-  return d_assignment[x] < d_upperBound[x];
 }
 
-bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x){
+bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x) const{
   Assert(inMaps(x));
   if(!hasLowerBound(x)){ // l = -\infty
     return true;
+  }else{
+    return getLowerBound(x) < d_assignment[x];
   }
-  return  d_lowerBound[x] < d_assignment[x];
 }
 
-// /**
-//  * x <= u
-//  * ? c < u
-//  */
-// bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x, const DeltaRational& c){
-//   Assert(inMaps(x));
-//   if(!hasUpperBound(x)){ // u = \infty
-//     return true;
-//   }
-//   return c < d_upperBound[x];
-// }
-
-// /**
-//  * x <= u
-//  * ? c < u
-//  */
-// bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x, const DeltaRational& c){
-//   Assert(inMaps(x));
-//   if(!hasLowerBound(x)){ // l = -\infty
-//     return true;
-//   }
-//   return  d_lowerBound[x] < c;
-// }
-
-bool ArithPartialModel::assignmentIsConsistent(ArithVar x){
+bool ArithPartialModel::assignmentIsConsistent(ArithVar x) const{
   const DeltaRational& beta = getAssignment(x);
 
   //l_i <= beta(x_i) <= u_i
-  return  cmpToLowerBound(x,beta) >= 0 && cmpToUpperBound(x,beta) <= 0;
+  return  greaterThanLowerBound(x,beta) && lessThanUpperBound(x,beta);
 }
 
 
@@ -355,13 +261,13 @@ void ArithPartialModel::printModel(ArithVar x){
     Debug("model") << "no lb ";
   }else{
     Debug("model") << getLowerBound(x) << " ";
-    Debug("model") << getLowerConstraint(x) << " ";
+    Debug("model") << getLowerBoundConstraint(x) << " ";
   }
   if(!hasUpperBound(x)){
     Debug("model") << "no ub ";
   }else{
     Debug("model") << getUpperBound(x) << " ";
-    Debug("model") << getUpperConstraint(x) << " ";
+    Debug("model") << getUpperBoundConstraint(x) << " ";
   }
 }