minor change to order fn in sat solver's ElimLt

(better, (marginally) faster -- regressions 3605, 3606)

diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 9b5e5d45cf817dbc1e7bdf9780b672fc7e6faf75..68ea6e463d91ac4de6234d9965efc8eac5438bc1 100644 (file)
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -114,13 +114,14 @@ class SimpSolver : public Solver {
         // TODO: are 64-bit operations here noticably bad on 32-bit platforms? Could use a saturating
         // 32-bit implementation instead then, but this will have to do for now.
         uint64_t cost  (Var x)        const { return (uint64_t)n_occ[toInt(mkLit(x))] * (uint64_t)n_occ[toInt(~mkLit(x))]; }
-        bool operator()(Var x, Var y) const { return cost(x) < cost(y); }
+
+        // old ordering function
+        // bool operator()(Var x, Var y) const { return cost(x) < cost(y); }
         
-        // TODO: investigate this order alternative more.
-        // bool operator()(Var x, Var y) const { 
-        //     int c_x = cost(x);
-        //     int c_y = cost(y);
-        //     return c_x < c_y || c_x == c_y && x < y; }
+         bool operator()(Var x, Var y) const { 
+             int c_x = cost(x);
+             int c_y = cost(y);
+             return c_x < c_y || c_x == c_y && x < y; }
     };
 
     struct ClauseDeleted {