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

diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp
index c3e59892b5a29581a0815d06681534a6762f50e6..a7e29fdc0569ca0d6fceaea8c6f19bd459ef7b90 100644 (file)
--- 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 9d832905a828a7118c15f691d46ae40264a48f9d..36351ea660e24134c065e5abda5ce98a89fddc83 100644 (file)
--- 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 edc7354341ea4115bd5814e1f752436f2da92771..62d450f6eb7d6d78624f7abdbdaa84648b1f748a 100644 (file)
--- 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