diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 2323a305b..f953f97b9 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -90,8 +90,7 @@ Node TheoryEngine::rewrite(TNode in) { return getRewriteCache(in); } - if(in.getKind() == kind::VARIABLE || - in.getKind() == kind::SKOLEM) { + if(in.getMetaKind() == kind::metakind::VARIABLE) { return in; } @@ -108,6 +107,7 @@ Node TheoryEngine::rewrite(TNode in) { } */ + // these special cases should go away when theory rewriting comes online if(in.getKind() == kind::EQUAL) { Assert(in.getNumChildren() == 2); if(in[0] == in[1]) { @@ -115,6 +115,22 @@ Node TheoryEngine::rewrite(TNode in) { //setRewriteCache(in, out); return out; } + } else if(in.getKind() == kind::DISTINCT) { + vector<Node> diseqs; + for(TNode::iterator i = in.begin(); i != in.end(); ++i) { + TNode::iterator j = i; + while(++j != in.end()) { + Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, *i, *j); + Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq); + diseqs.push_back(neq); + } + } + Node out = + diseqs.size() == 1 + ? diseqs[0] + : NodeManager::currentNM()->mkNode(CVC4::kind::AND, diseqs); + //setRewriteCache(in, out); + return out; } else { Node out = rewriteChildren(in); //setRewriteCache(in, out); |