]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
projects / francis / stp.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1ed7e9a) | patch
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
tree48c04d34674ab2828d5421c08e6461939c43c551tree | snapshot
parent1ed7e9aed374bf9974c45895ff528455af8be177commit | diff
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 diff | blob | history
src/sat/cryptominisat2/Conglomerate.cpp diff | blob | history
src/sat/cryptominisat2/FailedVarSearcher.cpp diff | blob | history
src/sat/cryptominisat2/FindUndef.cpp diff | blob | history
src/sat/cryptominisat2/Logger.cpp diff | blob | history
src/sat/cryptominisat2/Makefile diff | blob | history
src/sat/cryptominisat2/Solver.cpp 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
src/sat/cryptominisat2/VarReplacer.cpp diff | blob | history
src/sat/cryptominisat2/constants.h diff | blob | history
STP Constraint Solver.