diff options
author | Tim King <taking@cs.nyu.edu> | 2013-11-25 18:36:06 -0500 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-11-25 18:36:06 -0500 |
commit | 22df6e9e8618614e8c33700c55705266912500ae (patch) | |
tree | 20d78676c1e819517f371e8bc5e6363008fc9154 /src/util | |
parent | 91424455840a7365a328cbcc3d02ec453fe9d0ea (diff) |
Substantial Changes:
-ITE Simplification
-- Moved the utilities in src/theory/ite_simplifier.{h,cpp} to ite_utilities.
-- Separated simpWithCare from simpITE.
-- Disabled ite simplification on repeat simplification by default. Currently, ite simplification cannot help unless we internally make new constant leaf ites equal to constants.
-- simplifyWithCare() is now only run on QF_AUFBV by default. Speeds up nec benchmarks dramatically.
-- Added a new compress ites pass that is only run on QF_LIA by default. This targets the perverse structure of ites generated during ite simplification on nec benchmarks.
-- After ite simplification, if the ite simplifier was used many times and the NodeManager's node pool is large enough, this garbage collects: zombies from the NodeManager repeatedly, the ite simplification caches, and the theory rewrite caches.
- TheoryEngine
-- Added TheoryEngine::donePPSimpITE() which orchestrates a number of ite simplifications above.
-- Switched UnconstrainedSimplifier to a pointer.
- RemoveITEs
-- Added a heuristic for checking whether or not a node contains term ites and if not, not bothering to invoke the rest of RemoveITE::run(). This safely changes the type of the cache used on misses of run. This cache can be cleared in the future. Currently disabled pending additional testing.
- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.
- Theory Bool Rewriter
-- Added additional simplifications for boolean ites.
Minor Changes:
- TheoryModel
-- Removed vestigial copy of the ITESimplifier.
- AttributeManager
-- Fixed a garbage collection bug when deleting the node table caused the NodeManager to reclaimZombies() which caused memory corruption by deleting from the attributeManager.
- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.
-NodeManager
-- Added additional functions for reclaiming zombies.
-- Exposed the size of the node pool for heuristics that worry about memory consumption.
- NaryBuilder
-- Added convenience classes for constructing associative and commutative n-ary operators.
-- Added a pass that turns associative and commutative n-ary operators into binary operators. (Mostly for printing expressions for strict parsers.)
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 2 | ||||
-rw-r--r-- | src/util/ite_removal.cpp | 57 | ||||
-rw-r--r-- | src/util/ite_removal.h | 29 | ||||
-rw-r--r-- | src/util/nary_builder.cpp | 183 | ||||
-rw-r--r-- | src/util/nary_builder.h | 38 |
5 files changed, 292 insertions, 17 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 156288600..5647a2057 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -76,6 +76,8 @@ libutil_la_SOURCES = \ boolean_simplification.cpp \ ite_removal.h \ ite_removal.cpp \ + nary_builder.h \ + nary_builder.cpp \ node_visitor.h \ chain.h \ index.h \ diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp index 7d4948251..5231e05c2 100644 --- a/src/util/ite_removal.cpp +++ b/src/util/ite_removal.cpp @@ -17,15 +17,37 @@ #include <vector> #include "util/ite_removal.h" -#include "theory/rewriter.h" #include "expr/command.h" #include "theory/quantifiers/options.h" +#include "theory/ite_utilities.h" using namespace CVC4; using namespace std; namespace CVC4 { +RemoveITE::RemoveITE(context::UserContext* u) + : d_iteCache(u) +{ + d_containsVisitor = new theory::ContainsTermITEVistor(); +} + +RemoveITE::~RemoveITE(){ + delete d_containsVisitor; +} + +void RemoveITE::garbageCollect(){ + d_containsVisitor->garbageCollect(); +} + +theory::ContainsTermITEVistor* 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) { for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { @@ -38,18 +60,28 @@ void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap) } } +bool RemoveITE::containsTermITE(TNode e){ + return d_containsVisitor->containsTermITE(e); +} + Node RemoveITE::run(TNode node, std::vector<Node>& output, - IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar) { + IteSkolemMap& iteSkolemMap, + std::vector<Node>& quantVar) { // 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 NodeManager *nodeManager = NodeManager::currentNM(); - ITECache::iterator i = d_iteCache.find(node); + ITECache::const_iterator i = d_iteCache.find(node); if(i != d_iteCache.end()) { - Node cachedRewrite = (*i).second; - Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl; - return cachedRewrite.isNull() ? Node(node) : cachedRewrite; + Node cached = (*i).second; + Debug("ite") << "removeITEs: in-cache: " << cached << endl; + return cached.isNull() ? Node(node) : cached; } // If an ITE replace it @@ -81,7 +113,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; // Attach the skolem - d_iteCache[node] = skolem; + d_iteCache.insert(node, skolem); // Remove ITEs from the new assertion, rewrite it and push it to the output newAssertion = run(newAssertion, output, iteSkolemMap, quantVar); @@ -127,17 +159,18 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, // If changes, we rewrite if(somethingChanged) { - Node cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren); - d_iteCache[node] = cachedRewrite; - return cachedRewrite; + Node cached = nodeManager->mkNode(node.getKind(), newChildren); + d_iteCache.insert(node, cached); + return cached; } else { - d_iteCache[node] = Node::null(); + d_iteCache.insert(node, Node::null()); return node; } } else { - d_iteCache[node] = Node::null(); + d_iteCache.insert(node, Node::null()); return node; } } + }/* CVC4 namespace */ diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h index 03197be89..9d79687f4 100644 --- a/src/util/ite_removal.h +++ b/src/util/ite_removal.h @@ -22,21 +22,25 @@ #include "expr/node.h" #include "util/dump.h" #include "context/context.h" -#include "context/cdhashmap.h" +#include "context/cdinsert_hashmap.h" namespace CVC4 { +namespace theory { +class ContainsTermITEVistor; +} + typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap; class RemoveITE { - typedef context::CDHashMap<Node, Node, NodeHashFunction> ITECache; + typedef context::CDInsertHashMap<Node, Node, NodeHashFunction> ITECache; ITECache d_iteCache; + public: - RemoveITE(context::UserContext* u) : - d_iteCache(u) { - } + RemoveITE(context::UserContext* u); + ~RemoveITE(); /** * Removes the ITE nodes by introducing skolem variables. All @@ -57,6 +61,21 @@ public: Node run(TNode node, std::vector<Node>& additionalAssertions, IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar); + /** Returns true if e contains a term ite.*/ + bool containsTermITE(TNode e); + + /** Returns the collected size of the caches.*/ + size_t collectedCacheSizes() const; + + /** Garbage collects non-context dependent data-structures.*/ + void garbageCollect(); + + /** Return the RemoveITE's containsVisitor.*/ + theory::ContainsTermITEVistor* getContainsVisitor(); + +private: + theory::ContainsTermITEVistor* d_containsVisitor; + };/* class RemoveTTE */ }/* CVC4 namespace */ diff --git a/src/util/nary_builder.cpp b/src/util/nary_builder.cpp new file mode 100644 index 000000000..004dd3382 --- /dev/null +++ b/src/util/nary_builder.cpp @@ -0,0 +1,183 @@ + +#include "util/nary_builder.h" +#include "expr/metakind.h" +using namespace std; + +namespace CVC4 { +namespace util { + +Node NaryBuilder::mkAssoc(Kind kind, const std::vector<Node>& children){ + if(children.size() == 0){ + return zeroArity(kind); + }else if(children.size() == 1){ + return children[0]; + }else{ + const unsigned int max = kind::metakind::getUpperBoundForKind(kind); + const unsigned int min = kind::metakind::getLowerBoundForKind(kind); + + Assert(min <= children.size()); + + unsigned int numChildren = children.size(); + NodeManager* nm = NodeManager::currentNM(); + if( numChildren <= max ) { + return nm->mkNode(kind,children); + } + + typedef std::vector<Node>::const_iterator const_iterator; + const_iterator it = children.begin() ; + const_iterator end = children.end() ; + + /* The new top-level children and the children of each sub node */ + std::vector<Node> newChildren; + std::vector<Node> subChildren; + + while( it != end && numChildren > max ) { + /* Grab the next max children and make a node for them. */ + for(const_iterator next = it + max; it != next; ++it, --numChildren ) { + subChildren.push_back(*it); + } + Node subNode = nm->mkNode(kind,subChildren); + newChildren.push_back(subNode); + subChildren.clear(); + } + + /* If there's children left, "top off" the Expr. */ + if(numChildren > 0) { + /* If the leftovers are too few, just copy them into newChildren; + * otherwise make a new sub-node */ + if(numChildren < min) { + for(; it != end; ++it) { + newChildren.push_back(*it); + } + } else { + for(; it != end; ++it) { + subChildren.push_back(*it); + } + Node subNode = nm->mkNode(kind, subChildren); + newChildren.push_back(subNode); + } + } + + /* It's inconceivable we could have enough children for this to fail + * (more than 2^32, in most cases?). */ + AlwaysAssert( newChildren.size() <= max, + "Too many new children in mkAssociative" ); + + /* It would be really weird if this happened (it would require + * min > 2, for one thing), but let's make sure. */ + AlwaysAssert( newChildren.size() >= min, + "Too few new children in mkAssociative" ); + + return nm->mkNode(kind,newChildren); + } +} + +Node NaryBuilder::zeroArity(Kind k){ + using namespace kind; + NodeManager* nm = NodeManager::currentNM(); + switch(k){ + case AND: + return nm->mkConst(true); + case OR: + return nm->mkConst(false); + case PLUS: + return nm->mkConst(Rational(0)); + case MULT: + return nm->mkConst(Rational(1)); + default: + return Node::null(); + } +} + + +RePairAssocCommutativeOperators::RePairAssocCommutativeOperators() + : d_cache() +{} +RePairAssocCommutativeOperators::~RePairAssocCommutativeOperators(){} +size_t RePairAssocCommutativeOperators::size() const{ return d_cache.size(); } +void RePairAssocCommutativeOperators::clear(){ d_cache.clear(); } + +bool RePairAssocCommutativeOperators::isAssociateCommutative(Kind k){ + using namespace kind; + switch(k){ + case BITVECTOR_CONCAT: + case BITVECTOR_AND: + case BITVECTOR_OR: + case BITVECTOR_XOR: + case BITVECTOR_MULT: + case BITVECTOR_PLUS: + case DISTINCT: + case PLUS: + case MULT: + case AND: + case OR: + return true; + default: + return false; + } +} + +Node RePairAssocCommutativeOperators::rePairAssocCommutativeOperators(TNode n){ + if(d_cache.find(n) != d_cache.end()){ + return d_cache[n]; + } + Node result = + isAssociateCommutative(n.getKind()) ? + case_assoccomm(n) : case_other(n); + + d_cache[n] = result; + return result; +} + +Node RePairAssocCommutativeOperators::case_assoccomm(TNode n){ + Kind k = n.getKind(); + Assert(isAssociateCommutative(k)); + Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED); + unsigned N = n.getNumChildren(); + Assert(N >= 2); + + + Node last = rePairAssocCommutativeOperators( n[N-1]); + Node nextToLast = rePairAssocCommutativeOperators(n[N-2]); + + NodeManager* nm = NodeManager::currentNM(); + Node last2 = nm->mkNode(k, nextToLast, last); + + if(N <= 2){ + return last2; + } else{ + Assert(N > 2); + Node prevRound = last2; + for(unsigned prevPos = N-2; prevPos > 0; --prevPos){ + unsigned currPos = prevPos-1; + Node curr = rePairAssocCommutativeOperators(n[currPos]); + Node round = nm->mkNode(k, curr, prevRound); + prevRound = round; + } + return prevRound; + } +} + +Node RePairAssocCommutativeOperators::case_other(TNode n){ + if(n.isConst() || n.isVar()){ + return n; + } + + NodeBuilder<> nb(n.getKind()); + + if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { + nb << n.getOperator(); + } + + // Remove the ITEs from the children + for(TNode::const_iterator i = n.begin(), end = n.end(); i != end; ++i) { + Node newChild = rePairAssocCommutativeOperators(*i); + nb << newChild; + } + + Node result = (Node)nb; + return result; +} + +}/* util namespace */ +}/* CVC4 namespace */ diff --git a/src/util/nary_builder.h b/src/util/nary_builder.h new file mode 100644 index 000000000..ceaa44e77 --- /dev/null +++ b/src/util/nary_builder.h @@ -0,0 +1,38 @@ + +#include "cvc4_private.h" + +#pragma once + +#include <vector> +#include "expr/node.h" + +namespace CVC4{ +namespace util { + +class NaryBuilder { +public: + static Node mkAssoc(Kind k, const std::vector<Node>& children); + static Node zeroArity(Kind k); +};/* class NaryBuilder */ + +class RePairAssocCommutativeOperators { +public: + RePairAssocCommutativeOperators(); + ~RePairAssocCommutativeOperators(); + + Node rePairAssocCommutativeOperators(TNode n); + + static bool isAssociateCommutative(Kind k); + + size_t size() const; + void clear(); +private: + Node case_assoccomm(TNode n); + Node case_other(TNode n); + + typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + NodeMap d_cache; +};/* class RePairAssocCommutativeOperators */ + +}/* util namespace */ +}/* CVC4 namespace */ |