]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
Updating CMS2 to fix some bugs
authormsoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Thu, 22 Apr 2010 11:34:23 +0000 (11:34 +0000)
committermsoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Thu, 22 Apr 2010 11:34:23 +0000 (11:34 +0000)
commit238d688c137cacb67e5ab3d0682a5ab36c2984c7
tree48c04d34674ab2828d5421c08e6461939c43c551
parent1ed7e9aed374bf9974c45895ff528455af8be177
Updating CMS2 to fix some bugs

* Conglomerate was freeing the same clause. Fixed.
* Gaussian elimination is now disabled (was broken)
* Some code cleanup
* After solution extension, propagate was not called when decisionLevel
  was 0. This lead to assertion failure when adding clause during
  library usage

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@699 e59a4935-1847-0410-ae03-e826735625c1
12 files changed:
src/sat/cryptominisat2/ClauseCleaner.cpp
src/sat/cryptominisat2/Conglomerate.cpp
src/sat/cryptominisat2/FailedVarSearcher.cpp
src/sat/cryptominisat2/FindUndef.cpp
src/sat/cryptominisat2/Logger.cpp
src/sat/cryptominisat2/Makefile
src/sat/cryptominisat2/Solver.cpp
src/sat/cryptominisat2/Solver.h
src/sat/cryptominisat2/Subsumer.cpp
src/sat/cryptominisat2/VERSION
src/sat/cryptominisat2/VarReplacer.cpp
src/sat/cryptominisat2/constants.h