- Removes arith_constants.h

- Adds ArithStaticLearner.  Consolidates and cleans up the code for static learning in arithmetic.  Static learning is now associated with a small amount of state between calls. This is used to track the data for the miplib trick.  The goal is to make this inference work without relying on the fact that all of the miplib problem is asserted under the same AND node.
- This commit contains miscellaneous other arithmetic cleanup.

1 files changed, 5 insertions, 9 deletions

diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index c6bc3c434..6f3ff073f 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -25,9 +25,6 @@ namespace arith {
 class SimplexDecisionProcedure {
 private:
 
-  /** Stores system wide constants to avoid unnessecary reconstruction. */
-  const ArithConstants& d_constants;
-
   /**
    * Manages information about the assignment and upper and lower bounds on
    * variables.
@@ -44,23 +41,22 @@ private:
   std::vector<Node> d_delayedLemmas;
   uint32_t d_delayedLemmasPos;
 
+  Rational d_ZERO;
+
 public:
-  SimplexDecisionProcedure(const ArithConstants& constants,
-                           ArithPartialModel& pm,
+  SimplexDecisionProcedure(ArithPartialModel& pm,
                            OutputChannel* out,
                            Tableau& tableau) :
-    d_constants(constants),
     d_partialModel(pm),
     d_out(out),
     d_tableau(tableau),
     d_queue(pm, tableau),
     d_numVariables(0),
     d_delayedLemmas(),
-    d_delayedLemmasPos(0)
+    d_delayedLemmasPos(0),
+    d_ZERO(0)
   {}
 
-
-public:
   /**
    * Assert*(n, orig) takes an bound n that is implied by orig.
    * and asserts that as a new bound if it is tighter than the current bound