/********************* */
/*! \file ite_removal.cpp
** \verbatim
- ** Original author: dejan
- ** Major contributors: mdeters
- ** 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
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: Tim King, Morgan Deters
+ ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds, Clark Barrett
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
#include <vector>
#include "util/ite_removal.h"
-#include "theory/rewriter.h"
#include "expr/command.h"
+#include "theory/ite_utilities.h"
+#include "proof/proof_manager.h"
using namespace CVC4;
using namespace std;
namespace CVC4 {
-struct IteRewriteAttrTag {};
-typedef expr::Attribute<IteRewriteAttrTag, Node> IteRewriteAttr;
+RemoveITE::RemoveITE(context::UserContext* u)
+ : d_iteCache(u)
+{
+ d_containsVisitor = new theory::ContainsTermITEVisitor();
+}
+
+RemoveITE::~RemoveITE(){
+ delete d_containsVisitor;
+}
+
+void RemoveITE::garbageCollect(){
+ d_containsVisitor->garbageCollect();
+}
-void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
+theory::ContainsTermITEVisitor* RemoveITE::getContainsVisitor() {
+ return d_containsVisitor;
+}
+
+size_t RemoveITE::collectedCacheSizes() const{
+ return d_containsVisitor->cache_size() + d_iteCache.size();
+}
+
+void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps)
{
+ size_t n = output.size();
for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
- output[i] = run(output[i], output, iteSkolemMap);
+ // Do this in two steps to avoid Node problems(?)
+ // Appears related to bug 512, splitting this into two lines
+ // fixes the bug on clang on Mac OS
+ Node itesRemoved = run(output[i], output, iteSkolemMap, false);
+ // In some calling contexts, not necessary to report dependence information.
+ if(reportDeps && options::unsatCores()) {
+ // new assertions have a dependence on the node
+ PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); )
+ while(n < output.size()) {
+ PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); )
+ ++n;
+ }
+ }
+ output[i] = itesRemoved;
}
}
+bool RemoveITE::containsTermITE(TNode e) const {
+ return d_containsVisitor->containsTermITE(e);
+}
+
Node RemoveITE::run(TNode node, std::vector<Node>& output,
- IteSkolemMap& iteSkolemMap) {
+ IteSkolemMap& iteSkolemMap, bool inQuant) {
// Current node
Debug("ite") << "removeITEs(" << node << ")" << endl;
+ if(node.isVar() || node.isConst() ||
+ (options::biasedITERemoval() && !containsTermITE(node))){
+ return Node(node);
+ }
+
// The result may be cached already
- Node cachedRewrite;
+ std::pair<Node, bool> cacheKey(node, inQuant);
NodeManager *nodeManager = NodeManager::currentNM();
- if(nodeManager->getAttribute(node, IteRewriteAttr(), cachedRewrite)) {
- Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl;
- return cachedRewrite.isNull() ? Node(node) : cachedRewrite;
+ ITECache::const_iterator i = d_iteCache.find(cacheKey);
+ if(i != d_iteCache.end()) {
+ Node cached = (*i).second;
+ Debug("ite") << "removeITEs: in-cache: " << cached << endl;
+ return cached.isNull() ? Node(node) : cached;
+ }
+
+ // Remember that we're inside a quantifier
+ if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+ inQuant = true;
}
// If an ITE replace it
if(node.getKind() == kind::ITE) {
TypeNode nodeType = node.getType();
- if(!nodeType.isBoolean()) {
+ if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) {
+ Node skolem;
// Make the skolem to represent the ITE
- Node skolem = nodeManager->mkVar(nodeType);
-
- Dump.declareVar(skolem.toExpr(), "a variable introduced due to term-level ITE removal");
+ skolem = nodeManager->mkSkolem("termITE", nodeType, "a variable introduced due to term-level ITE removal");
// The new assertion
Node newAssertion =
Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
// Attach the skolem
- nodeManager->setAttribute(node, IteRewriteAttr(), skolem);
+ d_iteCache.insert(cacheKey, skolem);
// Remove ITEs from the new assertion, rewrite it and push it to the output
- newAssertion = run(newAssertion, output, iteSkolemMap);
+ newAssertion = run(newAssertion, output, iteSkolemMap, inQuant);
+
iteSkolemMap[skolem] = output.size();
output.push_back(newAssertion);
}
// Remove the ITEs from the children
for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
- Node newChild = run(*it, output, iteSkolemMap);
+ Node newChild = run(*it, output, iteSkolemMap, inQuant);
+ somethingChanged |= (newChild != *it);
+ newChildren.push_back(newChild);
+ }
+
+ // If changes, we rewrite
+ if(somethingChanged) {
+ Node cached = nodeManager->mkNode(node.getKind(), newChildren);
+ d_iteCache.insert(cacheKey, cached);
+ return cached;
+ } else {
+ d_iteCache.insert(cacheKey, Node::null());
+ return node;
+ }
+}
+
+Node RemoveITE::replace(TNode node, bool inQuant) const {
+ if(node.isVar() || node.isConst() ||
+ (options::biasedITERemoval() && !containsTermITE(node))){
+ return Node(node);
+ }
+
+ // Check the cache
+ NodeManager *nodeManager = NodeManager::currentNM();
+ ITECache::const_iterator i = d_iteCache.find(make_pair(node, inQuant));
+ if(i != d_iteCache.end()) {
+ Node cached = (*i).second;
+ return cached.isNull() ? Node(node) : cached;
+ }
+
+ // Remember that we're inside a quantifier
+ if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+ inQuant = true;
+ }
+
+ vector<Node> newChildren;
+ bool somethingChanged = false;
+ if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ newChildren.push_back(node.getOperator());
+ }
+ // Replace in children
+ for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
+ Node newChild = replace(*it, inQuant);
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;
+ return nodeManager->mkNode(node.getKind(), newChildren);
} else {
- nodeManager->setAttribute(node, IteRewriteAttr(), Node::null());
return node;
}
}