git.unchartedbackwaters.co.uk Git - francis/stp.git/commit

]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit

author	trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
	Mon, 5 Jul 2010 04:43:52 +0000 (04:43 +0000)
committer	trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
	Mon, 5 Jul 2010 04:43:52 +0000 (04:43 +0000)
commit	cef8b193fa6528cfa051be78b3201460addea28a
tree	800a5786e5663293fdb29e7f46e4969ddfcea981	tree \| snapshot
parent	0daef886b5269c246f64a67180897a3939eff8e9	commit \| diff

Add the interface code for constant bit propagation. This isn't all of the code, just the code required to interface with the bit blaster.

This code isn't called. So this patch doesn't change STP at all.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@923 e59a4935-1847-0410-ae03-e826735625c1

15 files changed:

src/STPManager/UserDefinedFlags.h		diff \| blob \| history
src/simplifier/Makefile		diff \| blob \| history
src/simplifier/SubstitutionMap.cpp		diff \| blob \| history
src/simplifier/SubstitutionMap.h		diff \| blob \| history
src/simplifier/constantBitP/ConstantBitP_Utility.cpp	[new file with mode: 0644]	blob
src/simplifier/constantBitP/ConstantBitP_Utility.h	[new file with mode: 0644]	blob
src/simplifier/constantBitP/ConstantBitPropagation.cpp	[new file with mode: 0644]	blob
src/simplifier/constantBitP/ConstantBitPropagation.h	[new file with mode: 0644]	blob
src/simplifier/constantBitP/Dependencies.h	[new file with mode: 0644]	blob
src/simplifier/constantBitP/FixedBits.cpp	[new file with mode: 0644]	blob
src/simplifier/constantBitP/FixedBits.h	[new file with mode: 0644]	blob
src/simplifier/constantBitP/NodeToFixedBitsMap.h	[new file with mode: 0644]	blob
src/simplifier/constantBitP/WorkList.h	[new file with mode: 0644]	blob
src/to-sat/BitBlaster.cpp		diff \| blob \| history
src/to-sat/BitBlaster.h		diff \| blob \| history

STP Constraint Solver.

RSS Atom