diff options
Diffstat (limited to 'src/theory/substitutions.h')
-rw-r--r-- | src/theory/substitutions.h | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index c03baa1ac..1ade4815d 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -48,6 +48,9 @@ public: typedef context::CDMap<Node, Node, NodeHashFunction> NodeMap; + typedef NodeMap::iterator iterator; + typedef NodeMap::const_iterator const_iterator; + private: typedef std::hash_map<Node, Node, NodeHashFunction> NodeCache; @@ -115,6 +118,22 @@ public: return const_cast<SubstitutionMap*>(this)->apply(t); } + iterator begin() { + return d_substitutions.begin(); + } + + iterator end() { + return d_substitutions.end(); + } + + const_iterator begin() const { + return d_substitutions.begin(); + } + + const_iterator end() const { + return d_substitutions.end(); + } + // NOTE [MGD]: removed clear() and swap() from the interface // when this data structure became context-dependent // because they weren't used---and it's not clear how they @@ -134,6 +153,9 @@ inline std::ostream& operator << (std::ostream& out, const SubstitutionMap& subs } }/* CVC4::theory namespace */ + +std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i); + }/* CVC4 namespace */ #endif /* __CVC4__THEORY__SUBSTITUTIONS_H */ |