<!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: CVC3::ExprHashMap< Data > Class Template Reference</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 class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="inherits.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a></li><li class="navelem"><a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="summary">
<a href="#nested-classes">Classes</a> |
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pri-types">Private Types</a> |
<a href="#pri-attribs">Private Attributes</a> |
<a href="classCVC3_1_1ExprHashMap-members.html">List of all members</a> </div>
<div class="headertitle">
<div class="title">CVC3::ExprHashMap< Data > Class Template Reference</div> </div>
</div><!--header-->
<div class="contents">
<p><code>#include <<a class="el" href="expr__map_8h_source.html">expr_map.h</a>></code></p>
<div class="dynheader">
Collaboration diagram for CVC3::ExprHashMap< Data >:</div>
<div class="dyncontent">
<div class="center"><img src="classCVC3_1_1ExprHashMap__coll__graph.gif" border="0" usemap="#CVC3_1_1ExprHashMap_3_01Data_01_4_coll__map" alt="Collaboration graph"/></div>
<map name="CVC3_1_1ExprHashMap_3_01Data_01_4_coll__map" id="CVC3_1_1ExprHashMap_3_01Data_01_4_coll__map">
</map>
</div>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="nested-classes"></a>
Classes</h2></td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">class  </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html">const_iterator</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">class  </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap_1_1iterator.html">iterator</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pub-methods"></a>
Public Member Functions</h2></td></tr>
<tr class="memitem:a10db8a05fc988fcdf829290fd76b3aa7"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#a10db8a05fc988fcdf829290fd76b3aa7">ExprHashMap</a> ()</td></tr>
<tr class="memdesc:a10db8a05fc988fcdf829290fd76b3aa7"><td class="mdescLeft"> </td><td class="mdescRight">Default constructor. <a href="#a10db8a05fc988fcdf829290fd76b3aa7"></a><br/></td></tr>
<tr class="separator:a10db8a05fc988fcdf829290fd76b3aa7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:afd06f26950a017d13b5ea50289880596"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#afd06f26950a017d13b5ea50289880596">ExprHashMap</a> (size_t n)</td></tr>
<tr class="memdesc:afd06f26950a017d13b5ea50289880596"><td class="mdescLeft"> </td><td class="mdescRight">Constructor specifying the initial number of buckets. <a href="#afd06f26950a017d13b5ea50289880596"></a><br/></td></tr>
<tr class="separator:afd06f26950a017d13b5ea50289880596"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af06cf167cea59e5ae7badaa9f0ebe3e9"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#af06cf167cea59e5ae7badaa9f0ebe3e9">ExprHashMap</a> (const <a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a> &map)</td></tr>
<tr class="separator:af06cf167cea59e5ae7badaa9f0ebe3e9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:acacf635065039ccea5acb5b91dbaa4bb"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#acacf635065039ccea5acb5b91dbaa4bb">empty</a> () const </td></tr>
<tr class="separator:acacf635065039ccea5acb5b91dbaa4bb"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9d792cf5282604c376d329ae325c983e"><td class="memItemLeft" align="right" valign="top">size_t </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#a9d792cf5282604c376d329ae325c983e">size</a> () const </td></tr>
<tr class="separator:a9d792cf5282604c376d329ae325c983e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a7819727fbff7291cd64e99511d730bf7"><td class="memItemLeft" align="right" valign="top">size_t </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#a7819727fbff7291cd64e99511d730bf7">count</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e) const </td></tr>
<tr class="separator:a7819727fbff7291cd64e99511d730bf7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a373ccb2d238750dbe7f97e8d1b8599ba"><td class="memItemLeft" align="right" valign="top">Data & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#a373ccb2d238750dbe7f97e8d1b8599ba">operator[]</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:a373ccb2d238750dbe7f97e8d1b8599ba"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa20f14dba09537171af45bf479b99c66"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#aa20f14dba09537171af45bf479b99c66">clear</a> ()</td></tr>
<tr class="separator:aa20f14dba09537171af45bf479b99c66"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a7fb3e24bb67239243212af626cc2f976"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#a7fb3e24bb67239243212af626cc2f976">insert</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const Data &d)</td></tr>
<tr class="separator:a7fb3e24bb67239243212af626cc2f976"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a77637e1f3754b7153cbd1b903a5acb76"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#a77637e1f3754b7153cbd1b903a5acb76">erase</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:a77637e1f3754b7153cbd1b903a5acb76"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ace00ef7f782ac879a2956e35e157e860"><td class="memTemplParams" colspan="2">template<class InputIterator > </td></tr>
<tr class="memitem:ace00ef7f782ac879a2956e35e157e860"><td class="memTemplItemLeft" align="right" valign="top">void </td><td class="memTemplItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#ace00ef7f782ac879a2956e35e157e860">insert</a> (InputIterator l, InputIterator r)</td></tr>
<tr class="separator:ace00ef7f782ac879a2956e35e157e860"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1734babe9550a306aa049c352cf31d82"><td class="memTemplParams" colspan="2">template<class InputIterator > </td></tr>
<tr class="memitem:a1734babe9550a306aa049c352cf31d82"><td class="memTemplItemLeft" align="right" valign="top">void </td><td class="memTemplItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#a1734babe9550a306aa049c352cf31d82">erase</a> (InputIterator l, InputIterator r)</td></tr>
<tr class="separator:a1734babe9550a306aa049c352cf31d82"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1a0ea7ed7eb73e3f08ccce9f29e90c71"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprHashMap_1_1iterator.html">iterator</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#a1a0ea7ed7eb73e3f08ccce9f29e90c71">begin</a> ()</td></tr>
<tr class="separator:a1a0ea7ed7eb73e3f08ccce9f29e90c71"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0ea2aa250fd1431c311d83f32862bba7"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprHashMap_1_1iterator.html">iterator</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#a0ea2aa250fd1431c311d83f32862bba7">end</a> ()</td></tr>
<tr class="separator:a0ea2aa250fd1431c311d83f32862bba7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a24ec23a15b7f6c121042f4b28fd83615"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html">const_iterator</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#a24ec23a15b7f6c121042f4b28fd83615">begin</a> () const </td></tr>
<tr class="separator:a24ec23a15b7f6c121042f4b28fd83615"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad99d1aa47182ed209670d3b7bdef61f5"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html">const_iterator</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#ad99d1aa47182ed209670d3b7bdef61f5">end</a> () const </td></tr>
<tr class="separator:ad99d1aa47182ed209670d3b7bdef61f5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aeffd58f05fbeb8f381ba2050adef7a2d"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprHashMap_1_1iterator.html">iterator</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#aeffd58f05fbeb8f381ba2050adef7a2d">find</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:aeffd58f05fbeb8f381ba2050adef7a2d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aaa311b8de687f72bf8a7296a3e68ef46"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html">const_iterator</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#aaa311b8de687f72bf8a7296a3e68ef46">find</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e) const </td></tr>
<tr class="separator:aaa311b8de687f72bf8a7296a3e68ef46"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-types"></a>
Private Types</h2></td></tr>
<tr class="memitem:a578d3b96ce2e21e0997603e61b006ef6"><td class="memItemLeft" align="right" valign="top">typedef <a class="el" href="classHash_1_1hash__map.html">std::hash_map</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, Data > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#a578d3b96ce2e21e0997603e61b006ef6">ExprHashMapType</a></td></tr>
<tr class="separator:a578d3b96ce2e21e0997603e61b006ef6"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-attribs"></a>
Private Attributes</h2></td></tr>
<tr class="memitem:a2b821e44541ec2a2635cc8ac11f7d3ca"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprHashMap.html#a578d3b96ce2e21e0997603e61b006ef6">ExprHashMapType</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1ExprHashMap.html#a2b821e44541ec2a2635cc8ac11f7d3ca">d_map</a></td></tr>
<tr class="separator:a2b821e44541ec2a2635cc8ac11f7d3ca"><td class="memSeparator" colspan="2"> </td></tr>
</table>
<a name="details" id="details"></a><h2 class="groupheader">Detailed Description</h2>
<div class="textblock"><h3>template<class Data><br/>
class CVC3::ExprHashMap< Data ></h3>
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00206">206</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
</div><h2 class="groupheader">Member Typedef Documentation</h2>
<a class="anchor" id="a578d3b96ce2e21e0997603e61b006ef6"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">typedef <a class="el" href="classHash_1_1hash__map.html">std::hash_map</a><<a class="el" href="classCVC3_1_1Expr.html">Expr</a>, Data> <a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::<a class="el" href="classCVC3_1_1ExprHashMap.html#a578d3b96ce2e21e0997603e61b006ef6">ExprHashMapType</a></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00209">209</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
</div>
</div>
<h2 class="groupheader">Constructor & Destructor Documentation</h2>
<a class="anchor" id="a10db8a05fc988fcdf829290fd76b3aa7"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::<a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a> </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Default constructor. </p>
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00298">298</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
</div>
</div>
<a class="anchor" id="afd06f26950a017d13b5ea50289880596"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::<a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a> </td>
<td>(</td>
<td class="paramtype">size_t </td>
<td class="paramname"><em>n</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Constructor specifying the initial number of buckets. </p>
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00300">300</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
</div>
</div>
<a class="anchor" id="af06cf167cea59e5ae7badaa9f0ebe3e9"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::<a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a> </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>< Data > & </td>
<td class="paramname"><em>map</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00302">302</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Function Documentation</h2>
<a class="anchor" id="acacf635065039ccea5acb5b91dbaa4bb"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::empty </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00305">305</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
<p>Referenced by <a class="el" href="search__theorem__producer_8cpp_source.html#l00221">CVC3::SearchEngineTheoremProducer::conflictClause()</a>.</p>
</div>
</div>
<a class="anchor" id="a9d792cf5282604c376d329ae325c983e"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">size_t <a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::size </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00306">306</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
<p>Referenced by <a class="el" href="theory__uf_8cpp_source.html#l00509">CVC3::TheoryUF::computeModel()</a>, <a class="el" href="theory__array_8cpp_source.html#l00939">CVC3::TheoryArray::computeModel()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00226">CVC3::ExprManager::rebuild()</a>, and <a class="el" href="expr_8cpp_source.html#l00199">CVC3::Expr::substExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="a7819727fbff7291cd64e99511d730bf7"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">size_t <a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::count </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00308">308</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l03713">CVC3::TheoryCore::assignValue()</a>, <a class="el" href="theory__core_8cpp_source.html#l03862">CVC3::TheoryCore::buildModel()</a>, <a class="el" href="theory__core_8cpp_source.html#l03763">CVC3::TheoryCore::collectBasicVars()</a>, <a class="el" href="theory__core_8cpp_source.html#l03954">CVC3::TheoryCore::collectModelValues()</a>, and <a class="el" href="expr_8cpp_source.html#l00063">CVC3::Expr::recursiveSubst()</a>.</p>
</div>
</div>
<a class="anchor" id="a373ccb2d238750dbe7f97e8d1b8599ba"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Data& <a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::operator[] </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00309">309</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
</div>
</div>
<a class="anchor" id="aa20f14dba09537171af45bf479b99c66"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void <a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::clear </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00310">310</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
<p>Referenced by <a class="el" href="search__simple_8cpp_source.html#l00126">CVC3::SearchSimple::checkValidMain()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, <a class="el" href="theory__core_8cpp_source.html#l03763">CVC3::TheoryCore::collectBasicVars()</a>, <a class="el" href="theory__core_8cpp_source.html#l02055">CVC3::TheoryCore::print()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00317">CVC3::SearchImplBase::processResult()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00226">CVC3::ExprManager::rebuild()</a>, <a class="el" href="expr_8cpp_source.html#l00063">CVC3::Expr::recursiveSubst()</a>, and <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03867">CVC3::ArithTheoremProducerOld::rewriteLeavesConst()</a>.</p>
</div>
</div>
<a class="anchor" id="a7fb3e24bb67239243212af626cc2f976"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void <a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::insert </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const Data & </td>
<td class="paramname"><em>d</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00312">312</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
<p>Referenced by <a class="el" href="expr_8cpp_source.html#l00063">CVC3::Expr::recursiveSubst()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00621">CVC3::CoreTheoremProducer::rewriteAndSubterms()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00647">CVC3::CoreTheoremProducer::rewriteOrSubterms()</a>, <a class="el" href="expr_8cpp_source.html#l00178">CVC3::Expr::substExpr()</a>, and <a class="el" href="expr_8cpp_source.html#l00217">CVC3::Expr::substExprQuant()</a>.</p>
</div>
</div>
<a class="anchor" id="a77637e1f3754b7153cbd1b903a5acb76"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void <a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::erase </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00313">313</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00317">CVC3::SearchImplBase::processResult()</a>.</p>
</div>
</div>
<a class="anchor" id="ace00ef7f782ac879a2956e35e157e860"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<div class="memtemplate">
template<class InputIterator > </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void <a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::insert </td>
<td>(</td>
<td class="paramtype">InputIterator </td>
<td class="paramname"><em>l</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">InputIterator </td>
<td class="paramname"><em>r</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00316">316</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
</div>
</div>
<a class="anchor" id="a1734babe9550a306aa049c352cf31d82"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<div class="memtemplate">
template<class InputIterator > </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void <a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::erase </td>
<td>(</td>
<td class="paramtype">InputIterator </td>
<td class="paramname"><em>l</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">InputIterator </td>
<td class="paramname"><em>r</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00319">319</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
</div>
</div>
<a class="anchor" id="a1a0ea7ed7eb73e3f08ccce9f29e90c71"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprHashMap_1_1iterator.html">iterator</a> <a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::begin </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00325">325</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
<p>Referenced by <a class="el" href="theory__uf_8cpp_source.html#l00509">CVC3::TheoryUF::computeModel()</a>, <a class="el" href="theory__array_8cpp_source.html#l00939">CVC3::TheoryArray::computeModel()</a>, <a class="el" href="expr_8cpp_source.html#l00063">CVC3::Expr::recursiveSubst()</a>, and <a class="el" href="expr_8cpp_source.html#l00199">CVC3::Expr::substExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="a0ea2aa250fd1431c311d83f32862bba7"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprHashMap_1_1iterator.html">iterator</a> <a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::end </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00326">326</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l03862">CVC3::TheoryCore::buildModel()</a>, <a class="el" href="theory__core_8cpp_source.html#l03954">CVC3::TheoryCore::collectModelValues()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00509">CVC3::TheoryUF::computeModel()</a>, <a class="el" href="theory__array_8cpp_source.html#l00939">CVC3::TheoryArray::computeModel()</a>, <a class="el" href="theory__core_8cpp_source.html#l02033">containsRec()</a>, <a class="el" href="cnf__manager_8h_source.html#l00236">SAT::CNF_Manager::getCNFLit()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03838">CVC3::ArithTheoremProducerOld::getLeaves()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00251">CVC3::ExprManager::rebuildRec()</a>, <a class="el" href="expr_8cpp_source.html#l00260">CVC3::Expr::recursiveQuantSubst()</a>, <a class="el" href="expr_8cpp_source.html#l00063">CVC3::Expr::recursiveSubst()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00074">SAT::CNF_Manager::replaceITErec()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00296">CVC3::ExprTransform::specialSimplify()</a>, <a class="el" href="expr_8cpp_source.html#l00199">CVC3::Expr::substExpr()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00434">CVC3::ExprTransform::substitute()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00147">SAT::CNF_Manager::translateExprRec()</a>.</p>
</div>
</div>
<a class="anchor" id="a24ec23a15b7f6c121042f4b28fd83615"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html">const_iterator</a> <a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::begin </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00327">327</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
</div>
</div>
<a class="anchor" id="ad99d1aa47182ed209670d3b7bdef61f5"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html">const_iterator</a> <a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::end </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00328">328</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
</div>
</div>
<a class="anchor" id="aeffd58f05fbeb8f381ba2050adef7a2d"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprHashMap_1_1iterator.html">iterator</a> <a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::find </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00329">329</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l03862">CVC3::TheoryCore::buildModel()</a>, <a class="el" href="theory__core_8cpp_source.html#l03954">CVC3::TheoryCore::collectModelValues()</a>, <a class="el" href="theory__core_8cpp_source.html#l02033">containsRec()</a>, <a class="el" href="cnf__manager_8h_source.html#l00236">SAT::CNF_Manager::getCNFLit()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03838">CVC3::ArithTheoremProducerOld::getLeaves()</a>, <a class="el" href="theory__core_8cpp_source.html#l00595">CVC3::TheoryCore::getModelValue()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00251">CVC3::ExprManager::rebuildRec()</a>, <a class="el" href="expr_8cpp_source.html#l00260">CVC3::Expr::recursiveQuantSubst()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00074">SAT::CNF_Manager::replaceITErec()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00296">CVC3::ExprTransform::specialSimplify()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00434">CVC3::ExprTransform::substitute()</a>, and <a class="el" href="cnf__manager_8cpp_source.html#l00147">SAT::CNF_Manager::translateExprRec()</a>.</p>
</div>
</div>
<a class="anchor" id="aaa311b8de687f72bf8a7296a3e68ef46"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprHashMap_1_1const__iterator.html">const_iterator</a> <a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::find </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00330">330</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Data Documentation</h2>
<a class="anchor" id="a2b821e44541ec2a2635cc8ac11f7d3ca"></a>
<div class="memitem">
<div class="memproto">
<div class="memtemplate">
template<class Data> </div>
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprHashMap.html#a578d3b96ce2e21e0997603e61b006ef6">ExprHashMapType</a> <a class="el" href="classCVC3_1_1ExprHashMap.html">CVC3::ExprHashMap</a>< Data >::d_map</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr__map_8h_source.html#l00211">211</a> of file <a class="el" href="expr__map_8h_source.html">expr_map.h</a>.</p>
<p>Referenced by <a class="el" href="expr__map_8h_source.html#l00325">CVC3::ExprHashMap< std::vector< Circuit * > >::begin()</a>, <a class="el" href="expr__map_8h_source.html#l00310">CVC3::ExprHashMap< std::vector< Circuit * > >::clear()</a>, <a class="el" href="expr__map_8h_source.html#l00308">CVC3::ExprHashMap< std::vector< Circuit * > >::count()</a>, <a class="el" href="expr__map_8h_source.html#l00305">CVC3::ExprHashMap< std::vector< Circuit * > >::empty()</a>, <a class="el" href="expr__map_8h_source.html#l00326">CVC3::ExprHashMap< std::vector< Circuit * > >::end()</a>, <a class="el" href="expr__map_8h_source.html#l00313">CVC3::ExprHashMap< std::vector< Circuit * > >::erase()</a>, <a class="el" href="expr__map_8h_source.html#l00329">CVC3::ExprHashMap< std::vector< Circuit * > >::find()</a>, <a class="el" href="expr__map_8h_source.html#l00312">CVC3::ExprHashMap< std::vector< Circuit * > >::insert()</a>, <a class="el" href="expr__map_8h_source.html#l00309">CVC3::ExprHashMap< std::vector< Circuit * > >::operator[]()</a>, and <a class="el" href="expr__map_8h_source.html#l00306">CVC3::ExprHashMap< std::vector< Circuit * > >::size()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following file:<ul>
<li><a class="el" href="expr__map_8h_source.html">expr_map.h</a></li>
</ul>
</div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:17 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>
