Put the clauses of the SAT solver in a separate heap. This reduces the number of...

I'm not yet sure if the extra memory usage is justified.

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

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index a01953bfb3770619160d955e4edbf51d03949c34..566a235f5921e84c90e416410ea8bd512236b506 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -74,6 +74,8 @@ else
   CFLAGS = $(CFLAGS_BASE) $(CFLAGS_M32) -I../AST
 endif
 
+CFLAGS += -DONLY_MSPACES -DMSPACES
+
 #CXXFLAGS = $(CFLAGS) -Wall -Wextra -DEXT_HASH_MAP -Wno-deprecated
 #CXXFLAGS = $(CFLAGS) -Wextra -DEXT_HASH_MAP -Wno-deprecated
 CXXFLAGS = $(CFLAGS) -DEXT_HASH_MAP -Wno-deprecated

diff --git a/src/sat/Makefile b/src/sat/Makefile
index 35771187b84751de389961d3127134169c4a7f65..682f12489b4c0541ce828583221aa39419358fac 100644 (file)
--- a/src/sat/Makefile
+++ b/src/sat/Makefile
@@ -1,6 +1,6 @@
 .PHONY: core
 core:
-       $(MAKE) -C core lib all 
+       $(MAKE) -C core all     
        $(MAKE) -C simp lib all
 
 .PHONY: cryptominisat2

diff --git a/src/sat/core/Makefile b/src/sat/core/Makefile
index ce26507315e285bb0e9ef0582c37f6e3ab871900..b70b92d055d1580331b8533060dca0fe966d4b32 100644 (file)
--- a/src/sat/core/Makefile
+++ b/src/sat/core/Makefile
@@ -2,22 +2,11 @@ TOP = ../../..
 include $(TOP)/scripts/Makefile.common
 
 MTL       = ../mtl
-SOURCES   = Solver.C
-OBJECTS   = $(SOURCES:.C=.o)
-LIB       = libminisat.a
+SOURCES   = Solver.C dlmalloc.c
+OBJECTS   = Solver.o dlmalloc.o
 CFLAGS    += -I$(MTL) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c
-EXEC      = minisat
-LFLAGS    = -lz
 
-all: $(LIB) #$(EXEC)
-lib: $(LIB)
-
-$(LIB): $(OBJECTS)
-       rm -f $@
-       ar cq $@ $(OBJECTS)
-       ranlib $@
-       cp $(LIB) ../
-       cp $(OBJECTS) ../
+all: $(OBJECTS)
 
 clean:
        rm -f $(OBJECTS) $(LIB)

diff --git a/src/sat/core/Solver.C b/src/sat/core/Solver.C
index 8523996792d425dd3099a885d7c15f9ebfbed71d..0de12236676ca8b2b755d5732676454414a615dc 100644 (file)
--- a/src/sat/core/Solver.C
+++ b/src/sat/core/Solver.C
@@ -23,6 +23,26 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 namespace MINISAT {
 
+/// This creates a separate "memory space" for the clauses built by minisat. This
+/// stops the clauses being mixed in with the rest of STPs data (like ASTNodes).
+/// The memory spaces are separate heaps. More memory is used, but the SAT solver's
+/// clauses are all lumped together in memory so there are fewer data cache misses.
+#if 1
+mspace tlms =0;
+
+void*  tlmalloc(size_t bytes) {
+       if (tlms == 0) tlms = create_mspace(0, 0);
+      return mspace_malloc(tlms, bytes);
+    }
+
+void  tlfree(void* mem) { mspace_free(tlms, mem); }
+#else
+       void*  tlmalloc(size_t bytes) { return malloc(bytes);}
+       void   tlfree(void* mem) { free(tlms); }
+#endif
+///
+
+
 //=================================================================================================
 // Constructor/Destructor:
 
@@ -58,8 +78,8 @@ Solver::Solver() :
 
 Solver::~Solver()
 {
-    for (int i = 0; i < learnts.size(); i++) free(learnts[i]);
-    for (int i = 0; i < clauses.size(); i++) free(clauses[i]);
+    for (int i = 0; i < learnts.size(); i++) tlfree(learnts[i]);
+    for (int i = 0; i < clauses.size(); i++) tlfree(clauses[i]);
 }
 
 
@@ -143,7 +163,7 @@ void Solver::detachClause(Clause& c) {
 
 void Solver::removeClause(Clause& c) {
     detachClause(c);
-    free(&c); }
+    tlfree(&c); }
 
 
 bool Solver::satisfied(const Clause& c) const {

diff --git a/src/sat/core/SolverTypes.h b/src/sat/core/SolverTypes.h
index b9ee0dfc15325a0fe266a02772086ec5a35ae893..1223184603895dd7c43389003685575f79860f44 100644 (file)
--- a/src/sat/core/SolverTypes.h
+++ b/src/sat/core/SolverTypes.h
@@ -23,9 +23,14 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include <cassert>
 #include <stdint.h>
+#define ONLY_MSPACES 1
+#include "dlmalloc.h"
 
 namespace MINISAT{
 
+void*  tlmalloc(size_t bytes);
+void  tlfree(void* mem);
+
 //=================================================================================================
 // Variables, literals, lifted booleans, clauses:
 
@@ -124,7 +129,7 @@ public:
     friend Clause* Clause_new(const V& ps, bool learnt = false) {
         assert(sizeof(Lit)      == sizeof(uint32_t));
         assert(sizeof(float)    == sizeof(uint32_t));
-        void* mem = malloc(sizeof(Clause) + sizeof(uint32_t)*(ps.size()));
+        void* mem = tlmalloc(sizeof(Clause) + sizeof(uint32_t)*(ps.size()));
         return new (mem) Clause(ps, learnt); }
 
     int          size        ()      const   { return size_etc >> 3; }

diff --git a/src/sat/simp/Makefile b/src/sat/simp/Makefile
index 7158c19eda653f5b9d992087e76e9f436dbb9791..0ed8881311a80afa8abcaaa12cc506cc2d664d8d 100644 (file)
--- a/src/sat/simp/Makefile
+++ b/src/sat/simp/Makefile
@@ -2,10 +2,11 @@ TOP = ../../..
 include $(TOP)/scripts/Makefile.common
 
 MTL       = ../mtl
-SOURCES   = SimpSolver.C ../core/Solver.C
+SOURCES   = SimpSolver.C ../core/Solver.C 
 OBJECTS   = $(SOURCES:.C=.o)
+OBJECTS    += ../core/dlmalloc.o
 LIB       = libminisat.a
-CFLAGS    += -I$(MTL) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c
+CFLAGS    += -I$(MTL) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c -DMSPACES
 EXEC      = minisat
 LFLAGS    = -lz