diff options
Diffstat (limited to 'src/util/ite_removal.cpp')
-rw-r--r-- | src/util/ite_removal.cpp | 138 |
1 files changed, 72 insertions, 66 deletions
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp index 0dfea4399..1ceedc688 100644 --- a/src/util/ite_removal.cpp +++ b/src/util/ite_removal.cpp @@ -18,7 +18,6 @@ #include "util/ite_removal.h" #include "expr/command.h" -#include "theory/quantifiers/options.h" #include "theory/ite_utilities.h" using namespace CVC4; @@ -29,7 +28,7 @@ namespace CVC4 { RemoveITE::RemoveITE(context::UserContext* u) : d_iteCache(u) { - d_containsVisitor = new theory::ContainsTermITEVistor(); + d_containsVisitor = new theory::ContainsTermITEVisitor(); } RemoveITE::~RemoveITE(){ @@ -40,7 +39,7 @@ void RemoveITE::garbageCollect(){ d_containsVisitor->garbageCollect(); } -theory::ContainsTermITEVistor* RemoveITE::getContainsVisitor(){ +theory::ContainsTermITEVisitor* RemoveITE::getContainsVisitor() { return d_containsVisitor; } @@ -51,22 +50,20 @@ size_t RemoveITE::collectedCacheSizes() const{ void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap) { for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { - std::vector<Node> quantVar; // 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, quantVar); + Node itesRemoved = run(output[i], output, iteSkolemMap, false); output[i] = itesRemoved; } } -bool RemoveITE::containsTermITE(TNode e){ +bool RemoveITE::containsTermITE(TNode e) const { return d_containsVisitor->containsTermITE(e); } Node RemoveITE::run(TNode node, std::vector<Node>& output, - IteSkolemMap& iteSkolemMap, - std::vector<Node>& quantVar) { + IteSkolemMap& iteSkolemMap, bool inQuant) { // Current node Debug("ite") << "removeITEs(" << node << ")" << endl; @@ -76,35 +73,28 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, } // The result may be cached already + std::pair<Node, bool> cacheKey(node, inQuant); NodeManager *nodeManager = NodeManager::currentNM(); - ITECache::const_iterator i = d_iteCache.find(node); + 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())) { +Debug("ite") << "CAN REMOVE ITE " << node << " BECAUSE " << inQuant << " " << node.hasBoundVar() << endl; Node skolem; // Make the skolem to represent the ITE - if( quantVar.empty() ){ - skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal"); - }else{ - //if in the scope of free variables, make a skolem operator - vector< TypeNode > argTypes; - for( size_t i=0; i<quantVar.size(); i++ ){ - argTypes.push_back( quantVar[i].getType() ); - } - TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, nodeType ); - Node op = NodeManager::currentNM()->mkSkolem( "termITEop_$$", typ, "a function variable introduced due to term-level ITE removal" ); - vector< Node > funcArgs; - funcArgs.push_back( op ); - funcArgs.insert( funcArgs.end(), quantVar.begin(), quantVar.end() ); - skolem = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs ); - } + skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal"); // The new assertion Node newAssertion = @@ -113,18 +103,10 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; // Attach the skolem - d_iteCache.insert(node, 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, quantVar); - - if( !quantVar.empty() ){ - //if in the scope of free variables, it is a quantified assertion - vector< Node > children; - children.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, quantVar ) ); - children.push_back( newAssertion ); - newAssertion = NodeManager::currentNM()->mkNode( kind::FORALL, children ); - } + newAssertion = run(newAssertion, output, iteSkolemMap, inQuant); iteSkolemMap[skolem] = output.size(); output.push_back(newAssertion); @@ -135,42 +117,66 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, } // If not an ITE, go deep - if( ( node.getKind() != kind::FORALL || options::iteRemoveQuant() ) && - node.getKind() != kind::EXISTS && - node.getKind() != kind::REWRITE_RULE ) { - std::vector< Node > newQuantVar; - newQuantVar.insert( newQuantVar.end(), quantVar.begin(), quantVar.end() ); - if( node.getKind()==kind::FORALL ){ - for( size_t i=0; i<node[0].getNumChildren(); i++ ){ - newQuantVar.push_back( node[0][i] ); - } - } - 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, iteSkolemMap, newQuantVar); - somethingChanged |= (newChild != *it); - newChildren.push_back(newChild); - } + 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, 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(node, cached); - return cached; - } else { - d_iteCache.insert(node, Node::null()); - return node; - } + // If changes, we rewrite + if(somethingChanged) { + Node cached = nodeManager->mkNode(node.getKind(), newChildren); + d_iteCache.insert(cacheKey, cached); + return cached; } else { - d_iteCache.insert(node, Node::null()); + 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) { + return nodeManager->mkNode(node.getKind(), newChildren); + } else { + return node; + } +} }/* CVC4 namespace */ |