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/ite_simplifier.h | |
parent | 0a7dc7687a4989641d8c101ba3b2d4737eaea24f (diff) |
Fixed performance issue with ite_simplifier on some QF_AUFBV benchmarks
Diffstat (limited to 'src/theory/ite_simplifier.h')
-rw-r--r-- | src/theory/ite_simplifier.h | 17 |
1 files changed, 16 insertions, 1 deletions
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); |