From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 28 Nov 2010 02:45:43 +0000 (+0000)
Subject: Patch from Markus Groß. Thanks. Here is the description that Markus provided:
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=8d4a9b77bf2ec860f0afe558571daf7349ae4003;p=francis%2Fstp.git

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 4b89533..57de857 100644
--- 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 b04a259..c193378 100644
--- 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 db38eea..4bf378a 100644
--- 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 6ff7a07..0655d1f 100644
--- 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 a46acd6..fac0a0d 100644
--- 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 7850c33..08f6491 100644
--- 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 2af492f..aaa3c29 100644
--- 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 2098872..72f4aa3 100644
--- 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"
 
 //-------------------------------------------------------------------------------------------------