Fix the renameAllSiblings option in the CNF generator. It is still disabled by defaul...

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 4dc37231bd92b957d613ba833d0edcee043c2cef..b0195e5d0927c6d64a7e719048c6f4e4190be9b8 100644 (file)
--- 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 84d5ee6e66a04a1d06b6296e57134525eba67dd6..a7ce3ac3790fc340c53f659afa9645893a3e8e39 100644 (file)
--- 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 539c706c24b577ed6c65ac41fbb13a945d81c081..9b683300515425cc59d9ad3221e035a03f6f327c 100644 (file)
--- 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");\r
        output.append(":source {automatically generated}\n");\r
        output.append(":status unknown\n");\r
-       output.append(":logic QF_BV\n");\r
+       output.append(":logic QF_AUFBV\n");\r
 \r
        for (String s : bits)\r
        {\r