projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b44f183) | patch
congruence closure module now supports things other than APPLY_UF; ported from "array...
authorMorgan Deters <mdeters@gmail.com>
Tue, 14 Dec 2010 21:07:46 +0000 (21:07 +0000)
committerMorgan Deters <mdeters@gmail.com>
Tue, 14 Dec 2010 21:07:46 +0000 (21:07 +0000)
commit96ce991a4b8593f7ec831c3a9b40b214d2ac3761
treebf804dcc18a20394a6fba8ac4bed6932ca4c7c02tree
parentb44f183a75deea11fa379554b893b6656e1864b2commit | diff
congruence closure module now supports things other than APPLY_UF; ported from "arrays" branch to trunk
src/expr/node_manager.cpp diff | blob | history
src/expr/node_manager.h diff | blob | history
src/expr/type_constant.h diff | blob | history
src/printer/Makefile.am diff | blob | history
src/theory/uf/morgan/theory_uf_morgan.h diff | blob | history
src/util/congruence_closure.h diff | blob | history
test/unit/util/congruence_closure_white.h diff | blob | history