Fixing problem with CRYPTOMINSAT2 from an STP point of view. simplify() does not...

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

diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp
index c93cf89e3346902b0624cfbb7f2e697d98b8a7ac..a3e7317bb6d1e9d5d694bdb7d865a1007adfc982 100644 (file)
--- a/src/to-sat/CallSAT.cpp
+++ b/src/to-sat/CallSAT.cpp
@@ -80,7 +80,7 @@ namespace BEEV
     CNFMgr* cm = new CNFMgr(bm);
     ClauseList* cl = cm->convertToCNF(BBFormula);
 
-#ifdef CRYPTOMINISAT
+#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2
     ClauseList* xorcl = cm->ReturnXorClauses();
 #endif
 
@@ -97,7 +97,7 @@ namespace BEEV
         return sat;
       }
 
-#ifdef CRYPTOMINISAT
+#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2
     if(!xorcl->empty())
       { 
         sat = toSATandSolve(SatSolver, *xorcl, true);

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index b807f2e9a6af94c6075d81f855226df565e62c9c..de26935ba3f23051d59fec82b53795f618c11432 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -132,13 +132,8 @@ namespace BEEV
             bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
             bm->GetRunTimes()->start(RunTimes::Solving);
 
-#if defined CRYPTOMINISAT
-            if (newS.simplify() == MINISAT::l_Undef)
-#endif
-
 #if defined CRYPTOMINISAT2
              newS.set_gaussian_decision_until(100);
-            if (newS.simplify() == MINISAT::l_Undef)
 #endif
               newS.solve();
             bm->GetRunTimes()->stop(RunTimes::Solving);
@@ -165,10 +160,7 @@ namespace BEEV
     bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
     bm->GetRunTimes()->start(RunTimes::Solving);
 
-#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2
-    if (newS.simplify() == MINISAT::l_Undef)
-#endif
-      newS.solve();
+    newS.solve();
     bm->GetRunTimes()->stop(RunTimes::Solving);
     bm->PrintStats(newS);
     if (newS.okay())