From b7a2b2389934e204e02b9c4362f03f7a2ac99592 Mon Sep 17 00:00:00 2001 From: msoos Date: Tue, 1 Dec 2009 22:31:09 +0000 Subject: [PATCH] Fixing problem with CRYPTOMINSAT2 from an STP point of view. simplify() does not need to be called before solve() in either CRYPTOMINISAT1 or 2 git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@437 e59a4935-1847-0410-ae03-e826735625c1 --- src/to-sat/CallSAT.cpp | 4 ++-- src/to-sat/ToSAT.cpp | 10 +--------- 2 files changed, 3 insertions(+), 11 deletions(-) diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp index c93cf89..a3e7317 100644 --- 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 b807f2e..de26935 100644 --- 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()) -- 2.47.3