diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-07 10:24:04 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-07 23:48:49 -0500 |
commit | d01269e2d5a02952fbda74dcd9629acfbf23dfd4 (patch) | |
tree | d8f2a90ddd94ade15edf84b48523e7ff76f78554 /src/util | |
parent | 01cff049fac316d84ee05f747975a26b04e9c3a2 (diff) |
Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodies; fix bug 551, improper ITE removal under quantifiers.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/ite_removal.cpp | 138 | ||||
-rw-r--r-- | src/util/ite_removal.h | 30 |
2 files changed, 91 insertions, 77 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 */ diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h index c2464636e..de5f83f27 100644 --- a/src/util/ite_removal.h +++ b/src/util/ite_removal.h @@ -23,17 +23,19 @@ #include "util/dump.h" #include "context/context.h" #include "context/cdinsert_hashmap.h" +#include "util/hash.h" +#include "util/bool.h" namespace CVC4 { namespace theory { -class ContainsTermITEVistor; -} + class ContainsTermITEVisitor; +}/* CVC4::theory namespace */ typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap; class RemoveITE { - typedef context::CDInsertHashMap<Node, Node, NodeHashFunction> ITECache; + typedef context::CDInsertHashMap< std::pair<Node, bool>, Node, PairHashFunction<Node, bool, NodeHashFunction, BoolHashFunction> > ITECache; ITECache d_iteCache; @@ -59,22 +61,28 @@ public: * ite created in conjunction with that skolem variable. */ Node run(TNode node, std::vector<Node>& additionalAssertions, - IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar); + IteSkolemMap& iteSkolemMap, bool inQuant); - /** Returns true if e contains a term ite.*/ - bool containsTermITE(TNode e); + /** + * Substitute under node using pre-existing cache. Do not remove + * any ITEs not seen during previous runs. + */ + Node replace(TNode node, bool inQuant = false) const; + + /** Returns true if e contains a term ite. */ + bool containsTermITE(TNode e) const; - /** Returns the collected size of the caches.*/ + /** Returns the collected size of the caches. */ size_t collectedCacheSizes() const; - /** Garbage collects non-context dependent data-structures.*/ + /** Garbage collects non-context dependent data-structures. */ void garbageCollect(); - /** Return the RemoveITE's containsVisitor.*/ - theory::ContainsTermITEVistor* getContainsVisitor(); + /** Return the RemoveITE's containsVisitor. */ + theory::ContainsTermITEVisitor* getContainsVisitor(); private: - theory::ContainsTermITEVistor* d_containsVisitor; + theory::ContainsTermITEVisitor* d_containsVisitor; };/* class RemoveTTE */ |