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

diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 7fce748dc..5837d4793 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -33,15 +33,13 @@ static const uint32_t NUM_CHECKS = 10;
 static const bool CHECK_AFTER_PIVOT = true;
 static const uint32_t VARORDER_CHECK_PERIOD = 200;
 
-SimplexDecisionProcedure::SimplexDecisionProcedure(ArithPropManager& propManager,
-                                                   LinearEqualityModule& linEq) :
+SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, NodeCallBack& conflictChannel) :
   d_linEq(linEq),
   d_partialModel(d_linEq.getPartialModel()),
   d_tableau(d_linEq.getTableau()),
   d_queue(d_partialModel, d_tableau),
-  d_propManager(propManager),
   d_numVariables(0),
-  d_delayedLemmas(),
+  d_conflictChannel(conflictChannel),
   d_pivotsInRound(),
   d_DELTA_ZERO(0,0)
 {
@@ -77,7 +75,7 @@ SimplexDecisionProcedure::Statistics::Statistics():
   d_weakeningSuccesses("theory::arith::weakening::success",0),
   d_weakenings("theory::arith::weakening::total",0),
   d_weakenTime("theory::arith::weakening::time"),
-  d_delayedConflicts("theory::arith::delayedConflicts",0)
+  d_simplexConflicts("theory::arith::simplexConflicts",0)
 {
   StatisticsRegistry::registerStat(&d_statUpdateConflicts);
 
@@ -99,7 +97,7 @@ SimplexDecisionProcedure::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_weakenings);
   StatisticsRegistry::registerStat(&d_weakenTime);
 
-  StatisticsRegistry::registerStat(&d_delayedConflicts);
+  StatisticsRegistry::registerStat(&d_simplexConflicts);
 }
 
 SimplexDecisionProcedure::Statistics::~Statistics(){
@@ -123,7 +121,7 @@ SimplexDecisionProcedure::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_weakenings);
   StatisticsRegistry::unregisterStat(&d_weakenTime);
 
-  StatisticsRegistry::unregisterStat(&d_delayedConflicts);
+  StatisticsRegistry::unregisterStat(&d_simplexConflicts);
 }
 
 
@@ -203,7 +201,7 @@ Node betterConflict(TNode x, TNode y){
   else return y;
 }
 
-Node SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type, bool returnFirst) {
+bool SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) {
   TimerStat::CodeTimer codeTimer(d_statistics.d_findConflictOnTheQueueTime);
 
   switch(type){
@@ -215,7 +213,6 @@ Node SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type, bool re
   }
 
   bool success = false;
-  Node firstConflict = Node::null();
   ArithPriorityQueue::const_iterator i = d_queue.begin();
   ArithPriorityQueue::const_iterator end = d_queue.end();
   for(; i != end; ++i){
@@ -225,11 +222,7 @@ Node SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type, bool re
       Node possibleConflict = checkBasicForConflict(x_i);
       if(!possibleConflict.isNull()){
         success = true;
-        if(returnFirst && firstConflict.isNull()){
-          firstConflict = possibleConflict;
-        }else{
-          delayConflictAsLemma(possibleConflict);
-        }
+        reportConflict(possibleConflict);
       }
     }
   }
@@ -242,13 +235,14 @@ Node SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type, bool re
     case AfterVarOrderSearch:  ++(d_statistics.d_successAfterVarOrderSearch); break;
     }
   }
-  return firstConflict;
+  return success;
 }
 
