Last commit accidentally lacked r2778 and r2779 from integer2. I have manually brought these changes over. Changed the tests used by test/regress/regress0/arith/integers/Makefile.am to be 15 of the more interesting tests. Did a bit of cleanup on TheoryArith to eliminate a warning and remove dead code.

1 files changed, 5 insertions, 10 deletions

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 6b14ae6ff..256a197cd 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -58,6 +58,10 @@ namespace arith {
 class TheoryArith : public Theory {
 private:
 
+  /**
+   * This counter is false if nothing has been done since the last cut.
+   * This is used to break an infinite loop.
+   */
   bool d_hasDoneWorkSinceCut;
 
   /**
@@ -165,7 +169,7 @@ private:
 
   Comparison mkIntegerEqualityFromAssignment(ArithVar v);
 
-  #warning "DO NOT COMMIT TO TRUNK, USE MORE EFFICIENT CHECK INSTEAD"
+  //TODO Replace with a more efficient check
   CDArithVarSet d_varsInDioSolver;
 
   /**
@@ -325,15 +329,6 @@ private:
   /** Initial (not context dependent) sets up for a new slack variable.*/
   void setupSlack(TNode left);
 
-  /**
-   * Performs *permanent* static setup for equalities that have not been
-   * preregistered.
-   * Currently these MUST be introduced by combination.
-   */
-  //void delayedSetupEquality(TNode equality);
-
-  //void delayedSetupPolynomial(TNode polynomial);
-  //void delayedSetupMonomial(const Monomial& mono);
 
   /**
    * Performs a check to see if it is definitely true that setup can be avoided.