summaryrefslogtreecommitdiff
path: root/src/prop/minisat/utils
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/minisat/utils')
-rw-r--r--src/prop/minisat/utils/Makefile4
-rw-r--r--src/prop/minisat/utils/Options.cc91
-rw-r--r--src/prop/minisat/utils/Options.h386
-rw-r--r--src/prop/minisat/utils/ParseUtils.h122
-rw-r--r--src/prop/minisat/utils/System.cc95
-rw-r--r--src/prop/minisat/utils/System.h60
6 files changed, 0 insertions, 758 deletions
diff --git a/src/prop/minisat/utils/Makefile b/src/prop/minisat/utils/Makefile
deleted file mode 100644
index 204cea541..000000000
--- a/src/prop/minisat/utils/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-EXEC = system_test
-DEPDIR = mtl
-
-include $(MROOT)/mtl/template.mk
diff --git a/src/prop/minisat/utils/Options.cc b/src/prop/minisat/utils/Options.cc
deleted file mode 100644
index ec5a6e930..000000000
--- a/src/prop/minisat/utils/Options.cc
+++ /dev/null
@@ -1,91 +0,0 @@
-/**************************************************************************************[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);
-}
-
diff --git a/src/prop/minisat/utils/Options.h b/src/prop/minisat/utils/Options.h
deleted file mode 100644
index 9c1f40699..000000000
--- a/src/prop/minisat/utils/Options.h
+++ /dev/null
@@ -1,386 +0,0 @@
-/***************************************************************************************[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
diff --git a/src/prop/minisat/utils/ParseUtils.h b/src/prop/minisat/utils/ParseUtils.h
deleted file mode 100644
index d3071649d..000000000
--- a/src/prop/minisat/utils/ParseUtils.h
+++ /dev/null
@@ -1,122 +0,0 @@
-/************************************************************************************[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
diff --git a/src/prop/minisat/utils/System.cc b/src/prop/minisat/utils/System.cc
deleted file mode 100644
index a7cf53f55..000000000
--- a/src/prop/minisat/utils/System.cc
+++ /dev/null
@@ -1,95 +0,0 @@
-/***************************************************************************************[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
diff --git a/src/prop/minisat/utils/System.h b/src/prop/minisat/utils/System.h
deleted file mode 100644
index 17581927a..000000000
--- a/src/prop/minisat/utils/System.h
+++ /dev/null
@@ -1,60 +0,0 @@
-/****************************************************************************************[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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback