diff options
| author | Tim King <taking@cs.nyu.edu> | 2010-05-28 20:17:48 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2010-05-28 20:17:48 +0000 |
| commit | 7d9d562bb560cb4b83ffaaf94918f834916dad2f (patch) | |
| tree | 0ebef47f2ea702d36afe53fb9e82ac31304811be /src/prop/cnf_stream.h | |
| parent | 4806691be59909eeaecb0fa652d84e40c966fe2e (diff) | |
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.
Diffstat (limited to 'src/prop/cnf_stream.h')
| -rw-r--r-- | src/prop/cnf_stream.h | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 1ea600322..a574adf23 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -215,9 +215,6 @@ private: SatLiteral handleAnd(TNode node); SatLiteral handleOr(TNode node); - struct IteRewriteTag {}; - typedef expr::Attribute<IteRewriteTag, Node> IteRewriteAttr; - Node handleNonAtomicNode(TNode node); /** * Transforms the node into CNF recursively. |