]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
projects / francis / stp.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a16d688) | patch
Free up more memory before SAT solving. In particular this deletes the Tseitin variab...
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sat, 12 Jun 2010 14:55:37 +0000 (14:55 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sat, 12 Jun 2010 14:55:37 +0000 (14:55 +0000)
commit1b7855194005d5aa0adb244ec22124144deb841e
treefe14be0b504a7c4b54a14d8faeb7b7002347f64etree | snapshot
parenta16d68889ba8e43831e7168440e14007f5d34675commit | diff
Free up more memory before SAT solving. In particular this deletes the Tseitin variables before calling the SAT solver. This makes good sense for problems that aren't solved by abstraction / refinement. However, I'm not sure how it impacts difficult array problems.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@836 e59a4935-1847-0410-ae03-e826735625c1
src/STPManager/STP.cpp diff | blob | history
src/STPManager/STPManager.cpp diff | blob | history
src/absrefine_counterexample/CounterExample.cpp diff | blob | history
src/simplifier/simplifier.cpp diff | blob | history
src/simplifier/simplifier.h diff | blob | history
src/to-sat/ToSAT.cpp diff | blob | history
src/to-sat/ToSAT.h diff | blob | history
STP Constraint Solver.