projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 933a1ea) | patch
* merging some uf stuff from incremental_work branch that somehow nobody merged-in
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Mon, 12 Dec 2011 09:47:37 +0000 (09:47 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Mon, 12 Dec 2011 09:47:37 +0000 (09:47 +0000)
commit6d04f19e1c1fbf7714fbb95dc62648ac44b419dd
tree7f5486f7b4a88323708f693b5905afb6375d8ca3tree
parent933a1ea506fd553e756be942087ef82154b6f959commit | diff
* merging some uf stuff from incremental_work branch that somehow nobody merged-in
* since two theories can propagate the same literal minisat now explicitly checks that a propagated literal has not been asserted yet
src/prop/minisat/core/Solver.cc diff | blob | history
src/theory/arith/difference_manager.cpp diff | blob | history
src/theory/uf/equality_engine.h diff | blob | history
src/theory/uf/equality_engine_impl.h diff | blob | history
src/theory/uf/theory_uf.cpp diff | blob | history