From d25af2d436b1ac19733d2707fdcc6567ec879bc9 Mon Sep 17 00:00:00 2001
From: msoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 7 Dec 2009 23:39:27 +0000
Subject: [PATCH] Updating CryptoMiniSat to r579, fixing a small bug, and
 adding a minor performance-increasing patch

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@481 e59a4935-1847-0410-ae03-e826735625c1
---
 src/sat/cryptominisat2/Solver.cpp      | 4 ++--
 src/sat/cryptominisat2/VERSION         | 4 ++--
 src/sat/cryptominisat2/VarReplacer.cpp | 7 ++++++-
 src/sat/cryptominisat2/VarReplacer.h   | 1 +
 4 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp
index 59fda20..a7acf2a 100644
--- 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 ddf9a02..79378eb 100644
--- 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 8dcabfd..b04f9e0 100644
--- 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 a61b99b..24d94d7 100644
--- 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;
-- 
2.47.3