diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-07 19:34:21 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-07 19:34:21 +0000 |
commit | d71827eef17c181d225f64ea59d26c34d76b9b1e (patch) | |
tree | a875b974e56a2ad886e498b0b9011f367c82feb5 /src/theory | |
parent | 0a7dc7687a4989641d8c101ba3b2d4737eaea24f (diff) |
Fixed performance issue with ite_simplifier on some QF_AUFBV benchmarks
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/ite_simplifier.cpp | 27 | ||||
-rw-r--r-- | src/theory/ite_simplifier.h | 17 |
2 files changed, 28 insertions, 16 deletions
diff --git a/src/theory/ite_simplifier.cpp b/src/theory/ite_simplifier.cpp index 7d2b6e333..c70e9be6a 100644 --- a/src/theory/ite_simplifier.cpp +++ b/src/theory/ite_simplifier.cpp @@ -92,8 +92,8 @@ bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid) Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVar) { - NodeMap::iterator it; - it = d_simpConstCache.find(iteNode); + NodePairMap::iterator it; + it = d_simpConstCache.find(pair<Node, Node>(simpContext,iteNode)); if (it != d_simpConstCache.end()) { return (*it).second; } @@ -112,30 +112,28 @@ Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVa // Mark the substitution and continue Node result = builder; result = Rewriter::rewrite(result); - d_simpConstCache[iteNode] = result; + d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = result; return result; } if (!containsTermITE(iteNode)) { Node n = Rewriter::rewrite(simpContext.substitute(simpVar, iteNode)); - d_simpConstCache[iteNode] = n; + d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n; return n; } Node iteNode2; Node simpVar2; - d_simpConstCache.clear(); + d_simpContextCache.clear(); Node simpContext2 = createSimpContext(iteNode, iteNode2, simpVar2); if (!simpContext2.isNull()) { Assert(!iteNode2.isNull()); simpContext2 = simpContext.substitute(simpVar, simpContext2); - d_simpConstCache.clear(); Node n = simpConstants(simpContext2, iteNode2, simpVar2); if (n.isNull()) { return n; } - d_simpConstCache.clear(); - d_simpConstCache[iteNode] = n; + d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n; return n; } return Node(); @@ -160,13 +158,13 @@ Node ITESimplifier::getSimpVar(TypeNode t) Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar) { NodeMap::iterator it; - it = d_simpConstCache.find(c); - if (it != d_simpConstCache.end()) { + it = d_simpContextCache.find(c); + if (it != d_simpContextCache.end()) { return (*it).second; } if (!containsTermITE(c)) { - d_simpConstCache[c] = c; + d_simpContextCache[c] = c; return c; } @@ -180,7 +178,7 @@ Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar) if (simpVar.isNull()) { return Node(); } - d_simpConstCache[c] = simpVar; + d_simpContextCache[c] = simpVar; iteNode = c; return simpVar; } @@ -199,7 +197,7 @@ Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar) } // Mark the substitution and continue Node result = builder; - d_simpConstCache[c] = result; + d_simpContextCache[c] = result; return result; } @@ -209,14 +207,13 @@ Node ITESimplifier::simpITEAtom(TNode atom) if (leavesAreConst(atom)) { Node iteNode; Node simpVar; - d_simpConstCache.clear(); + d_simpContextCache.clear(); Node simpContext = createSimpContext(atom, iteNode, simpVar); if (!simpContext.isNull()) { if (iteNode.isNull()) { Assert(leavesAreConst(simpContext) && !containsTermITE(simpContext)); return Rewriter::rewrite(simpContext); } - d_simpConstCache.clear(); Node n = simpConstants(simpContext, iteNode, simpVar); if (!n.isNull()) { return n; diff --git a/src/theory/ite_simplifier.h b/src/theory/ite_simplifier.h index 50d37f502..ae11f429c 100644 --- a/src/theory/ite_simplifier.h +++ b/src/theory/ite_simplifier.h @@ -62,10 +62,25 @@ class ITESimplifier { typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap; - NodeMap d_simpConstCache; + typedef std::pair<Node, Node> NodePair; + struct NodePairHashFunction { + size_t operator () (const NodePair& pair) const { + size_t hash = 0; + hash = 0x9e3779b9 + NodeHashFunction().operator()(pair.first); + hash ^= 0x9e3779b9 + NodeHashFunction().operator()(pair.second) + (hash << 6) + (hash >> 2); + return hash; + } + }; + + typedef std::hash_map<NodePair, Node, NodePairHashFunction> NodePairMap; + + + NodePairMap d_simpConstCache; Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar); std::hash_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars; Node getSimpVar(TypeNode t); + + NodeMap d_simpContextCache; Node createSimpContext(TNode c, Node& iteNode, Node& simpVar); Node simpITEAtom(TNode atom); |