Updating CryptoMiniSat to r579, fixing a small bug, and adding a minor performance...

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

diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp
index 59fda2021f82361cf4c79aa7917f02deb5678f8d..a7acf2a8c0b86d729add58d4ddd569e9cd1df0ce 100644 (file)
--- a/src/sat/cryptominisat2/Solver.cpp
+++ b/src/sat/cryptominisat2/Solver.cpp
@@ -182,7 +182,7 @@ bool Solver::addXorClause(vec<Lit>& ps, bool xor_clause_inverted, const uint gro
         return false;
 
     // Check if clause is satisfied and remove false/duplicate literals:
-    if (toReplace->getNumReplacedLits()) {
+    if (toReplace->getNumLastReplacedVars()) {
         for (int i = 0; i != ps.size(); i++) {
             ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
         }
@@ -263,7 +263,7 @@ bool Solver::addClause(vec<Lit>& ps, const uint group, char* group_name)
         return false;
 
     // Check if clause is satisfied and remove false/duplicate literals:
-    if (toReplace->getNumReplacedLits()) {
+    if (toReplace->getNumLastReplacedVars()) {
         for (int i = 0; i != ps.size(); i++) {
             ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
         }

diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION
index ddf9a023360d77bdbc48f26eba63bb6025e58945..79378ebf45633ad612b5e4b246d942c632134785 100644 (file)
--- a/src/sat/cryptominisat2/VERSION
+++ b/src/sat/cryptominisat2/VERSION
@@ -1,3 +1,3 @@
 CryptoMiniSat
-SVN revision: 577
-GIT revision: 2db0ff9414cbeae2c64bb74a0ec4fc2199b30c8a
+SVN revision: 579
+GIT revision: d7ef400c6dbb9bc0b6b3fd98a0c43b178916a849

diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp
index 8dcabfd9a5e772791a12f983d4d12d1e5e26df80..b04f9e0c50201f4544bb59a2a8c583d39cd5cf2f 100644 (file)
--- a/src/sat/cryptominisat2/VarReplacer.cpp
+++ b/src/sat/cryptominisat2/VarReplacer.cpp
@@ -45,7 +45,7 @@ void VarReplacer::performReplace()
     S->clauseCleaner->cleanClauses(S->learnts, ClauseCleaner::learnts);
     S->clauseCleaner->cleanClauses(S->xorclauses, ClauseCleaner::xorclauses);
     
-    if (!addedNewClause && replacedVars == lastReplacedVars) return;
+    if (replacedVars == lastReplacedVars) return;
     
     #ifdef VERBOSE_DEBUG
     {
@@ -261,6 +261,11 @@ const uint VarReplacer::getNumReplacedVars() const
     return replacedVars;
 }
 
+const uint VarReplacer::getNumLastReplacedVars() const
+{
+    return lastReplacedVars;
+}
+
 const vector<Lit>& VarReplacer::getReplaceTable() const
 {
     return table;

diff --git a/src/sat/cryptominisat2/VarReplacer.h b/src/sat/cryptominisat2/VarReplacer.h
index a61b99b0a5f5d0ef146f4e831fc6fdb1599dd69d..24d94d73746eae9629b806b3ca8d3d704489f47d 100644 (file)
--- a/src/sat/cryptominisat2/VarReplacer.h
+++ b/src/sat/cryptominisat2/VarReplacer.h
@@ -27,6 +27,7 @@ class VarReplacer
         void performReplace();
         const uint getNumReplacedLits() const;
         const uint getNumReplacedVars() const;
+        const uint getNumLastReplacedVars() const;
         const vector<Var> getReplacingVars() const;
         const vector<Lit>& getReplaceTable() const;
         const vec<Clause*>& getClauses() const;