Merge branch 'cryptominisat1_removed_and_rest_cleaned'

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

diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp
index 4e89eb3285f96ea8cef698a47d540abd4e4117c5..3f9ac522b9deb55605aec7b2ba04a8a50e47d73b 100644 (file)
--- a/src/STPManager/STPManager.cpp
+++ b/src/STPManager/STPManager.cpp
@@ -602,20 +602,17 @@ namespace BEEV
   {
     if (!UserFlags.stats_flag)
       return;
-#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2
-#else
     double cpu_time = MINISAT::cpuTime();
     uint64_t mem_used = MINISAT::memUsed();
-    reportf("restarts              : %"PRIu64"\n",                      s.starts);
-    reportf("conflicts             : %"PRIu64"   (%.0f /sec)\n",        s.conflicts   , s.conflicts   /cpu_time);
-    reportf("decisions             : %"PRIu64"   (%.0f /sec)\n",        s.decisions   , s.decisions   /cpu_time);
-    reportf("propagations          : %"PRIu64"   (%.0f /sec)\n",        s.propagations, s.propagations/cpu_time);
-    reportf("conflict literals     : %"PRIu64"   (%4.2f %% deleted)\n", s.tot_literals,
+    printf("restarts              : %"PRIu64"\n",                      s.starts);
+    printf("conflicts             : %"PRIu64"   (%.0f /sec)\n",        s.conflicts   , s.conflicts   /cpu_time);
+    printf("decisions             : %"PRIu64"   (%.0f /sec)\n",        s.decisions   , s.decisions   /cpu_time);
+    printf("propagations          : %"PRIu64"   (%.0f /sec)\n",        s.propagations, s.propagations/cpu_time);
+    printf("conflict literals     : %"PRIu64"   (%4.2f %% deleted)\n", s.tot_literals,
             (s.max_literals - s.tot_literals)*100 / (double)s.max_literals);
     if (mem_used != 0)
-      reportf("Memory used           : %.2f MB\n", mem_used / 1048576.0);
-    reportf("CPU time              : %g s\n", cpu_time);
-#endif
+        printf("Memory used           : %.2f MB\n", mem_used / 1048576.0);
+    printf("CPU time              : %g s\n", cpu_time);
   } //end of PrintStats()
 
 

diff --git a/src/main/Globals.h b/src/main/Globals.h
index c72bb627b2a7a211727b347ea16c9904fba22474..1a78af388e20b9dd73a78155144e228abdad6cee 100644 (file)
--- a/src/main/Globals.h
+++ b/src/main/Globals.h
@@ -23,10 +23,6 @@
 namespace MINISAT
 {
   class Solver;
-#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2
-#else
-  typedef int Var;
-#endif
 }
 
 namespace BEEV

diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h
index 6c0ab67463446b5b755cf8d6a21b62748849d27d..be234d459dca0fb0fa84cd63b37f1874a61537ab 100644 (file)
--- a/src/sat/cryptominisat2/Solver.h
+++ b/src/sat/cryptominisat2/Solver.h
@@ -25,12 +25,14 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <cstdio>
 #include <string.h>
 #include <stdio.h>
+
 #ifdef _MSC_VER
 #include <msvc/stdint.h>
 #else
 #include <stdint.h>
 #endif //_MSC_VER
 
+#include "time_mem.h"
 #include "Vec.h"
 #include "Heap.h"
 #include "Alg.h"

diff --git a/src/sat/cryptominisat2/time_mem.h b/src/sat/cryptominisat2/time_mem.h
index c76b445f1f7083babda59ccbd46fce87bfb29156..f923c9a072a0fd1a9ceee869af190390724d6ba4 100644 (file)
--- a/src/sat/cryptominisat2/time_mem.h
+++ b/src/sat/cryptominisat2/time_mem.h
@@ -22,40 +22,31 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #define TIME_MEM_H
 
 #ifdef _MSC_VER
-#include <msvc/stdint.h>
+  #include <ctime>
+  #include <msvc/stdint.h>
 #else
-#include <stdint.h>
-#endif //_MSC_VER
-
-#ifdef _MSC_VER
-#include <ctime>
+  #include <sys/time.h>
+  #include <sys/resource.h>
+  #include <unistd.h>
+  #include <stdint.h>
+#endif
 
-static inline double cpuTime(void)
+namespace MINISAT
 {
-    return (double)clock() / CLOCKS_PER_SEC;
-}
-#else //_MSC_VER
-#ifdef CROSS_COMPILE
-#include <ctime>
+using namespace MINISAT;
 
-static inline double cpuTime(void)
-{
-    return (double)clock() / CLOCKS_PER_SEC;
-}
-#else //CROSS_COMPILE
-#include <sys/time.h>
-#include <sys/resource.h>
-#include <unistd.h>
+/*************************************************************************************/
+#ifdef _MSC_VER
 
-static inline double cpuTime(void)
-{
+static inline double cpuTime(void) {
+    return (double)clock() / CLOCKS_PER_SEC; }
+#else
+
+static inline double cpuTime(void) {
     struct rusage ru;
     getrusage(RUSAGE_SELF, &ru);
-    return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000;
-}
-#endif //CROSS_COMPILE
-#endif //_MSC_VER
-
+    return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
+#endif
 
 #if defined(__linux__)
 static inline int memReadStat(int field)
@@ -71,26 +62,24 @@ static inline int memReadStat(int field)
     fclose(in);
     return value;
 }
-static inline uint64_t memUsed()
-{
-    return (uint64_t)memReadStat(0) * (uint64_t)getpagesize();
-}
+static inline uint64_t memUsed() { return (uint64_t)memReadStat(0) * (uint64_t)getpagesize(); }
 
 
 #elif defined(__FreeBSD__)
-static inline uint64_t memUsed(void)
-{
+static inline uint64_t memUsed(void) {
     struct rusage ru;
     getrusage(RUSAGE_SELF, &ru);
-    return ru.ru_maxrss*1024;
-}
+    return ru.ru_maxrss*1024; }
 
 
 #else
-static inline uint64_t memUsed()
-{
-    return 0;
-}
+static inline uint64_t memUsed() { return 0; }
 #endif
 
+#if defined(__linux__)
+#include <fpu_control.h>
+#endif
+
+};
+
 #endif //TIME_MEM_H

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index d20df58a58277f4bcdd48e5eebd6d9a9a0a7bfc8..70e68f626b464c8e0268ff8f33cd33d5cb2edd3d 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -87,16 +87,9 @@ namespace BEEV
       {
 #ifdef CRYPTOMINISAT2
        newSolver.setSeed(bm->UserFlags.random_seed);
-       //newSolver.greedyUnbound = true;
-       //      cerr << "We have set the seed value to "
-       //           << bm->UserFlags.random_seed 
-       //           << endl;
 #endif
       }
 
-#ifdef CRYPTOMINISAT
-    newSolver.startClauseAdding();
-#endif
     //iterate through the list (conjunction) of ASTclauses cll
     ClauseList::const_iterator i = cll.begin(), iend = cll.end();    
     for (int count=0, flag=0; i != iend; i++)
@@ -127,13 +120,12 @@ namespace BEEV
         //        }
 #if defined CRYPTOMINISAT || defined CRYPTOMINISAT2
         if(add_xor_clauses)
-          {         
-            //cout << "addXorClause:\n";
-            newSolver.addXorClause(satSolverClause, false, 0, (char*)"z");
+          {
+            newSolver.addXorClause(satSolverClause, false);
           }
         else 
           {
-            newSolver.addClause(satSolverClause,0,(char*)"z");
+            newSolver.addClause(satSolverClause);
           }
 #else
         newSolver.addClause(satSolverClause);