Patch from Markus Groß. Thanks. Here is the description that Markus provided:

1. To fix a missing boost header the src/sat/Makefile has to be fixed
This is mentioned and described here: http://groups.google.com/group/stp-users/browse_thread/thread/94246a7cf288d57

2. To fix compile errors regarding PRIu64 the src/sat/mtl/IntTypes.h has to be renamed.
Because most osx systems have a case insensitive file system #include <inttypes.h> includes the src/sat/mtl/IntTypes.h and therefore the inttypes.h from the c library is never included.
I renamed the file from IntTypes.h to IntTypesMtl.h.
This fixes the bug reported here: http://groups.google.com/group/stp-users/browse_thread/thread/c00ab4b90c4ae86a

3. In src/sat/cryptominisat2/ClauseAllocator.h I changed two variable types from uint to uint32_t (otherwise I get: unknown type uint)

4. In src/sat/utils/System.cc
The part ifdef __APPLE__ is missing the memUsedPeak function which leads to an linker error.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1028 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/sat/Makefile b/src/sat/Makefile
index 4b89533c858cda7dc35c544e1669923d9c5041dd..57de857b8b9a4233c733bc745b388e3ac2dd7598 100644 (file)
--- a/src/sat/Makefile
+++ b/src/sat/Makefile
@@ -27,4 +27,4 @@ clean:
        $(MAKE) -C cryptominisat2 clean
 
 CryptoMinisat.o: CryptoMinisat.cpp
-       $(CC) $(CFLAGS) -Icryptominisat2/mtl -Imtl CryptoMinisat.cpp -c 
+       $(CC) $(CFLAGS) -Icryptominisat2/mtl -Imtl CryptoMinisat.cpp -c -I$(TOP)/src

diff --git a/src/sat/core/SolverTypes.h b/src/sat/core/SolverTypes.h
index b04a2598c193d0b32e9a7ef556f04c9507ace22c..c193378b1a93ef8bb35b0ecc40998a19b5746d0e 100644 (file)
--- a/src/sat/core/SolverTypes.h
+++ b/src/sat/core/SolverTypes.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include <assert.h>
 
-#include "../mtl/IntTypes.h"
+#include "../mtl/IntTypesMtl.h"
 #include "../mtl/Alg.h"
 #include "../mtl/Vec.h"
 #include "../mtl/Map.h"

diff --git a/src/sat/cryptominisat2/ClauseAllocator.h b/src/sat/cryptominisat2/ClauseAllocator.h
index db38eea0db6d792e4ec6a6f33cd240a451b5eeeb..4bf378a913d0d2e6c2bc9d79c01687491e81a905 100644 (file)
--- a/src/sat/cryptominisat2/ClauseAllocator.h
+++ b/src/sat/cryptominisat2/ClauseAllocator.h
@@ -47,9 +47,9 @@ class ClauseAllocator {
         ~ClauseAllocator();
         
         template<class T>
-        Clause* Clause_new(const T& ps, const uint group, const bool learnt = false);
+        Clause* Clause_new(const T& ps, const uint32_t group, const bool learnt = false);
         template<class T>
-        XorClause* XorClause_new(const T& ps, const bool inverted, const uint group);
+        XorClause* XorClause_new(const T& ps, const bool inverted, const uint32_t group);
         Clause* Clause_new(Clause& c);
 
         const ClauseOffset getOffset(const Clause* ptr) const;

diff --git a/src/sat/mtl/IntTypes.h b/src/sat/mtl/IntTypesMtl.h
similarity index 100%
rename from src/sat/mtl/IntTypes.h
rename to src/sat/mtl/IntTypesMtl.h

diff --git a/src/sat/mtl/Map.h b/src/sat/mtl/Map.h
index 6ff7a070de0b8a66171a25662dd89cfa977ca02a..0655d1f9f99bf52f2fb41ee81d4eb0b0b362865b 100644 (file)
--- a/src/sat/mtl/Map.h
+++ b/src/sat/mtl/Map.h
@@ -20,7 +20,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_Map_h
 #define Minisat_Map_h
 
-#include "../mtl/IntTypes.h"
+#include "../mtl/IntTypesMtl.h"
 #include "../mtl/Vec.h"
 
 namespace Minisat {

diff --git a/src/sat/mtl/Vec.h b/src/sat/mtl/Vec.h
index a46acd67e376206a071e1f85ffcb7fe9b5dc5234..fac0a0d83181a02e6d7daccb6e6743bfaa2e3992 100644 (file)
--- a/src/sat/mtl/Vec.h
+++ b/src/sat/mtl/Vec.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <assert.h>
 #include <new>
 
-#include "../mtl/IntTypes.h"
+#include "../mtl/IntTypesMtl.h"
 #include "../mtl/XAlloc.h"
 
 namespace Minisat {

diff --git a/src/sat/utils/Options.h b/src/sat/utils/Options.h
index 7850c33b6ab2030372dec2b3ef44ae8382931c35..08f6491a44e709eebd10528cffc217f6d44f0fdb 100644 (file)
--- a/src/sat/utils/Options.h
+++ b/src/sat/utils/Options.h
@@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <math.h>
 #include <string.h>
 
-#include "../mtl/IntTypes.h"
+#include "../mtl/IntTypesMtl.h"
 #include "../mtl/Vec.h"
 #include "../utils/ParseUtils.h"
 

diff --git a/src/sat/utils/System.cc b/src/sat/utils/System.cc
index 2af492fc1a1f588d0f856f2c1466da0bcf67dda1..aaa3c295c4121a4436b0eb23938bb2f9002e5af5 100644 (file)
--- a/src/sat/utils/System.cc
+++ b/src/sat/utils/System.cc
@@ -88,7 +88,7 @@ double Minisat::memUsed(void) {
     malloc_statistics_t t;
     malloc_zone_statistics(NULL, &t);
     return (double)t.max_size_in_use / (1024*1024); }
-
+double Minisat::memUsedPeak(void) { return memUsed();}
 #else
 double Minisat::memUsed() { 
     return 0; }

diff --git a/src/sat/utils/System.h b/src/sat/utils/System.h
index 2098872866aa79c4ee9535f3184bf5ae57535df9..72f4aa3f8d2ec8411c02eee10e64855f34af470a 100644 (file)
--- a/src/sat/utils/System.h
+++ b/src/sat/utils/System.h
@@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <fpu_control.h>
 #endif
 
-#include "../mtl/IntTypes.h"
+#include "../mtl/IntTypesMtl.h"
 
 //-------------------------------------------------------------------------------------------------