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/theory/uf | |
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/theory/uf')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 12 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 8 |
2 files changed, 20 insertions, 0 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 2d7d4e91f..1f09ce81d 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -35,6 +35,18 @@ TheoryUF::TheoryUF(Context* c, OutputChannel& out) : TheoryUF::~TheoryUF() { } +Node TheoryUF::rewrite(TNode n){ + Debug("uf") << "uf: begin rewrite(" << n << ")" << std::endl; + Node ret(n); + if(n.getKind() == EQUAL){ + Assert(n.getNumChildren() == 2); + if(n[0] == n[1]) { + ret = NodeManager::currentNM()->mkConst(true); + } + } + Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << std::endl; + return ret; +} void TheoryUF::preRegisterTerm(TNode n) { Debug("uf") << "uf: begin preRegisterTerm(" << n << ")" << std::endl; Debug("uf") << "uf: end preRegisterTerm(" << n << ")" << std::endl; diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 5863a31fc..be08cfee7 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -119,6 +119,14 @@ public: */ void check(Effort level); + + /** + * Rewrites a node in the theory of uninterpreted functions. + * This is fairly basic and only ensures that atoms that are + * unsatisfiable or a valid are rewritten to false or true respectively. + */ + Node rewrite(TNode n); + /** * Propagates theory literals. Currently does nothing. * |