Updating CMS2 to fix two bugs

One was a bug relating to binarary xor-finding while doing failed
var searching: the xor-clauses were not cleaned beforehand.

The second bug was an inverted shrinking of memory contents in
operator= of Heap.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@683 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/sat/cryptominisat2/BitArray.h b/src/sat/cryptominisat2/BitArray.h
index 7edc6dbaac06d1895ce20d1d38a02f5815822e7f..1e52009823c75de3aa820bcdcbc74774cf138d8b 100644 (file)
--- a/src/sat/cryptominisat2/BitArray.h
+++ b/src/sat/cryptominisat2/BitArray.h
@@ -60,7 +60,7 @@ public:
         return *this;
     }
     
-    void resize(uint _size)
+    void resize(uint _size, const bool fill)
     {
         _size = _size/64 + (bool)(_size%64);
         if (size != _size) {
@@ -68,6 +68,8 @@ public:
             size = _size;
             mp = new uint64_t[size];
         }
+        if (fill) setOne();
+        else setZero();
     }
     
     ~BitArray()
@@ -89,6 +91,11 @@ public:
     {
         memset(mp, 0, size*sizeof(uint64_t));
     }
+    
+    inline void setOne()
+    {
+        memset(mp, 0, size*sizeof(uint64_t));
+    }
 
     inline void clearBit(const uint i)
     {

diff --git a/src/sat/cryptominisat2/FailedVarSearcher.cpp b/src/sat/cryptominisat2/FailedVarSearcher.cpp
index 7699b69c7c143c71648dad3b89feae2ca3edd782..227875ee068a55c425b750484d58354408fa9243 100644 (file)
--- a/src/sat/cryptominisat2/FailedVarSearcher.cpp
+++ b/src/sat/cryptominisat2/FailedVarSearcher.cpp
@@ -27,8 +27,9 @@ using std::set;
 #include "ClauseCleaner.h"
 #include "time_mem.h"
 #include "VarReplacer.h"
+#include "ClauseCleaner.h"
 
-//#define FINDBINARYXOR
+//#define VERBOSE_DEUBUG
 
 namespace MINISAT
 {
@@ -55,7 +56,7 @@ void FailedVarSearcher::addFromSolver(const vec< XorClause* >& cs)
     uint32_t i = 0;
     for (XorClause * const*it = cs.getData(), * const*end = it + cs.size(); it !=  end; it++, i++) {
         if (it+1 != end)
-            __builtin_prefetch(*(it+1), 1, 1);
+            __builtin_prefetch(*(it+1), 0, 0);
         
         const XorClause& cl = **it;
         xorClauseSizes[i] = cl.size();
@@ -105,6 +106,13 @@ const TwoLongXor FailedVarSearcher::getTwoLongXor(const XorClause& c)
         }
     }
     
+    #ifdef VERBOSE_DEUBUG
+    if (num != 2) {
+        std::cout << "Num:" << num << std::endl;
+        c.plainPrint();
+    }
+    #endif
+    
     std::sort(&tmp.var[0], &tmp.var[0]+2);
     assert(num == 2);
     return tmp;
@@ -144,9 +152,9 @@ const bool FailedVarSearcher::search(uint64_t numProps)
     
     //For BothSame
     BitArray propagated;
-    propagated.resize(solver.nVars());
+    propagated.resize(solver.nVars(), 0);
     BitArray propValue;
-    propValue.resize(solver.nVars());
+    propValue.resize(solver.nVars(), 0);
     vector<pair<Var, bool> > bothSame;
     
     //For 2-long xor (rule 6 of  Equivalent literal propagation in the DLL procedure by Chu-Min Li)
@@ -159,8 +167,11 @@ const bool FailedVarSearcher::search(uint64_t numProps)
         solver.order_heap.size() > 30000 ||
         solver.nClauses() > 100000)
         binXorFind = false;
-    if (binXorFind) addFromSolver(solver.xorclauses);
-    xorClauseTouched.resize(solver.xorclauses.size());
+    if (binXorFind) {
+        solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses);
+        addFromSolver(solver.xorclauses);
+    }
+    xorClauseTouched.resize(solver.xorclauses.size(), 0);
     
     finishedLastTime = true;
     lastTimeWentUntil = solver.nVars();
@@ -210,7 +221,7 @@ const bool FailedVarSearcher::search(uint64_t numProps)
                 }
                 
                 if (binXorFind) {
-                    for (uint32_t *it = investigateXor.getData(), *end = it + investigateXor.size(); it != end; it++) {
+                    for (uint32_t *it = investigateXor.getData(), *end = investigateXor.getDataEnd(); it != end; it++) {
                         if (xorClauseSizes[*it] == 2)
                             twoLongXors.insert(getTwoLongXor(*solver.xorclauses[*it]));
                     }

diff --git a/src/sat/cryptominisat2/Gaussian.cpp b/src/sat/cryptominisat2/Gaussian.cpp
index 2b1938f6e78e0de13982680cd30481dbfbd0c97f..e7c31ffb950b215ae22c9d0db33bb7db01b68cbf 100644 (file)
--- a/src/sat/cryptominisat2/Gaussian.cpp
+++ b/src/sat/cryptominisat2/Gaussian.cpp
@@ -149,10 +149,8 @@ uint Gaussian::select_columnorder(vector<uint16_t>& var_to_col, matrixset& origM
             largest_used_var = i;
     var_to_col.resize(largest_used_var + 1);
     
-    var_is_in.resize(var_to_col.size());
-    var_is_in.setZero();
-    origMat.var_is_set.resize(var_to_col.size());
-    origMat.var_is_set.setZero();
+    var_is_in.resize(var_to_col.size(), 0);
+    origMat.var_is_set.resize(var_to_col.size(), 0);
 
     origMat.col_to_var.clear();
     Heap<Solver::VarOrderLt> order_heap(solver.order_heap);

diff --git a/src/sat/cryptominisat2/Logger.cpp b/src/sat/cryptominisat2/Logger.cpp
index 9677b5c15fe142d6df471bdec81b2b7e9723b75a..441b4a09aa95d5724e96c768376799281d47bb63 100644 (file)
--- a/src/sat/cryptominisat2/Logger.cpp
+++ b/src/sat/cryptominisat2/Logger.cpp
@@ -119,11 +119,17 @@ void Logger::cut_name_to_size(string& name) const
 }
 
 // Adds the new clause group's name to the information stored
-void Logger::set_group_name(const uint group, string name)
+void Logger::set_group_name(const uint group, char* name_tmp)
 {
     if (!statistics_on && !proof_graph_on)
         return;
     
+    string name;
+    if (name_tmp == NULL)
+        name = "";
+    else
+        name = name_tmp;
+    
     new_group(group);
     cut_name_to_size(name);
 
@@ -140,12 +146,19 @@ void Logger::set_group_name(const uint group, string name)
 }
 
 // sets the variable's name
-void Logger::set_variable_name(const uint var, string name)
+void Logger::set_variable_name(const uint var, char* name_tmp)
 {
     if (!statistics_on && !proof_graph_on)
         return;
     
     new_var(var);
+    
+    string name;
+    if (name_tmp == NULL)
+        name = "";
+    else
+        name = name_tmp;
+    
     cut_name_to_size(name);
     
     if (varnames[var] == "Noname") {

diff --git a/src/sat/cryptominisat2/Logger.h b/src/sat/cryptominisat2/Logger.h
index 3e87fab3a7219680c74b94d6bde4e252cda5288d..a00c785576a07d3f4a959f7e85511b7e66b4ca5c 100644 (file)
--- a/src/sat/cryptominisat2/Logger.h
+++ b/src/sat/cryptominisat2/Logger.h
@@ -78,10 +78,10 @@ public:
 
     //functions to add/name variables
     void new_var(const Var var);
-    void set_variable_name(const uint var, string name);
+    void set_variable_name(const uint var, char* name_tmp);
 
     //function to name clause groups
-    void set_group_name(const uint group, string name);
+    void set_group_name(const uint group, char* name_tmp);
 
     void begin();
     void end(const finish_type finish);

diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h
index 9a1eda5332e8763d38348ddbe8a1da64bfddaa77..6c0ab67463446b5b755cf8d6a21b62748849d27d 100644 (file)
--- a/src/sat/cryptominisat2/Solver.h
+++ b/src/sat/cryptominisat2/Solver.h
@@ -80,9 +80,9 @@ public:
     //
     Var     newVar    (bool dvar = true); // Add a new variable with parameters specifying variable mode.
     template<class T>
-    bool    addClause (T& ps, const uint group = 0, char* group_name = "");  // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method!
+    bool    addClause (T& ps, const uint group = 0, char* group_name = NULL);  // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method!
     template<class T>
-    bool    addXorClause (T& ps, bool xor_clause_inverted, const uint group = 0, char* group_name = "");  // Add a xor-clause to the solver. NOTE! 'ps' may be shrunk by this method!
+    bool    addXorClause (T& ps, bool xor_clause_inverted, const uint group = 0, char* group_name = NULL);  // Add a xor-clause to the solver. NOTE! 'ps' may be shrunk by this method!
 
     // Solving:
     //

diff --git a/src/sat/cryptominisat2/Subsumer.cpp b/src/sat/cryptominisat2/Subsumer.cpp
index 29b041933c6acdcd2efc457c0a37fd7182cdf1e7..f0c9492c576936c734d23a481e821c66e8ae4cae 100644 (file)
--- a/src/sat/cryptominisat2/Subsumer.cpp
+++ b/src/sat/cryptominisat2/Subsumer.cpp
@@ -1393,7 +1393,7 @@ const bool Subsumer::hyperBinRes()
     double myTime = cpuTime();
     
     BitArray inside;
-    inside.resize(solver.nVars()*2);
+    inside.resize(solver.nVars()*2, 0);
     uint32_t hyperBinAdded = 0;
     uint32_t hyperBinUnitary = 0;
     vec<ClauseSimp> addToClauses;

diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION
index 9891684c5d96e231660db62fa42ffc34976f6b6c..053ca7f7b0516d445def6cfabcfd5014f40f5f48 100644 (file)
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,2 +1,3 @@
 CryptoMiniSat
-GIT revision: 1d73485d3a23121ac2d9c5cf4732f0a914018fec
+GIT revision: fb3f0713d5864d50cae28535b577fb74fd65899c
+