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, 17 insertions, 35 deletions

diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 39c0bc20b..4e5ba3d9e 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -56,11 +56,11 @@
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/tableau.h"
 #include "theory/arith/partial_model.h"
-#include "theory/arith/arith_prop_manager.h"
 #include "theory/arith/linear_equality.h"
 
-#include "util/options.h"
+#include "context/cdlist.h"
 
+#include "util/options.h"
 #include "util/stats.h"
 
 #include <queue>
@@ -91,13 +91,11 @@ private:
   /** Contains a superset of the basic variables in violation of their bounds. */
   ArithPriorityQueue d_queue;
 
-  /** A link to the propagation manager. This is used to generate weaker conflicts. */
-  ArithPropManager& d_propManager;
-
   /** Number of variables in the system. This is used for tuning heuristics. */
   ArithVar d_numVariables;
 
-  std::queue<Node> d_delayedLemmas;
+  /** This is the call back channel for Simplex to report conflicts. */
+  NodeCallBack& d_conflictChannel;
 
   /** Maps a variable to how many times they have been used as a pivot in the simplex search. */
   ArithVarMultiset d_pivotsInRound;
@@ -106,8 +104,7 @@ private:
   DeltaRational d_DELTA_ZERO;
 
 public:
-  SimplexDecisionProcedure(ArithPropManager& propManager,
-                           LinearEqualityModule& linEq);
+  SimplexDecisionProcedure(LinearEqualityModule& linEq, NodeCallBack& conflictChannel);
 
   /**
    * This must be called when the value of a basic variable may now voilate one
@@ -123,14 +120,15 @@ public:
    * This is done by a simplex search through the possible bases of the tableau.
    *
    * If all of the variables can be made consistent with their bounds
-   * Node::null() is returned. Otherwise a minimized conflict is returned.
+   * false is returned. Otherwise true is returned, and at least 1 conflict
+   * was reported on the conflictCallback passed to the Module.
    *
    * Tableau pivoting is performed so variables may switch from being basic to
    * nonbasic and vice versa.
    *
    * Corresponds to the "check()" procedure in [Cav06].
    */
-  Node findModel();
+  bool findModel();
 
 private:
 
@@ -158,6 +156,7 @@ private:
    * during the VarOrder stage of findModel.
    */
   static ArithVar minColLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y);
+
   /**
    * minBoundAndRowCount is a PreferenceFunction for preferring a variable
    * without an asserted bound over variables with an asserted bound.
@@ -173,11 +172,11 @@ private:
 
 
 private:
-  Node searchForFeasibleSolution(uint32_t maxIterations);
+  bool searchForFeasibleSolution(uint32_t maxIterations);
 
   enum SearchPeriod {BeforeDiffSearch, DuringDiffSearch, AfterDiffSearch, DuringVarOrderSearch, AfterVarOrderSearch};
 
-  Node findConflictOnTheQueue(SearchPeriod period, bool returnFirst = true);
+  bool findConflictOnTheQueue(SearchPeriod period);
 
 
   /**
@@ -217,29 +216,12 @@ private:
 public:
   void increaseMax() {d_numVariables++;}
 
-  /** Returns true if the simplex procedure has more delayed lemmas in its queue.*/
-  bool hasMoreLemmas() const {
-    return !d_delayedLemmas.empty();
-  }
-  /** Returns the next delayed lemmas on the queue.*/
-  Node popLemma(){
-    Assert(hasMoreLemmas());
-    Node lemma = d_delayedLemmas.front();
-    d_delayedLemmas.pop();
-    return lemma;
-  }
-
 private:
-  /** Adds a lemma to the queue. */
-  void pushLemma(Node lemma){
-    d_delayedLemmas.push(lemma);
-    ++(d_statistics.d_delayedConflicts);
-  }
 
-  /** Adds a conflict as a lemma to the queue. */
-  void delayConflictAsLemma(Node conflict){
-   Node negatedConflict = negateConjunctionAsClause(conflict);
-    pushLemma(negatedConflict);
+  /** Reports a conflict to on the output channel. */
+  void reportConflict(Node conflict){
+    d_conflictChannel(conflict);
+    ++(d_statistics.d_simplexConflicts);
   }
 
   template <bool above>
@@ -259,7 +241,7 @@ private:
   Node checkBasicForConflict(ArithVar b);
 
   Node weakenConflict(bool aboveUpper, ArithVar basicVar);
-  TNode weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic);
+  Constraint weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic);
 
 
 
@@ -280,7 +262,7 @@ private:
     TimerStat d_weakenTime;
 
 
-    IntStat d_delayedConflicts;
+    IntStat d_simplexConflicts;
 
     Statistics();
     ~Statistics();