From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 9 Dec 2009 19:45:20 +0000 (+0000)
Subject: added SAT verbosity to statistics option
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=8cf2fd8a2f5efbe4f795caf3d34f1d432d50bdcc;p=francis%2Fstp.git

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 396ffc0..70d7bc5 100644
--- 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 bd0646a..d5ff134 100644
--- 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 36351ea..8519e76 100644
--- 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 f4877fd..262d827 100644
--- 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