Added libs/minisat (copy of minisat git master)

1 files changed, 171 insertions, 0 deletions

diff --git a/libs/minisat/System.cc b/libs/minisat/System.cc
new file mode 100644
index 00000000..01d0dfe1
--- /dev/null
+++ b/libs/minisat/System.cc
@@ -0,0 +1,171 @@
+#define __STDC_FORMAT_MACROS
+#define __STDC_LIMIT_MACROS
+/***************************************************************************************[System.cc]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#include <signal.h>
+#include <stdio.h>
+
+#include "libs/minisat/System.h"
+
+#if defined(__linux__)
+
+#include <stdlib.h>
+
+using namespace Minisat;
+
+static inline int memReadStat(int field)
+{
+    char  name[256];
+    pid_t pid = getpid();
+    int   value;
+
+    sprintf(name, "/proc/%d/statm", pid);
+    FILE* in = fopen(name, "rb");
+    if (in == NULL) return 0;
+
+    for (; field >= 0; field--)
+        if (fscanf(in, "%d", &value) != 1)
+            printf("ERROR! Failed to parse memory statistics from \"/proc\".\n"), exit(1);
+    fclose(in);
+    return value;
+}
+
+
+static inline int memReadPeak(void)
+{
+    char  name[256];
+    pid_t pid = getpid();
+
+    sprintf(name, "/proc/%d/status", pid);
+    FILE* in = fopen(name, "rb");
+    if (in == NULL) return 0;
+
+    // Find the correct line, beginning with "VmPeak:":
+    int peak_kb = 0;
+    while (!feof(in) && fscanf(in, "VmPeak: %d kB", &peak_kb) != 1)
+        while (!feof(in) && fgetc(in) != '\n')
+            ;
+    fclose(in);
+
+    return peak_kb;
+}
+
+double Minisat::memUsed() { return (double)memReadStat(0) * (double)getpagesize() / (1024*1024); }
+double Minisat::memUsedPeak(bool strictlyPeak) { 
+    double peak = memReadPeak() / (double)1024;
+    return peak == 0 && !strictlyPeak ? memUsed() : peak; }
+
+#elif defined(__FreeBSD__) || defined(__FreeBSD_kernel__) || defined(__gnu_hurd__)
+
+double Minisat::memUsed() {
+    struct rusage ru;
+    getrusage(RUSAGE_SELF, &ru);
+    return (double)ru.ru_maxrss / 1024; }
+double Minisat::memUsedPeak() { return memUsed(); }
+
+
+#elif defined(__APPLE__)
+#include <malloc/malloc.h>
+
+double Minisat::memUsed() {
+    malloc_statistics_t t;
+    malloc_zone_statistics(NULL, &t);
+    return (double)t.max_size_in_use / (1024*1024); }
+double Minisat::memUsedPeak() { return memUsed(); }
+
+#else
+double Minisat::memUsed()     { return 0; }
+double Minisat::memUsedPeak() { return 0; }
+#endif
+
+
+void Minisat::setX86FPUPrecision()
+{
+#if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE) && defined(_FPU_GETCW)
+    // Only correct FPU precision on Linux architectures that needs and supports it:
+    fpu_control_t oldcw, newcw;
+    _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
+    printf("WARNING: for repeatability, setting FPU to use double precision\n");
+#endif
+}
+
+
+#if !defined(_MSC_VER) && !defined(__MINGW32__)
+void Minisat::limitMemory(uint64_t max_mem_mb)
+{
+// FIXME: OpenBSD does not support RLIMIT_AS. Not sure how well RLIMIT_DATA works instead.
+#if defined(__OpenBSD__)
+#define RLIMIT_AS RLIMIT_DATA
+#endif
+
+    // Set limit on virtual memory:
+    if (max_mem_mb != 0){
+        rlim_t new_mem_lim = (rlim_t)max_mem_mb * 1024*1024;
+        rlimit rl;
+        getrlimit(RLIMIT_AS, &rl);
+        if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){
+            rl.rlim_cur = new_mem_lim;
+            if (setrlimit(RLIMIT_AS, &rl) == -1)
+                printf("WARNING! Could not set resource limit: Virtual memory.\n");
+        }
+    }
+
+#if defined(__OpenBSD__)
+#undef RLIMIT_AS
+#endif
+}
+#else
+void Minisat::limitMemory(uint64_t /*max_mem_mb*/)
+{
+    printf("WARNING! Memory limit not supported on this architecture.\n");
+}
+#endif
+
+
+#if !defined(_MSC_VER) && !defined(__MINGW32__)
+void Minisat::limitTime(uint32_t max_cpu_time)
+{
+    if (max_cpu_time != 0){
+        rlimit rl;
+        getrlimit(RLIMIT_CPU, &rl);
+        if (rl.rlim_max == RLIM_INFINITY || (rlim_t)max_cpu_time < rl.rlim_max){
+            rl.rlim_cur = max_cpu_time;
+            if (setrlimit(RLIMIT_CPU, &rl) == -1)
+                printf("WARNING! Could not set resource limit: CPU-time.\n");
+        }
+    }
+}
+#else
+void Minisat::limitTime(uint32_t /*max_cpu_time*/)
+{
+    printf("WARNING! CPU-time limit not supported on this architecture.\n");
+}
+#endif
+
+
+void Minisat::sigTerm(void handler(int))
+{
+    signal(SIGINT, handler);
+    signal(SIGTERM,handler);
+#ifdef SIGXCPU
+    signal(SIGXCPU,handler);
+#endif
+}