]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
projects / francis / stp.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bd7bcd8) | patch
Updating CMS2 to fix two bugs
authormsoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Fri, 16 Apr 2010 12:59:14 +0000 (12:59 +0000)
committermsoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Fri, 16 Apr 2010 12:59:14 +0000 (12:59 +0000)
commitdfcd136299883462bd9ddf916a869210a8cbc6dd
treedba2a38923f752cff3dbd13e557630493e4faff6tree | snapshot
parentbd7bcd8d5ef49da039c61e754f783f28db662ca4commit | diff
Updating CMS2 to fix two bugs

One was a bug relating to binarary xor-finding while doing failed
var searching: the xor-clauses were not cleaned beforehand.

The second bug was an inverted shrinking of memory contents in
operator= of Heap.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@683 e59a4935-1847-0410-ae03-e826735625c1
src/sat/cryptominisat2/BitArray.h diff | blob | history
src/sat/cryptominisat2/FailedVarSearcher.cpp diff | blob | history
src/sat/cryptominisat2/Gaussian.cpp diff | blob | history
src/sat/cryptominisat2/Logger.cpp diff | blob | history
src/sat/cryptominisat2/Logger.h diff | blob | history
src/sat/cryptominisat2/Solver.h diff | blob | history
src/sat/cryptominisat2/Subsumer.cpp diff | blob | history
src/sat/cryptominisat2/VERSION diff | blob | history
STP Constraint Solver.