added xor clause adding to cryptominisat. still being debugged

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

diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp
index ef1a4f143eeda2152465fc9b798481b6d5b06f5a..01e4abe2ec291d1c166db492889a88194f222929 100644 (file)
--- a/src/to-sat/CallSAT.cpp
+++ b/src/to-sat/CallSAT.cpp
@@ -8,7 +8,7 @@
  ********************************************************************/
 
 #include "ToSAT.h"
-#define MAX_BUCKET_LIMIT 3
+#define MAX_BUCKET_LIMIT 2
 
 namespace BEEV
 {
@@ -79,9 +79,27 @@ namespace BEEV
 
     CNFMgr* cm = new CNFMgr(bm);
     ClauseList* cl = cm->convertToCNF(BBFormula);
+
+#ifdef CRYPTOMINISAT
+    ClauseList* xorcl = cm->ReturnXorClauses();
+#endif
+
     ClauseBuckets * cb = Sort_ClauseList_IntoBuckets(cl);
     //bool sat = toSATandSolve(SatSolver, *cl);
     bool sat = CallSAT_On_ClauseBuckets(SatSolver, cb);
+    if(!sat)
+      {
+       return sat;
+      }
+
+#ifdef CRYPTOMINISAT
+    if(!xorcl->empty())
+      {        
+       sat = toSATandSolve(SatSolver, *xorcl, true);
+      }
+    cm->DELETE(xorcl);
+#endif 
+
     cm->DELETE(cl);
     delete cm;
     return sat;

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index f46bb620a256ec82825571c6951739a91df902ef..9a3e156470e114c076793e8e344086b988594b2c 100644 (file)
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -1,6 +1,6 @@
 // -*- c++ -*-
 /********************************************************************
- * AUTHORS: Vijay Ganesh, Mike Katelman
+ * AUTHORS: Mike Katelman
  *
  * BEGIN DATE: November, 2005
  *
@@ -401,6 +401,13 @@ namespace BEEV
     return psi;
   } //End of SINGLETON()
 
+  static ASTNode GetNodeFrom_SINGLETON(ClauseList *cl)
+  {
+    ClausePtr c = (*cl)[0];
+    const ASTNode * a = (*c)[0];
+    return *a;
+  }
+
   ClauseList* CNFMgr::UNION(const ClauseList& varphi1, 
                             const ClauseList& varphi2)
   {    
@@ -775,6 +782,40 @@ namespace BEEV
     setWasRenamedPos(*x);
   }//End of doRenamingPos
   
+
+  void CNFMgr::doRenamingPosXor(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->clausespos = SINGLETON(psi);
+    setWasRenamedPos(*x);
+  }//End of doRenamingPos
+  
+
   void CNFMgr::doRenamingNeg(const ASTNode& varphi, ClauseList* defs)
   {
     CNFInfo* x = info[varphi];
@@ -1219,6 +1260,34 @@ namespace BEEV
   void CNFMgr::convertFormulaToCNFPosXOR(const ASTNode& varphi, 
                                          ClauseList* defs)
   {
+#ifdef CRYPTOMINISAT
+    ASTVec::const_iterator it = varphi.GetChildren().begin();
+    ClausePtr xor_clause = new vector<const ASTNode*>();
+
+    for (; it != varphi.GetChildren().end(); it++)
+      {
+        convertFormulaToCNF(*it, defs); // make pos and neg clause set
+
+       //Creating a new variable name for each of the children of the
+       //XOR node
+       doRenamingPos(*it, defs);
+       xor_clause->insert(xor_clause->end(), 
+                          ((*(info[*it]->clausespos))[0])->begin(),
+                          ((*(info[*it]->clausespos))[0])->end());
+      }
+    doRenamingPosXor(varphi);
+    //doRenamingPos(varphi, defs);
+    ASTNode varXorNode = GetNodeFrom_SINGLETON(info[varphi]->clausespos);
+    ASTNode NotVarXorNode = bm->CreateNode(NOT, varXorNode);
+    xor_clause->push_back(ASTNodeToASTNodePtr(NotVarXorNode));
+    clausesxor->push_back(xor_clause);
+
+    ASTVec::const_iterator it2 = varphi.GetChildren().begin();
+    for (; it2 != varphi.GetChildren().end(); it2++){
+      reduceMemoryFootprintPos(*it2);
+      reduceMemoryFootprintNeg(*it2);
+    }
+#else
     ASTVec::const_iterator it = varphi.GetChildren().begin();
     for (; it != varphi.GetChildren().end(); it++)
       {
@@ -1231,13 +1300,13 @@ namespace BEEV
       reduceMemoryFootprintPos(*it2);
       reduceMemoryFootprintNeg(*it2);
     }
+#endif
   } //End of convertFormulaToCNFPosXOR()
 
   ClauseList* CNFMgr::convertFormulaToCNFPosXORAux(const ASTNode& varphi, 
                                                    unsigned int idx, 
                                                    ClauseList* defs)
   {
-
     bool renamesibs;
     ClauseList* psi;
     ClauseList* psi1;
@@ -1246,8 +1315,8 @@ namespace BEEV
     if (idx == varphi.GetChildren().size() - 2)
       {
         //****************************************
-        // (pos) XOR ~> UNION
-        //    (PRODUCT       [idx]   ;     [idx+1])
+        // (pos) XOR ~> UNION (AND)
+        //    (PRODUCT  (OR) [idx]   ;     [idx+1])
         //  ; (PRODUCT NOT   [idx]   ; NOT [idx+1])
         //****************************************
         renamesibs = 
@@ -1738,6 +1807,7 @@ namespace BEEV
   CNFMgr::CNFMgr(STPMgr *bmgr)
   {
     bm = bmgr;
+    clausesxor = new ClauseList();
   }
 
   //########################################
@@ -1749,8 +1819,10 @@ namespace BEEV
     for (; it1 != store.end(); it1++)
       {
         delete it1->second;
-      }    
-    store.clear();    
+      }
+    store.clear();
+    
+    //FIXME: Delete clausesxor
   }
 
   //########################################
@@ -1778,6 +1850,12 @@ namespace BEEV
     return defs;
   }//End of convertToCNF()
 
+  //All XOR clauses are stored here. Return it after CNF translation
+  ClauseList* CNFMgr::ReturnXorClauses(void)
+  {
+    return clausesxor;
+  }
+
   void CNFMgr::DELETE(ClauseList* varphi)
   {
     ClauseList::const_iterator it = varphi->begin();

diff --git a/src/to-sat/ToCNF.h b/src/to-sat/ToCNF.h
index f50e90e8352efce1158853afa5ccf459558f885c..b4c7bff16b964497630b6561fd453a87666b45d8 100644 (file)
--- a/src/to-sat/ToCNF.h
+++ b/src/to-sat/ToCNF.h
@@ -37,6 +37,9 @@ namespace BEEV
       };
     } CNFInfo;
 
+    //Collect all XOR Clauses here
+    ClauseList* clausesxor;
+
     typedef HASHMAP<
       ASTNode, 
       CNFInfo*, 
@@ -163,6 +166,8 @@ namespace BEEV
 
     void doRenamingPos(const ASTNode& varphi, ClauseList* defs);    
 
+    void doRenamingPosXor(const ASTNode& varphi);    
+
     void doRenamingNeg(const ASTNode& varphi, ClauseList* defs);    
 
     //########################################
@@ -246,6 +251,8 @@ namespace BEEV
 
     ClauseList* convertToCNF(const ASTNode& varphi);    
 
+    ClauseList* ReturnXorClauses(void);
+
     void DELETE(ClauseList* varphi);
 
     void PrintClauseList(ostream& os, ClauseList& cll);

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 0ab7c1e0d503282d402b6ab7fa377af269d1272b..a95f36ae5c9e0de7bd57fca8713b78d7763c7dee 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -43,7 +43,8 @@ namespace BEEV
    * and calls solve(). If solve returns unsat, then stop and return
    * unsat. else continue.
    */
-  bool ToSAT::toSATandSolve(MINISAT::Solver& newS, ClauseList& cll)
+  bool ToSAT::toSATandSolve(MINISAT::Solver& newS,
+                           ClauseList& cll, bool add_xor_clauses)
   {
     CountersAndStats("SAT Solver", bm);
     bm->GetRunTimes()->start(RunTimes::SendingToSAT);
@@ -87,11 +88,18 @@ namespace BEEV
         //          continue;
         //        }
 #ifdef CRYPTOMINISAT
-        newS.addClause(satSolverClause,0,"z");
+       if(add_xor_clauses)
+         {
+           newS.addXorClause(satSolverClause, false, 0, "z");
+         }
+       else 
+         {
+           newS.addClause(satSolverClause,0,"z");
+         }
 #else
         newS.addClause(satSolverClause);
 #endif
-        float percentage=0.6;
+        float percentage=CLAUSAL_ABSTRACTION_CUTOFF;
         if(count++ >= input_clauselist_size*percentage)
           {
             //Arbitrary adding only 60% of the clauses in the hopes of

diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h
index b74d8de0382a7fec5c4d1d3000d131bcfa49c818..4e10b6af198ef3ade618c8512ee35950fb44f569 100644 (file)
--- a/src/to-sat/ToSAT.h
+++ b/src/to-sat/ToSAT.h
@@ -23,6 +23,8 @@
 
 namespace BEEV
 {
+  #define CLAUSAL_ABSTRACTION_CUTOFF 0.6
+
   class ToSAT {
   private:
     /****************************************************************
@@ -109,7 +111,8 @@ namespace BEEV
                                  ClauseBuckets * cb);
     
     // Converts the clause to SAT and calls SAT solver
-    bool toSATandSolve(MINISAT::Solver& S, ClauseList& cll);
+    bool toSATandSolve(MINISAT::Solver& S,
+                      ClauseList& cll, bool add_xor_clauses=false);
     
     // Calls SAT simplifier, array transformer (abstraction
     // refinement), bitvector solver, and SAT solver. Returns the