projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9154e64) | patch
Changes to SAT solver:
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Wed, 16 May 2012 17:53:41 +0000 (17:53 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Wed, 16 May 2012 17:53:41 +0000 (17:53 +0000)
commit5ec347a55a3b32e9d92d8a6a5d683cb9f3f3fee5
tree871a53d147d218f926d53421b48db872c9d6747dtree
parent9154e647013e4575f60807d5b73582bccfd052e2commit | diff
Changes to SAT solver:
* allowing propagation of false literals (handles conflict)
* allowing lemmas during BCP (bug 337)
* UF does direct propagation, without checking for literal value anymore
src/prop/minisat/core/Solver.cc diff | blob | history
src/theory/term_registration_visitor.cpp diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/uf/theory_uf.cpp diff | blob | history