Moving the ITE removal from CnfStream to TheoryEngine, which is a bit closer to its...
authorTim King <taking@cs.nyu.edu>
Fri, 28 May 2010 20:17:48 +0000 (20:17 +0000)
committerTim King <taking@cs.nyu.edu>
Fri, 28 May 2010 20:17:48 +0000 (20:17 +0000)
commit7d9d562bb560cb4b83ffaaf94918f834916dad2f
tree0ebef47f2ea702d36afe53fb9e82ac31304811be
parent4806691be59909eeaecb0fa652d84e40c966fe2e
Moving the ITE removal from CnfStream to TheoryEngine, which is a bit closer to its final destination. Added a basic rewriter to TheoryUF. (x=x rewrites to true.) Added DIVISION to src/expr/node_manager.cpp's getType. Fixed the theory returned for variables in theoryOf() for bool and arith. Fixed TheoryEngine rewrite children to properly handle APPLY_UFs. Removed the special case for equality in TheoryEngine rewrite. A few tests are currently broken due to deallocation errors. Morgan and I will try to commit a fix to this in a little bit.
src/expr/node_manager.cpp
src/prop/cnf_stream.cpp
src/prop/cnf_stream.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/theory_uf.cpp
src/theory/uf/theory_uf.h