Fixed a couple of bugs in the way that we do clause generation for

Cryptominisat.

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

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 6e6e784bfe8fd333534a8b8b7dcbd380bff8ddb7..c1504c33d0574b3b944941532c12e26a8992a5eb 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -16,12 +16,12 @@ OPTIMIZE      = -O3 -DNDEBUG      # Maximum optimization
 CFLAGS_BASE   = $(OPTIMIZE)
 
 # OPTION to compile CRYPTOMiniSAT
-#CRYPTOMINISAT = true
-#CFLAGS_BASE   = $(OPTIMIZE) -DCRYPTOMINISAT
+CRYPTOMINISAT = true
+CFLAGS_BASE   = $(OPTIMIZE) -DCRYPTOMINISAT
 
 # OPTION to compile MiniSAT
-CORE          = true
-CFLAGS_BASE   = $(OPTIMIZE) -DCORE
+#CORE          = true
+#CFLAGS_BASE   = $(OPTIMIZE) -DCORE
 
 # OPTION to compile UNSOUND MiniSAT
 #UNSOUND       = true

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 75f39604baed0c876b62cc177ede87cf1cc158c8..7dd563a57b1525b587f96a7bda14fb6cd57ed2c1 100644 (file)
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -463,9 +463,10 @@ namespace BEEV
   //########################################
   //prep. for cnf conversion
 
-  void CNFMgr::scanFormula(const ASTNode& varphi, bool isPos)
+  void CNFMgr::scanFormula(const ASTNode& varphi, bool isPos, bool isXorChild)
   {    
     CNFInfo* x;
+    Kind k = varphi.GetKind();
     
     //########################################
     // step 1, get the info associated with this node
@@ -481,6 +482,13 @@ namespace BEEV
       {
         x = info[varphi];
       }
+
+#ifdef CRYPTOMINISAT
+    if(isXorChild)
+      {
+        setDoRenamePos(*x);
+      }
+#endif
     
     //########################################
     // step 2, we only need to know if shares >= 2
@@ -531,11 +539,11 @@ namespace BEEV
           {
             if (onChildDoPos(varphi, i))
               {
-                scanFormula(varphi[i], isPos);
+                scanFormula(varphi[i], isPos, k == XOR);
               }
             if (onChildDoNeg(varphi, i))
               {
-                scanFormula(varphi[i], !isPos);
+                scanFormula(varphi[i], !isPos, false);
               }
           }
       }
@@ -588,8 +596,8 @@ namespace BEEV
       }
     else if (isITE(varphi))
       {
-        scanFormula(varphi[0], true);
-        scanFormula(varphi[0], false);
+        scanFormula(varphi[0], true, false);
+        scanFormula(varphi[0], false, false);
         scanTerm(varphi[1]);
         scanTerm(varphi[2]);
       }
@@ -628,6 +636,17 @@ namespace BEEV
         convertFormulaToCNFPosCases(varphi, defs);
       }
     
+#ifdef CRYPTOMINISAT
+    if ((x->clausespos != NULL && x->clausespos->size() > 1) || (doRenamePos(*x) && !wasVisited(*x)))
+      {
+        if (doSibRenamingPos(*x) || sharesPos(*x) > 1 || doRenamePos(*x))
+          {
+            doRenamingPos(varphi, defs);
+          }
+      }
+
+#else
+
     if (x->clausespos != NULL && x->clausespos->size() > 1)
       {
         if (doSibRenamingPos(*x) || sharesPos(*x) > 1)
@@ -635,6 +654,7 @@ namespace BEEV
             doRenamingPos(varphi, defs);
           }
       }
+#endif
     
     if (sharesNeg(*x) > 0 && !wasVisited(*x))
       {
@@ -1270,7 +1290,8 @@ namespace BEEV
 
        //Creating a new variable name for each of the children of the
        //XOR node
-       doRenamingPos(*it, defs);
+       //doRenamingPos(*it, defs);
+       doRenamingNeg(*it, defs);
        xor_clause->insert(xor_clause->end(), 
                           ((*(info[*it]->clausespos))[0])->begin(),
                           ((*(info[*it]->clausespos))[0])->end());
@@ -1831,7 +1852,7 @@ namespace BEEV
   ClauseList* CNFMgr::convertToCNF(const ASTNode& varphi)
   {
     bm->GetRunTimes()->start(RunTimes::CNFConversion);
-    scanFormula(varphi, true);
+    scanFormula(varphi, true, false);
     ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*");
     ClauseList* defs = SINGLETON(dummy_true_var);
     convertFormulaToCNF(varphi, defs);

diff --git a/src/to-sat/ToCNF.h b/src/to-sat/ToCNF.h
index b4c7bff16b964497630b6561fd453a87666b45d8..ac61d9bce93660cdd743a643ae8767674a066e00 100644 (file)
--- a/src/to-sat/ToCNF.h
+++ b/src/to-sat/ToCNF.h
@@ -146,7 +146,7 @@ namespace BEEV
     //########################################
     //prep. for cnf conversion
 
-    void scanFormula(const ASTNode& varphi, bool isPos);    
+    void scanFormula(const ASTNode& varphi, bool isPos, bool isXorChild);    
 
     void scanTerm(const ASTNode& varphi);