Merge from theory-break-dependences branch to break Theory and TheoryEngine dependenc...
authorMorgan Deters <mdeters@gmail.com>
Sat, 26 Feb 2011 21:24:18 +0000 (21:24 +0000)
committerMorgan Deters <mdeters@gmail.com>
Sat, 26 Feb 2011 21:24:18 +0000 (21:24 +0000)
commitedf6aaa87da179948e6b233d16fa37d2aea58bbb
treefc5429ce891f579b6e5daedd52e423c13d4f4ec8
parent5c9af4e1382d32352aae7f8c31795831882931b2
Merge from theory-break-dependences branch to break Theory and TheoryEngine dependences; now, if you touch theory_engine.h, only a few things in theory need be recompiled (TheoryEngine, SharedTermManager, .... but no theory implementations), along with the PropEngine and SmtEngine.  If you touch a specific theory's .h file, only that theory must be recompiled (along with the TheoryEngine, since it uses traits, and SmtEngine, since it tells the TheoryEngine which theory implementations to use).
21 files changed:
src/theory/Makefile.am
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h
src/theory/arrays/theory_arrays.cpp
src/theory/arrays/theory_arrays.h
src/theory/booleans/theory_bool.cpp
src/theory/booleans/theory_bool.h
src/theory/builtin/theory_builtin.cpp
src/theory/builtin/theory_builtin.h
src/theory/bv/theory_bv.cpp
src/theory/bv/theory_bv.h
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/morgan/theory_uf_morgan.cpp
src/theory/uf/morgan/theory_uf_morgan.h
src/theory/uf/tim/theory_uf_tim.h
src/theory/valuation.cpp [new file with mode: 0644]
src/theory/valuation.h [new file with mode: 0644]
test/unit/theory/theory_black.h
test/unit/theory/theory_engine_white.h