From ca8411fd89030ac0e60d179fe67da57d09705d3a Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 9 Dec 2009 02:11:49 +0000
Subject: [PATCH] fixed the bug in CNF translation that caused test000013.cvc
 to slow down

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@494 e59a4935-1847-0410-ae03-e826735625c1
---
 src/to-sat/CallSAT.cpp | 18 +++++++--------
 src/to-sat/ToCNF.cpp   | 50 ++++++++++++++++++++++++++++++++++--------
 src/to-sat/ToCNF.h     |  9 ++++++++
 3 files changed, 59 insertions(+), 18 deletions(-)

diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp
index c3e5989..a7e29fd 100644
--- a/src/to-sat/CallSAT.cpp
+++ b/src/to-sat/CallSAT.cpp
@@ -25,10 +25,10 @@ namespace BEEV
           {
             cl_size = CLAUSAL_BUCKET_LIMIT;
           }
-	// else
-	// 	  {
-	// 	    cl_size = CLAUSAL_BUCKET_LIMIT-1;
-	// 	  }
+	else
+	  {
+	    cl_size = CLAUSAL_BUCKET_LIMIT-1;
+	  }
 
         //If no clauses of size cl_size have been seen, then create a
         //bucket for that size
@@ -58,11 +58,11 @@ namespace BEEV
     for(int count=1;it!=itend;it++, count++)
       {
         ClauseList *cl = (*it).second;
-	if(CLAUSAL_BUCKET_LIMIT == count)
-	  {
-	    sat = toSATandSolve(SatSolver,*cl, false, true);
-	  }
-	else
+// 	if(CLAUSAL_BUCKET_LIMIT == count)
+// 	  {
+// 	    sat = toSATandSolve(SatSolver,*cl, false, true);
+// 	  }
+// 	else
 	  {
 	    sat = toSATandSolve(SatSolver,*cl);
 	  }
diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 9d83290..36351ea 100644
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -638,23 +638,32 @@ namespace BEEV
     
 #if defined CRYPTOMINISAT || defined CRYPTOMINISAT2
     if ((x->clausespos != NULL 
-         && x->clausespos->size() > 1) 
-        || (doRenamePos(*x) && !wasVisited(*x)))
+         && (x->clausespos->size() > 1 
+	     || (renameAllSiblings 
+		 && !(x->clausespos->size()==1)  
+		 && !wasRenamedPos(*x))) 
+	 || (doRenamePos(*x) 
+	     && !wasVisited(*x))))
       {
         if (doSibRenamingPos(*x) 
             || sharesPos(*x) > 1 
-            || doRenamePos(*x))
+            || doRenamePos(*x)
+	    || renameAllSiblings)
           {
             doRenamingPos(varphi, defs);
           }
       }
-
 #else
 
-    if (x->clausespos != NULL && x->clausespos->size() > 1)
+    if (x->clausespos != NULL 
+	&& (x->clausespos->size() > 1
+	    || (renameAllSiblings 
+		&& !(x->clausesneg->size() == 1)  
+		&& !wasRenamedNeg(*x))))
       {
         if (doSibRenamingPos(*x) 
-            || sharesPos(*x) > 1)
+            || sharesPos(*x) > 1
+	    || renameAllSiblings)
           {
             doRenamingPos(varphi, defs);
           }
@@ -666,9 +675,15 @@ namespace BEEV
         convertFormulaToCNFNegCases(varphi, defs);
       }
     
-    if (x->clausesneg != NULL && x->clausesneg->size() > 1)
+    if (x->clausesneg != NULL 
+	&& (x->clausesneg->size() > 1
+	    || (renameAllSiblings
+		&& !(x->clausesneg->size() == 1)
+		&& !wasRenamedNeg(*x))))
       {
-        if (doSibRenamingNeg(*x) || sharesNeg(*x) > 1)
+        if (doSibRenamingNeg(*x) 
+	    || sharesNeg(*x) > 1
+	    || renameAllSiblings)
           {
             doRenamingNeg(varphi, defs);
           }
@@ -676,7 +691,13 @@ namespace BEEV
     
     //########################################
     //mark that we've already done the hard work
-    
+	
+    if(renameAllSiblings)
+      {
+	assert(info[varphi]->clausesneg == NULL 
+	       || info[varphi]->clausesneg->size() ==1);
+      }
+
     setWasVisited(*x);
   } //End of convertFormulaToCNF()
 
@@ -1156,6 +1177,11 @@ namespace BEEV
         reduceMemoryFootprintPos(*it);
       }
     }
+    if (renameAllSiblings)
+      {
+	assert(((unsigned)psi->size()) == varphi.GetChildren().size());
+      }
+
     info[varphi]->clausespos = psi;
   } //End of convertFormulaToCNFPosAND()
 
@@ -1334,6 +1360,11 @@ namespace BEEV
         xor_clause->insert(xor_clause->end(), 
                            ((*(info[*it]->clausespos))[0])->begin(),
                            ((*(info[*it]->clausespos))[0])->end());
+	if(renameAllSiblings)
+          {
+	    assert(info[*it]->clausespos->size() ==1);
+	    assert(info[*it]->clausesneg->size() ==1);
+          }
       }
     doRenamingPosXor(varphi);
     //ClauseList* psi = convertFormulaToCNFPosXORAux(varphi, 0, defs);
@@ -1909,6 +1940,7 @@ namespace BEEV
   {
     bm = bmgr;
     clausesxor = new ClauseList();
+    renameAllSiblings = true;
   }
 
   //########################################
diff --git a/src/to-sat/ToCNF.h b/src/to-sat/ToCNF.h
index edc7354..62d450f 100644
--- a/src/to-sat/ToCNF.h
+++ b/src/to-sat/ToCNF.h
@@ -20,6 +20,15 @@ namespace BEEV
   class CNFMgr
   {  
   private:
+
+    // Setting this to true changes the behaviour of when new
+    // Tseitin variables are created.  Normally a Tseitin
+    // variable is created only if: (the number of clauses is
+    // >1) && (renaming of the node is enabled || the node is
+    // shared). When this is set, every node is replaced by a
+    // new tseitin variable.
+    bool renameAllSiblings;
+
     //########################################
     //########################################
     // data types
-- 
2.47.3