]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commitdiff
For low-cutoff speed reasons, it's best not to subsume learnts
authormsoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Mon, 5 Jul 2010 08:48:57 +0000 (08:48 +0000)
committermsoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Mon, 5 Jul 2010 08:48:57 +0000 (08:48 +0000)
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@924 e59a4935-1847-0410-ae03-e826735625c1

src/sat/cryptominisat2/Subsumer.cpp

index 27126c22207947748d87642a2191b09f847d0c39..1b056c0f93c0589dbc18e3dbf01493675df660b3 100644 (file)
@@ -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);