From 710a24b180d26d2d395869d57d61cec0b898196b Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 9 Nov 2009 03:55:50 +0000
Subject: [PATCH] Option currently disabled. To not use Tseitin variables as
 decision variables. On problems that spend the majority of time in the SAT
 solver, this gives 35% improved performance. I don't yet understand how it
 interacts with the CNF bucketisation, so until then won't enable it by
 default.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@392 e59a4935-1847-0410-ae03-e826735625c1
---
 src/STPManager/UserDefinedFlags.h |  4 ++++
 src/to-sat/BitBlast.cpp           |  6 +++---
 src/to-sat/ToSAT.cpp              | 35 ++++++++++++++++++++++++-------
 src/to-sat/ToSAT.h                |  2 +-
 4 files changed, 36 insertions(+), 11 deletions(-)

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index 8755b1e..b9beb3a 100644
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -86,6 +86,8 @@ namespace BEEV
     
     bool quick_statistics_flag;
   
+    bool tseitin_are_decision_variables_flag;
+
     //CONSTRUCTOR    
     UserDefinedFlags()
     {  
@@ -152,6 +154,8 @@ namespace BEEV
       division_by_zero_returns_one_flag = false;
       
       quick_statistics_flag=false;
+
+      tseitin_are_decision_variables_flag=true;
     } //End of constructor for UserDefinedFlags
 
   }; //End of struct UserDefinedFlags
diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index 78d156a..4193e4b 100644
--- a/src/to-sat/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -748,9 +748,9 @@ namespace BEEV
   {
     // For some unexplained reason, XORs are faster than converting
     // them to cluases at this point
-    ASTNode S0 = _bm->CreateSimpForm(XOR, 
-                                     _bm->CreateSimpForm(XOR, xi, yi), 
-                                     cin);    
+    ASTNode S0 = _bm->CreateSimpForm(XOR,
+                                     _bm->CreateSimpForm(XOR, xi, yi),
+                                     cin);
     return S0;
     // ASTNode S1 = _bm->CreateSimpForm(OR,xi,yi,cin);
     //     ASTNode S2 = _bm->CreateSimpForm(OR,
diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 949d064..1f774d5 100644
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -10,10 +10,25 @@
 
 namespace BEEV
 {
-  /* FUNCTION: lookup or create a new MINISAT literal
-   * lookup or create new MINISAT Vars from the global MAP
-   * _ASTNode_to_SATVar.
-   */
+
+bool isTseitinVariable(const ASTNode& n) {
+	if (n.GetKind() == SYMBOL && n.GetType() == BOOLEAN_TYPE) {
+		const char * zz = n.GetName();
+		//if the variables ARE cnf variables then dont make them
+		// decision variables.
+		if (0 == strncmp("cnf", zz, 3))
+		{
+			return true;
+		}
+	}
+	return false;
+}
+
+	/* FUNCTION: lookup or create a new MINISAT literal
+	   * lookup or create new MINISAT Vars from the global MAP
+	   * _ASTNode_to_SATVar.
+	   */
+
   MINISAT::Var 
   ToSAT::LookupOrCreateSATVar(MINISAT::Solver& newS, const ASTNode& n)
   {
@@ -31,7 +46,14 @@ namespace BEEV
         //by 1 each time it is called, and the initial value of a
         //MINISAT::Var is 0.
         _SATVar_to_AST_Vector.push_back(n);
-      }
+
+        // experimental. Don't add Tseitin variables as decision variables.
+        if (!bm->UserFlags.tseitin_are_decision_variables_flag && isTseitinVariable(n))
+        {
+        	newS.setDecisionVar(v,false);
+        }
+
+       }
     else
       v = it->second;
     return v;
@@ -103,7 +125,7 @@ namespace BEEV
         float percentage=CLAUSAL_ABSTRACTION_CUTOFF;
         if(count++ >= input_clauselist_size*percentage)
           {
-            //Arbitrary adding only 60% of the clauses in the hopes of
+        	//Arbitrary adding only 60% of the clauses in the hopes of
             //terminating early 
             //      cout << "Percentage clauses added: " 
             //           << percentage << endl;
@@ -132,7 +154,6 @@ namespace BEEV
       } // End of For-loop adding the clauses 
 
     bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
-    //cout << "Added remaining clauses\n";
     bm->GetRunTimes()->start(RunTimes::Solving);
     newS.solve();
     bm->GetRunTimes()->stop(RunTimes::Solving);
diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h
index 4e10b6a..c80f9c7 100644
--- a/src/to-sat/ToSAT.h
+++ b/src/to-sat/ToSAT.h
@@ -23,7 +23,7 @@
 
 namespace BEEV
 {
-  #define CLAUSAL_ABSTRACTION_CUTOFF 0.6
+  #define CLAUSAL_ABSTRACTION_CUTOFF 1.1
 
   class ToSAT {
   private:
-- 
2.47.3