From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 25 Apr 2010 14:28:32 +0000 (+0000)
Subject: Fix the renameAllSiblings option in the CNF generator. It is still disabled by defaul... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=18f104634c416136e37b4d8e0efd22017fb8146a;p=francis%2Fstp.git

Fix the renameAllSiblings option in the CNF generator. It is still disabled by default until I measure its usefulnes..



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

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index 4dc3723..b0195e5 100644
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -106,6 +106,9 @@ namespace BEEV
   
     bool tseitin_are_decision_variables_flag;
 
+    // Create a new Tseitin variable for every intermediate value.
+    bool renameAllInCNF_flag;
+
     // Available back-end SAT solvers.
     enum SATSolvers
       {
@@ -205,6 +208,10 @@ namespace BEEV
       // use minisat by default.
       solver_to_use = MINISAT_SOLVER;
 
+      // The special Cryptominisat2 CNF generation with this flag enabled seems to go into an infinite loop.
+      // beware of turning this on if you are using cryptominsat2.
+      renameAllInCNF_flag= false;
+
     } //End of constructor for UserDefinedFlags
 
   }; //End of struct UserDefinedFlags
diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 84d5ee6..a7ce3ac 100644
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -642,7 +642,7 @@ namespace BEEV
     if ((x->clausespos != NULL 
          && (x->clausespos->size() > 1 
 	     || (renameAllSiblings 
-		 && !(x->clausespos->size()==1)  
+    	    		 && !(x->clausespos->size() == 1 && x->clausespos[0].size() ==1)
 		 && !wasRenamedPos(*x))) 
 	 || (doRenamePos(*x) 
 	     && !wasVisited(*x))))
@@ -657,10 +657,11 @@ namespace BEEV
       }
 #else
 
+    
     if (x->clausespos != NULL 
 	&& (x->clausespos->size() > 1
 	    || (renameAllSiblings 
-		&& !(x->clausesneg->size() == 1)  
+	    && !(x->clausespos->size() == 1 && x->clausespos[0].size() ==1)
 		&& !wasRenamedNeg(*x))))
       {
         if (doSibRenamingPos(*x) 
@@ -678,10 +679,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 && x->clausesneg[0].size() ==1)
+ 		&& !wasRenamedNeg(*x))))
       {
         if (doSibRenamingNeg(*x) 
 	    || sharesNeg(*x) > 1
@@ -698,6 +699,9 @@ namespace BEEV
       {
 	assert(info[varphi]->clausesneg == NULL 
 	       || info[varphi]->clausesneg->size() ==1);
+
+	assert(info[varphi]->clausespos == NULL
+		       || info[varphi]->clausespos->size() ==1);
       }
 
     setWasVisited(*x);
@@ -1386,6 +1390,10 @@ namespace BEEV
     for (; it != varphi.GetChildren().end(); it++)
       {
         convertFormulaToCNF(*it, defs); // make pos and neg clause sets
+		if (renameAllSiblings) {
+			assert(info[*it]->clausespos->size() ==1);
+			assert(info[*it]->clausesneg->size() ==1);
+      }
       }
     ClauseList* psi = convertFormulaToCNFPosXORAux(varphi, 0, defs);
     info[varphi]->clausespos = psi;
@@ -1942,7 +1950,7 @@ namespace BEEV
   {
     bm = bmgr;
     clausesxor = new ClauseList();
-    renameAllSiblings = false;
+    renameAllSiblings = bm->UserFlags.renameAllInCNF_flag;
   }
 
   //########################################
diff --git a/tests/generated_tests/ArrayGenerator.java b/tests/generated_tests/ArrayGenerator.java
index 539c706..9b68330 100644
--- a/tests/generated_tests/ArrayGenerator.java
+++ b/tests/generated_tests/ArrayGenerator.java
@@ -37,7 +37,7 @@ public class ArrayGenerator
 	output.append("benchmark t.smt\n");
 	output.append(":source {automatically generated}\n");
 	output.append(":status unknown\n");
-	output.append(":logic QF_BV\n");
+	output.append(":logic QF_AUFBV\n");
 
 	for (String s : bits)
 	{