]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
projects / francis / stp.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 310e6a3) | patch
Measure the difficulty of formula by using a simple function, that amongst other...
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Fri, 25 Jun 2010 05:25:17 +0000 (05:25 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Fri, 25 Jun 2010 05:25:17 +0000 (05:25 +0000)
commit8022a9f782ea95f366ac1009d26b106f83913bfb
tree37fcf32c05f899362803d509e38dc0f93cc64674tree | snapshot
parent310e6a3e7fbba4f749271cccc9d97305aa0a4ac3commit | diff
Measure the difficulty of formula by using a simple function, that amongst other things counts the number of multiplications in the input. If after simplifications the difficulty has increased. Then the original formula is used instead of the not-simplified one.

This is a very rough way of performing DAG aware simplifications.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@885 e59a4935-1847-0410-ae03-e826735625c1
src/STPManager/DifficultyScore.h [new file with mode: 0644] blob
src/STPManager/STP.cpp diff | blob | history
src/simplifier/simplifier.cpp diff | blob | history
src/simplifier/simplifier.h diff | blob | history
STP Constraint Solver.