diff options
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 45c9afbde..974a1ed94 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -166,7 +166,20 @@ class NodeManager { /** * A map of tuple and record types to their corresponding datatype. */ - std::hash_map<TypeNode, TypeNode, TypeNodeHashFunction> d_tupleAndRecordTypes; + class TupleTypeCache { + public: + std::map< TypeNode, TupleTypeCache > d_children; + TypeNode d_data; + TypeNode getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index = 0 ); + }; + class RecTypeCache { + public: + std::map< TypeNode, std::map< std::string, RecTypeCache > > d_children; + TypeNode d_data; + TypeNode getRecordType( NodeManager * nm, const Record& rec, unsigned index = 0 ); + }; + TupleTypeCache d_tt_cache; + RecTypeCache d_rt_cache; /** * Keep a count of all abstract values produced by this NodeManager. |