added SAT verbosity to statistics option

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

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 396ffc042ab394cf85ce408dc69b608274eb8548..70d7bc51c28fed1a805a34626b247e3e9a262dc8 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -17,16 +17,16 @@ OPTIMIZE      = -O3 -fPIC         # Maximum optimization
 CFLAGS_BASE   = $(OPTIMIZE)
 
 # OPTION to compile CRYPTOMiniSAT
-CRYPTOMINISAT  = true
-CFLAGS_BASE    = $(OPTIMIZE) -DCRYPTOMINISAT
-MTL            = ../sat/cryptominisat/mtl
-SOLVER_INCLUDE = ../sat/cryptominisat
+# CRYPTOMINISAT  = true
+# CFLAGS_BASE    = $(OPTIMIZE) -DCRYPTOMINISAT
+# MTL            = ../sat/cryptominisat/mtl
+# SOLVER_INCLUDE = ../sat/cryptominisat
 
 # OPTION to compile CRYPTOMiniSAT version 2.x
-# CRYPTOMINISAT2 = true
-# CFLAGS_BASE    = $(OPTIMIZE) -DCRYPTOMINISAT2
-# MTL            = ../sat/cryptominisat2/mtl
-# SOLVER_INCLUDE = ../sat/cryptominisat2
+CRYPTOMINISAT2 = true
+CFLAGS_BASE    = $(OPTIMIZE) -DCRYPTOMINISAT2
+MTL            = ../sat/cryptominisat2/mtl
+SOLVER_INCLUDE = ../sat/cryptominisat2
 
 # OPTION to compile MiniSAT
 #CORE          = true

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index bd0646abe34472bdf0b26da0573512ca86052047..d5ff134b29b1ea42d0a2b45fa421d5a9faa4ebe2 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -41,6 +41,11 @@ namespace BEEV {
 #ifdef UNSOUND
     MINISAT::UnsoundSimpSolver NewSolver;
 #endif
+
+    if(bm->UserFlags.stats_flag)
+      {
+       NewSolver.verbosity = 1;
+      }
     
     if(bm->UserFlags.num_absrefine_flag)
       {

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 36351ea660e24134c065e5abda5ce98a89fddc83..8519e76861e5e413ea1936b85ab965d5ed2bfcf3 100644 (file)
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -676,10 +676,10 @@ namespace BEEV
       }
     
     if (x->clausesneg != NULL 
-       && (x->clausesneg->size() > 1
-           || (renameAllSiblings
-               && !(x->clausesneg->size() == 1)
-               && !wasRenamedNeg(*x))))
+       && (x->clausesneg->size() > 1))
+//         || (renameAllSiblings
+//             && !(x->clausesneg->size() == 1)
+//             && !wasRenamedNeg(*x))))
       {
         if (doSibRenamingNeg(*x) 
            || sharesNeg(*x) > 1

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index f4877fd3b6535de63127c6e77f2753fffa113139..262d8275cbaaf3b9933bac0a54a6e3c3a64ba3e6 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -136,7 +136,7 @@ namespace BEEV
 #endif
 
 #if defined CRYPTOMINISAT2
-       newSolver.set_gaussian_decision_until(50);
+       //newSolver.set_gaussian_decision_until(50);
        newSolver.performReplace = false;
        newSolver.xorFinder = false;
 #endif