<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: expr_map.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="dir_68267d1309a1af8e8297ef4c3efbcdba.html">src</a></li><li class="navelem"><a class="el" href="dir_b0856f6b0d80ccb263b2f415c91f9e17.html">include</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">expr_map.h</div> </div>
</div><!--header-->
<div class="contents">
<a href="expr__map_8h.html">Go to the documentation of this file.</a><div class="fragment"><div class="line"><a name="l00001"></a><span class="lineno"> 1</span> <span class="comment">/*****************************************************************************/</span><span class="comment"></span></div>
<div class="line"><a name="l00002"></a><span class="lineno"> 2</span> <span class="comment">/*!</span></div>
<div class="line"><a name="l00003"></a><span class="lineno"> 3</span> <span class="comment"> * \file expr_map.h</span></div>
<div class="line"><a name="l00004"></a><span class="lineno"> 4</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00005"></a><span class="lineno"> 5</span> <span class="comment"> * Author: Sergey Berezin</span></div>
<div class="line"><a name="l00006"></a><span class="lineno"> 6</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00007"></a><span class="lineno"> 7</span> <span class="comment"> * Created: Dec 11 01:22:49 GMT 2002</span></div>
<div class="line"><a name="l00008"></a><span class="lineno"> 8</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00009"></a><span class="lineno"> 9</span> <span class="comment"> * <hr></span></div>
<div class="line"><a name="l00010"></a><span class="lineno"> 10</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00011"></a><span class="lineno"> 11</span> <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span></div>
<div class="line"><a name="l00012"></a><span class="lineno"> 12</span> <span class="comment"> * and its documentation for any purpose is hereby granted without</span></div>
<div class="line"><a name="l00013"></a><span class="lineno"> 13</span> <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span></div>
<div class="line"><a name="l00014"></a><span class="lineno"> 14</span> <span class="comment"> * LICENSE file provided with this distribution.</span></div>
<div class="line"><a name="l00015"></a><span class="lineno"> 15</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00016"></a><span class="lineno"> 16</span> <span class="comment"> * <hr></span></div>
<div class="line"><a name="l00017"></a><span class="lineno"> 17</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00018"></a><span class="lineno"> 18</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00019"></a><span class="lineno"> 19</span> <span class="comment">/*****************************************************************************/</span></div>
<div class="line"><a name="l00020"></a><span class="lineno"> 20</span> <span class="comment">// CLASS: ExprMap<Data></span></div>
<div class="line"><a name="l00021"></a><span class="lineno"> 21</span> <span class="comment">//</span></div>
<div class="line"><a name="l00022"></a><span class="lineno"> 22</span> <span class="comment">// AUTHOR: Sergey Berezin, 12/10/2002</span></div>
<div class="line"><a name="l00023"></a><span class="lineno"> 23</span> <span class="comment">//</span></div>
<div class="line"><a name="l00024"></a><span class="lineno"> 24</span> <span class="comment">// Abstract:</span></div>
<div class="line"><a name="l00025"></a><span class="lineno"> 25</span> <span class="comment">//</span></div>
<div class="line"><a name="l00026"></a><span class="lineno"> 26</span> <span class="comment">// An abstract interface mapping Expr values to Data. The</span></div>
<div class="line"><a name="l00027"></a><span class="lineno"> 27</span> <span class="comment">// implementation is a hash table.</span></div>
<div class="line"><a name="l00028"></a><span class="lineno"> 28</span> <span class="comment">//</span></div>
<div class="line"><a name="l00029"></a><span class="lineno"> 29</span> <span class="comment">// Subclassing is NOT allowed; this would lose the iterators (can we</span></div>
<div class="line"><a name="l00030"></a><span class="lineno"> 30</span> <span class="comment">// fix it? Maybe not worth the trouble.)</span></div>
<div class="line"><a name="l00031"></a><span class="lineno"> 31</span> <span class="comment">//</span></div>
<div class="line"><a name="l00032"></a><span class="lineno"> 32</span> <span class="comment">// Functions follow the style of STL 'map' container.</span></div>
<div class="line"><a name="l00033"></a><span class="lineno"> 33</span> <span class="comment">// </span></div>
<div class="line"><a name="l00034"></a><span class="lineno"> 34</span> <span class="comment">// ExprMap<Data>() [Default constructor] Creates an empty map</span></div>
<div class="line"><a name="l00035"></a><span class="lineno"> 35</span> <span class="comment">// int count(Expr e) Counts the number of elements mapped from e.</span></div>
<div class="line"><a name="l00036"></a><span class="lineno"> 36</span> <span class="comment">// Normally, returns 0 or 1.</span></div>
<div class="line"><a name="l00037"></a><span class="lineno"> 37</span> <span class="comment">// Data& operator[](e) Returns Data associated with e. If e is not mapped,</span></div>
<div class="line"><a name="l00038"></a><span class="lineno"> 38</span> <span class="comment">// insert new Data() into ExprMap.</span></div>
<div class="line"><a name="l00039"></a><span class="lineno"> 39</span> <span class="comment">// Can be used to populate ExprMap as follows:</span></div>
<div class="line"><a name="l00040"></a><span class="lineno"> 40</span> <span class="comment">// ExprMap map;</span></div>
<div class="line"><a name="l00041"></a><span class="lineno"> 41</span> <span class="comment">// map[e1] = data1; map[e2] = data2; ...</span></div>
<div class="line"><a name="l00042"></a><span class="lineno"> 42</span> <span class="comment">// Caveat: Data must have a default constructor and be assignable.</span></div>
<div class="line"><a name="l00043"></a><span class="lineno"> 43</span> <span class="comment">// void erase(Expr e) Erase e->data mapping from ExprMap.</span></div>
<div class="line"><a name="l00044"></a><span class="lineno"> 44</span> <span class="comment">// void insert(Expr e, Data d) Insert e->d mapping.</span></div>
<div class="line"><a name="l00045"></a><span class="lineno"> 45</span> <span class="comment">// iterator begin() Return simple "input" iterators for ExprMap</span></div>
<div class="line"><a name="l00046"></a><span class="lineno"> 46</span> <span class="comment">// iterator end() (as defined in STL)</span></div>
<div class="line"><a name="l00047"></a><span class="lineno"> 47</span> <span class="comment">// size_t size() Return size of the map</span></div>
<div class="line"><a name="l00048"></a><span class="lineno"> 48</span> <span class="comment">// bool empty() Check for emptiness </span><span class="comment"></span></div>
<div class="line"><a name="l00049"></a><span class="lineno"> 49</span> <span class="comment">///////////////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00050"></a><span class="lineno"> 50</span> <span class="comment"></span><span class="preprocessor">#ifndef _cvc3__expr_h_</span></div>
<div class="line"><a name="l00051"></a><span class="lineno"> 51</span> <span class="preprocessor"></span><span class="preprocessor">#include "<a class="code" href="expr_8h.html" title="Definition of the API to expression package. See class Expr for details.">expr.h</a>"</span></div>
<div class="line"><a name="l00052"></a><span class="lineno"> 52</span> <span class="preprocessor">#endif</span></div>
<div class="line"><a name="l00053"></a><span class="lineno"> 53</span> <span class="preprocessor"></span></div>
<div class="line"><a name="l00054"></a><span class="lineno"> 54</span> <span class="preprocessor">#ifndef _cvc3__expr_map_h_</span></div>
<div class="line"><a name="l00055"></a><span class="lineno"> 55</span> <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__expr_map_h_</span></div>
<div class="line"><a name="l00056"></a><span class="lineno"> 56</span> <span class="preprocessor"></span></div>
<div class="line"><a name="l00057"></a><span class="lineno"> 57</span> <span class="preprocessor">#include "<a class="code" href="expr__hash_8h.html" title="Definition of the API to expression package. See class Expr for details.">expr_hash.h</a>"</span></div>
<div class="line"><a name="l00058"></a><span class="lineno"> 58</span> </div>
<div class="line"><a name="l00059"></a><span class="lineno"> 59</span> <span class="keyword">namespace </span>CVC3 {</div>
<div class="line"><a name="l00060"></a><span class="lineno"> 60</span> </div>
<div class="line"><a name="l00061"></a><span class="lineno"> 61</span>  <span class="keyword">template</span><<span class="keyword">class</span> Data></div>
<div class="line"><a name="l00062"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html"> 62</a></span>  <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a> {</div>
<div class="line"><a name="l00063"></a><span class="lineno"> 63</span>  <span class="keyword">private</span>:</div>
<div class="line"><a name="l00064"></a><span class="lineno"> 64</span> </div>
<div class="line"><a name="l00065"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#a013b2551d6b935eb81e2157265973dea"> 65</a></span>  <span class="keyword">typedef</span> std::map<Expr, Data> <a class="code" href="classCVC3_1_1ExprMap.html#a013b2551d6b935eb81e2157265973dea">ExprMapType</a>;</div>
<div class="line"><a name="l00066"></a><span class="lineno"> 66</span>  <span class="comment">// Private members</span></div>
<div class="line"><a name="l00067"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20"> 67</a></span>  <a class="code" href="classCVC3_1_1ExprMap.html#a013b2551d6b935eb81e2157265973dea">ExprMapType</a> <a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a>;</div>
<div class="line"><a name="l00068"></a><span class="lineno"> 68</span> </div>
<div class="line"><a name="l00069"></a><span class="lineno"> 69</span>  <span class="keyword">public</span>:</div>
<div class="line"><a name="l00070"></a><span class="lineno"> 70</span> <span class="comment"></span></div>
<div class="line"><a name="l00071"></a><span class="lineno"> 71</span> <span class="comment"> //////////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00072"></a><span class="lineno"> 72</span> <span class="comment"></span> <span class="comment">// Class: ExprMap::iterator</span></div>
<div class="line"><a name="l00073"></a><span class="lineno"> 73</span>  <span class="comment">// Author: Sergey Berezin</span></div>
<div class="line"><a name="l00074"></a><span class="lineno"> 74</span>  <span class="comment">// Created: Tue Dec 10 16:25:19 2002</span></div>
<div class="line"><a name="l00075"></a><span class="lineno"> 75</span>  <span class="comment">// Description: </span><span class="comment"></span></div>
<div class="line"><a name="l00076"></a><span class="lineno"> 76</span> <span class="comment"> //////////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00077"></a><span class="lineno"> 77</span> <span class="comment"></span></div>
<div class="line"><a name="l00078"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html"> 78</a></span>  <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html">const_iterator</a>: <span class="keyword">public</span> std::iterator<std::input_iterator_tag, std::pair<Expr,Data>,std::ptrdiff_t> {</div>
<div class="line"><a name="l00079"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a4b5ec157d5a76b10f26e8695279743d1"> 79</a></span>  <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a>;</div>
<div class="line"><a name="l00080"></a><span class="lineno"> 80</span>  <span class="keyword">private</span>:</div>
<div class="line"><a name="l00081"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a710a4316c39cc387c585380f2060a527"> 81</a></span>  <span class="keyword">typename</span> ExprMapType::const_iterator <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a710a4316c39cc387c585380f2060a527">d_it</a>;</div>
<div class="line"><a name="l00082"></a><span class="lineno"> 82</span>  <span class="comment">// Private constructor</span></div>
<div class="line"><a name="l00083"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a59ba32f23ca8b6defce403052ac8321c"> 83</a></span>  <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a460a03e95fddd12c2f5fc7f747091196">const_iterator</a>(<span class="keyword">const</span> <span class="keyword">typename</span> ExprMapType::const_iterator& it)</div>
<div class="line"><a name="l00084"></a><span class="lineno"> 84</span>  : <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a710a4316c39cc387c585380f2060a527">d_it</a>(it) { }</div>
<div class="line"><a name="l00085"></a><span class="lineno"> 85</span>  <span class="keyword">public</span>:</div>
<div class="line"><a name="l00086"></a><span class="lineno"> 86</span>  <span class="comment">// Default constructor</span></div>
<div class="line"><a name="l00087"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a460a03e95fddd12c2f5fc7f747091196"> 87</a></span>  <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a460a03e95fddd12c2f5fc7f747091196">const_iterator</a>() { }</div>
<div class="line"><a name="l00088"></a><span class="lineno"> 88</span>  <span class="comment">// (Dis)equality</span></div>
<div class="line"><a name="l00089"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a2efab3176fb933235e7663e51bc08dcb"> 89</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a2efab3176fb933235e7663e51bc08dcb">operator==</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html">const_iterator</a>& i)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a710a4316c39cc387c585380f2060a527">d_it</a> == i.<a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a710a4316c39cc387c585380f2060a527">d_it</a>; }</div>
<div class="line"><a name="l00090"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#ad01d6cc98eac8759a7df7cdd71169e32"> 90</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#ad01d6cc98eac8759a7df7cdd71169e32">operator!=</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html">const_iterator</a>& i)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a710a4316c39cc387c585380f2060a527">d_it</a> != i.<a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a710a4316c39cc387c585380f2060a527">d_it</a>; }</div>
<div class="line"><a name="l00091"></a><span class="lineno"> 91</span>  <span class="comment">// Dereference operators.</span></div>
<div class="line"><a name="l00092"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a9f36b472705bf695bf7494ac45909877"> 92</a></span>  <span class="keyword">const</span> std::pair<const Expr,Data>& <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a9f36b472705bf695bf7494ac45909877">operator*</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> *<a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a710a4316c39cc387c585380f2060a527">d_it</a>; }</div>
<div class="line"><a name="l00093"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a10981ed9000eb1753f025b95497413d5"> 93</a></span>  <span class="keyword">const</span> std::pair<const Expr,Data>* <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a10981ed9000eb1753f025b95497413d5">operator-></a>()<span class="keyword"> const </span>{</div>
<div class="line"><a name="l00094"></a><span class="lineno"> 94</span>  <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a710a4316c39cc387c585380f2060a527">d_it</a>.operator->();</div>
<div class="line"><a name="l00095"></a><span class="lineno"> 95</span>  }</div>
<div class="line"><a name="l00096"></a><span class="lineno"> 96</span>  <span class="comment">// Prefix increment</span></div>
<div class="line"><a name="l00097"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#ac56f8e8fa8c07fe5ddafe2a1e957dab6"> 97</a></span>  <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html">const_iterator</a>& <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#ac56f8e8fa8c07fe5ddafe2a1e957dab6">operator++</a>() { ++<a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a710a4316c39cc387c585380f2060a527">d_it</a>; <span class="keywordflow">return</span> *<span class="keyword">this</span>; }</div>
<div class="line"><a name="l00098"></a><span class="lineno"> 98</span>  <span class="comment">// Postfix increment: requires a Proxy object to hold the</span></div>
<div class="line"><a name="l00099"></a><span class="lineno"> 99</span>  <span class="comment">// intermediate value for dereferencing</span></div>
<div class="line"><a name="l00100"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator_1_1Proxy.html"> 100</a></span>  <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator_1_1Proxy.html">Proxy</a> {</div>
<div class="line"><a name="l00101"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator_1_1Proxy.html#a4b0cc38aa38601782135cc6b5f461cb1"> 101</a></span>  <span class="keyword">const</span> std::pair<const Expr,Data>& <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator_1_1Proxy.html#a4b0cc38aa38601782135cc6b5f461cb1">d_pair</a>;</div>
<div class="line"><a name="l00102"></a><span class="lineno"> 102</span>  <span class="keyword">public</span>:</div>
<div class="line"><a name="l00103"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator_1_1Proxy.html#a73c8a36b39090a887ad37a58fa08a211"> 103</a></span>  <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator_1_1Proxy.html#a73c8a36b39090a887ad37a58fa08a211">Proxy</a>(<span class="keyword">const</span> std::pair<Expr,Data>& pair) : <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator_1_1Proxy.html#a4b0cc38aa38601782135cc6b5f461cb1">d_pair</a>(pair) { }</div>
<div class="line"><a name="l00104"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator_1_1Proxy.html#ae5d598486dfba7962d05fccf1b63b888"> 104</a></span>  std::pair<const Expr,Data> <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator_1_1Proxy.html#ae5d598486dfba7962d05fccf1b63b888">operator*</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator_1_1Proxy.html#a4b0cc38aa38601782135cc6b5f461cb1">d_pair</a>; }</div>
<div class="line"><a name="l00105"></a><span class="lineno"> 105</span>  }; <span class="comment">// end of class Proxy</span></div>
<div class="line"><a name="l00106"></a><span class="lineno"> 106</span>  <span class="comment">// Actual postfix increment: returns Proxy with the old value.</span></div>
<div class="line"><a name="l00107"></a><span class="lineno"> 107</span>  <span class="comment">// Now, an expression like *i++ will return the current *i, and</span></div>
<div class="line"><a name="l00108"></a><span class="lineno"> 108</span>  <span class="comment">// then advance the iterator. However, don't try to use Proxy for</span></div>
<div class="line"><a name="l00109"></a><span class="lineno"> 109</span>  <span class="comment">// anything else.</span></div>
<div class="line"><a name="l00110"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#ad86749c9532fb661459ee8f90ef42b46"> 110</a></span>  <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator_1_1Proxy.html">Proxy</a> <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#ad86749c9532fb661459ee8f90ef42b46">operator++</a>(<span class="keywordtype">int</span>) {</div>
<div class="line"><a name="l00111"></a><span class="lineno"> 111</span>  <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator_1_1Proxy.html">Proxy</a> tmp(*(*<span class="keyword">this</span>));</div>
<div class="line"><a name="l00112"></a><span class="lineno"> 112</span>  ++(*this);</div>
<div class="line"><a name="l00113"></a><span class="lineno"> 113</span>  <span class="keywordflow">return</span> tmp;</div>
<div class="line"><a name="l00114"></a><span class="lineno"> 114</span>  }</div>
<div class="line"><a name="l00115"></a><span class="lineno"> 115</span>  <span class="comment">// Prefix decrement</span></div>
<div class="line"><a name="l00116"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#ab23e0b615ad6b13195b89e43a0595c21"> 116</a></span>  <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html">const_iterator</a>& <a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#ab23e0b615ad6b13195b89e43a0595c21">operator--</a>() { --<a class="code" href="classCVC3_1_1ExprMap_1_1const__iterator.html#a710a4316c39cc387c585380f2060a527">d_it</a>; <span class="keywordflow">return</span> *<span class="keyword">this</span>; }</div>
<div class="line"><a name="l00117"></a><span class="lineno"> 117</span>  }; <span class="comment">// end of class const_iterator</span></div>
<div class="line"><a name="l00118"></a><span class="lineno"> 118</span> </div>
<div class="line"><a name="l00119"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html"> 119</a></span>  <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html">iterator</a>: <span class="keyword">public</span> std::iterator<std::input_iterator_tag, std::pair<Expr,Data>,std::ptrdiff_t> {</div>
<div class="line"><a name="l00120"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a4b5ec157d5a76b10f26e8695279743d1"> 120</a></span>  <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a>;</div>
<div class="line"><a name="l00121"></a><span class="lineno"> 121</span>  <span class="keyword">private</span>:</div>
<div class="line"><a name="l00122"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a0a784d10c7f67ef5fed42f66d67f0a91"> 122</a></span>  <span class="keyword">typename</span> ExprMapType::iterator <a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a0a784d10c7f67ef5fed42f66d67f0a91">d_it</a>;</div>
<div class="line"><a name="l00123"></a><span class="lineno"> 123</span>  <span class="comment">// Private constructor</span></div>
<div class="line"><a name="l00124"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#aedd09d173fde51bcf2200b246a075447"> 124</a></span>  <a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a8c274875e80c02c02226a12f60fbaec2">iterator</a>(<span class="keyword">const</span> <span class="keyword">typename</span> ExprMapType::iterator& it)</div>
<div class="line"><a name="l00125"></a><span class="lineno"> 125</span>  : <a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a0a784d10c7f67ef5fed42f66d67f0a91">d_it</a>(it) { }</div>
<div class="line"><a name="l00126"></a><span class="lineno"> 126</span>  <span class="keyword">public</span>:</div>
<div class="line"><a name="l00127"></a><span class="lineno"> 127</span>  <span class="comment">// Default constructor</span></div>
<div class="line"><a name="l00128"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a8c274875e80c02c02226a12f60fbaec2"> 128</a></span>  <a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a8c274875e80c02c02226a12f60fbaec2">iterator</a>() { }</div>
<div class="line"><a name="l00129"></a><span class="lineno"> 129</span>  <span class="comment">// (Dis)equality</span></div>
<div class="line"><a name="l00130"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a9392fa8076cd0b33b18db2171729d922"> 130</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a9392fa8076cd0b33b18db2171729d922">operator==</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html">iterator</a>& i)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a0a784d10c7f67ef5fed42f66d67f0a91">d_it</a> == i.<a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a0a784d10c7f67ef5fed42f66d67f0a91">d_it</a>; }</div>
<div class="line"><a name="l00131"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a670c71d27031240a1ff8b0ed06549aa4"> 131</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a670c71d27031240a1ff8b0ed06549aa4">operator!=</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html">iterator</a>& i)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a0a784d10c7f67ef5fed42f66d67f0a91">d_it</a> != i.<a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a0a784d10c7f67ef5fed42f66d67f0a91">d_it</a>; }</div>
<div class="line"><a name="l00132"></a><span class="lineno"> 132</span>  <span class="comment">// Dereference operators.</span></div>
<div class="line"><a name="l00133"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a8721450fdae749b6f920476b57bb90b0"> 133</a></span>  std::pair<const Expr,Data>& <a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a8721450fdae749b6f920476b57bb90b0">operator*</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> *<a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a0a784d10c7f67ef5fed42f66d67f0a91">d_it</a>; }</div>
<div class="line"><a name="l00134"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a92339a0c1838488afa0cb458df80d8b9"> 134</a></span>  std::pair<const Expr,Data>* <a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a92339a0c1838488afa0cb458df80d8b9">operator-></a>()<span class="keyword"> const </span>{</div>
<div class="line"><a name="l00135"></a><span class="lineno"> 135</span>  <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a0a784d10c7f67ef5fed42f66d67f0a91">d_it</a>.operator->();</div>
<div class="line"><a name="l00136"></a><span class="lineno"> 136</span>  }</div>
<div class="line"><a name="l00137"></a><span class="lineno"> 137</span>  <span class="comment">// Prefix increment</span></div>
<div class="line"><a name="l00138"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a93a6c166d227642679a4521b2f5016c6"> 138</a></span>  <a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html">iterator</a>& <a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a93a6c166d227642679a4521b2f5016c6">operator++</a>() { ++<a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a0a784d10c7f67ef5fed42f66d67f0a91">d_it</a>; <span class="keywordflow">return</span> *<span class="keyword">this</span>; }</div>
<div class="line"><a name="l00139"></a><span class="lineno"> 139</span>  <span class="comment">// Postfix increment: requires a Proxy object to hold the</span></div>
<div class="line"><a name="l00140"></a><span class="lineno"> 140</span>  <span class="comment">// intermediate value for dereferencing</span></div>
<div class="line"><a name="l00141"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1iterator_1_1Proxy.html"> 141</a></span>  <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprMap_1_1iterator_1_1Proxy.html">Proxy</a> {</div>
<div class="line"><a name="l00142"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1iterator_1_1Proxy.html#a3efd01c2a65021f437ca1c72b3c300b8"> 142</a></span>  std::pair<const Expr,Data>& <a class="code" href="classCVC3_1_1ExprMap_1_1iterator_1_1Proxy.html#a3efd01c2a65021f437ca1c72b3c300b8">d_pair</a>;</div>
<div class="line"><a name="l00143"></a><span class="lineno"> 143</span>  <span class="keyword">public</span>:</div>
<div class="line"><a name="l00144"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1iterator_1_1Proxy.html#aeb2f4b187d13cd8047adbce4f5b592a3"> 144</a></span>  <a class="code" href="classCVC3_1_1ExprMap_1_1iterator_1_1Proxy.html#aeb2f4b187d13cd8047adbce4f5b592a3">Proxy</a>(std::pair<const Expr,Data>& pair) : <a class="code" href="classCVC3_1_1ExprMap_1_1iterator_1_1Proxy.html#a3efd01c2a65021f437ca1c72b3c300b8">d_pair</a>(pair) { }</div>
<div class="line"><a name="l00145"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1iterator_1_1Proxy.html#aa736d668372979b1b25bf6f3e34e8d46"> 145</a></span>  std::pair<const Expr,Data> <a class="code" href="classCVC3_1_1ExprMap_1_1iterator_1_1Proxy.html#aa736d668372979b1b25bf6f3e34e8d46">operator*</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprMap_1_1iterator_1_1Proxy.html#a3efd01c2a65021f437ca1c72b3c300b8">d_pair</a>; }</div>
<div class="line"><a name="l00146"></a><span class="lineno"> 146</span>  }; <span class="comment">// end of class Proxy</span></div>
<div class="line"><a name="l00147"></a><span class="lineno"> 147</span>  <span class="comment">// Actual postfix increment: returns Proxy with the old value.</span></div>
<div class="line"><a name="l00148"></a><span class="lineno"> 148</span>  <span class="comment">// Now, an expression like *i++ will return the current *i, and</span></div>
<div class="line"><a name="l00149"></a><span class="lineno"> 149</span>  <span class="comment">// then advance the iterator. However, don't try to use Proxy for</span></div>
<div class="line"><a name="l00150"></a><span class="lineno"> 150</span>  <span class="comment">// anything else.</span></div>
<div class="line"><a name="l00151"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a130ad1003ad1ae13c0202820ff46c12a"> 151</a></span>  <a class="code" href="classCVC3_1_1ExprMap_1_1iterator_1_1Proxy.html">Proxy</a> <a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a130ad1003ad1ae13c0202820ff46c12a">operator++</a>(<span class="keywordtype">int</span>) {</div>
<div class="line"><a name="l00152"></a><span class="lineno"> 152</span>  <a class="code" href="classCVC3_1_1ExprMap_1_1iterator_1_1Proxy.html">Proxy</a> tmp(*(*<span class="keyword">this</span>));</div>
<div class="line"><a name="l00153"></a><span class="lineno"> 153</span>  ++(*this);</div>
<div class="line"><a name="l00154"></a><span class="lineno"> 154</span>  <span class="keywordflow">return</span> tmp;</div>
<div class="line"><a name="l00155"></a><span class="lineno"> 155</span>  }</div>
<div class="line"><a name="l00156"></a><span class="lineno"> 156</span>  <span class="comment">// Prefix decrement</span></div>
<div class="line"><a name="l00157"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a9b905e8c3090e714dc9e3dbc89458787"> 157</a></span>  <a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html">iterator</a>& <a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a9b905e8c3090e714dc9e3dbc89458787">operator--</a>() { --<a class="code" href="classCVC3_1_1ExprMap_1_1iterator.html#a0a784d10c7f67ef5fed42f66d67f0a91">d_it</a>; <span class="keywordflow">return</span> *<span class="keyword">this</span>; }</div>
<div class="line"><a name="l00158"></a><span class="lineno"> 158</span>  }; <span class="comment">// end of class iterator</span></div>
<div class="line"><a name="l00159"></a><span class="lineno"> 159</span> <span class="comment"></span></div>
<div class="line"><a name="l00160"></a><span class="lineno"> 160</span> <span class="comment"> //////////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00161"></a><span class="lineno"> 161</span> <span class="comment"></span> <span class="comment">// Public methods</span><span class="comment"></span></div>
<div class="line"><a name="l00162"></a><span class="lineno"> 162</span> <span class="comment"> //////////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00163"></a><span class="lineno"> 163</span> <span class="comment"></span></div>
<div class="line"><a name="l00164"></a><span class="lineno"> 164</span>  <span class="comment">// Default constructor</span></div>
<div class="line"><a name="l00165"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#a5bf0c30b9291bba62bcbed4e31d5d692"> 165</a></span>  <a class="code" href="classCVC3_1_1ExprMap.html#a5bf0c30b9291bba62bcbed4e31d5d692">ExprMap</a>() { }</div>
<div class="line"><a name="l00166"></a><span class="lineno"> 166</span>  <span class="comment">// Copy constructor</span></div>
<div class="line"><a name="l00167"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#ae2e3a0d415df7b4a502e4ffa82011d3c"> 167</a></span>  <a class="code" href="classCVC3_1_1ExprMap.html#ae2e3a0d415df7b4a502e4ffa82011d3c">ExprMap</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a>& map): <a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a>(map.<a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a>) { }</div>
<div class="line"><a name="l00168"></a><span class="lineno"> 168</span> </div>
<div class="line"><a name="l00169"></a><span class="lineno"> 169</span>  <span class="comment">// Other methods</span></div>
<div class="line"><a name="l00170"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#a292270a9283cbdcfd5a3ddccd4e33262"> 170</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprMap.html#a292270a9283cbdcfd5a3ddccd4e33262">empty</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a>.empty(); }</div>
<div class="line"><a name="l00171"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#a62589c597d245f3245df6d6a5fe6f4f1"> 171</a></span>  <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1ExprMap.html#a62589c597d245f3245df6d6a5fe6f4f1">size</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a>.size(); }</div>
<div class="line"><a name="l00172"></a><span class="lineno"> 172</span> </div>
<div class="line"><a name="l00173"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#aa96dfa3a54a131cdb0964ef4b80e324f"> 173</a></span>  <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1ExprMap.html#aa96dfa3a54a131cdb0964ef4b80e324f">count</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a>.count(e); }</div>
<div class="line"><a name="l00174"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#a53c955e68ddbde38deebbebb4221539c"> 174</a></span>  Data& <a class="code" href="classCVC3_1_1ExprMap.html#a53c955e68ddbde38deebbebb4221539c">operator[]</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a>[e]; }</div>
<div class="line"><a name="l00175"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#a173c2cf4753189d956073d74c36c7c58"> 175</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ExprMap.html#a173c2cf4753189d956073d74c36c7c58">clear</a>() { <a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a>.clear(); }</div>
<div class="line"><a name="l00176"></a><span class="lineno"> 176</span> </div>
<div class="line"><a name="l00177"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#a89122ac9deffe3cd839d067b6b92af1d"> 177</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ExprMap.html#a89122ac9deffe3cd839d067b6b92af1d">insert</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keyword">const</span> Data& d) { <a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a>[e] = d; }</div>
<div class="line"><a name="l00178"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#a2997aa3f20d09f6bf49b09da9a177003"> 178</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ExprMap.html#a2997aa3f20d09f6bf49b09da9a177003">erase</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) { <a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a>.erase(e); }</div>
<div class="line"><a name="l00179"></a><span class="lineno"> 179</span> </div>
<div class="line"><a name="l00180"></a><span class="lineno"> 180</span>  <span class="keyword">template</span><<span class="keyword">class</span> InputIterator></div>
<div class="line"><a name="l00181"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#a28340c9e1b82b1fa781c3ee87a41ca32"> 181</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ExprMap.html#a28340c9e1b82b1fa781c3ee87a41ca32">insert</a>(InputIterator l, InputIterator r) { <a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a>.insert(l,r); }</div>
<div class="line"><a name="l00182"></a><span class="lineno"> 182</span> </div>
<div class="line"><a name="l00183"></a><span class="lineno"> 183</span>  <span class="keyword">template</span><<span class="keyword">class</span> InputIterator></div>
<div class="line"><a name="l00184"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#a1ef9e067cb30e26ba6fd3cb675936bf2"> 184</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ExprMap.html#a1ef9e067cb30e26ba6fd3cb675936bf2">erase</a>(InputIterator l, InputIterator r) {</div>
<div class="line"><a name="l00185"></a><span class="lineno"> 185</span>  <span class="keywordflow">for</span>(; l!=r; ++l) {</div>
<div class="line"><a name="l00186"></a><span class="lineno"> 186</span>  <a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a>.erase((*l).first);</div>
<div class="line"><a name="l00187"></a><span class="lineno"> 187</span>  }</div>
<div class="line"><a name="l00188"></a><span class="lineno"> 188</span>  }</div>
<div class="line"><a name="l00189"></a><span class="lineno"> 189</span> </div>
<div class="line"><a name="l00190"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#a3db85401f8535daf4054fde531cd46b1"> 190</a></span>  iterator <a class="code" href="classCVC3_1_1ExprMap.html#a3db85401f8535daf4054fde531cd46b1">begin</a>() { <span class="keywordflow">return</span> iterator(<a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a>.begin()); }</div>
<div class="line"><a name="l00191"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#a283ae6c44308cbdda0d82da5a16e52c8"> 191</a></span>  iterator <a class="code" href="classCVC3_1_1ExprMap.html#a283ae6c44308cbdda0d82da5a16e52c8">end</a>() { <span class="keywordflow">return</span> iterator(<a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a>.end()); }</div>
<div class="line"><a name="l00192"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#a347f85caefbf03fe8308125f6ccb2857"> 192</a></span>  const_iterator <a class="code" href="classCVC3_1_1ExprMap.html#a347f85caefbf03fe8308125f6ccb2857">begin</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> const_iterator(<a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a>.begin()); }</div>
<div class="line"><a name="l00193"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#a6cc77f91c512579e142b8569ecc89bd7"> 193</a></span>  const_iterator <a class="code" href="classCVC3_1_1ExprMap.html#a6cc77f91c512579e142b8569ecc89bd7">end</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> const_iterator(<a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a>.end()); }</div>
<div class="line"><a name="l00194"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#ae50ab1874dd63b575553e7db769abe28"> 194</a></span>  iterator <a class="code" href="classCVC3_1_1ExprMap.html#ae50ab1874dd63b575553e7db769abe28">find</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) { <span class="keywordflow">return</span> iterator(<a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a>.find(e)); }</div>
<div class="line"><a name="l00195"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#af705ffda7fc59b727775311d21ee0e75"> 195</a></span>  const_iterator <a class="code" href="classCVC3_1_1ExprMap.html#af705ffda7fc59b727775311d21ee0e75">find</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> const_iterator(<a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a>.find(e)); }</div>
<div class="line"><a name="l00196"></a><span class="lineno"> 196</span> </div>
<div class="line"><a name="l00197"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#a319469b0a35fc68ed7ff75dcccc56359"> 197</a></span>  <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprMap.html#a319469b0a35fc68ed7ff75dcccc56359">operator==</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a>& m1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a>& m2) {</div>
<div class="line"><a name="l00198"></a><span class="lineno"> 198</span>  <span class="keywordflow">return</span> m1.<a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a> == m2.<a class="code" href="classCVC3_1_1ExprMap.html#a6241e6eb48ce7304d0e1e73d57a0eb20">d_map</a>;</div>
<div class="line"><a name="l00199"></a><span class="lineno"> 199</span>  }</div>
<div class="line"><a name="l00200"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprMap.html#a84df2ed8e4e875eae591adb7c3d5f301"> 200</a></span>  <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprMap.html#a84df2ed8e4e875eae591adb7c3d5f301">operator!=</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a>& m1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a>& m2) {</div>
<div class="line"><a name="l00201"></a><span class="lineno"> 201</span>  <span class="keywordflow">return</span> !(m1 == m2);</div>
<div class="line"><a name="l00202"></a><span class="lineno"> 202</span>  }</div>
<div class="line"><a name="l00203"></a><span class="lineno"> 203</span>  }; <span class="comment">// end of class ExprMap</span></div>
<div class="line"><a name="l00204"></a><span class="lineno"> 204</span> </div>
<div class="line"><a name="l00205"></a><span class="lineno"> 205</span>  <span class="keyword">template</span><<span class="keyword">class</span> Data></div>
<div class="line"><a name="l00206"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html"> 206</a></span>  <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a> {</div>
<div class="line"><a name="l00207"></a><span class="lineno"> 207</span>  <span class="keyword">private</span>:</div>
<div class="line"><a name="l00208"></a><span class="lineno"> 208</span> </div>
<div class="line"><a name="l00209"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#a578d3b96ce2e21e0997603e61b006ef6"> 209</a></span>  <span class="keyword">typedef</span> <a class="code" href="classHash_1_1hash__map.html">std::hash_map<Expr, Data></a> <a class="code" href="classCVC3_1_1ExprHashMap.html#a578d3b96ce2e21e0997603e61b006ef6">ExprHashMapType</a>;</div>
<div class="line"><a name="l00210"></a><span class="lineno"> 210</span>  <span class="comment">// Private members</span></div>
<div class="line"><a name="l00211"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca"> 211</a></span>  <a class="code" href="classHash_1_1hash__map.html">ExprHashMapType</a> <a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a>;</div>
<div class="line"><a name="l00212"></a><span class="lineno"> 212</span> </div>
<div class="line"><a name="l00213"></a><span class="lineno"> 213</span>  <span class="keyword">public</span>:</div>
<div class="line"><a name="l00214"></a><span class="lineno"> 214</span> </div>
<div class="line"><a name="l00215"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html"> 215</a></span>  <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html">const_iterator</a>: <span class="keyword">public</span> std::iterator<std::input_iterator_tag, std::pair<Expr,Data>,std::ptrdiff_t> {</div>
<div class="line"><a name="l00216"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#a09556ca6a1d3ba2b3df351f6dee5cb37"> 216</a></span>  <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>;</div>
<div class="line"><a name="l00217"></a><span class="lineno"> 217</span>  <span class="keyword">private</span>:</div>
<div class="line"><a name="l00218"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#aae67dcc0156d8df9b6bf09de2da74d9f"> 218</a></span>  <span class="keyword">typename</span> <a class="code" href="classHash_1_1hash__map.html#a34789fb591a84314e78bd17b69aa6065">ExprHashMapType::const_iterator</a> <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#aae67dcc0156d8df9b6bf09de2da74d9f">d_it</a>;</div>
<div class="line"><a name="l00219"></a><span class="lineno"> 219</span>  <span class="comment">// Private constructor</span></div>
<div class="line"><a name="l00220"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#a39634829c269a15dd5ce327923d04bec"> 220</a></span>  <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#af0583093737a30de8e42d0c3ce697c88">const_iterator</a>(<span class="keyword">const</span> <span class="keyword">typename</span> <a class="code" href="classHash_1_1hash__map.html#a34789fb591a84314e78bd17b69aa6065">ExprHashMapType::const_iterator</a>& it)</div>
<div class="line"><a name="l00221"></a><span class="lineno"> 221</span>  : <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#aae67dcc0156d8df9b6bf09de2da74d9f">d_it</a>(it) { }</div>
<div class="line"><a name="l00222"></a><span class="lineno"> 222</span>  <span class="keyword">public</span>:</div>
<div class="line"><a name="l00223"></a><span class="lineno"> 223</span>  <span class="comment">// Default constructor</span></div>
<div class="line"><a name="l00224"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#af0583093737a30de8e42d0c3ce697c88"> 224</a></span>  <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#af0583093737a30de8e42d0c3ce697c88">const_iterator</a>() { }</div>
<div class="line"><a name="l00225"></a><span class="lineno"> 225</span>  <span class="comment">// (Dis)equality</span></div>
<div class="line"><a name="l00226"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#a5902eddc41369311f738fdd40aada5bf"> 226</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#a5902eddc41369311f738fdd40aada5bf">operator==</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html">const_iterator</a>& i)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#aae67dcc0156d8df9b6bf09de2da74d9f">d_it</a> == i.<a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#aae67dcc0156d8df9b6bf09de2da74d9f">d_it</a>; }</div>
<div class="line"><a name="l00227"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#a597e73348b54d3ef747f6394a4d59fb1"> 227</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#a597e73348b54d3ef747f6394a4d59fb1">operator!=</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html">const_iterator</a>& i)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#aae67dcc0156d8df9b6bf09de2da74d9f">d_it</a> != i.<a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#aae67dcc0156d8df9b6bf09de2da74d9f">d_it</a>; }</div>
<div class="line"><a name="l00228"></a><span class="lineno"> 228</span>  <span class="comment">// Dereference operators.</span></div>
<div class="line"><a name="l00229"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#a361af3103afa93f47dfab8a1a01a06e1"> 229</a></span>  <span class="keyword">const</span> std::pair<const Expr,Data>& <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#a361af3103afa93f47dfab8a1a01a06e1">operator*</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> *<a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#aae67dcc0156d8df9b6bf09de2da74d9f">d_it</a>; }</div>
<div class="line"><a name="l00230"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#a4085ad1b63cc296d1f121239766fffac"> 230</a></span>  <span class="keyword">const</span> std::pair<const Expr,Data>* <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#a4085ad1b63cc296d1f121239766fffac">operator-></a>()<span class="keyword"> const </span>{</div>
<div class="line"><a name="l00231"></a><span class="lineno"> 231</span>  <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#aae67dcc0156d8df9b6bf09de2da74d9f">d_it</a>.operator->();</div>
<div class="line"><a name="l00232"></a><span class="lineno"> 232</span>  }</div>
<div class="line"><a name="l00233"></a><span class="lineno"> 233</span>  <span class="comment">// Prefix increment</span></div>
<div class="line"><a name="l00234"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#a0c37de4d81598233fbc1d32253457ed8"> 234</a></span>  <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html">const_iterator</a>& <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#a0c37de4d81598233fbc1d32253457ed8">operator++</a>() { ++<a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#aae67dcc0156d8df9b6bf09de2da74d9f">d_it</a>; <span class="keywordflow">return</span> *<span class="keyword">this</span>; }</div>
<div class="line"><a name="l00235"></a><span class="lineno"> 235</span>  <span class="comment">// Postfix increment: requires a Proxy object to hold the</span></div>
<div class="line"><a name="l00236"></a><span class="lineno"> 236</span>  <span class="comment">// intermediate value for dereferencing</span></div>
<div class="line"><a name="l00237"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator_1_1Proxy.html"> 237</a></span>  <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator_1_1Proxy.html">Proxy</a> {</div>
<div class="line"><a name="l00238"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator_1_1Proxy.html#add630532a1537003054e5c7602c69879"> 238</a></span>  <span class="keyword">const</span> std::pair<const Expr,Data>& <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator_1_1Proxy.html#add630532a1537003054e5c7602c69879">d_pair</a>;</div>
<div class="line"><a name="l00239"></a><span class="lineno"> 239</span>  <span class="keyword">public</span>:</div>
<div class="line"><a name="l00240"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator_1_1Proxy.html#a88357aa5b15ebe24bcdbb94d8993418f"> 240</a></span>  <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator_1_1Proxy.html#a88357aa5b15ebe24bcdbb94d8993418f">Proxy</a>(<span class="keyword">const</span> std::pair<Expr,Data>& pair) : <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator_1_1Proxy.html#add630532a1537003054e5c7602c69879">d_pair</a>(pair) { }</div>
<div class="line"><a name="l00241"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator_1_1Proxy.html#af81bc8d0bb360dc89df6cc20644c7fed"> 241</a></span>  std::pair<const Expr,Data> <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator_1_1Proxy.html#af81bc8d0bb360dc89df6cc20644c7fed">operator*</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator_1_1Proxy.html#add630532a1537003054e5c7602c69879">d_pair</a>; }</div>
<div class="line"><a name="l00242"></a><span class="lineno"> 242</span>  }; <span class="comment">// end of class Proxy</span></div>
<div class="line"><a name="l00243"></a><span class="lineno"> 243</span>  <span class="comment">// Actual postfix increment: returns Proxy with the old value.</span></div>
<div class="line"><a name="l00244"></a><span class="lineno"> 244</span>  <span class="comment">// Now, an expression like *i++ will return the current *i, and</span></div>
<div class="line"><a name="l00245"></a><span class="lineno"> 245</span>  <span class="comment">// then advance the iterator. However, don't try to use Proxy for</span></div>
<div class="line"><a name="l00246"></a><span class="lineno"> 246</span>  <span class="comment">// anything else.</span></div>
<div class="line"><a name="l00247"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#af3869606d6c9c76f597edceb4475ec00"> 247</a></span>  <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator_1_1Proxy.html">Proxy</a> <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html#af3869606d6c9c76f597edceb4475ec00">operator++</a>(<span class="keywordtype">int</span>) {</div>
<div class="line"><a name="l00248"></a><span class="lineno"> 248</span>  <a class="code" href="classCVC3_1_1ExprHashMap_1_1const__iterator_1_1Proxy.html">Proxy</a> tmp(*(*<span class="keyword">this</span>));</div>
<div class="line"><a name="l00249"></a><span class="lineno"> 249</span>  ++(*this);</div>
<div class="line"><a name="l00250"></a><span class="lineno"> 250</span>  <span class="keywordflow">return</span> tmp;</div>
<div class="line"><a name="l00251"></a><span class="lineno"> 251</span>  }</div>
<div class="line"><a name="l00252"></a><span class="lineno"> 252</span>  }; <span class="comment">// end of class const_iterator</span></div>
<div class="line"><a name="l00253"></a><span class="lineno"> 253</span> </div>
<div class="line"><a name="l00254"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html"> 254</a></span>  <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html">iterator</a>: <span class="keyword">public</span> std::iterator<std::input_iterator_tag, std::pair<Expr,Data>,std::ptrdiff_t> {</div>
<div class="line"><a name="l00255"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a09556ca6a1d3ba2b3df351f6dee5cb37"> 255</a></span>  <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>;</div>
<div class="line"><a name="l00256"></a><span class="lineno"> 256</span>  <span class="keyword">private</span>:</div>
<div class="line"><a name="l00257"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a925d1de55893af024a3567f20df0a71a"> 257</a></span>  <span class="keyword">typename</span> <a class="code" href="classHash_1_1hash__map.html#a0fae180472ddfd8822c881caf23c11a9">ExprHashMapType::iterator</a> <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a925d1de55893af024a3567f20df0a71a">d_it</a>;</div>
<div class="line"><a name="l00258"></a><span class="lineno"> 258</span>  <span class="comment">// Private constructor</span></div>
<div class="line"><a name="l00259"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a7182951dee91d9d36761482ce98ecd43"> 259</a></span>  <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a21b803efa155e623a151b87586720481">iterator</a>(<span class="keyword">const</span> <span class="keyword">typename</span> <a class="code" href="classHash_1_1hash__map.html#a0fae180472ddfd8822c881caf23c11a9">ExprHashMapType::iterator</a>& it)</div>
<div class="line"><a name="l00260"></a><span class="lineno"> 260</span>  : <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a925d1de55893af024a3567f20df0a71a">d_it</a>(it) { }</div>
<div class="line"><a name="l00261"></a><span class="lineno"> 261</span>  <span class="keyword">public</span>:</div>
<div class="line"><a name="l00262"></a><span class="lineno"> 262</span>  <span class="comment">// Default constructor</span></div>
<div class="line"><a name="l00263"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a21b803efa155e623a151b87586720481"> 263</a></span>  <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a21b803efa155e623a151b87586720481">iterator</a>() { }</div>
<div class="line"><a name="l00264"></a><span class="lineno"> 264</span>  <span class="comment">// (Dis)equality</span></div>
<div class="line"><a name="l00265"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#ab2b3ba1e93fe6964216e85168594d818"> 265</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#ab2b3ba1e93fe6964216e85168594d818">operator==</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html">iterator</a>& i)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a925d1de55893af024a3567f20df0a71a">d_it</a> == i.<a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a925d1de55893af024a3567f20df0a71a">d_it</a>; }</div>
<div class="line"><a name="l00266"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a789fb4cd5918fb18b089ea8361ddc149"> 266</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a789fb4cd5918fb18b089ea8361ddc149">operator!=</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html">iterator</a>& i)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a925d1de55893af024a3567f20df0a71a">d_it</a> != i.<a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a925d1de55893af024a3567f20df0a71a">d_it</a>; }</div>
<div class="line"><a name="l00267"></a><span class="lineno"> 267</span>  <span class="comment">// Dereference operators.</span></div>
<div class="line"><a name="l00268"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#adb6561793ee7210d81749d17159fb767"> 268</a></span>  std::pair<const Expr,Data>& <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#adb6561793ee7210d81749d17159fb767">operator*</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> *<a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a925d1de55893af024a3567f20df0a71a">d_it</a>; }</div>
<div class="line"><a name="l00269"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#ae9f9392f0998d681ebda2471195eb4ef"> 269</a></span>  std::pair<const Expr,Data>* <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#ae9f9392f0998d681ebda2471195eb4ef">operator-></a>()<span class="keyword"> const </span>{</div>
<div class="line"><a name="l00270"></a><span class="lineno"> 270</span>  <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a925d1de55893af024a3567f20df0a71a">d_it</a>.operator->();</div>
<div class="line"><a name="l00271"></a><span class="lineno"> 271</span>  }</div>
<div class="line"><a name="l00272"></a><span class="lineno"> 272</span>  <span class="comment">// Prefix increment</span></div>
<div class="line"><a name="l00273"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a07579d1211a9cee1e59413cc8cd5d05b"> 273</a></span>  <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html">iterator</a>& <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a07579d1211a9cee1e59413cc8cd5d05b">operator++</a>() { ++<a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a925d1de55893af024a3567f20df0a71a">d_it</a>; <span class="keywordflow">return</span> *<span class="keyword">this</span>; }</div>
<div class="line"><a name="l00274"></a><span class="lineno"> 274</span>  <span class="comment">// Postfix increment: requires a Proxy object to hold the</span></div>
<div class="line"><a name="l00275"></a><span class="lineno"> 275</span>  <span class="comment">// intermediate value for dereferencing</span></div>
<div class="line"><a name="l00276"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator_1_1Proxy.html"> 276</a></span>  <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator_1_1Proxy.html">Proxy</a> {</div>
<div class="line"><a name="l00277"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator_1_1Proxy.html#a2582594b08df0cf92d638d5b9b2664aa"> 277</a></span>  std::pair<const Expr,Data>& <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator_1_1Proxy.html#a2582594b08df0cf92d638d5b9b2664aa">d_pair</a>;</div>
<div class="line"><a name="l00278"></a><span class="lineno"> 278</span>  <span class="keyword">public</span>:</div>
<div class="line"><a name="l00279"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator_1_1Proxy.html#aae381aa71cac430c454af93eb468b4b7"> 279</a></span>  <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator_1_1Proxy.html#aae381aa71cac430c454af93eb468b4b7">Proxy</a>(std::pair<const Expr,Data>& pair) : <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator_1_1Proxy.html#a2582594b08df0cf92d638d5b9b2664aa">d_pair</a>(pair) { }</div>
<div class="line"><a name="l00280"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator_1_1Proxy.html#ab1f67df105a19f5342f4368cfb909e6a"> 280</a></span>  std::pair<const Expr,Data> <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator_1_1Proxy.html#ab1f67df105a19f5342f4368cfb909e6a">operator*</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator_1_1Proxy.html#a2582594b08df0cf92d638d5b9b2664aa">d_pair</a>; }</div>
<div class="line"><a name="l00281"></a><span class="lineno"> 281</span>  }; <span class="comment">// end of class Proxy</span></div>
<div class="line"><a name="l00282"></a><span class="lineno"> 282</span>  <span class="comment">// Actual postfix increment: returns Proxy with the old value.</span></div>
<div class="line"><a name="l00283"></a><span class="lineno"> 283</span>  <span class="comment">// Now, an expression like *i++ will return the current *i, and</span></div>
<div class="line"><a name="l00284"></a><span class="lineno"> 284</span>  <span class="comment">// then advance the iterator. However, don't try to use Proxy for</span></div>
<div class="line"><a name="l00285"></a><span class="lineno"> 285</span>  <span class="comment">// anything else.</span></div>
<div class="line"><a name="l00286"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a83da91bfb2451c07d4fe266b43ca99f6"> 286</a></span>  <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator_1_1Proxy.html">Proxy</a> <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator.html#a83da91bfb2451c07d4fe266b43ca99f6">operator++</a>(<span class="keywordtype">int</span>) {</div>
<div class="line"><a name="l00287"></a><span class="lineno"> 287</span>  <a class="code" href="classCVC3_1_1ExprHashMap_1_1iterator_1_1Proxy.html">Proxy</a> tmp(*(*<span class="keyword">this</span>));</div>
<div class="line"><a name="l00288"></a><span class="lineno"> 288</span>  ++(*this);</div>
<div class="line"><a name="l00289"></a><span class="lineno"> 289</span>  <span class="keywordflow">return</span> tmp;</div>
<div class="line"><a name="l00290"></a><span class="lineno"> 290</span>  }</div>
<div class="line"><a name="l00291"></a><span class="lineno"> 291</span>  }; <span class="comment">// end of class iterator</span></div>
<div class="line"><a name="l00292"></a><span class="lineno"> 292</span> <span class="comment"></span></div>
<div class="line"><a name="l00293"></a><span class="lineno"> 293</span> <span class="comment"> //////////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00294"></a><span class="lineno"> 294</span> <span class="comment"></span> <span class="comment">// Public methods</span><span class="comment"></span></div>
<div class="line"><a name="l00295"></a><span class="lineno"> 295</span> <span class="comment"> //////////////////////////////////////////////////////////////////////////</span></div>
<div class="line"><a name="l00296"></a><span class="lineno"> 296</span> <span class="comment"></span><span class="comment"></span></div>
<div class="line"><a name="l00297"></a><span class="lineno"> 297</span> <span class="comment"> //! Default constructor</span></div>
<div class="line"><a name="l00298"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#a10db8a05fc988fcdf829290fd76b3aa7"> 298</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1ExprHashMap.html#a10db8a05fc988fcdf829290fd76b3aa7" title="Default constructor.">ExprHashMap</a>() { }<span class="comment"></span></div>
<div class="line"><a name="l00299"></a><span class="lineno"> 299</span> <span class="comment"> //! Constructor specifying the initial number of buckets</span></div>
<div class="line"><a name="l00300"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#afd06f26950a017d13b5ea50289880596"> 300</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1ExprHashMap.html#afd06f26950a017d13b5ea50289880596" title="Constructor specifying the initial number of buckets.">ExprHashMap</a>(<span class="keywordtype">size_t</span> n): <a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a>(n) { }</div>
<div class="line"><a name="l00301"></a><span class="lineno"> 301</span>  <span class="comment">// Copy constructor</span></div>
<div class="line"><a name="l00302"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#af06cf167cea59e5ae7badaa9f0ebe3e9"> 302</a></span>  <a class="code" href="classCVC3_1_1ExprHashMap.html#af06cf167cea59e5ae7badaa9f0ebe3e9">ExprHashMap</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>& map): <a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a>(map.<a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a>) { }</div>
<div class="line"><a name="l00303"></a><span class="lineno"> 303</span> </div>
<div class="line"><a name="l00304"></a><span class="lineno"> 304</span>  <span class="comment">// Other methods</span></div>
<div class="line"><a name="l00305"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#acacf635065039ccea5acb5b91dbaa4bb"> 305</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprHashMap.html#acacf635065039ccea5acb5b91dbaa4bb">empty</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a>.<a class="code" href="classHash_1_1hash__map.html#a12f477e90d48f319433bb5cc605ce00f">empty</a>(); }</div>
<div class="line"><a name="l00306"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#a9d792cf5282604c376d329ae325c983e"> 306</a></span>  <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1ExprHashMap.html#a9d792cf5282604c376d329ae325c983e">size</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a>.<a class="code" href="classHash_1_1hash__map.html#a1440a04e68060e58f053a38976bc6f9b">size</a>(); }</div>
<div class="line"><a name="l00307"></a><span class="lineno"> 307</span> </div>
<div class="line"><a name="l00308"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#a7819727fbff7291cd64e99511d730bf7"> 308</a></span>  <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1ExprHashMap.html#a7819727fbff7291cd64e99511d730bf7">count</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a>.<a class="code" href="classHash_1_1hash__map.html#a3d52fe0d391d58e9573ce84472dfea24">count</a>(e); }</div>
<div class="line"><a name="l00309"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#a373ccb2d238750dbe7f97e8d1b8599ba"> 309</a></span>  Data& <a class="code" href="classCVC3_1_1ExprHashMap.html#a373ccb2d238750dbe7f97e8d1b8599ba">operator[]</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a>[e]; }</div>
<div class="line"><a name="l00310"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#aa20f14dba09537171af45bf479b99c66"> 310</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ExprHashMap.html#aa20f14dba09537171af45bf479b99c66">clear</a>() { <a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a>.<a class="code" href="classHash_1_1hash__map.html#a18703659be23b5ff0b7d7b5c796e6abd">clear</a>(); }</div>
<div class="line"><a name="l00311"></a><span class="lineno"> 311</span> </div>
<div class="line"><a name="l00312"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#a7fb3e24bb67239243212af626cc2f976"> 312</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ExprHashMap.html#a7fb3e24bb67239243212af626cc2f976">insert</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keyword">const</span> Data& d) { <a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a>[e] = d; }</div>
<div class="line"><a name="l00313"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#a77637e1f3754b7153cbd1b903a5acb76"> 313</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ExprHashMap.html#a77637e1f3754b7153cbd1b903a5acb76">erase</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) { <a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a>.<a class="code" href="classHash_1_1hash__map.html#a9e69b0959edfd246d77df4097a24aaae">erase</a>(e); }</div>
<div class="line"><a name="l00314"></a><span class="lineno"> 314</span> </div>
<div class="line"><a name="l00315"></a><span class="lineno"> 315</span>  <span class="keyword">template</span><<span class="keyword">class</span> InputIterator></div>
<div class="line"><a name="l00316"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#ace00ef7f782ac879a2956e35e157e860"> 316</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ExprHashMap.html#ace00ef7f782ac879a2956e35e157e860">insert</a>(InputIterator l, InputIterator r) { <a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a>.<a class="code" href="classHash_1_1hash__map.html#ac90ce3f2c448b2c9c633fb417f4b171d">insert</a>(l,r); }</div>
<div class="line"><a name="l00317"></a><span class="lineno"> 317</span> </div>
<div class="line"><a name="l00318"></a><span class="lineno"> 318</span>  <span class="keyword">template</span><<span class="keyword">class</span> InputIterator></div>
<div class="line"><a name="l00319"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#a1734babe9550a306aa049c352cf31d82"> 319</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ExprHashMap.html#a1734babe9550a306aa049c352cf31d82">erase</a>(InputIterator l, InputIterator r) {</div>
<div class="line"><a name="l00320"></a><span class="lineno"> 320</span>  <span class="keywordflow">for</span>(; l!=r; ++l) {</div>
<div class="line"><a name="l00321"></a><span class="lineno"> 321</span>  <a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a>.<a class="code" href="classHash_1_1hash__map.html#a9e69b0959edfd246d77df4097a24aaae">erase</a>((*l).first);</div>
<div class="line"><a name="l00322"></a><span class="lineno"> 322</span>  }</div>
<div class="line"><a name="l00323"></a><span class="lineno"> 323</span>  }</div>
<div class="line"><a name="l00324"></a><span class="lineno"> 324</span> </div>
<div class="line"><a name="l00325"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#a1a0ea7ed7eb73e3f08ccce9f29e90c71"> 325</a></span>  iterator <a class="code" href="classCVC3_1_1ExprHashMap.html#a1a0ea7ed7eb73e3f08ccce9f29e90c71">begin</a>() { <span class="keywordflow">return</span> iterator(<a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a>.<a class="code" href="classHash_1_1hash__map.html#a478f2d66eb11d4ca51bc2b630373e9ad" title="iterators">begin</a>()); }</div>
<div class="line"><a name="l00326"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#a0ea2aa250fd1431c311d83f32862bba7"> 326</a></span>  iterator <a class="code" href="classCVC3_1_1ExprHashMap.html#a0ea2aa250fd1431c311d83f32862bba7">end</a>() { <span class="keywordflow">return</span> iterator(<a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a>.<a class="code" href="classHash_1_1hash__map.html#a2c776e055f3d17226605157e1c37dbc9">end</a>()); }</div>
<div class="line"><a name="l00327"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#a24ec23a15b7f6c121042f4b28fd83615"> 327</a></span>  const_iterator <a class="code" href="classCVC3_1_1ExprHashMap.html#a24ec23a15b7f6c121042f4b28fd83615">begin</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> const_iterator(<a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a>.<a class="code" href="classHash_1_1hash__map.html#a478f2d66eb11d4ca51bc2b630373e9ad" title="iterators">begin</a>()); }</div>
<div class="line"><a name="l00328"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#ad99d1aa47182ed209670d3b7bdef61f5"> 328</a></span>  const_iterator <a class="code" href="classCVC3_1_1ExprHashMap.html#ad99d1aa47182ed209670d3b7bdef61f5">end</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> const_iterator(<a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a>.<a class="code" href="classHash_1_1hash__map.html#a2c776e055f3d17226605157e1c37dbc9">end</a>()); }</div>
<div class="line"><a name="l00329"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#aeffd58f05fbeb8f381ba2050adef7a2d"> 329</a></span>  iterator <a class="code" href="classCVC3_1_1ExprHashMap.html#aeffd58f05fbeb8f381ba2050adef7a2d">find</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) { <span class="keywordflow">return</span> iterator(<a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a>.<a class="code" href="classHash_1_1hash__map.html#af3317f9087a35d09985b6513c45d2ab8" title="operations">find</a>(e)); }</div>
<div class="line"><a name="l00330"></a><span class="lineno"><a class="code" href="classCVC3_1_1ExprHashMap.html#aaa311b8de687f72bf8a7296a3e68ef46"> 330</a></span>  const_iterator <a class="code" href="classCVC3_1_1ExprHashMap.html#aaa311b8de687f72bf8a7296a3e68ef46">find</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> const_iterator(<a class="code" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a>.<a class="code" href="classHash_1_1hash__map.html#af3317f9087a35d09985b6513c45d2ab8" title="operations">find</a>(e)); }</div>
<div class="line"><a name="l00331"></a><span class="lineno"> 331</span> </div>
<div class="line"><a name="l00332"></a><span class="lineno"> 332</span>  <span class="comment">// These aren't implemented</span></div>
<div class="line"><a name="l00333"></a><span class="lineno"> 333</span> <span class="comment">// friend bool operator==(const ExprHashMap& m1, const ExprHashMap& m2) {</span></div>
<div class="line"><a name="l00334"></a><span class="lineno"> 334</span> <span class="comment">// return m1.d_map == m2.d_map;</span></div>
<div class="line"><a name="l00335"></a><span class="lineno"> 335</span> <span class="comment">// }</span></div>
<div class="line"><a name="l00336"></a><span class="lineno"> 336</span> <span class="comment">// friend bool operator!=(const ExprHashMap& m1, const ExprHashMap& m2) {</span></div>
<div class="line"><a name="l00337"></a><span class="lineno"> 337</span> <span class="comment">// return !(m1 == m2);</span></div>
<div class="line"><a name="l00338"></a><span class="lineno"> 338</span> <span class="comment">// }</span></div>
<div class="line"><a name="l00339"></a><span class="lineno"> 339</span>  }; <span class="comment">// end of class ExprHashMap</span></div>
<div class="line"><a name="l00340"></a><span class="lineno"> 340</span> </div>
<div class="line"><a name="l00341"></a><span class="lineno"> 341</span> } <span class="comment">// end of namespace CVC3</span></div>
<div class="line"><a name="l00342"></a><span class="lineno"> 342</span> </div>
<div class="line"><a name="l00343"></a><span class="lineno"> 343</span> <span class="preprocessor">#endif</span></div>
</div><!-- fragment --></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:14 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
