Skip to content

Instantly share code, notes, and snippets.

@msakai

msakai/open-wbo-1.3-cryptominisat4.diff

Created January 8, 2015 23:50
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save msakai/5ae96caf0584468fa9a3 to your computer and use it in GitHub Desktop.
Save msakai/5ae96caf0584468fa9a3 to your computer and use it in GitHub Desktop.
Download ZIP
Patch for using Cryptominisat4 within open-wbo version 1.3
Raw
open-wbo-1.3-cryptominisat4.diff
diff -uprN open-wbo.orig/Makefile open-wbo/Makefile
--- open-wbo.orig/Makefile 2015-01-02 23:11:06.000000000 -0500
+++ open-wbo/Makefile 2015-01-08 08:48:47.418892000 -0500
@@ -10,10 +10,14 @@
# SOLVERDIR = minisat
# NSPACE = Minisat
#
+#VERSION = core
+#SOLVERNAME = "Glucose3.0"
+#SOLVERDIR = glucose3.0
+#NSPACE = Glucose
VERSION = core
-SOLVERNAME = "Glucose3.0"
-SOLVERDIR = glucose3.0
-NSPACE = Glucose
+SOLVERNAME = "CryptoMinisat4"
+SOLVERDIR = cryptominisat4
+NSPACE = Minisat
# THE REMAINING OF THE MAKEFILE SHOULD BE LEFT UNCHANGED
EXEC = open-wbo
DEPDIR = mtl utils core
@@ -29,4 +33,7 @@ CFLAGS += -DGLUCORED
DEPDIR += reducer glucored
endif
endif
+ifeq ($(SOLVERDIR),cryptominisat4)
+LFLAGS += -lcryptominisat4
+endif
include $(MROOT)/mtl/template.mk
diff -uprN open-wbo.orig/solvers/cryptominisat4/core/Solver.cc open-wbo/solvers/cryptominisat4/core/Solver.cc
--- open-wbo.orig/solvers/cryptominisat4/core/Solver.cc 1969-12-31 19:00:00.000000000 -0500
+++ open-wbo/solvers/cryptominisat4/core/Solver.cc 2015-01-08 08:54:24.010892000 -0500
@@ -0,0 +1,9 @@
+#include "core/Solver.h"
+
+namespace Minisat {
+
+Solver::~Solver()
+{
+}
+
+}
diff -uprN open-wbo.orig/solvers/cryptominisat4/core/Solver.h open-wbo/solvers/cryptominisat4/core/Solver.h
--- open-wbo.orig/solvers/cryptominisat4/core/Solver.h 1969-12-31 19:00:00.000000000 -0500
+++ open-wbo/solvers/cryptominisat4/core/Solver.h 2015-01-08 18:44:44.170892000 -0500
@@ -0,0 +1,112 @@
+#ifndef Minisat_Solver_h
+#define Minisat_Solver_h
+
+#include <cryptominisat4/cryptominisat.h>
+#include <stdio.h>
+#include <string.h>
+#include <math.h>
+#include "mtl/Vec.h"
+
+using CMSat::Var;
+using CMSat::Lit;
+using CMSat::lit_Undef;
+using CMSat::lit_Error;
+using CMSat::lbool;
+using CMSat::l_True;
+using CMSat::l_False;
+
+namespace Minisat {
+
+//=================================================================================================
+// Solver -- the main class:
+
+ class Solver {
+ CMSat::SATSolver cmsat;
+public:
+
+ // Constructor/Destructor:
+ //
+ Solver();
+ virtual ~Solver();
+
+ // Problem specification:
+ //
+ Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
+
+ bool addClause (const vec<Lit>& ps); // Add a clause to the solver.
+ bool addClause (Lit p); // Add a unit clause to the solver.
+
+ // Solving:
+ //
+ bool solve (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions.
+ lbool solveLimited (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions (With resource constraints).
+ bool solve (); // Search without assumptions.
+ bool okay () const; // FALSE means solver is in a conflicting state
+
+ // Read state:
+ int nVars () const; // The current number of variables.
+
+ // Extra results: (read-only member variable)
+ //
+ vec<lbool> model; // If problem is satisfiable, this vector contains the model (if any).
+ vec<Lit> conflict; // If problem is unsatisfiable (possibly under assumptions),
+ // this vector represent the final conflict clause expressed in the assumptions.
+};
+
+inline Solver::Solver() : cmsat() {}
+inline Var Solver::newVar (bool polarity, bool dvar) { Var v = cmsat.nVars(); cmsat.new_var(); return v; }
+inline bool Solver::addClause (const vec<Lit>& ps) { std::vector<Lit> ps2((const Lit*)ps, (const Lit*)ps + ps.size()); return cmsat.add_clause(ps2); }
+inline bool Solver::addClause (Lit p) { std::vector<Lit> ps2; ps2.push_back(p); return cmsat.add_clause(ps2); }
+
+inline int Solver::nVars () const { return cmsat.nVars(); }
+
+namespace {
+ template<class T> void vector2vec(const std::vector<T> &s, vec<T> &d) {
+ d.clear();
+ for (int i = 0; i < s.size(); i++)
+ d.push(s[i]);
+ }
+}
+
+inline bool Solver::solve () {
+ model.clear();
+ conflict.clear();
+ lbool ret = cmsat.solve();
+ if (ret == l_True)
+ vector2vec(cmsat.get_model(), model);
+ return ret == l_True;
+}
+
+inline bool Solver::solve (const vec<Lit>& assumps){
+ model.clear();
+ conflict.clear();
+ std::vector<Lit> assumptions((const Lit*)assumps, (const Lit*)assumps + assumps.size());
+ lbool ret = cmsat.solve(&assumptions);
+ if (ret == l_True)
+ vector2vec(cmsat.get_model(), model);
+ else if (ret == l_False)
+ vector2vec(cmsat.get_conflict(), conflict);
+ return ret == l_True;
+}
+
+inline lbool Solver::solveLimited (const vec<Lit>& assumps){
+ model.clear();
+ conflict.clear();
+ std::vector<Lit> assumptions((const Lit*)assumps, (const Lit*)assumps + assumps.size());
+ lbool ret = cmsat.solve(&assumptions);
+ if (ret == l_True)
+ vector2vec(cmsat.get_model(), model);
+ else if (ret == l_False)
+ vector2vec(cmsat.get_conflict(), conflict);
+ return ret;
+}
+
+inline bool Solver::okay () const { return cmsat.okay(); }
+
+inline Lit mkLit(Var var, bool is_inverted = false) { return Lit(var, is_inverted); }
+inline Var var(Lit lit) { return lit.var(); }
+inline bool sign(Lit lit) { return lit.sign(); }
+
+}
+
+#endif
diff -uprN open-wbo.orig/solvers/cryptominisat4/mtl/config.mk open-wbo/solvers/cryptominisat4/mtl/config.mk
--- open-wbo.orig/solvers/cryptominisat4/mtl/config.mk 1969-12-31 19:00:00.000000000 -0500
+++ open-wbo/solvers/cryptominisat4/mtl/config.mk 2015-01-02 23:11:06.000000000 -0500
@@ -0,0 +1,6 @@
+##
+## This file is for system specific configurations. For instance, on
+## some systems the path to zlib needs to be added. Example:
+##
+## CFLAGS += -I/usr/local/include
+## LFLAGS += -L/usr/local/lib
diff -uprN open-wbo.orig/solvers/cryptominisat4/mtl/IntTypes.h open-wbo/solvers/cryptominisat4/mtl/IntTypes.h
--- open-wbo.orig/solvers/cryptominisat4/mtl/IntTypes.h 1969-12-31 19:00:00.000000000 -0500
+++ open-wbo/solvers/cryptominisat4/mtl/IntTypes.h 2015-01-02 23:11:06.000000000 -0500
@@ -0,0 +1,42 @@
+/**************************************************************************************[IntTypes.h]
+Copyright (c) 2009-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_IntTypes_h
+#define Minisat_IntTypes_h
+
+#ifdef __sun
+ // Not sure if there are newer versions that support C99 headers. The
+ // needed features are implemented in the headers below though:
+
+# include <sys/int_types.h>
+# include <sys/int_fmtio.h>
+# include <sys/int_limits.h>
+
+#else
+
+# include <stdint.h>
+# include <inttypes.h>
+
+#endif
+
+#include <limits.h>
+
+//=================================================================================================
+
+#endif
diff -uprN open-wbo.orig/solvers/cryptominisat4/mtl/Sort.h open-wbo/solvers/cryptominisat4/mtl/Sort.h
--- open-wbo.orig/solvers/cryptominisat4/mtl/Sort.h 1969-12-31 19:00:00.000000000 -0500
+++ open-wbo/solvers/cryptominisat4/mtl/Sort.h 2015-01-02 23:11:06.000000000 -0500
@@ -0,0 +1,98 @@
+/******************************************************************************************[Sort.h]
+Copyright (c) 2003-2007, 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_Sort_h
+#define Minisat_Sort_h
+
+#include "mtl/Vec.h"
+
+//=================================================================================================
+// Some sorting algorithms for vec's
+
+
+namespace Minisat {
+
+template<class T>
+struct LessThan_default {
+ bool operator () (T x, T y) { return x < y; }
+};
+
+
+template <class T, class LessThan>
+void selectionSort(T* array, int size, LessThan lt)
+{
+ int i, j, best_i;
+ T tmp;
+
+ for (i = 0; i < size-1; i++){
+ best_i = i;
+ for (j = i+1; j < size; j++){
+ if (lt(array[j], array[best_i]))
+ best_i = j;
+ }
+ tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
+ }
+}
+template <class T> static inline void selectionSort(T* array, int size) {
+ selectionSort(array, size, LessThan_default<T>()); }
+
+template <class T, class LessThan>
+void sort(T* array, int size, LessThan lt)
+{
+ if (size <= 15)
+ selectionSort(array, size, lt);
+
+ else{
+ T pivot = array[size / 2];
+ T tmp;
+ int i = -1;
+ int j = size;
+
+ for(;;){
+ do i++; while(lt(array[i], pivot));
+ do j--; while(lt(pivot, array[j]));
+
+ if (i >= j) break;
+
+ tmp = array[i]; array[i] = array[j]; array[j] = tmp;
+ }
+
+ sort(array , i , lt);
+ sort(&array[i], size-i, lt);
+ }
+}
+template <class T> static inline void sort(T* array, int size) {
+ sort(array, size, LessThan_default<T>()); }
+
+
+//=================================================================================================
+// For 'vec's:
+
+
+template <class T, class LessThan> void sort(vec<T>& v, LessThan lt) {
+ sort((T*)v, v.size(), lt); }
+template <class T> void sort(vec<T>& v) {
+ sort(v, LessThan_default<T>()); }
+
+
+//=================================================================================================
+}
+
+#endif
diff -uprN open-wbo.orig/solvers/cryptominisat4/mtl/template.mk open-wbo/solvers/cryptominisat4/mtl/template.mk
--- open-wbo.orig/solvers/cryptominisat4/mtl/template.mk 1969-12-31 19:00:00.000000000 -0500
+++ open-wbo/solvers/cryptominisat4/mtl/template.mk 2015-01-02 23:11:06.000000000 -0500
@@ -0,0 +1,107 @@
+##
+## Template makefile for Standard, Profile, Debug, Release, and Release-static versions
+##
+## eg: "make rs" for a statically linked release version.
+## "make d" for a debug version (no optimizations).
+## "make" for the standard version (optimized, but with debug information and assertions active)
+
+PWD = $(shell pwd)
+EXEC ?= $(notdir $(PWD))
+
+CSRCS = $(wildcard $(PWD)/*.cc)
+DSRCS = $(foreach dir, $(DEPDIR), $(filter-out $(MROOT)/$(dir)/Main.cc, $(wildcard $(MROOT)/$(dir)/*.cc)))
+CHDRS = $(wildcard $(PWD)/*.h)
+COBJS = $(CSRCS:.cc=.o) $(DSRCS:.cc=.o)
+
+PCOBJS = $(addsuffix p, $(COBJS))
+DCOBJS = $(addsuffix d, $(COBJS))
+RCOBJS = $(addsuffix r, $(COBJS))
+
+#CXX ?= /usr/gcc-/bin/g++-4.7.0
+CXX ?= g++
+CFLAGS ?= -Wall -Wno-parentheses
+LFLAGS ?= -Wall
+
+COPTIMIZE ?= -O3
+
+CFLAGS += -I$(MROOT) -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS
+LFLAGS += -lz
+
+.PHONY : s p d r rs clean
+
+s: $(EXEC)
+p: $(EXEC)_profile
+d: $(EXEC)_debug
+r: $(EXEC)_release
+rs: $(EXEC)_static
+
+libs: lib$(LIB)_standard.a
+libp: lib$(LIB)_profile.a
+libd: lib$(LIB)_debug.a
+libr: lib$(LIB)_release.a
+
+## Compile options
+%.o: CFLAGS +=$(COPTIMIZE) -g -D DEBUG
+%.op: CFLAGS +=$(COPTIMIZE) -pg -g -D NDEBUG
+%.od: CFLAGS +=-O0 -g -D DEBUG
+%.or: CFLAGS +=$(COPTIMIZE) -g -D NDEBUG
+
+## Link options
+$(EXEC): LFLAGS += -g
+$(EXEC)_profile: LFLAGS += -g -pg
+$(EXEC)_debug: LFLAGS += -g
+#$(EXEC)_release: LFLAGS += ...
+$(EXEC)_static: LFLAGS += --static
+
+## Dependencies
+$(EXEC): $(COBJS)
+$(EXEC)_profile: $(PCOBJS)
+$(EXEC)_debug: $(DCOBJS)
+$(EXEC)_release: $(RCOBJS)
+$(EXEC)_static: $(RCOBJS)
+
+lib$(LIB)_standard.a: $(filter-out */Main.o, $(COBJS))
+lib$(LIB)_profile.a: $(filter-out */Main.op, $(PCOBJS))
+lib$(LIB)_debug.a: $(filter-out */Main.od, $(DCOBJS))
+lib$(LIB)_release.a: $(filter-out */Main.or, $(RCOBJS))
+
+
+## Build rule
+%.o %.op %.od %.or: %.cc
+ @echo Compiling: $(subst $(MROOT)/,,$@)
+ @$(CXX) $(CFLAGS) -c -o $@ $<
+
+## Linking rules (standard/profile/debug/release)
+$(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static:
+ @echo Linking: "$@ ( $(foreach f,$^,$(subst $(MROOT)/,,$f)) )"
+ @$(CXX) $^ $(LFLAGS) -o $@
+
+## Library rules (standard/profile/debug/release)
+lib$(LIB)_standard.a lib$(LIB)_profile.a lib$(LIB)_release.a lib$(LIB)_debug.a:
+ @echo Making library: "$@ ( $(foreach f,$^,$(subst $(MROOT)/,,$f)) )"
+ @$(AR) -rcsv $@ $^
+
+## Library Soft Link rule:
+libs libp libd libr:
+ @echo "Making Soft Link: $^ -> lib$(LIB).a"
+ @ln -sf $^ lib$(LIB).a
+
+## Clean rule
+clean:
+ @rm -f $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static \
+ $(COBJS) $(PCOBJS) $(DCOBJS) $(RCOBJS) *.core depend.mk
+
+## Make dependencies
+depend.mk: $(CSRCS) $(CHDRS)
+ @echo Making dependencies
+ @$(CXX) $(CFLAGS) -I$(MROOT) \
+ $(CSRCS) -MM | sed 's|\(.*\):|$(PWD)/\1 $(PWD)/\1r $(PWD)/\1d $(PWD)/\1p:|' > depend.mk
+ @for dir in $(DEPDIR); do \
+ if [ -r $(MROOT)/$${dir}/depend.mk ]; then \
+ echo Depends on: $${dir}; \
+ cat $(MROOT)/$${dir}/depend.mk >> depend.mk; \
+ fi; \
+ done
+
+-include $(MROOT)/mtl/config.mk
+-include depend.mk
diff -uprN open-wbo.orig/solvers/cryptominisat4/mtl/Vec.h open-wbo/solvers/cryptominisat4/mtl/Vec.h
--- open-wbo.orig/solvers/cryptominisat4/mtl/Vec.h 1969-12-31 19:00:00.000000000 -0500
+++ open-wbo/solvers/cryptominisat4/mtl/Vec.h 2015-01-08 08:30:40.570892000 -0500
@@ -0,0 +1,131 @@
+/*******************************************************************************************[Vec.h]
+Copyright (c) 2003-2007, 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_Vec_h
+#define Minisat_Vec_h
+
+#include <assert.h>
+#include <new>
+
+#include "mtl/IntTypes.h"
+#include "mtl/XAlloc.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// Automatically resizable arrays
+//
+// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)
+
+template<class T>
+class vec {
+ T* data;
+ int sz;
+ int cap;
+
+ // Don't allow copying (error prone):
+ vec<T>& operator = (vec<T>& other) { assert(0); return *this; }
+ vec (vec<T>& other) { assert(0); }
+
+ // Helpers for calculating next capacity:
+ static inline int imax (int x, int y) { int mask = (y-x) >> (sizeof(int)*8-1); return (x&mask) + (y&(~mask)); }
+ //static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; }
+ static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; }
+
+public:
+ // Constructors:
+ vec() : data(NULL) , sz(0) , cap(0) { }
+ explicit vec(int size) : data(NULL) , sz(0) , cap(0) { growTo(size); }
+ vec(int size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); }
+ ~vec() { clear(true); }
+
+ // Pointer to first element:
+ operator const T* (void) const { return data; }
+ operator T* (void) { return data; }
+
+ // Size operations:
+ int size (void) const { return sz; }
+ void shrink (int nelems) { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); }
+ void shrink_ (int nelems) { assert(nelems <= sz); sz -= nelems; }
+ int capacity (void) const { return cap; }
+ void capacity (int min_cap);
+ void growTo (int size);
+ void growTo (int size, const T& pad);
+ void clear (bool dealloc = false);
+
+ // Stack interface:
+ void push (void) { if (sz == cap) capacity(sz+1); new (&data[sz]) T(); sz++; }
+ void push (const T& elem) { if (sz == cap) capacity(sz+1); data[sz++] = elem; }
+ void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; }
+ void pop (void) { assert(sz > 0); sz--, data[sz].~T(); }
+ // NOTE: it seems possible that overflow can happen in the 'sz+1' expression of 'push()', but
+ // in fact it can not since it requires that 'cap' is equal to INT_MAX. This in turn can not
+ // happen given the way capacities are calculated (below). Essentially, all capacities are
+ // even, but INT_MAX is odd.
+
+ const T& last (void) const { return data[sz-1]; }
+ T& last (void) { return data[sz-1]; }
+
+ // Vector interface:
+ const T& operator [] (int index) const { return data[index]; }
+ T& operator [] (int index) { return data[index]; }
+
+ // Duplicatation (preferred instead):
+ void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
+ void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
+};
+
+
+template<class T>
+void vec<T>::capacity(int min_cap) {
+ if (cap >= min_cap) return;
+ int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
+ if (add > INT_MAX - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)
+ throw OutOfMemoryException();
+ }
+
+
+template<class T>
+void vec<T>::growTo(int size, const T& pad) {
+ if (sz >= size) return;
+ capacity(size);
+ for (int i = sz; i < size; i++) data[i] = pad;
+ sz = size; }
+
+
+template<class T>
+void vec<T>::growTo(int size) {
+ if (sz >= size) return;
+ capacity(size);
+ for (int i = sz; i < size; i++) new (&data[i]) T();
+ sz = size; }
+
+
+template<class T>
+void vec<T>::clear(bool dealloc) {
+ if (data != NULL){
+ for (int i = 0; i < sz; i++) data[i].~T();
+ sz = 0;
+ if (dealloc) free(data), data = NULL, cap = 0; } }
+
+//=================================================================================================
+}
+
+#endif
diff -uprN open-wbo.orig/solvers/cryptominisat4/mtl/XAlloc.h open-wbo/solvers/cryptominisat4/mtl/XAlloc.h
--- open-wbo.orig/solvers/cryptominisat4/mtl/XAlloc.h 1969-12-31 19:00:00.000000000 -0500
+++ open-wbo/solvers/cryptominisat4/mtl/XAlloc.h 2015-01-02 23:11:06.000000000 -0500
@@ -0,0 +1,45 @@
+/****************************************************************************************[XAlloc.h]
+Copyright (c) 2009-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_XAlloc_h
+#define Minisat_XAlloc_h
+
+#include <errno.h>
+#include <stdlib.h>
+
+namespace Minisat {
+
+//=================================================================================================
+// Simple layer on top of malloc/realloc to catch out-of-memory situtaions and provide some typing:
+
+class OutOfMemoryException{};
+static inline void* xrealloc(void *ptr, size_t size)
+{
+ void* mem = realloc(ptr, size);
+ if (mem == NULL && errno == ENOMEM){
+ throw OutOfMemoryException();
+ }else
+ return mem;
+}
+
+//=================================================================================================
+}
+
+#endif
diff -uprN open-wbo.orig/solvers/cryptominisat4/utils/Options.cc open-wbo/solvers/cryptominisat4/utils/Options.cc
--- open-wbo.orig/solvers/cryptominisat4/utils/Options.cc 1969-12-31 19:00:00.000000000 -0500
+++ open-wbo/solvers/cryptominisat4/utils/Options.cc 2015-01-02 23:11:06.000000000 -0500
@@ -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 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 -uprN open-wbo.orig/solvers/cryptominisat4/utils/Options.h open-wbo/solvers/cryptominisat4/utils/Options.h
--- open-wbo.orig/solvers/cryptominisat4/utils/Options.h 1969-12-31 19:00:00.000000000 -0500
+++ open-wbo/solvers/cryptominisat4/utils/Options.h 2015-01-02 23:11:06.000000000 -0500
@@ -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 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 -uprN open-wbo.orig/solvers/cryptominisat4/utils/ParseUtils.h open-wbo/solvers/cryptominisat4/utils/ParseUtils.h
--- open-wbo.orig/solvers/cryptominisat4/utils/ParseUtils.h 1969-12-31 19:00:00.000000000 -0500
+++ open-wbo/solvers/cryptominisat4/utils/ParseUtils.h 2015-01-02 23:11:06.000000000 -0500
@@ -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 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 -uprN open-wbo.orig/solvers/cryptominisat4/utils/System.cc open-wbo/solvers/cryptominisat4/utils/System.cc
--- open-wbo.orig/solvers/cryptominisat4/utils/System.cc 1969-12-31 19:00:00.000000000 -0500
+++ open-wbo/solvers/cryptominisat4/utils/System.cc 2015-01-02 23:11:06.000000000 -0500
@@ -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 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 -uprN open-wbo.orig/solvers/cryptominisat4/utils/System.h open-wbo/solvers/cryptominisat4/utils/System.h
--- open-wbo.orig/solvers/cryptominisat4/utils/System.h 1969-12-31 19:00:00.000000000 -0500
+++ open-wbo/solvers/cryptominisat4/utils/System.h 2015-01-02 23:11:06.000000000 -0500
@@ -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 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment