Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.

1 files changed, 11 insertions, 11 deletions

diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index 5039f826c..32b8382fa 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -102,17 +102,17 @@ private:
   };
   context::CDList<Constraint> d_trail;
 
-  /** Compare by d_minimal. */
-  struct TrailMinimalCoefficientOrder {
-    const context::CDList<Constraint>& d_trail;
-    TrailMinimalCoefficientOrder(const context::CDList<Constraint>& trail):
-      d_trail(trail)
-    {}
-
-    bool operator()(TrailIndex i, TrailIndex j){
-      return d_trail[i].d_minimalMonomial.absLessThan(d_trail[j].d_minimalMonomial);
-    }
-  };
+  // /** Compare by d_minimal. */
+  // struct TrailMinimalCoefficientOrder {
+  //   const context::CDList<Constraint>& d_trail;
+  //   TrailMinimalCoefficientOrder(const context::CDList<Constraint>& trail):
+  //     d_trail(trail)
+  //   {}
+
+  //   bool operator()(TrailIndex i, TrailIndex j){
+  //     return d_trail[i].d_minimalMonomial.absLessThan(d_trail[j].d_minimalMonomial);
+  //   }
+  // };
 
   /**
    * A substitution is stored as a constraint in the trail together with