From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 22 Feb 2012 03:00:24 +0000 (+0000)
Subject: minor change to order fn in sat solver's ElimLt
X-Git-Tag: cvc5-1.0.0~8314
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5113a97006ab1ed6de2eec471b9ad624d14e8d27;p=cvc5.git

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 9b5e5d45c..68ea6e463 100644
--- 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 {