diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-05 16:21:50 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-05 16:21:50 +0000 |
commit | 7342d1ca87397f3d5beb2c04b819243303e69a7c (patch) | |
tree | 9e166f1884275be7d4b33b13b8bcfe9418e61033 /src/util/ite_removal.cpp | |
parent | af25c3f8498198dd6dd114c3b4ef39af54611e1e (diff) |
updated preprocessing and rewriting input equalities into inequalities for LRA
Diffstat (limited to 'src/util/ite_removal.cpp')
-rw-r--r-- | src/util/ite_removal.cpp | 94 |
1 files changed, 94 insertions, 0 deletions
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp new file mode 100644 index 000000000..e9c5122b3 --- /dev/null +++ b/src/util/ite_removal.cpp @@ -0,0 +1,94 @@ +/********************* */ +/*! \file ite_removal.cpp + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Representation of cardinality + ** + ** Simple class to represent a cardinality; used by the CVC4 type system + ** give the cardinality of sorts. + **/ + +#include <vector> + +#include "util/ite_removal.h" +#include "theory/rewriter.h" + +using namespace CVC4; +using namespace std; + +struct IteRewriteAttrTag {}; +typedef expr::Attribute<IteRewriteAttrTag, Node> IteRewriteAttr; + +void RemoveITE::run(std::vector<Node>& output) { + for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { + output[i] = run(output[i], output); + } +} + +Node RemoveITE::run(TNode node, std::vector<Node>& output) +{ + // Current node + Debug("ite") << "removeITEs(" << node << ")" << endl; + + // The result may be cached already + Node cachedRewrite; + NodeManager *nodeManager = NodeManager::currentNM(); + if(nodeManager->getAttribute(node, IteRewriteAttr(), cachedRewrite)) { + Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl; + return cachedRewrite.isNull() ? Node(node) : cachedRewrite; + } + + // If an ITE replace it + if(node.getKind() == kind::ITE) { + TypeNode nodeType = node.getType(); + if(!nodeType.isBoolean()) { + // Make the skolem to represent the ITE + Node skolem = nodeManager->mkVar(nodeType); + + // The new assertion + Node newAssertion = nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2])); + Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; + + // Attach the skolem + nodeManager->setAttribute(node, IteRewriteAttr(), skolem); + + // Remove ITEs from the new assertion, rewrite it and push it to the output + output.push_back(run(newAssertion, output)); + + // The representation is now the skolem + return skolem; + } + } + + // If not an ITE, go deep + vector<Node> newChildren; + bool somethingChanged = false; + if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { + newChildren.push_back(node.getOperator()); + } + // Remove the ITEs from the children + for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { + Node newChild = run(*it, output); + somethingChanged |= (newChild != *it); + newChildren.push_back(newChild); + } + + // If changes, we rewrite + if(somethingChanged) { + cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren); + nodeManager->setAttribute(node, IteRewriteAttr(), cachedRewrite); + return cachedRewrite; + } else { + nodeManager->setAttribute(node, IteRewriteAttr(), Node::null()); + return node; + } +}; |