Fixed -x bug in the CNF converter, and added a test, rna2.cvc, to the

regressions. All of the modified files in the various branches, I am not sure
about, except that since they are my branches, it doesn't really matter.

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

diff --git a/scripts/config.info b/scripts/config.info
index 9613a5bfae6330f672438018140654dab358df3f..6befdf280068c2ffbb75ab90f69816262a160820 100644 (file)
--- a/scripts/config.info
+++ b/scripts/config.info
@@ -1 +1 @@
-PREFIX=/afs/csail.mit.edu/u/v/vganesh
+PREFIX=/Users/katelman

diff --git a/src/AST/ToCNF.cpp b/src/AST/ToCNF.cpp
index 76daf4f613db2141efa8f413ec6fea4a63be6ed0..3291d7e0f6241bda2da2adb09a308a698836a046 100644 (file)
--- a/src/AST/ToCNF.cpp
+++ b/src/AST/ToCNF.cpp
@@ -608,6 +608,7 @@ private:
                                }
                        }
                }
+
        }
 
        void scanTerm(const ASTNode& varphi)
@@ -1274,8 +1275,18 @@ private:
 
        void convertFormulaToCNFPosXOR(const ASTNode& varphi, BeevMgr::ClauseList* defs)
        {
+               ASTVec::const_iterator it = varphi.GetChildren().begin();
+               for (; it != varphi.GetChildren().end(); it++)
+    {
+                 convertFormulaToCNF(*it, defs); // make pos and neg clause sets
+    }
                BeevMgr::ClauseList* psi = convertFormulaToCNFPosXORAux(varphi, 0, defs);
                info[varphi]->clausespos = psi;
+               ASTVec::const_iterator it2 = varphi.GetChildren().begin();
+               for (; it2 != varphi.GetChildren().end(); it2++){
+                 reduceMemoryFootprintPos(*it2);
+                 reduceMemoryFootprintNeg(*it2);
+    }
        }
 
        BeevMgr::ClauseList* convertFormulaToCNFPosXORAux(const ASTNode& varphi, unsigned int idx, BeevMgr::ClauseList* defs)
@@ -1293,7 +1304,6 @@ private:
                        //    (PRODUCT       [idx]   ;     [idx+1])
                        //  ; (PRODUCT NOT   [idx]   ; NOT [idx+1])
                        //****************************************
-                       convertFormulaToCNF(varphi[idx], defs);
                        renamesibs = (info[varphi[idx]]->clausespos)->size() > 1 ? true : false;
                        if (renamesibs)
                        {
@@ -1304,15 +1314,10 @@ private:
                        {
                                setDoSibRenamingNeg(*info[varphi[idx + 1]]);
                        }
-                       convertFormulaToCNF(varphi[idx + 1], defs);
 
                        psi1 = PRODUCT(*(info[varphi[idx]]->clausespos), *(info[varphi[idx + 1]]->clausespos));
                        psi2 = PRODUCT(*(info[varphi[idx]]->clausesneg), *(info[varphi[idx + 1]]->clausesneg));
                        NOCOPY_INPLACE_UNION(psi1, psi2);
-                       reduceMemoryFootprintPos(varphi[idx]);
-                       reduceMemoryFootprintPos(varphi[idx + 1]);
-                       reduceMemoryFootprintNeg(varphi[idx]);
-                       reduceMemoryFootprintNeg(varphi[idx + 1]);
 
                        psi = psi1;
                }
@@ -1337,15 +1342,12 @@ private:
                        {
                                setDoSibRenamingNeg(*info[varphi[idx]]);
                        }
-                       convertFormulaToCNF(varphi[idx], defs);
 
                        psi1 = PRODUCT(*(info[varphi[idx]]->clausespos), *theta1);
                        psi2 = PRODUCT(*(info[varphi[idx]]->clausesneg), *theta2);
                        DELETE(theta1);
                        DELETE(theta2);
                        NOCOPY_INPLACE_UNION(psi1, psi2);
-                       reduceMemoryFootprintPos(varphi[idx]);
-                       reduceMemoryFootprintNeg(varphi[idx]);
 
                        psi = psi1;
                }
@@ -1567,8 +1569,18 @@ private:
 
        void convertFormulaToCNFNegXOR(const ASTNode& varphi, BeevMgr::ClauseList* defs)
        {
+               ASTVec::const_iterator it = varphi.GetChildren().begin();
+               for (; it != varphi.GetChildren().end(); it++)
+    {
+                 convertFormulaToCNF(*it, defs); // make pos and neg clause sets
+    }
                BeevMgr::ClauseList* psi = convertFormulaToCNFNegXORAux(varphi, 0, defs);
                info[varphi]->clausesneg = psi;
+               ASTVec::const_iterator it2 = varphi.GetChildren().begin();
+               for (; it2 != varphi.GetChildren().end(); it2++){
+                 reduceMemoryFootprintPos(*it2);
+                 reduceMemoryFootprintNeg(*it2);
+    }
        }
 
        BeevMgr::ClauseList* convertFormulaToCNFNegXORAux(const ASTNode& varphi, unsigned int idx, BeevMgr::ClauseList* defs)
@@ -1593,7 +1605,6 @@ private:
                        {
                                setDoSibRenamingPos(*info[varphi[idx + 1]]);
                        }
-                       convertFormulaToCNF(varphi[idx + 1], defs);
 
                        convertFormulaToCNF(varphi[idx], defs);
                        renamesibs = (info[varphi[idx]]->clausespos)->size() > 1 ? true : false;
@@ -1601,21 +1612,15 @@ private:
                        {
                                setDoSibRenamingNeg(*info[varphi[idx + 1]]);
                        }
-                       convertFormulaToCNF(varphi[idx + 1], defs);
 
                        psi1 = PRODUCT(*(info[varphi[idx]]->clausesneg), *(info[varphi[idx + 1]]->clausespos));
                        psi2 = PRODUCT(*(info[varphi[idx]]->clausespos), *(info[varphi[idx + 1]]->clausesneg));
                        NOCOPY_INPLACE_UNION(psi1, psi2);
-                       reduceMemoryFootprintNeg(varphi[idx]);
-                       reduceMemoryFootprintPos(varphi[idx + 1]);
-                       reduceMemoryFootprintPos(varphi[idx]);
-                       reduceMemoryFootprintNeg(varphi[idx + 1]);
 
                        psi = psi1;
                }
                else
                {
-
                        //****************************************
                        // (neg) XOR ~> UNION
                        //    (PRODUCT NOT   [idx] ; XOR      [idx+1..])
@@ -1637,15 +1642,12 @@ private:
                        {
                                setDoSibRenamingPos(*info[varphi[idx]]);
                        }
-                       convertFormulaToCNF(varphi[idx], defs);
 
                        psi1 = PRODUCT(*(info[varphi[idx]]->clausesneg), *theta1);
                        psi2 = PRODUCT(*(info[varphi[idx]]->clausespos), *theta2);
                        DELETE(theta1);
                        DELETE(theta2);
                        NOCOPY_INPLACE_UNION(psi1, psi2);
-                       reduceMemoryFootprintNeg(varphi[idx]);
-                       reduceMemoryFootprintPos(varphi[idx]);
 
                        psi = psi1;
                }