IMPORTANT:

STP appears to be failing about half of the regressions in stp-tests/test. I
have just noticed this an made no attempt to fix it. I suspect it is due to
recent changes, as my personal branch 02_07_2009 does not have the same
problem.

OTHER:

I fixed a CNF conversion memory bug. IMPLIES and ITE cases were not setting the
sibling rename flag correctly, well, at all.

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

diff --git a/AST/ToCNF.cpp b/AST/ToCNF.cpp
index 59d2d21bd8ceb1df15cff1100275b4f16e5dcaef..d66a7d0a4ab03431bbb82d7b260feba1a5bebbf1 100644 (file)
--- a/AST/ToCNF.cpp
+++ b/AST/ToCNF.cpp
@@ -1061,6 +1061,9 @@ private:
       CNFInfo* x0 = info[varphi[0]];
       CNFInfo* x1 = info[varphi[1]];
       convertFormulaToCNF(varphi[0], defs);
+      if(x0->clausesneg->size() > 1){
+         setDoSibRenamingPos(*x1);
+      }
       convertFormulaToCNF(varphi[1], defs);
       BeevMgr::ClauseList* psi = 
          PRODUCT(*(x0->clausesneg), *(x1->clausespos));
@@ -1078,7 +1081,13 @@ private:
       CNFInfo* x1 = info[varphi[1]];
       CNFInfo* x2 = info[varphi[2]];
       convertFormulaToCNF(varphi[0], defs);
+      if(x0->clausesneg->size() > 1){
+         setDoSibRenamingPos(*x1);
+      }
       convertFormulaToCNF(varphi[1], defs);
+      if(x0->clausespos->size() > 1){
+         setDoSibRenamingPos(*x2);
+      }
       convertFormulaToCNF(varphi[2], defs);
       BeevMgr::ClauseList* psi1 = PRODUCT(*(x0->clausesneg)
          , *(x1->clausespos));
@@ -1335,7 +1344,13 @@ private:
       CNFInfo* x1 = info[varphi[1]];
       CNFInfo* x2 = info[varphi[2]];
       convertFormulaToCNF(varphi[0], defs);
+      if(x0->clausesneg->size() > 1){
+         setDoSibRenamingNeg(*x1);
+      }
       convertFormulaToCNF(varphi[1], defs);
+      if(x0->clausespos->size() > 1){
+         setDoSibRenamingNeg(*x2);
+      }
       convertFormulaToCNF(varphi[2], defs);
       BeevMgr::ClauseList* psi1 = PRODUCT(*(x0->clausesneg)
          , *(x1->clausesneg));