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
treebf804dcc18a20394a6fba8ac4bed6932ca4c7c02
parentb44f183a75deea11fa379554b893b6656e1864b2
congruence closure module now supports things other than APPLY_UF; ported from "arrays" branch to trunk
src/expr/node_manager.cpp
src/expr/node_manager.h
src/expr/type_constant.h
src/printer/Makefile.am
src/theory/uf/morgan/theory_uf_morgan.h
src/util/congruence_closure.h
test/unit/util/congruence_closure_white.h