From deb3e8ba7c77d02e7c47f7df7b879bba73009f27 Mon Sep 17 00:00:00 2001 From: msoos Date: Fri, 16 Apr 2010 14:51:57 +0000 Subject: [PATCH] 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 --- src/STPManager/STPManager.cpp | 17 ++++---- src/main/Globals.h | 4 -- src/sat/cryptominisat2/Solver.h | 2 + src/sat/cryptominisat2/time_mem.h | 67 +++++++++++++------------------ src/to-sat/ToSAT.cpp | 14 ++----- 5 files changed, 40 insertions(+), 64 deletions(-) diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp index 4e89eb3..3f9ac52 100644 --- 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 c72bb62..1a78af3 100644 --- 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 6c0ab67..be234d4 100644 --- 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 #include #include + #ifdef _MSC_VER #include #else #include #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 c76b445..f923c9a 100644 --- 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 + #include + #include #else -#include -#endif //_MSC_VER - -#ifdef _MSC_VER -#include + #include + #include + #include + #include +#endif -static inline double cpuTime(void) +namespace MINISAT { - return (double)clock() / CLOCKS_PER_SEC; -} -#else //_MSC_VER -#ifdef CROSS_COMPILE -#include +using namespace MINISAT; -static inline double cpuTime(void) -{ - return (double)clock() / CLOCKS_PER_SEC; -} -#else //CROSS_COMPILE -#include -#include -#include +/*************************************************************************************/ +#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 +#endif + +}; + #endif //TIME_MEM_H diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index d20df58..70e68f6 100644 --- 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); -- 2.47.3