mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

expose iterators in expr_map

Browse source
This commit is contained in:
Arie Gurfinkel 2017-06-20 20:10:22 -04:00
parent e9100854b9
commit 6eced8836d
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/ast/expr_map.h
View file

@ -35,6 +35,13 @@ class expr_map {
obj_map<expr, expr*> m_expr2expr; obj_map<expr, expr*> m_expr2expr;
obj_map<expr, proof*> m_expr2pr; obj_map<expr, proof*> m_expr2pr;
public: public:
typedef obj_map<expr, expr*> Map;
typedef Map::iterator iterator;
typedef Map::key key;
typedef Map::value value;
typedef Map::data data;
typedef Map::entry entry;
expr_map(ast_manager & m); expr_map(ast_manager & m);
expr_map(ast_manager & m, bool store_proofs); expr_map(ast_manager & m, bool store_proofs);
~expr_map(); ~expr_map();
@ -44,6 +51,8 @@ public:
void erase(expr * k); void erase(expr * k);
void reset(); void reset();
void flush(); void flush();
iterator begin () const { return m_expr2expr.begin (); }
iterator end () const {return m_expr2expr.end (); }
void set_store_proofs(bool f) { void set_store_proofs(bool f) {
if (m_store_proofs != f) flush(); if (m_store_proofs != f) flush();
m_store_proofs = f; m_store_proofs = f;