From: msoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 28 Apr 2010 12:25:09 +0000 (+0000)
Subject: Turning on simplification&subpart-solving in CMS2
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=cba4184a3fdd68dc02a0f16c254f4cefbfc83ac1;p=francis%2Fstp.git

Turning on simplification&subpart-solving in CMS2

Simplification is carried if the problem seems difficult. It is carried
out in steps, so the complete algorithm's time demands do not have to
absorbed the first time it is run. Subpart-solving regularly checks for
parts of the problem that are disconnected, solves them, and returns to
the original problem instance -- essentially executing a
divide-and-conquer algorithm

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

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 555660e..dc7952d 100644
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -135,9 +135,10 @@ namespace BEEV
 
 #if defined CRYPTOMINISAT2
     newSolver.findNormalXors = false;
-    newSolver.doSubsumption = false;
+    newSolver.doSubsumption = true;
     newSolver.verbosity = 0;
-    newSolver.doPartHandler = false;
+    //newSolver.fixRestartType = static_restart;
+    newSolver.doPartHandler = true;
 #endif
 
 // 	if(enable_clausal_abstraction &&