From bdb2be3c561a0ffc57adfd7e726e3f4f7ed11b6f Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 18 Nov 2009 21:18:56 +0000
Subject: [PATCH] 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
---
 src/STPManager/STP.cpp |  3 +-
 src/to-sat/ToCNF.cpp   | 78 ++++++++++++++++++++++--------------------
 2 files changed, 41 insertions(+), 40 deletions(-)

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index a6a4265..0fadf1b 100644
--- 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 4916b0c..b41d714 100644
--- 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);
-- 
2.47.3