diff options
Diffstat (limited to 'libs')
-rw-r--r-- | libs/ezsat/ezminisat.cc | 6 | ||||
-rw-r--r-- | libs/minisat/00_PATCH_no_fpu_control.patch | 43 | ||||
-rw-r--r-- | libs/minisat/00_PATCH_remove_zlib.patch | 17 | ||||
-rw-r--r-- | libs/minisat/00_PATCH_typofixes.patch | 20 | ||||
-rwxr-xr-x[-rw-r--r--] | libs/minisat/00_UPDATE.sh | 6 | ||||
-rw-r--r-- | libs/minisat/Dimacs.h | 8 | ||||
-rw-r--r-- | libs/minisat/Options.cc | 4 | ||||
-rw-r--r-- | libs/minisat/SimpSolver.cc | 4 | ||||
-rw-r--r-- | libs/minisat/Solver.cc | 4 | ||||
-rw-r--r-- | libs/minisat/System.cc | 15 | ||||
-rw-r--r-- | libs/minisat/System.h | 7 | ||||
-rw-r--r-- | libs/subcircuit/subcircuit.h | 2 |
12 files changed, 110 insertions, 26 deletions
diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc index e0ee6292..4be5fd49 100644 --- a/libs/ezsat/ezminisat.cc +++ b/libs/ezsat/ezminisat.cc @@ -18,8 +18,12 @@ */ // needed for MiniSAT headers (see Minisat Makefile) -#define __STDC_LIMIT_MACROS +#ifndef __STDC_FORMAT_MACROS #define __STDC_FORMAT_MACROS +#endif +#ifndef __STDC_LIMIT_MACROS +#define __STDC_LIMIT_MACROS +#endif #include "ezminisat.h" diff --git a/libs/minisat/00_PATCH_no_fpu_control.patch b/libs/minisat/00_PATCH_no_fpu_control.patch new file mode 100644 index 00000000..6c754b1e --- /dev/null +++ b/libs/minisat/00_PATCH_no_fpu_control.patch @@ -0,0 +1,43 @@ +--- System.cc ++++ System.cc +@@ -97,17 +97,6 @@ double Minisat::memUsedPeak(bool) { 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) + { +--- System.h ++++ System.h +@@ -21,10 +21,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA + #ifndef Minisat_System_h + #define Minisat_System_h + +-#if defined(__linux__) +-#include <fpu_control.h> +-#endif +- + #include "IntTypes.h" + + //------------------------------------------------------------------------------------------------- +@@ -36,9 +32,6 @@ static inline double cpuTime(void); // CPU-time in seconds. + extern double memUsed(); // Memory in mega bytes (returns 0 for unsupported architectures). + extern double memUsedPeak(bool strictlyPeak = false); // Peak-memory in mega bytes (returns 0 for unsupported architectures). + +-extern void setX86FPUPrecision(); // Make sure double's are represented with the same precision +- // in memory and registers. +- + extern void limitMemory(uint64_t max_mem_mb); // Set a limit on total memory usage. The exact + // semantics varies depending on architecture. + diff --git a/libs/minisat/00_PATCH_remove_zlib.patch b/libs/minisat/00_PATCH_remove_zlib.patch index 61a36f7e..068356b7 100644 --- a/libs/minisat/00_PATCH_remove_zlib.patch +++ b/libs/minisat/00_PATCH_remove_zlib.patch @@ -36,3 +36,20 @@ int operator * () const { return (pos >= size) ? EOF : buf[pos]; } void operator ++ () { pos++; assureLookahead(); } +--- Dimacs.h ++++ Dimacs.h +@@ -76,10 +76,10 @@ static void parse_DIMACS_main(B& in, Solver& S, bool strictp = false) { + + // Inserts problem into solver. + // +-template<class Solver> +-static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) { +- StreamBuffer in(input_stream); +- parse_DIMACS_main(in, S, strictp); } ++//template<class Solver> ++//static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) { ++// StreamBuffer in(input_stream); ++// parse_DIMACS_main(in, S, strictp); } + + //================================================================================================= + } diff --git a/libs/minisat/00_PATCH_typofixes.patch b/libs/minisat/00_PATCH_typofixes.patch new file mode 100644 index 00000000..175f483b --- /dev/null +++ b/libs/minisat/00_PATCH_typofixes.patch @@ -0,0 +1,20 @@ +--- Solver.h ++++ Solver.h +@@ -103,7 +103,7 @@ public: + int nFreeVars () const; + void printStats () const; // Print some current statistics to standard output. + +- // Resource contraints: ++ // Resource constraints: + // + void setConfBudget(int64_t x); + void setPropBudget(int64_t x); +@@ -230,7 +230,7 @@ protected: + double learntsize_adjust_confl; + int learntsize_adjust_cnt; + +- // Resource contraints: ++ // Resource constraints: + // + int64_t conflict_budget; // -1 means no budget. + int64_t propagation_budget; // -1 means no budget. diff --git a/libs/minisat/00_UPDATE.sh b/libs/minisat/00_UPDATE.sh index 96a34ec9..ea26215a 100644..100755 --- a/libs/minisat/00_UPDATE.sh +++ b/libs/minisat/00_UPDATE.sh @@ -9,9 +9,11 @@ rm -rf minisat_upstream sed -i -e 's,^#include *"minisat/[^/]\+/\?,#include ",' *.cc *.h sed -i -e 's/Minisat::memUsedPeak()/Minisat::memUsedPeak(bool)/' System.cc sed -i -e 's/PRI[iu]64/ & /' Options.h Solver.cc -sed -i -e '1 i #define __STDC_LIMIT_MACROS' *.cc -sed -i -e '1 i #define __STDC_FORMAT_MACROS' *.cc +sed -i -e '1 i #ifndef __STDC_LIMIT_MACROS\n#define __STDC_LIMIT_MACROS\n#endif' *.cc +sed -i -e '1 i #ifndef __STDC_FORMAT_MACROS\n#define __STDC_FORMAT_MACROS\n#endif' *.cc patch -p0 < 00_PATCH_mkLit_default_arg.patch patch -p0 < 00_PATCH_remove_zlib.patch +patch -p0 < 00_PATCH_no_fpu_control.patch +patch -p0 < 00_PATCH_typofixes.patch diff --git a/libs/minisat/Dimacs.h b/libs/minisat/Dimacs.h index ccfa1c01..61b9d3ca 100644 --- a/libs/minisat/Dimacs.h +++ b/libs/minisat/Dimacs.h @@ -76,10 +76,10 @@ static void parse_DIMACS_main(B& in, Solver& S, bool strictp = false) { // Inserts problem into solver. // -template<class Solver> -static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) { - StreamBuffer in(input_stream); - parse_DIMACS_main(in, S, strictp); } +//template<class Solver> +//static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) { +// StreamBuffer in(input_stream); +// parse_DIMACS_main(in, S, strictp); } //================================================================================================= } diff --git a/libs/minisat/Options.cc b/libs/minisat/Options.cc index 1aff3fab..5c45dd6a 100644 --- a/libs/minisat/Options.cc +++ b/libs/minisat/Options.cc @@ -1,5 +1,9 @@ +#ifndef __STDC_FORMAT_MACROS #define __STDC_FORMAT_MACROS +#endif +#ifndef __STDC_LIMIT_MACROS #define __STDC_LIMIT_MACROS +#endif /**************************************************************************************[Options.cc] Copyright (c) 2008-2010, Niklas Sorensson diff --git a/libs/minisat/SimpSolver.cc b/libs/minisat/SimpSolver.cc index fd5774e0..7348a905 100644 --- a/libs/minisat/SimpSolver.cc +++ b/libs/minisat/SimpSolver.cc @@ -1,5 +1,9 @@ +#ifndef __STDC_FORMAT_MACROS #define __STDC_FORMAT_MACROS +#endif +#ifndef __STDC_LIMIT_MACROS #define __STDC_LIMIT_MACROS +#endif /***********************************************************************************[SimpSolver.cc] Copyright (c) 2006, Niklas Een, Niklas Sorensson Copyright (c) 2007-2010, Niklas Sorensson diff --git a/libs/minisat/Solver.cc b/libs/minisat/Solver.cc index ab476853..f6d4fb5a 100644 --- a/libs/minisat/Solver.cc +++ b/libs/minisat/Solver.cc @@ -1,5 +1,9 @@ +#ifndef __STDC_FORMAT_MACROS #define __STDC_FORMAT_MACROS +#endif +#ifndef __STDC_LIMIT_MACROS #define __STDC_LIMIT_MACROS +#endif /***************************************************************************************[Solver.cc] Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson Copyright (c) 2007-2010, Niklas Sorensson diff --git a/libs/minisat/System.cc b/libs/minisat/System.cc index febe3b40..1921a1d7 100644 --- a/libs/minisat/System.cc +++ b/libs/minisat/System.cc @@ -1,5 +1,9 @@ +#ifndef __STDC_FORMAT_MACROS #define __STDC_FORMAT_MACROS +#endif +#ifndef __STDC_LIMIT_MACROS #define __STDC_LIMIT_MACROS +#endif /***************************************************************************************[System.cc] Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson Copyright (c) 2007-2010, Niklas Sorensson @@ -97,17 +101,6 @@ double Minisat::memUsedPeak(bool) { 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) { diff --git a/libs/minisat/System.h b/libs/minisat/System.h index ee92a6e0..cd9d020c 100644 --- a/libs/minisat/System.h +++ b/libs/minisat/System.h @@ -21,10 +21,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_System_h #define Minisat_System_h -#if defined(__linux__) -#include <fpu_control.h> -#endif - #include "IntTypes.h" //------------------------------------------------------------------------------------------------- @@ -36,9 +32,6 @@ static inline double cpuTime(void); // CPU-time in seconds. extern double memUsed(); // Memory in mega bytes (returns 0 for unsupported architectures). extern double memUsedPeak(bool strictlyPeak = false); // Peak-memory in mega bytes (returns 0 for unsupported architectures). -extern void setX86FPUPrecision(); // Make sure double's are represented with the same precision - // in memory and registers. - extern void limitMemory(uint64_t max_mem_mb); // Set a limit on total memory usage. The exact // semantics varies depending on architecture. diff --git a/libs/subcircuit/subcircuit.h b/libs/subcircuit/subcircuit.h index 5291c642..8368efab 100644 --- a/libs/subcircuit/subcircuit.h +++ b/libs/subcircuit/subcircuit.h @@ -131,7 +131,7 @@ namespace SubCircuit public: Solver(); - ~Solver(); + virtual ~Solver(); void setVerbose(); void addGraph(std::string graphId, const Graph &graph); |