]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
projects / francis / stp.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 009d243) | patch
Improvement. Add a size reducing phase prior to performing simplifications that may...
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sat, 12 Mar 2011 12:28:33 +0000 (12:28 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sat, 12 Mar 2011 12:28:33 +0000 (12:28 +0000)
commitc02442c8199134894c1fb2eb6232030f756bfb45
tree2088f92df10ff273ad99f23c04717f5d38a41ee9tree | snapshot
parent009d243b1c0cc57b1cbd7a4b5a248cf914159fa9commit | diff
Improvement. Add a size reducing phase prior to performing simplifications that may increase the size of the problem. If the the DAG gets bigger by some amount, then we revert back to the saved copy of the problem.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1202 e59a4935-1847-0410-ae03-e826735625c1
src/STPManager/STP.cpp diff | blob | history
src/STPManager/STP.h diff | blob | history
src/simplifier/SubstitutionMap.h diff | blob | history
src/simplifier/constantBitP/ConstantBitPropagation.cpp diff | blob | history
src/simplifier/constantBitP/ConstantBitPropagation.h diff | blob | history
src/simplifier/simplifier.h diff | blob | history
STP Constraint Solver.