From: msoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 5 Jul 2010 08:48:57 +0000 (+0000)
Subject: For low-cutoff speed reasons, it's best not to subsume learnts
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=32e0493affc0279ab38e193bf29c3fbd12c2ad31;p=francis%2Fstp.git

For low-cutoff speed reasons, it's best not to subsume learnts

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

diff --git a/src/sat/cryptominisat2/Subsumer.cpp b/src/sat/cryptominisat2/Subsumer.cpp
index 27126c2..1b056c0 100644
--- a/src/sat/cryptominisat2/Subsumer.cpp
+++ b/src/sat/cryptominisat2/Subsumer.cpp
@@ -1148,8 +1148,8 @@ const bool Subsumer::simplifyBySubsumption(const bool alsoLearnt)
     else fullSubsume = false;
     if (alsoLearnt) fullSubsume = true;
 
-    solver.clauseCleaner->cleanClauses(solver.learnts, ClauseCleaner::learnts);
-    addFromSolver<true>(solver.learnts, alsoLearnt);
+    //solver.clauseCleaner->cleanClauses(solver.learnts, ClauseCleaner::learnts);
+    //addFromSolver<true>(solver.learnts, alsoLearnt);
     solver.clauseCleaner->cleanClauses(solver.clauses, ClauseCleaner::clauses);
     addFromSolver<true>(solver.clauses, alsoLearnt);