-Node SimplexDecisionProcedure::findModel(){
+bool SimplexDecisionProcedure::findModel(){
   if(d_queue.empty()){
-    return Node::null();
+    return false;
   }
+  bool foundConflict = false;
 
   static CVC4_THREADLOCAL(unsigned int) instance = 0;
   instance = instance + 1;
@@ -256,45 +250,44 @@ Node SimplexDecisionProcedure::findModel(){
 
   d_queue.transitionToDifferenceMode();
 
-  Node possibleConflict = Node::null();
   if(d_queue.size() > 1){
-    possibleConflict = findConflictOnTheQueue(BeforeDiffSearch);
+    foundConflict = findConflictOnTheQueue(BeforeDiffSearch);
   }
-  if(possibleConflict.isNull()){
+  if(!foundConflict){
     uint32_t numHueristicPivots = d_numVariables + 1;
     uint32_t pivotsRemaining = numHueristicPivots;
     uint32_t pivotsPerCheck = (numHueristicPivots/NUM_CHECKS) + (NUM_CHECKS-1);
     while(!d_queue.empty() &&
-          possibleConflict.isNull() &&
+          !foundConflict &&
           pivotsRemaining > 0){
       uint32_t pivotsToDo = min(pivotsPerCheck, pivotsRemaining);
-      possibleConflict = searchForFeasibleSolution(pivotsToDo);
+      foundConflict = searchForFeasibleSolution(pivotsToDo);
       pivotsRemaining -= pivotsToDo;
       //Once every CHECK_PERIOD examine the entire queue for conflicts
-      if(possibleConflict.isNull()){
-        possibleConflict = findConflictOnTheQueue(DuringDiffSearch);
+      if(!foundConflict){
+        foundConflict = findConflictOnTheQueue(DuringDiffSearch);
       }else{
-        findConflictOnTheQueue(AfterDiffSearch, false);
+        findConflictOnTheQueue(AfterDiffSearch);
       }
     }
   }
 
-  if(!d_queue.empty() && possibleConflict.isNull()){
+  if(!d_queue.empty() && !foundConflict){
     d_queue.transitionToVariableOrderMode();
 
-    while(!d_queue.empty() && possibleConflict.isNull()){
-      possibleConflict = searchForFeasibleSolution(VARORDER_CHECK_PERIOD);
+    while(!d_queue.empty() && !foundConflict){
+      foundConflict = searchForFeasibleSolution(VARORDER_CHECK_PERIOD);
 
       //Once every CHECK_PERIOD examine the entire queue for conflicts
-      if(possibleConflict.isNull()){
-        possibleConflict = findConflictOnTheQueue(DuringVarOrderSearch);
-      }else{
-        findConflictOnTheQueue(AfterVarOrderSearch, false);
+      if(!foundConflict){
+        foundConflict = findConflictOnTheQueue(DuringVarOrderSearch);
+      } else{
+        findConflictOnTheQueue(AfterVarOrderSearch);
       }
     }
   }
 
-  Assert(!possibleConflict.isNull() || d_queue.empty());
+  Assert(foundConflict || d_queue.empty());
 
   // Curiously the invariant that we always do a full check
   // means that the assignment we can always empty these queues.
@@ -309,7 +302,7 @@ Node SimplexDecisionProcedure::findModel(){
 
   Debug("arith::findModel") << "end findModel() " << instance << endl;
 
-  return possibleConflict;
+  return foundConflict;
 }
 
 Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){
@@ -333,7 +326,7 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){
 
 //corresponds to Check() in dM06
 //template <SimplexDecisionProcedure::PreferenceFunction pf>
-Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){
+bool SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){
   Debug("arith") << "searchForFeasibleSolution" << endl;
   Assert(remainingIterations > 0);
 
@@ -344,7 +337,7 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
     Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl;
     if(x_i == ARITHVAR_SENTINEL){
       Debug("arith_update") << "No inconsistent variables" << endl;
-      return Node::null(); //sat
+      return false; //sat
     }
 
     --remainingIterations;
@@ -369,7 +362,9 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
       x_j = selectSlackUpperBound(x_i, pf);
       if(x_j == ARITHVAR_SENTINEL ){
         ++(d_statistics.d_statUpdateConflicts);
-        return generateConflictBelowLowerBound(x_i); //unsat
+        Node conflict = generateConflictBelowLowerBound(x_i); //unsat
+        reportConflict(conflict);
+        return true;
       }
       DeltaRational l_i = d_partialModel.getLowerBound(x_i);
       d_linEq.pivotAndUpdate(x_i, x_j, l_i);
@@ -378,7 +373,9 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
       x_j = selectSlackLowerBound(x_i, pf);
       if(x_j == ARITHVAR_SENTINEL ){
         ++(d_statistics.d_statUpdateConflicts);
-        return generateConflictAboveUpperBound(x_i); //unsat
+        Node conflict = generateConflictAboveUpperBound(x_i); //unsat
+        reportConflict(conflict);
+        return true;
       }
       DeltaRational u_i = d_partialModel.getUpperBound(x_i);
       d_linEq.pivotAndUpdate(x_i, x_j, u_i);
@@ -389,38 +386,50 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
     if(CHECK_AFTER_PIVOT){
       Node possibleConflict = checkBasicForConflict(x_j);
       if(!possibleConflict.isNull()){
-        return possibleConflict;
+        reportConflict(possibleConflict);
+        return true; // unsat
       }
     }
   }
   Assert(remainingIterations == 0);
 
-  return Node::null();
+  return false;
 }
 
 
 
-TNode SimplexDecisionProcedure::weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic){
+Constraint SimplexDecisionProcedure::weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic){
 
   int sgn = coeff.sgn();
   bool ub = aboveUpper?(sgn < 0) : (sgn > 0);
-  TNode exp = ub ?
-    d_partialModel.getUpperConstraint(v) :
-    d_partialModel.getLowerConstraint(v);
-  DeltaRational bound = ub?
-    d_partialModel.getUpperBound(v) :
-    d_partialModel.getLowerBound(v);
+
+  Constraint c = ub ?
+    d_partialModel.getUpperBoundConstraint(v) :
+    d_partialModel.getLowerBoundConstraint(v);
+
+// #warning "revisit"
+//   Node exp = ub ?
+//     d_partialModel.explainUpperBound(v) :
+//     d_partialModel.explainLowerBound(v);
 
   bool weakened;
   do{
+    const DeltaRational& bound = c->getValue();
+
     weakened = false;
 
-    Node weaker = ub?
-      d_propManager.strictlyWeakerAssertedUpperBound(v, bound):
-      d_propManager.strictlyWeakerAssertedLowerBound(v, bound);
+    Constraint weaker = ub?
+      c->getStrictlyWeakerUpperBound(true, true):
+      c->getStrictlyWeakerLowerBound(true, true);
+
+    // Node weaker = ub?
+    //   d_propManager.strictlyWeakerAssertedUpperBound(v, bound):
+    //   d_propManager.strictlyWeakerAssertedLowerBound(v, bound);
 
-    if(!weaker.isNull()){
-      DeltaRational weakerBound = asDeltaRational(weaker);
+    if(weaker != NullConstraint){
+    //if(!weaker.isNull()){
+      const DeltaRational& weakerBound = weaker->getValue();
+      //DeltaRational weakerBound = asDeltaRational(weaker);
 
       DeltaRational diff = aboveUpper ? bound - weakerBound : weakerBound - bound;
       //if var == basic,
@@ -438,24 +447,16 @@ TNode SimplexDecisionProcedure::weakestExplanation(bool aboveUpper, DeltaRationa
           Debug("weak") << "  basic: ";
         }
         Debug("weak") << "  " << surplus << " "<< diff  << endl
-                      << "  " << bound << exp << endl
+                      << "  " << bound << c << endl
                       << "  " << weakerBound << weaker << endl;
 
-        if(exp.getKind() == AND){
-          Debug("weak") << "VICTORY" << endl;
-        }
-
         Assert(diff > d_DELTA_ZERO);
-        exp = weaker;
-        bound = weakerBound;
+        c = weaker;
       }
     }
   }while(weakened);
 
-  if(exp.getKind() == AND){
-    Debug("weak") << "boo: " << exp << endl;
-  }
-  return exp;
+  return c;
 }
 
 Node SimplexDecisionProcedure::weakenConflict(bool aboveUpper, ArithVar basicVar){
@@ -479,7 +480,15 @@ Node SimplexDecisionProcedure::weakenConflict(bool aboveUpper, ArithVar basicVar
     const TableauEntry& entry = *i;
     ArithVar v = entry.getColVar();
     const Rational& coeff = entry.getCoefficient();
-    conflict << weakestExplanation(aboveUpper, surplus, v, coeff, anyWeakenings, basicVar);
+    bool weakening = false;
+    Constraint c = weakestExplanation(aboveUpper, surplus, v, coeff, weakening, basicVar);
+    Debug("weak") << "weak : " << weakening << " " << c->assertedToTheTheory()
+                  << c << endl
+                  << c->explainForConflict() << endl;
+    anyWeakenings = anyWeakenings || weakening;
+
+    Debug("weak") << "weak : " << c->explainForConflict() << endl;
+    c->explainForConflict(conflict);
   }
   ++d_statistics.d_weakeningAttempts;
   if(anyWeakenings){