--- /dev/null
+Release Notes for MiniSat 2.2.0
+===============================
+
+Changes since version 2.0:
+
+ * Started using a more standard release numbering.
+
+ * Includes some now well-known heuristics: phase-saving and luby
+ restarts. The old heuristics are still present and can be activated
+ if needed.
+
+ * Detection/Handling of out-of-memory and vector capacity
+ overflow. This is fairly new and relatively untested.
+
+ * Simple resource controls: CPU-time, memory, number of
+ conflicts/decisions.
+
+ * CPU-time limiting is implemented by a more general, but simple,
+ asynchronous interruption feature. This means that the solving
+ procedure can be interrupted from another thread or in a signal
+ handler.
+
+ * Improved portability with respect to building on Solaris and with
+ Visual Studio. This is not regularly tested and chances are that
+ this have been broken since, but should be fairly easy to fix if
+ so.
+
+ * Changed C++ file-extention to the less problematic ".cc".
+
+ * Source code is now namespace-protected
+
+ * Introducing a new Clause Memory Allocator that brings reduced
+ memory consumption on 64-bit architechtures and improved
+ performance (to some extent). The allocator uses a region-based
+ approach were all references to clauses are represented as a 32-bit
+ index into a global memory region that contains all clauses. To
+ free up and compact memory it uses a simple copying garbage
+ collector.
+
+ * Improved unit-propagation by Blocking Literals. For each entry in
+ the watcher lists, pair the pointer to a clause with some
+ (arbitrary) literal from the clause. The idea is that if the
+ literal is currently true (i.e. the clause is satisfied) the
+ watchers of the clause does not need to be altered. This can thus
+ be detected without touching the clause's memory at all. As often
+ as can be done cheaply, the blocking literal for entries to the
+ watcher list of a literal 'p' is set to the other literal watched
+ in the corresponding clause.
+
+ * Basic command-line/option handling system. Makes it easy to specify
+ options in the class that they affect, and whenever that class is
+ used in an executable, parsing of options and help messages are
+ brought in automatically.
+
+ * General clean-up and various minor bug-fixes.
+
+ * Changed implementation of variable-elimination/model-extension:
+
+ - The interface is changed so that arbitrary remembering is no longer
+ possible. If you need to mention some variable again in the future,
+ this variable has to be frozen.
+
+ - When eliminating a variable, only clauses that contain the variable
+ with one sign is necessary to store. Thereby making the other sign
+ a "default" value when extending models.
+
+ - The memory consumption for eliminated clauses is further improved
+ by storing all eliminated clauses in a single contiguous vector.
+
+ * Some common utility code (I/O, Parsing, CPU-time, etc) is ripped
+ out and placed in a separate "utils" directory.
+
+ * The DIMACS parse is refactored so that it can be reused in other
+ applications (not very elegant, but at least possible).
+
+ * Some simple improvements to scalability of preprocessing, using
+ more lazy clause removal from data-structures and a couple of
+ ad-hoc limits (the longest clause that can be produced in variable
+ elimination, and the longest clause used in backward subsumption).
--- /dev/null
+EXEC = system_test
+DEPDIR = mtl
+
+include $(MROOT)/mtl/template.mk
--- /dev/null
+/**************************************************************************************[Options.cc]
+Copyright (c) 2008-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 "mtl/Sort.h"
+#include "utils/Options.h"
+#include "utils/ParseUtils.h"
+
+using namespace Minisat;
+
+void Minisat::parseOptions(int& argc, char** argv, bool strict)
+{
+ int i, j;
+ for (i = j = 1; i < argc; i++){
+ const char* str = argv[i];
+ if (match(str, "--") && match(str, Option::getHelpPrefixString()) && match(str, "help")){
+ if (*str == '\0')
+ printUsageAndExit(argc, argv);
+ else if (match(str, "-verb"))
+ printUsageAndExit(argc, argv, true);
+ } else {
+ bool parsed_ok = false;
+
+ for (int k = 0; !parsed_ok && k < Option::getOptionList().size(); k++){
+ parsed_ok = Option::getOptionList()[k]->parse(argv[i]);
+
+ // fprintf(stderr, "checking %d: %s against flag <%s> (%s)\n", i, argv[i], Option::getOptionList()[k]->name, parsed_ok ? "ok" : "skip");
+ }
+
+ if (!parsed_ok)
+ if (strict && match(argv[i], "-"))
+ fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()), exit(1);
+ else
+ argv[j++] = argv[i];
+ }
+ }
+
+ argc -= (i - j);
+}
+
+
+void Minisat::setUsageHelp (const char* str){ Option::getUsageString() = str; }
+void Minisat::setHelpPrefixStr (const char* str){ Option::getHelpPrefixString() = str; }
+void Minisat::printUsageAndExit (int argc, char** argv, bool verbose)
+{
+ const char* usage = Option::getUsageString();
+ if (usage != NULL)
+ fprintf(stderr, usage, argv[0]);
+
+ sort(Option::getOptionList(), Option::OptionLt());
+
+ const char* prev_cat = NULL;
+ const char* prev_type = NULL;
+
+ for (int i = 0; i < Option::getOptionList().size(); i++){
+ const char* cat = Option::getOptionList()[i]->category;
+ const char* type = Option::getOptionList()[i]->type_name;
+
+ if (cat != prev_cat)
+ fprintf(stderr, "\n%s OPTIONS:\n\n", cat);
+ else if (type != prev_type)
+ fprintf(stderr, "\n");
+
+ Option::getOptionList()[i]->help(verbose);
+
+ prev_cat = Option::getOptionList()[i]->category;
+ prev_type = Option::getOptionList()[i]->type_name;
+ }
+
+ fprintf(stderr, "\nHELP OPTIONS:\n\n");
+ fprintf(stderr, " --%shelp Print help message.\n", Option::getHelpPrefixString());
+ fprintf(stderr, " --%shelp-verb Print verbose help message.\n", Option::getHelpPrefixString());
+ fprintf(stderr, "\n");
+ exit(0);
+}
+
--- /dev/null
+/***************************************************************************************[Options.h]
+Copyright (c) 2008-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.
+**************************************************************************************************/
+
+#ifndef Minisat_Options_h
+#define Minisat_Options_h
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <math.h>
+#include <string.h>
+
+#include "../mtl/IntTypes.h"
+#include "../mtl/Vec.h"
+#include "../utils/ParseUtils.h"
+
+namespace Minisat {
+
+//==================================================================================================
+// Top-level option parse/help functions:
+
+
+extern void parseOptions (int& argc, char** argv, bool strict = false);
+extern void printUsageAndExit(int argc, char** argv, bool verbose = false);
+extern void setUsageHelp (const char* str);
+extern void setHelpPrefixStr (const char* str);
+
+
+//==================================================================================================
+// Options is an abstract class that gives the interface for all types options:
+
+
+class Option
+{
+ protected:
+ const char* name;
+ const char* description;
+ const char* category;
+ const char* type_name;
+
+ static vec<Option*>& getOptionList () { static vec<Option*> options; return options; }
+ static const char*& getUsageString() { static const char* usage_str; return usage_str; }
+ static const char*& getHelpPrefixString() { static const char* help_prefix_str = ""; return help_prefix_str; }
+
+ struct OptionLt {
+ bool operator()(const Option* x, const Option* y) {
+ int test1 = strcmp(x->category, y->category);
+ return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0;
+ }
+ };
+
+ Option(const char* name_,
+ const char* desc_,
+ const char* cate_,
+ const char* type_) :
+ name (name_)
+ , description(desc_)
+ , category (cate_)
+ , type_name (type_)
+ {
+ getOptionList().push(this);
+ }
+
+ public:
+ virtual ~Option() {}
+
+ virtual bool parse (const char* str) = 0;
+ virtual void help (bool verbose = false) = 0;
+
+ friend void parseOptions (int& argc, char** argv, bool strict);
+ friend void printUsageAndExit (int argc, char** argv, bool verbose);
+ friend void setUsageHelp (const char* str);
+ friend void setHelpPrefixStr (const char* str);
+};
+
+
+//==================================================================================================
+// Range classes with specialization for floating types:
+
+
+struct IntRange {
+ int begin;
+ int end;
+ IntRange(int b, int e) : begin(b), end(e) {}
+};
+
+struct Int64Range {
+ int64_t begin;
+ int64_t end;
+ Int64Range(int64_t b, int64_t e) : begin(b), end(e) {}
+};
+
+struct DoubleRange {
+ double begin;
+ double end;
+ bool begin_inclusive;
+ bool end_inclusive;
+ DoubleRange(double b, bool binc, double e, bool einc) : begin(b), end(e), begin_inclusive(binc), end_inclusive(einc) {}
+};
+
+
+//==================================================================================================
+// Double options:
+
+
+class DoubleOption : public Option
+{
+ protected:
+ DoubleRange range;
+ double value;
+
+ public:
+ DoubleOption(const char* c, const char* n, const char* d, double def = double(), DoubleRange r = DoubleRange(-HUGE_VAL, false, HUGE_VAL, false))
+ : Option(n, d, c, "<double>"), range(r), value(def) {
+ // FIXME: set LC_NUMERIC to "C" to make sure that strtof/strtod parses decimal point correctly.
+ }
+
+ operator double (void) const { return value; }
+ operator double& (void) { return value; }
+ DoubleOption& operator=(double x) { value = x; return *this; }
+
+ virtual bool parse(const char* str){
+ const char* span = str;
+
+ if (!match(span, "-") || !match(span, name) || !match(span, "="))
+ return false;
+
+ char* end;
+ double tmp = strtod(span, &end);
+
+ if (end == NULL)
+ return false;
+ else if (tmp >= range.end && (!range.end_inclusive || tmp != range.end)){
+ fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
+ exit(1);
+ }else if (tmp <= range.begin && (!range.begin_inclusive || tmp != range.begin)){
+ fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
+ exit(1); }
+
+ value = tmp;
+ // fprintf(stderr, "READ VALUE: %g\n", value);
+
+ return true;
+ }
+
+ virtual void help (bool verbose = false){
+ fprintf(stderr, " -%-12s = %-8s %c%4.2g .. %4.2g%c (default: %g)\n",
+ name, type_name,
+ range.begin_inclusive ? '[' : '(',
+ range.begin,
+ range.end,
+ range.end_inclusive ? ']' : ')',
+ value);
+ if (verbose){
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
+ }
+};
+
+
+//==================================================================================================
+// Int options:
+
+
+class IntOption : public Option
+{
+ protected:
+ IntRange range;
+ int32_t value;
+
+ public:
+ IntOption(const char* c, const char* n, const char* d, int32_t def = int32_t(), IntRange r = IntRange(INT32_MIN, INT32_MAX))
+ : Option(n, d, c, "<int32>"), range(r), value(def) {}
+
+ operator int32_t (void) const { return value; }
+ operator int32_t& (void) { return value; }
+ IntOption& operator= (int32_t x) { value = x; return *this; }
+
+ virtual bool parse(const char* str){
+ const char* span = str;
+
+ if (!match(span, "-") || !match(span, name) || !match(span, "="))
+ return false;
+
+ char* end;
+ int32_t tmp = strtol(span, &end, 10);
+
+ if (end == NULL)
+ return false;
+ else if (tmp > range.end){
+ fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
+ exit(1);
+ }else if (tmp < range.begin){
+ fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
+ exit(1); }
+
+ value = tmp;
+
+ return true;
+ }
+
+ virtual void help (bool verbose = false){
+ fprintf(stderr, " -%-12s = %-8s [", name, type_name);
+ if (range.begin == INT32_MIN)
+ fprintf(stderr, "imin");
+ else
+ fprintf(stderr, "%4d", range.begin);
+
+ fprintf(stderr, " .. ");
+ if (range.end == INT32_MAX)
+ fprintf(stderr, "imax");
+ else
+ fprintf(stderr, "%4d", range.end);
+
+ fprintf(stderr, "] (default: %d)\n", value);
+ if (verbose){
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
+ }
+};
+
+
+// Leave this out for visual C++ until Microsoft implements C99 and gets support for strtoll.
+#ifndef _MSC_VER
+
+class Int64Option : public Option
+{
+ protected:
+ Int64Range range;
+ int64_t value;
+
+ public:
+ Int64Option(const char* c, const char* n, const char* d, int64_t def = int64_t(), Int64Range r = Int64Range(INT64_MIN, INT64_MAX))
+ : Option(n, d, c, "<int64>"), range(r), value(def) {}
+
+ operator int64_t (void) const { return value; }
+ operator int64_t& (void) { return value; }
+ Int64Option& operator= (int64_t x) { value = x; return *this; }
+
+ virtual bool parse(const char* str){
+ const char* span = str;
+
+ if (!match(span, "-") || !match(span, name) || !match(span, "="))
+ return false;
+
+ char* end;
+ int64_t tmp = strtoll(span, &end, 10);
+
+ if (end == NULL)
+ return false;
+ else if (tmp > range.end){
+ fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
+ exit(1);
+ }else if (tmp < range.begin){
+ fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
+ exit(1); }
+
+ value = tmp;
+
+ return true;
+ }
+
+ virtual void help (bool verbose = false){
+ fprintf(stderr, " -%-12s = %-8s [", name, type_name);
+ if (range.begin == INT64_MIN)
+ fprintf(stderr, "imin");
+ else
+ fprintf(stderr, "%4"PRIi64, range.begin);
+
+ fprintf(stderr, " .. ");
+ if (range.end == INT64_MAX)
+ fprintf(stderr, "imax");
+ else
+ fprintf(stderr, "%4"PRIi64, range.end);
+
+ fprintf(stderr, "] (default: %"PRIi64")\n", value);
+ if (verbose){
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
+ }
+};
+#endif
+
+//==================================================================================================
+// String option:
+
+
+class StringOption : public Option
+{
+ const char* value;
+ public:
+ StringOption(const char* c, const char* n, const char* d, const char* def = NULL)
+ : Option(n, d, c, "<string>"), value(def) {}
+
+ operator const char* (void) const { return value; }
+ operator const char*& (void) { return value; }
+ StringOption& operator= (const char* x) { value = x; return *this; }
+
+ virtual bool parse(const char* str){
+ const char* span = str;
+
+ if (!match(span, "-") || !match(span, name) || !match(span, "="))
+ return false;
+
+ value = span;
+ return true;
+ }
+
+ virtual void help (bool verbose = false){
+ fprintf(stderr, " -%-10s = %8s\n", name, type_name);
+ if (verbose){
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
+ }
+};
+
+
+//==================================================================================================
+// Bool option:
+
+
+class BoolOption : public Option
+{
+ bool value;
+
+ public:
+ BoolOption(const char* c, const char* n, const char* d, bool v)
+ : Option(n, d, c, "<bool>"), value(v) {}
+
+ operator bool (void) const { return value; }
+ operator bool& (void) { return value; }
+ BoolOption& operator=(bool b) { value = b; return *this; }
+
+ virtual bool parse(const char* str){
+ const char* span = str;
+
+ if (match(span, "-")){
+ bool b = !match(span, "no-");
+
+ if (strcmp(span, name) == 0){
+ value = b;
+ return true; }
+ }
+
+ return false;
+ }
+
+ virtual void help (bool verbose = false){
+
+ fprintf(stderr, " -%s, -no-%s", name, name);
+
+ for (uint32_t i = 0; i < 32 - strlen(name)*2; i++)
+ fprintf(stderr, " ");
+
+ fprintf(stderr, " ");
+ fprintf(stderr, "(default: %s)\n", value ? "on" : "off");
+ if (verbose){
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
+ }
+};
+
+//=================================================================================================
+}
+
+#endif
--- /dev/null
+/************************************************************************************[ParseUtils.h]
+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.
+**************************************************************************************************/
+
+#ifndef Minisat_ParseUtils_h
+#define Minisat_ParseUtils_h
+
+#include <stdlib.h>
+#include <stdio.h>
+
+#include <zlib.h>
+
+namespace Minisat {
+
+//-------------------------------------------------------------------------------------------------
+// A simple buffered character stream class:
+
+static const int buffer_size = 1048576;
+
+
+class StreamBuffer {
+ gzFile in;
+ unsigned char buf[buffer_size];
+ int pos;
+ int size;
+
+ void assureLookahead() {
+ if (pos >= size) {
+ pos = 0;
+ size = gzread(in, buf, sizeof(buf)); } }
+
+public:
+ explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0) { assureLookahead(); }
+
+ int operator * () const { return (pos >= size) ? EOF : buf[pos]; }
+ void operator ++ () { pos++; assureLookahead(); }
+ int position () const { return pos; }
+};
+
+
+//-------------------------------------------------------------------------------------------------
+// End-of-file detection functions for StreamBuffer and char*:
+
+
+static inline bool isEof(StreamBuffer& in) { return *in == EOF; }
+static inline bool isEof(const char* in) { return *in == '\0'; }
+
+//-------------------------------------------------------------------------------------------------
+// Generic parse functions parametrized over the input-stream type.
+
+
+template<class B>
+static void skipWhitespace(B& in) {
+ while ((*in >= 9 && *in <= 13) || *in == 32)
+ ++in; }
+
+
+template<class B>
+static void skipLine(B& in) {
+ for (;;){
+ if (isEof(in)) return;
+ if (*in == '\n') { ++in; return; }
+ ++in; } }
+
+
+template<class B>
+static int parseInt(B& in) {
+ int val = 0;
+ bool neg = false;
+ skipWhitespace(in);
+ if (*in == '-') neg = true, ++in;
+ else if (*in == '+') ++in;
+ if (*in < '0' || *in > '9') fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
+ while (*in >= '0' && *in <= '9')
+ val = val*10 + (*in - '0'),
+ ++in;
+ return neg ? -val : val; }
+
+
+// String matching: in case of a match the input iterator will be advanced the corresponding
+// number of characters.
+template<class B>
+static bool match(B& in, const char* str) {
+ int i;
+ for (i = 0; str[i] != '\0'; i++)
+ if (in[i] != str[i])
+ return false;
+
+ in += i;
+
+ return true;
+}
+
+// String matching: consumes characters eagerly, but does not require random access iterator.
+template<class B>
+static bool eagerMatch(B& in, const char* str) {
+ for (; *str != '\0'; ++str, ++in)
+ if (*str != *in)
+ return false;
+ return true; }
+
+
+//=================================================================================================
+}
+
+#endif
--- /dev/null
+/***************************************************************************************[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 "../utils/System.h"
+
+#if defined(__linux__)
+
+#include <stdio.h>
+#include <stdlib.h>
+
+using namespace Minisat;
+
+// TODO: split the memory reading functions into two: one for reading high-watermark of RSS, and
+// one for reading the current virtual memory size.
+
+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() {
+ double peak = memReadPeak() / 1024;
+ return peak == 0 ? memUsed() : peak; }
+
+#elif defined(__FreeBSD__)
+
+double Minisat::memUsed(void) {
+ struct rusage ru;
+ getrusage(RUSAGE_SELF, &ru);
+ return (double)ru.ru_maxrss / 1024; }
+double MiniSat::memUsedPeak(void) { return memUsed(); }
+
+
+#elif defined(__APPLE__)
+#include <malloc/malloc.h>
+
+double Minisat::memUsed(void) {
+ malloc_statistics_t t;
+ malloc_zone_statistics(NULL, &t);
+ return (double)t.max_size_in_use / (1024*1024); }
+
+#else
+double Minisat::memUsed() {
+ return 0; }
+#endif
--- /dev/null
+/****************************************************************************************[System.h]
+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.
+**************************************************************************************************/
+
+#ifndef Minisat_System_h
+#define Minisat_System_h
+
+#if defined(__linux__)
+#include <fpu_control.h>
+#endif
+
+#include "../mtl/IntTypes.h"
+
+//-------------------------------------------------------------------------------------------------
+
+namespace Minisat {
+
+static inline double cpuTime(void); // CPU-time in seconds.
+extern double memUsed(); // Memory in mega bytes (returns 0 for unsupported architectures).
+extern double memUsedPeak(); // Peak-memory in mega bytes (returns 0 for unsupported architectures).
+
+}
+
+//-------------------------------------------------------------------------------------------------
+// Implementation of inline functions:
+
+#if defined(_MSC_VER) || defined(__MINGW32__)
+#include <time.h>
+
+static inline double Minisat::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; }
+
+#else
+#include <sys/time.h>
+#include <sys/resource.h>
+#include <unistd.h>
+
+static inline double Minisat::cpuTime(void) {
+ struct rusage ru;
+ getrusage(RUSAGE_SELF, &ru);
+ return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
+
+#endif
+
+#endif
projects / francis / stp.git / commitdiff