Last commit contained some strange merging information that made a mess. Sorry, rever...

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

diff --git a/src/sat/cryptominisat2/ClauseCleaner.cpp b/src/sat/cryptominisat2/ClauseCleaner.cpp
index b7d34f239d7b1e57ceb12a7dad9a351e0156f518..d147e170ae6946ed97f8b9ebf327bbd401c6c519 100644 (file)
--- 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 a0f4f24c89f4cdaeccb0661ba848fc1096e1cb0d..ee986c3fd2653a181b8080007afcf3bf9a643d67 100644 (file)
--- 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 a39ea993dacf8e8c1eb2c1290108f6170f4d0011..9a1eda5332e8763d38348ddbe8a1da64bfddaa77 100644 (file)
--- 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)
 {