From b3f7f0dc79832c67eeeee760ad6b673f4acc79b9 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 13 Jun 2010 14:19:33 +0000 Subject: [PATCH] Put the clauses of the SAT solver in a separate heap. This reduces the number of cache misses in the inner loop of the SAT solver, but increases the amount of memory STP uses. 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 --- scripts/Makefile.common | 2 ++ src/sat/Makefile | 2 +- src/sat/core/Makefile | 17 +++-------------- src/sat/core/Solver.C | 26 +++++++++++++++++++++++--- src/sat/core/SolverTypes.h | 7 ++++++- src/sat/simp/Makefile | 5 +++-- 6 files changed, 38 insertions(+), 21 deletions(-) diff --git a/scripts/Makefile.common b/scripts/Makefile.common index a01953b..566a235 100644 --- 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 3577118..682f124 100644 --- 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 ce26507..b70b92d 100644 --- 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 8523996..0de1223 100644 --- 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 b9ee0df..1223184 100644 --- 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 #include +#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 7158c19..0ed8881 100644 --- 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 -- 2.47.3