lots of changes aimed at CryptoMiniSAT2

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

diff --git a/src/sat/cryptominisat/Solver.cpp b/src/sat/cryptominisat/Solver.cpp
index 01a4d8a586b3e20b344fbc0ec8ab18523b353cfb..b5c3af596b44500240ee68ad52518c6a113cb53c 100644 (file)
--- a/src/sat/cryptominisat/Solver.cpp
+++ b/src/sat/cryptominisat/Solver.cpp
@@ -17,6 +17,7 @@ NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FO
 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
+
 #include "Solver.h"
 #include "Sort.h"
 #include <cmath>

diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp
index 46f7062d87229914ebaa0cfe7732c307b2f953b6..0cb5424b84b8e08e3995af9de6db0a684827fd58 100644 (file)
--- a/src/sat/cryptominisat2/Solver.cpp
+++ b/src/sat/cryptominisat2/Solver.cpp
@@ -37,7 +37,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "Conglomerate.h"
 #include "XorFinder.h"
 
-#define DEBUG_LIB
+//#define DEBUG_LIB
 
 #ifdef DEBUG_LIB
 #include <sstream>

diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index a762e07001e481f16ee5f4852451eb4a2b142651..07d22ddb83a6ce291a270a623c9fdf59ebd5443e 100644 (file)
--- a/src/to-sat/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -6,7 +6,6 @@
  *
  * LICENSE: Please view LICENSE file in the home dir of this Program
  ********************************************************************/
-
 #include <cmath>
 #include <cassert>
 #include "../AST/AST.h"
@@ -968,7 +967,7 @@ namespace BEEV
         bit_comparisons.push_back(prev_eq_bit);
       }
     ASTNode output =
-      _bm->CreateSimpForm(OR, bit_comparisons);
+      _bm->CreateSimpForm(XOR, bit_comparisons);
 
     return output;
   }

diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp
index a3e7317bb6d1e9d5d694bdb7d865a1007adfc982..8a134a978af97066dbc08686304ee1645ee24fe7 100644 (file)
--- a/src/to-sat/CallSAT.cpp
+++ b/src/to-sat/CallSAT.cpp
@@ -6,7 +6,6 @@
  *
  * LICENSE: Please view LICENSE file in the home dir of this Program
  ********************************************************************/
-
 #include "ToSAT.h"
 #define MAX_BUCKET_LIMIT 3
 

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index de26935ba3f23051d59fec82b53795f618c11432..c6d309af86158829eec1b7461335cc0893d60795 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -134,6 +134,8 @@ namespace BEEV
 
 #if defined CRYPTOMINISAT2
              newS.set_gaussian_decision_until(100);
+             newS.performReplace = false;
+             newS.xorFinder = false;
 #endif
               newS.solve();
             bm->GetRunTimes()->stop(RunTimes::Solving);
@@ -159,7 +161,7 @@ namespace BEEV
 
     bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
     bm->GetRunTimes()->start(RunTimes::Solving);
-
+    
     newS.solve();
     bm->GetRunTimes()->stop(RunTimes::Solving);
     bm->PrintStats(newS);