From bf7cc5878195d540e2216d07ea746e36855b50a9 Mon Sep 17 00:00:00 2001
From: msoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 15 Apr 2010 13:05:48 +0000
Subject: [PATCH] Last commit contained some strange merging information that
 made a mess. Sorry, reverting.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@679 e59a4935-1847-0410-ae03-e826735625c1
---
 src/sat/cryptominisat2/ClauseCleaner.cpp |  2 +-
 src/sat/cryptominisat2/Solver.cpp        | 20 --------------------
 src/sat/cryptominisat2/Solver.h          |  8 --------
 3 files changed, 1 insertion(+), 29 deletions(-)

diff --git a/src/sat/cryptominisat2/ClauseCleaner.cpp b/src/sat/cryptominisat2/ClauseCleaner.cpp
index b7d34f2..d147e17 100644
--- a/src/sat/cryptominisat2/ClauseCleaner.cpp
+++ b/src/sat/cryptominisat2/ClauseCleaner.cpp
@@ -163,7 +163,7 @@ void ClauseCleaner::cleanClauses(vec<XorClause*>& cs, ClauseSetType type, const
         if (s+1 != end)
             __builtin_prefetch(*(s+1), 1, 0);
         if (cleanClause(**s)) {
-            solver.freeLater.push(*s);
+            free(*s);
             s++;
         } else {
             *ss++ = *s++;
diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp
index a0f4f24..ee986c3 100644
--- a/src/sat/cryptominisat2/Solver.cpp
+++ b/src/sat/cryptominisat2/Solver.cpp
@@ -351,15 +351,6 @@ Clause* Solver::addClauseInt(T& ps, uint group)
 template Clause* Solver::addClauseInt(Clause& ps, const uint group);
 template Clause* Solver::addClauseInt(vec<Lit>& ps, const uint group);
 
-template<class T>
-bool Solver::addClause(T& ps, const uint group, char* group_name)
-{
-    assert(decisionLevel() == 0);
-    if (ps.size() > (0x01UL << 18)) {
-        std::cout << "Too long clause!" << std::endl;
-        exit(-1);
-    }
-    
 template<class T>
 bool Solver::addClause(T& ps, const uint group, char* group_name)
 {
@@ -1031,7 +1022,6 @@ Clause* Solver::propagate(const bool update)
                     confl = k->clause;
                     //goto EndPropagate;
                 }
-                }
             }
         }
         if (confl != NULL)
@@ -1336,14 +1326,6 @@ void Solver::dumpSortedLearnts(const char* file, const uint32_t maxSize)
         }
     }
     
-    fprintf(outfile, "c clauses from binaryClauses\n");
-    if (maxSize >= 2) {
-        for (uint i = 0; i != binaryClauses.size(); i++) {
-            if (binaryClauses[i]->learnt())
-                binaryClauses[i]->plainPrint(outfile);
-        }
-    }
-    
     fprintf(outfile, "c clauses from learnts\n");
     std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_lt());
     for (int i = learnts.size()-1; i >= 0 ; i--) {
@@ -1426,8 +1408,6 @@ lbool Solver::simplify()
         lastNbBin = nbBin;
         becameBinary = 0;
     }
-    if (performReplace && varReplacer->performReplace() == false)
-        return l_False;
 
     // Remove satisfied clauses:
     clauseCleaner->removeAndCleanAll();
diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h
index a39ea99..9a1eda5 100644
--- a/src/sat/cryptominisat2/Solver.h
+++ b/src/sat/cryptominisat2/Solver.h
@@ -564,14 +564,6 @@ inline void Solver::reverse_binary_clause(Clause& c) const {
     }
 }*/
 
-        }
-        if (final)
-            c[0] = c[0].unsign() ^ !assigns[c[0].var()].getBool();
-        
-        c.setUpdateNeeded(false);
-    }
-}*/
-
 template<class T>
 inline void Solver::removeClause(T& c)
 {
-- 
2.47.3