minor changes

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

diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp
index 7d9ff84727e4a7ff7dad7e4f0d0bddf422371fce..a3970035e05e085123905c5255999b4e4cbed960 100644 (file)
--- a/src/to-sat/CallSAT.cpp
+++ b/src/to-sat/CallSAT.cpp
@@ -84,15 +84,14 @@ namespace BEEV
     ClauseList* xorcl = cm->ReturnXorClauses();
 #endif
 
-    ClauseBuckets * cb = Sort_ClauseList_IntoBuckets(cl);
+    ClauseBuckets * cb = Sort_ClauseList_IntoBuckets(cl);    
+    bool sat = CallSAT_On_ClauseBuckets(SatSolver, cb);    
     //bool sat = toSATandSolve(SatSolver, *cl);
-    bool sat = CallSAT_On_ClauseBuckets(SatSolver, cb);
 
     for (ClauseBuckets::iterator it = cb->begin(); it != cb->end(); it++)
-       delete it->second;
+      delete it->second;
     delete cb;
 
-
     if(!sat)
       {
        return sat;

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index faead4353551d2faf696484d9bffc40c0511cf54..75f39604baed0c876b62cc177ede87cf1cc158c8 100644 (file)
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -1276,7 +1276,8 @@ namespace BEEV
                           ((*(info[*it]->clausespos))[0])->end());
       }
     doRenamingPosXor(varphi);
-    //doRenamingPos(varphi, defs);
+    //ClauseList* psi = convertFormulaToCNFPosXORAux(varphi, 0, defs);
+    //info[varphi]->clausespos = psi;    
     ASTNode varXorNode = GetNodeFrom_SINGLETON(info[varphi]->clausespos);
     ASTNode NotVarXorNode = bm->CreateNode(NOT, varXorNode);
     xor_clause->push_back(ASTNodeToASTNodePtr(NotVarXorNode));
@@ -1842,7 +1843,9 @@ namespace BEEV
     if (bm->UserFlags.stats_flag)
       {
         cerr << "Number of clauses:" << defs->size() << endl;
-        //PrintClauseList(cout, *defs);
+        PrintClauseList(cout, *defs);
+       cerr << "Number of xor-clauses:" << clausesxor->size() << endl;
+       PrintClauseList(cout, *clausesxor);
       }
 
     return defs;

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index a95f36ae5c9e0de7bd57fca8713b78d7763c7dee..949d0648bc619785f515e86bf663f92087ca208e 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -89,7 +89,8 @@ namespace BEEV
         //        }
 #ifdef CRYPTOMINISAT
        if(add_xor_clauses)
-         {
+         {         
+           //cout << "addXorClause:\n";
            newS.addXorClause(satSolverClause, false, 0, "z");
          }
        else