added ability to generate xor-clauses with negation on top

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index a6a4265020b5d218bd9d8ad3ba7a3581ce91610a..0fadf1b37edb962101ed967f3115ff13c0943a49 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -19,7 +19,6 @@ namespace BEEV {
     ASTNode original_input = bm->CreateNode(AND, 
                                            inputasserts, 
                                            bm->CreateNode(NOT, query));
-    ASTNode modified_input = original_input;
     
     //solver instantiated here
 #ifdef CORE
@@ -43,7 +42,7 @@ namespace BEEV {
     else 
       {
        return TopLevelSTPAux(NewSolver, 
-                             modified_input, original_input);
+                             original_input, original_input);
       }
   } //End of TopLevelSTP()
   

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 4916b0cd93621eb02621113262246a55defa8920..b41d714b78f82eef89f41997d24284cf56a66518 100644 (file)
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -837,42 +837,43 @@ namespace BEEV
     //########################################
     
     x->clausespos = SINGLETON(psi);
-    //x->clausesneg = SINGLETON(psi);
+    x->clausesneg = SINGLETON(bm->CreateNode(NOT, psi));
     setWasRenamedPos(*x);
   }//End of doRenamingPos
   
-  void CNFMgr::doRenamingNegXor(const ASTNode& varphi)
-  {
-    CNFInfo* x = info[varphi];
-
-    //########################################
-    // step 1, calc new variable
-    //########################################
-    
-    ostringstream oss;
-    oss << "cnf" << "{" << varphi.GetNodeNum() << "}";
-    ASTNode psi = bm->CreateSymbol(oss.str().c_str());
-    
-    //########################################
-    // step 2, add defs
-    //########################################
-    
-    //     ClauseList* cl1;
-    //     cl1 = SINGLETON(bm->CreateNode(NOT, psi));
-    //     ClauseList* cl2 = PRODUCT(*(info[varphi]->clausespos), *cl1);
-    //     defs->insert(defs->end(), cl2->begin(), cl2->end());
-    //     DELETE(info[varphi]->clausespos);
-    //     DELETE(cl1);
-    //     delete cl2;
-    
-    //########################################
-    // step 3, update info[varphi]
-    //########################################
-    
-    //x->clausesneg = SINGLETON(bm->CreateNode(NOT,psi));
-    x->clausespos = SINGLETON(bm->CreateNode(NOT,psi));
-    setWasRenamedPos(*x);
-  }//End of doRenamingPos
+//   void CNFMgr::doRenamingNegXor(const ASTNode& varphi)
+//   {
+//     CNFInfo* x = info[varphi];
+
+//     //########################################
+//     // step 1, calc new variable
+//     //########################################
+    
+//     ostringstream oss;
+//     oss << "cnf" << "{" << varphi.GetNodeNum() << "}";
+//     ASTNode psi = bm->CreateSymbol(oss.str().c_str());
+    
+//     //########################################
+//     // step 2, add defs
+//     //########################################
+    
+//     //     ClauseList* cl1;
+//     //     cl1 = SINGLETON(bm->CreateNode(NOT, psi));
+//     //     ClauseList* cl2 = PRODUCT(*(info[varphi]->clausespos), *cl1);
+//     //     defs->insert(defs->end(), cl2->begin(), cl2->end());
+//     //     DELETE(info[varphi]->clausespos);
+//     //     DELETE(cl1);
+//     //     delete cl2;
+    
+//     //########################################
+//     // step 3, update info[varphi]
+//     //########################################
+    
+//     //x->clausesneg = SINGLETON(bm->CreateNode(NOT,psi));
+//     x->clausespos = SINGLETON(bm->CreateNode(NOT,psi));
+
+//     setWasRenamedPos(*x);
+//   }//End of doRenamingPos
   
   void CNFMgr::doRenamingNeg(const ASTNode& varphi, ClauseList* defs)
   {
@@ -1681,8 +1682,8 @@ namespace BEEV
   void CNFMgr::convertFormulaToCNFNegXOR(const ASTNode& varphi,
                                          ClauseList* defs)
   {
-#ifdef FALSE
-    //#ifdef CRYPTOMINISAT
+    //#ifdef FALSE
+#ifdef CRYPTOMINISAT
     CNFInfo * xx = info[varphi];
     if(NULL != xx
        && sharesPos(*xx) > 0
@@ -1700,15 +1701,16 @@ 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());
       }
-    doRenamingNegXor(varphi);
+    doRenamingPosXor(varphi);
     //ClauseList* psi = convertFormulaToCNFPosXORAux(varphi, 0, defs);
-    //info[varphi]->clausespos = psi;    
-    ASTNode varXorNode = GetNodeFrom_SINGLETON(info[varphi]->clausesneg);
+    //info[varphi]->clausespos = psi;
+    ASTNode varXorNode = GetNodeFrom_SINGLETON(info[varphi]->clausespos);
     ASTNode NotVarXorNode = bm->CreateNode(NOT, varXorNode);
     xor_clause->push_back(ASTNodeToASTNodePtr(NotVarXorNode));
     clausesxor->push_back(xor_clause);