]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
projects / francis / stp.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1b78551) | patch
Put the clauses of the SAT solver in a separate heap. This reduces the number of...
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sun, 13 Jun 2010 14:19:33 +0000 (14:19 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sun, 13 Jun 2010 14:19:33 +0000 (14:19 +0000)
commitb3f7f0dc79832c67eeeee760ad6b673f4acc79b9
tree9c22d1d2dc31bf65baff5a725abac340e4ef4ea3tree | snapshot
parent1b7855194005d5aa0adb244ec22124144deb841ecommit | diff
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 diff | blob | history
src/sat/Makefile diff | blob | history
src/sat/core/Makefile diff | blob | history
src/sat/core/Solver.C diff | blob | history
src/sat/core/SolverTypes.h diff | blob | history
src/sat/simp/Makefile diff | blob | history
STP Constraint Solver.