]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
projects / francis / stp.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6553049) | patch
Should cause not runtime effects.
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sat, 14 Aug 2010 01:56:11 +0000 (01:56 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sat, 14 Aug 2010 01:56:11 +0000 (01:56 +0000)
commit9ca8b1e335185cf9e4948f5c8713a2791aab0dc0
treeefc5d2b4940e3c318254f75849cc8299051a6758tree | snapshot
parent655304903a7899571a888808752002fabb520b86commit | diff
Should cause not runtime effects.

Add a new multiplication variant that uses bounds discovered during constant bit propagation to more efficiently encode multiplications.

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