- 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, 25 insertions, 14 deletions

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 1dcdceab0..ef93b7d64 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -35,6 +35,7 @@
 #include "theory/arith/partial_model.h"
 #include "theory/arith/unate_propagator.h"
 #include "theory/arith/simplex.h"
+#include "theory/arith/arith_static_learner.h"
 
 #include "util/stats.h"
 
@@ -54,26 +55,22 @@ namespace arith {
 class TheoryArith : public Theory {
 private:
 
-  /* TODO Everything in the chopping block needs to be killed. */
-  /* Chopping block begins */
-
-  std::vector<Node> d_splits;
-  //This stores the eager splits sent out of the theory.
-
-  /* Chopping block ends */
+  /** Static learner. */
+  ArithStaticLearner learner;
 
+  /**
+   * List of the variables in the system.
+   * This is needed to keep a positive ref count on slack variables.
+   */
   std::vector<Node> d_variables;
 
   /**
    * If ArithVar v maps to the node n in d_removednode,
    * then n = (= asNode(v) rhs) where rhs is a term that
-   * can be used to determine the value of n uysing getValue().
+   * can be used to determine the value of n using getValue().
    */
   std::map<ArithVar, Node> d_removedRows;
 
-  /** Stores system wide constants to avoid unnessecary reconstruction. */
-  ArithConstants d_constants;
-
   /**
    * Manages information about the assignment and upper and lower bounds on
    * variables.
@@ -178,9 +175,17 @@ public:
     d_simplex.notifyOptions(opt);
   }
 private:
+  /** The constant zero. */
+  DeltaRational d_DELTA_ZERO;
 
+  /**
+   * Using the simpleKind return the ArithVar associated with the
+   * left hand side of assertion.
+   */
   ArithVar determineLeftVariable(TNode assertion, Kind simpleKind);
 
+  /** Splits the disequalities in d_diseq that are violated using lemmas on demand. */
+  void splitDisequalities();
 
   /**
    * This requests a new unique ArithVar value for x.
@@ -203,6 +208,11 @@ private:
   bool assertionCases(TNode assertion);
 
   /**
+   * This is used for reporting conflicts caused by disequalities during assertionCases.
+   */
+  void disequalityConflict(TNode eq, TNode lb, TNode ub);
+
+  /**
    * Returns the basic variable with the shorted row containg a non-basic variable.
    * If no such row exists, return ARITHVAR_SENTINEL.
    */
@@ -225,6 +235,10 @@ private:
                  std::vector<Rational>& coeffs,
                  std::vector<ArithVar>& variables) const;
 
+  /** Routine for debugging. Print the assertions the theory is aware of. */
+  void debugPrintAssertions();
+  /** Debugging only routine. Prints the model. */
+  void debugPrintModel();
 
   /** These fields are designed to be accessable to TheoryArith methods. */
   class Statistics {
@@ -237,9 +251,6 @@ private:
     IntStat d_permanentlyRemovedVariables;
     TimerStat d_presolveTime;
 
-    IntStat d_miplibtrickApplications;
-    AverageStat d_avgNumMiplibtrickValues;
-
     BackedStat<double> d_initialTableauDensity;
     AverageStat d_avgTableauDensityAtRestart;
     IntStat d_tableauResets;