diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-02-25 18:23:10 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-02-25 18:23:10 +0000 |
commit | 7aa55e0d38e73a02b11ad0c5a60196b610674050 (patch) | |
tree | c59def0ed00dcde29a5a6498cf74ac87dc3a2a6f /src/prop/bvminisat/utils | |
parent | d8da6a3644d1cdbe62d44a8eb80068da4d1d2855 (diff) |
Refactored CnfStream to work with the bv theory Bitblaster:
* separated SatSolverInput interface class into two classes:
- TheoryProxy for the sat solver to communicate with the theories
- SatSolverInterface abstract class to communicate with the sat solver
* instead of using #ifdef typedef for SatClauses and SatLiterals, now there are CVC4 SatLiteral/SatClause types and mappings between them and the internal sat solver clause/literal representation
* added abstract classes for DPLLSatSolver and BVSatSolver different interfaces
Replaced TheoryBV with bitblasting implementation:
* all operators bitblasted
* only operator elimination rewrite rules so far
Diffstat (limited to 'src/prop/bvminisat/utils')
-rw-r--r-- | src/prop/bvminisat/utils/Makefile | 4 | ||||
-rw-r--r-- | src/prop/bvminisat/utils/Options.cc | 91 | ||||
-rw-r--r-- | src/prop/bvminisat/utils/Options.h | 386 | ||||
-rw-r--r-- | src/prop/bvminisat/utils/ParseUtils.h | 122 | ||||
-rw-r--r-- | src/prop/bvminisat/utils/System.cc | 95 | ||||
-rw-r--r-- | src/prop/bvminisat/utils/System.h | 60 |
6 files changed, 758 insertions, 0 deletions
diff --git a/src/prop/bvminisat/utils/Makefile b/src/prop/bvminisat/utils/Makefile new file mode 100644 index 000000000..204cea541 --- /dev/null +++ b/src/prop/bvminisat/utils/Makefile @@ -0,0 +1,4 @@ +EXEC = system_test +DEPDIR = mtl + +include $(MROOT)/mtl/template.mk diff --git a/src/prop/bvminisat/utils/Options.cc b/src/prop/bvminisat/utils/Options.cc new file mode 100644 index 000000000..a15220c4b --- /dev/null +++ b/src/prop/bvminisat/utils/Options.cc @@ -0,0 +1,91 @@ +/**************************************************************************************[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 BVMinisat; + +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/bvminisat/utils/Options.h b/src/prop/bvminisat/utils/Options.h new file mode 100644 index 000000000..1d41333ef --- /dev/null +++ b/src/prop/bvminisat/utils/Options.h @@ -0,0 +1,386 @@ +/***************************************************************************************[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 BVMinisat_Options_h +#define BVMinisat_Options_h + +#include <stdlib.h> +#include <stdio.h> +#include <math.h> +#include <string.h> + +#include "prop/bvminisat/mtl/IntTypes.h" +#include "prop/bvminisat/mtl/Vec.h" +#include "prop/bvminisat/utils/ParseUtils.h" + +namespace BVMinisat { + +//================================================================================================== +// 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/bvminisat/utils/ParseUtils.h b/src/prop/bvminisat/utils/ParseUtils.h new file mode 100644 index 000000000..920298abb --- /dev/null +++ b/src/prop/bvminisat/utils/ParseUtils.h @@ -0,0 +1,122 @@ +/************************************************************************************[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 BVMinisat_ParseUtils_h +#define BVMinisat_ParseUtils_h + +#include <stdlib.h> +#include <stdio.h> + +#include <zlib.h> + +namespace BVMinisat { + +//------------------------------------------------------------------------------------------------- +// 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/bvminisat/utils/System.cc b/src/prop/bvminisat/utils/System.cc new file mode 100644 index 000000000..9c2fcb083 --- /dev/null +++ b/src/prop/bvminisat/utils/System.cc @@ -0,0 +1,95 @@ +/***************************************************************************************[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 BVMinisat; + +// 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/bvminisat/utils/System.h b/src/prop/bvminisat/utils/System.h new file mode 100644 index 000000000..f9fe708bb --- /dev/null +++ b/src/prop/bvminisat/utils/System.h @@ -0,0 +1,60 @@ +/****************************************************************************************[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 BVMinisat_System_h +#define BVMinisat_System_h + +#if defined(__linux__) +#include <fpu_control.h> +#endif + +#include "mtl/IntTypes.h" + +//------------------------------------------------------------------------------------------------- + +namespace BVMinisat { + +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 BVMinisat::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 |