From: msoos Date: Fri, 16 Apr 2010 12:59:14 +0000 (+0000) Subject: Updating CMS2 to fix two bugs X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=dfcd136299883462bd9ddf916a869210a8cbc6dd;p=francis%2Fstp.git 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 7edc6db..1e52009 100644 --- 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 7699b69..227875e 100644 --- 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 > 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 2b1938f..e7c31ff 100644 --- a/src/sat/cryptominisat2/Gaussian.cpp +++ b/src/sat/cryptominisat2/Gaussian.cpp @@ -149,10 +149,8 @@ uint Gaussian::select_columnorder(vector& 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 order_heap(solver.order_heap); diff --git a/src/sat/cryptominisat2/Logger.cpp b/src/sat/cryptominisat2/Logger.cpp index 9677b5c..441b4a0 100644 --- 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 3e87fab..a00c785 100644 --- 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 9a1eda5..6c0ab67 100644 --- 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 - 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 - 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 29b0419..f0c9492 100644 --- 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 addToClauses; diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index 9891684..053ca7f 100644 --- a/src/sat/cryptominisat2/VERSION +++ b/src/sat/cryptominisat2/VERSION @@ -1,2 +1,3 @@ CryptoMiniSat -GIT revision: 1d73485d3a23121ac2d9c5cf4732f0a914018fec +GIT revision: fb3f0713d5864d50cae28535b577fb74fd65899c +