projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 41aba71) | patch
- Creates a queue for lemmas discovered during the simplex procedure. Lemmas are...
authorTim King <taking@cs.nyu.edu>
Thu, 3 Mar 2011 18:00:35 +0000 (18:00 +0000)
committerTim King <taking@cs.nyu.edu>
Thu, 3 Mar 2011 18:00:35 +0000 (18:00 +0000)
commit43bf1fc1ba1770715fbe9fa15fa0be2cf6fb164a
tree83ba0646f082451e93ffb848d7c4976a6a72b0cftree
parent41aba7156ae5954db53daf69cca2816a2c4d774dcommit | diff
- Creates a queue for lemmas discovered during the simplex procedure. Lemmas are sent to the sat solver during theory propagation. The lemmas currently come from additional conflicts that are discovered by findConflictOnTheQueue(...).
src/theory/arith/arith_utilities.h diff | blob | history
src/theory/arith/simplex.cpp diff | blob | history
src/theory/arith/simplex.h diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history