diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-15 18:10:42 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-15 18:10:42 -0600 |
commit | 80daa7fd5917526513a510261fd3901f03949dfa (patch) | |
tree | 7fa74722e30c6e5cc59d96b045273c2bdaf27701 /src/expr/node_manager.h | |
parent | f31163c1f6bb1816365e9f22505d9558a7bc1802 (diff) |
More simplification to internal implementation of tuples and records.
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. |