diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 49e4c2a88..2323a305b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -85,4 +85,44 @@ Node TheoryEngine::preprocess(TNode t) { return top; } +Node TheoryEngine::rewrite(TNode in) { + if(inRewriteCache(in)) { + return getRewriteCache(in); + } + + if(in.getKind() == kind::VARIABLE || + in.getKind() == kind::SKOLEM) { + return in; + } + + /* + theory::Theory* thy = theoryOf(in); + if(thy == NULL) { + Node out = rewriteBuiltins(in); + setRewriteCache(in, out); + return in; + } else { + Node out = thy->rewrite(in); + setRewriteCache(in, out); + return out; + } + */ + + if(in.getKind() == kind::EQUAL) { + Assert(in.getNumChildren() == 2); + if(in[0] == in[1]) { + Node out = NodeManager::currentNM()->mkNode(kind::TRUE); + //setRewriteCache(in, out); + return out; + } + } else { + Node out = rewriteChildren(in); + //setRewriteCache(in, out); + return out; + } + + //setRewriteCache(in, in); + return in; +} + }/* CVC4 namespace */ |