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