1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 expr_offset_map.h 7 8 Abstract: 9 10 A generic mapping from (expression, offset) to a value T. 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2008-02-01. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include "ast/substitution/expr_offset.h" 22 #include "util/vector.h" 23 24 /** 25 \brief A mapping from expr_offset to some value of type T. 26 */ 27 template<typename T> 28 class expr_offset_map { 29 struct data { 30 T m_data; 31 unsigned m_timestamp; datadata32 data():m_timestamp(0) {} 33 }; 34 vector<svector<data> > m_map; 35 unsigned m_timestamp; 36 public: expr_offset_map()37 expr_offset_map(): 38 m_timestamp(1) {} 39 contains(expr_offset const & n)40 bool contains(expr_offset const & n) const { 41 unsigned off = n.get_offset(); 42 if (off < m_map.size()) { 43 svector<data> const & v = m_map[off]; 44 unsigned id = n.get_expr()->get_id(); 45 if (id < v.size()) 46 return v[id].m_timestamp == m_timestamp; 47 } 48 return false; 49 } 50 find(expr_offset const & n,T & r)51 bool find(expr_offset const & n, T & r) const { 52 unsigned off = n.get_offset(); 53 if (off < m_map.size()) { 54 svector<data> const & v = m_map[off]; 55 unsigned id = n.get_expr()->get_id(); 56 if (id < v.size() && v[id].m_timestamp == m_timestamp) { 57 r = v[id].m_data; 58 return true; 59 } 60 } 61 return false; 62 } 63 insert(expr_offset const & n,T const & r)64 void insert(expr_offset const & n, T const & r) { 65 unsigned off = n.get_offset(); 66 if (off >= m_map.size()) 67 m_map.resize(off+1, svector<data>()); 68 svector<data> & v = m_map[off]; 69 unsigned id = n.get_expr()->get_id(); 70 if (id >= v.size()) 71 v.resize(id+1); 72 v[id].m_data = r; 73 v[id].m_timestamp = m_timestamp; 74 } 75 reset()76 void reset() { 77 m_timestamp++; 78 if (m_timestamp == UINT_MAX) { 79 typename vector<svector<data> >::iterator it = m_map.begin(); 80 typename vector<svector<data> >::iterator end = m_map.end(); 81 for (; it != end; ++it) { 82 svector<data> & v = *it; 83 typename svector<data>::iterator it2 = v.begin(); 84 typename svector<data>::iterator end2 = v.end(); 85 for (; it2 != end2; ++it2) 86 it2->m_timestamp = 0; 87 } 88 m_timestamp = 1; 89 } 90 } 91 }; 92 93