<!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"/>
<title>CVC3: expr_manager.cpp Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<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 class="header">
<div class="headertitle">
<div class="title">expr_manager.cpp</div> </div>
</div>
<div class="contents">
<a href="expr__manager_8cpp.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00002"></a>00002 <span class="comment">/*!</span>
<a name="l00003"></a>00003 <span class="comment"> * \file expr_manager.cpp</span>
<a name="l00004"></a>00004 <span class="comment"> *</span>
<a name="l00005"></a>00005 <span class="comment"> * Author: Sergey Berezin</span>
<a name="l00006"></a>00006 <span class="comment"> *</span>
<a name="l00007"></a>00007 <span class="comment"> * Created: Wed Dec 4 14:20:56 2002</span>
<a name="l00008"></a>00008 <span class="comment"> *</span>
<a name="l00009"></a>00009 <span class="comment"> * <hr></span>
<a name="l00010"></a>00010 <span class="comment"> *</span>
<a name="l00011"></a>00011 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00012"></a>00012 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00013"></a>00013 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00014"></a>00014 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00015"></a>00015 <span class="comment"> *</span>
<a name="l00016"></a>00016 <span class="comment"> * <hr></span>
<a name="l00017"></a>00017 <span class="comment"> *</span>
<a name="l00018"></a>00018 <span class="comment"> */</span>
<a name="l00019"></a>00019 <span class="comment">/*****************************************************************************/</span>
<a name="l00020"></a>00020
<a name="l00021"></a>00021 <span class="preprocessor">#include "<a class="code" href="expr__manager_8h.html" title="Expression manager API.">expr_manager.h</a>"</span>
<a name="l00022"></a>00022 <span class="preprocessor">#include "<a class="code" href="command__line__flags_8h.html">command_line_flags.h</a>"</span>
<a name="l00023"></a>00023 <span class="preprocessor">#include "<a class="code" href="expr__stream_8h.html">expr_stream.h</a>"</span>
<a name="l00024"></a>00024 <span class="preprocessor">#include "<a class="code" href="pretty__printer_8h.html">pretty_printer.h</a>"</span>
<a name="l00025"></a>00025 <span class="preprocessor">#include "<a class="code" href="memory__manager__malloc_8h.html">memory_manager_malloc.h</a>"</span>
<a name="l00026"></a>00026 <span class="preprocessor">#include "<a class="code" href="memory__manager__chunks_8h.html">memory_manager_chunks.h</a>"</span>
<a name="l00027"></a>00027
<a name="l00028"></a>00028 <span class="keyword">using namespace </span>CVC3;
<a name="l00029"></a>00029
<a name="l00030"></a>00030 <span class="keyword">using namespace </span>std;
<a name="l00031"></a>00031
<a name="l00032"></a>00032 <span class="comment">// File-local function which registers all the commonly declared</span>
<a name="l00033"></a>00033 <span class="comment">// kinds (defined below)</span>
<a name="l00034"></a>00034 <span class="keyword">static</span> <span class="keywordtype">void</span> <a class="code" href="expr__manager_8cpp.html#ae7ac6263bf1137d9d09d24e72f3f0e11">registerKinds</a>(<a class="code" href="classCVC3_1_1ExprManager.html">ExprManager</a>& em);
<a name="l00035"></a>00035
<a name="l00036"></a><a class="code" href="classCVC3_1_1ExprManager.html#a8719f1580a1e4bde43738f5d349f0e4a">00036</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1ExprManager.html#a8719f1580a1e4bde43738f5d349f0e4a">ExprManager::installExprValue</a>(<a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* p_ev)
<a name="l00037"></a>00037 {
<a name="l00038"></a>00038 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(isActive(), <span class="stringliteral">"ExprManager::installExprValue(ExprValue*)"</span>);
<a name="l00039"></a>00039 <span class="comment">// int maxHeight = 0;</span>
<a name="l00040"></a>00040 <span class="comment">// p_ev->d_highestKid = 0;</span>
<a name="l00041"></a>00041 <span class="comment">// for (unsigned i = 0; i < p_ev->arity(); i++)</span>
<a name="l00042"></a>00042 <span class="comment">// {</span>
<a name="l00043"></a>00043 <span class="comment">// int height = p_ev->getKids()[i].getHeight();</span>
<a name="l00044"></a>00044 <span class="comment">// if (height > maxHeight)</span>
<a name="l00045"></a>00045 <span class="comment">// {</span>
<a name="l00046"></a>00046 <span class="comment">// maxHeight = height;</span>
<a name="l00047"></a>00047 <span class="comment">// p_ev->d_highestKid = i;</span>
<a name="l00048"></a>00048 <span class="comment">// }</span>
<a name="l00049"></a>00049 <span class="comment">// }</span>
<a name="l00050"></a>00050
<a name="l00051"></a>00051 <span class="comment">// if (p_ev->d_kind == ITE && p_ev->arity() == 3)</span>
<a name="l00052"></a>00052 <span class="comment">// {</span>
<a name="l00053"></a>00053 <span class="comment">// if (p_ev->getKids()[1].getHeight() > p_ev->getKids()[2].getHeight())</span>
<a name="l00054"></a>00054 <span class="comment">// p_ev->d_highestKid = 1;</span>
<a name="l00055"></a>00055 <span class="comment">// else</span>
<a name="l00056"></a>00056 <span class="comment">// p_ev->d_highestKid = 2;</span>
<a name="l00057"></a>00057 <span class="comment">// }</span>
<a name="l00058"></a>00058
<a name="l00059"></a>00059 <span class="comment">// switch (p_ev->d_kind) {</span>
<a name="l00060"></a>00060 <span class="comment">// case NOT: case AND: case OR: case ITE: case IFF: case IMPLIES:</span>
<a name="l00061"></a>00061 <span class="comment">// maxHeight++;</span>
<a name="l00062"></a>00062 <span class="comment">// }</span>
<a name="l00063"></a>00063 <span class="comment">// p_ev->d_height = maxHeight;</span>
<a name="l00064"></a>00064
<a name="l00065"></a>00065 d_exprSet.insert(p_ev);
<a name="l00066"></a>00066 }
<a name="l00067"></a>00067
<a name="l00068"></a>00068
<a name="l00069"></a>00069 <span class="comment">// Constructor</span>
<a name="l00070"></a><a class="code" href="group__EM__Priv.html#gaf3af8657f4b2c64f189f0a50147d3589">00070</a> <a class="code" href="group__EM__Priv.html#gaf3af8657f4b2c64f189f0a50147d3589" title="Constructor.">ExprManager::ExprManager</a>(<a class="code" href="classCVC3_1_1ContextManager.html" title="Manager for multiple contexts. Also holds current context.">ContextManager</a>* cm, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CLFlags.html">CLFlags</a>& flags)
<a name="l00071"></a>00071 <span class="comment">// Initial number of buckets is 1024 (it's kinda arbitrary)</span>
<a name="l00072"></a>00072 : d_cm(cm), d_index(0), d_flagCounter(1), d_prettyPrinter(NULL),
<a name="l00073"></a>00073 d_printDepth(&(flags[<span class="stringliteral">"print-depth"</span>].getInt())),
<a name="l00074"></a>00074 d_withIndentation(&(flags[<span class="stringliteral">"indent"</span>].getBool())),
<a name="l00075"></a>00075 d_indent(0), d_indentTransient(0),
<a name="l00076"></a>00076 d_lineWidth(&(flags[<span class="stringliteral">"width"</span>].getInt())),
<a name="l00077"></a>00077 d_inputLang(&(flags[<span class="stringliteral">"lang"</span>].getString())),
<a name="l00078"></a>00078 d_outputLang(&(flags[<span class="stringliteral">"output-lang"</span>].getString())),
<a name="l00079"></a>00079 d_dagPrinting(&(flags[<span class="stringliteral">"dagify-exprs"</span>].getBool())),
<a name="l00080"></a>00080 d_mmFlag(flags[<span class="stringliteral">"mm"</span>].getString()),
<a name="l00081"></a>00081 d_exprSet(1024, <a class="code" href="classCVC3_1_1ExprManager_1_1HashEV.html" title="Private class for d_exprSet.">HashEV</a>(this), <a class="code" href="classCVC3_1_1ExprManager_1_1EqEV.html" title="Private class for d_exprSet.">EqEV</a>()),
<a name="l00082"></a>00082 d_mm(<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8a0ead87cd0a551c50f3b0e42cbe72f8b3">EXPR_VALUE_TYPE_LAST</a>),
<a name="l00083"></a>00083 d_simpCacheTagCurrent(1), d_disableGC(false), d_postponeGC(false),
<a name="l00084"></a>00084 d_inGC(false), d_typeComputer(NULL)
<a name="l00085"></a>00085 {
<a name="l00086"></a>00086 <span class="comment">// Initialize the notifier</span>
<a name="l00087"></a>00087 <a class="code" href="classCVC3_1_1ExprManager.html#abf2f3e04c70fc71ba01170007e3a0831" title="Notification on pop()">d_notifyObj</a> = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1ExprManagerNotifyObj.html" title="Notifies ExprManager before and after each pop()">ExprManagerNotifyObj</a>(<span class="keyword">this</span>, <a class="code" href="classCVC3_1_1ExprManager.html#ab4503774f636c29f72d680289f2783dc" title="For backtracking attributes.">d_cm</a>-><a class="code" href="classCVC3_1_1ContextManager.html#a66a7d900301c1459de90b048623d9297">getCurrentContext</a>());
<a name="l00088"></a>00088
<a name="l00089"></a>00089 <span class="comment">// Initialize core memory managers</span>
<a name="l00090"></a>00090 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1ExprManager.html#a5cfe801f6ae8f9fd7a51477a219685e8" title="Which memory manager to use (copy the flag value and keep it the same)">d_mmFlag</a> == <span class="stringliteral">"chunks"</span>) {
<a name="l00091"></a>00091 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8a45728d440ceb44bdb47f21351a153e88">EXPR_VALUE</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerChunks.html">MemoryManagerChunks</a>(<span class="keyword">sizeof</span>(<a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>));
<a name="l00092"></a>00092 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8a3893ed6eebbc5daca30a7aac2282fe6f">EXPR_NODE</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerChunks.html">MemoryManagerChunks</a>(<span class="keyword">sizeof</span>(<a class="code" href="classCVC3_1_1ExprNode.html">ExprNode</a>));
<a name="l00093"></a>00093 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8ac0f64afa0582818fffa2cc5403db8a0e" title="Application of functions and predicates.">EXPR_APPLY</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerChunks.html">MemoryManagerChunks</a>(<span class="keyword">sizeof</span>(<a class="code" href="classCVC3_1_1ExprApply.html">ExprApply</a>));
<a name="l00094"></a>00094 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8aaabca50d22455e77c3f61e8d5307989b">EXPR_STRING</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerChunks.html">MemoryManagerChunks</a>(<span class="keyword">sizeof</span>(<a class="code" href="classCVC3_1_1ExprString.html">ExprString</a>));
<a name="l00095"></a>00095 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8a424556ebe7d7485cbd13e5c1e5228811">EXPR_RATIONAL</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerChunks.html">MemoryManagerChunks</a>(<span class="keyword">sizeof</span>(<a class="code" href="classCVC3_1_1ExprRational.html">ExprRational</a>));
<a name="l00096"></a>00096 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8a82b57cae98f27f2d8f414efe70d1a1b1">EXPR_UCONST</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerChunks.html">MemoryManagerChunks</a>(<span class="keyword">sizeof</span>(<a class="code" href="classCVC3_1_1ExprVar.html">ExprVar</a>));
<a name="l00097"></a>00097 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8a54fe96ba026d0bef6191b315f7190262">EXPR_SYMBOL</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerChunks.html">MemoryManagerChunks</a>(<span class="keyword">sizeof</span>(<a class="code" href="classCVC3_1_1ExprSymbol.html">ExprSymbol</a>));
<a name="l00098"></a>00098 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8a58a9f13ea5962be2ef65dc0693743d81">EXPR_BOUND_VAR</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerChunks.html">MemoryManagerChunks</a>(<span class="keyword">sizeof</span>(<a class="code" href="classCVC3_1_1ExprBoundVar.html">ExprBoundVar</a>));
<a name="l00099"></a>00099 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8a93c8095a1c01d7a11081e615b94a3b2b">EXPR_CLOSURE</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerChunks.html">MemoryManagerChunks</a>(<span class="keyword">sizeof</span>(<a class="code" href="classCVC3_1_1ExprClosure.html" title="A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers...">ExprClosure</a>));
<a name="l00100"></a>00100 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8a4e7d647c7c01957f00b94b5a2c86e0a7">EXPR_SKOLEM</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerChunks.html">MemoryManagerChunks</a>(<span class="keyword">sizeof</span>(<a class="code" href="classCVC3_1_1ExprSkolem.html">ExprSkolem</a>));
<a name="l00101"></a>00101 } <span class="keywordflow">else</span> {
<a name="l00102"></a>00102 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8a45728d440ceb44bdb47f21351a153e88">EXPR_VALUE</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerMalloc.html">MemoryManagerMalloc</a>();
<a name="l00103"></a>00103 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8a3893ed6eebbc5daca30a7aac2282fe6f">EXPR_NODE</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerMalloc.html">MemoryManagerMalloc</a>();
<a name="l00104"></a>00104 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8ac0f64afa0582818fffa2cc5403db8a0e" title="Application of functions and predicates.">EXPR_APPLY</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerMalloc.html">MemoryManagerMalloc</a>();
<a name="l00105"></a>00105 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8aaabca50d22455e77c3f61e8d5307989b">EXPR_STRING</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerMalloc.html">MemoryManagerMalloc</a>();
<a name="l00106"></a>00106 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8a424556ebe7d7485cbd13e5c1e5228811">EXPR_RATIONAL</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerMalloc.html">MemoryManagerMalloc</a>();
<a name="l00107"></a>00107 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8a82b57cae98f27f2d8f414efe70d1a1b1">EXPR_UCONST</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerMalloc.html">MemoryManagerMalloc</a>();
<a name="l00108"></a>00108 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8a54fe96ba026d0bef6191b315f7190262">EXPR_SYMBOL</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerMalloc.html">MemoryManagerMalloc</a>();
<a name="l00109"></a>00109 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8a58a9f13ea5962be2ef65dc0693743d81">EXPR_BOUND_VAR</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerMalloc.html">MemoryManagerMalloc</a>();
<a name="l00110"></a>00110 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8a93c8095a1c01d7a11081e615b94a3b2b">EXPR_CLOSURE</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerMalloc.html">MemoryManagerMalloc</a>();
<a name="l00111"></a>00111 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[<a class="code" href="namespaceCVC3.html#a492cd44a88003acd985d3c05cbd36ea8a4e7d647c7c01957f00b94b5a2c86e0a7">EXPR_SKOLEM</a>] = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerMalloc.html">MemoryManagerMalloc</a>();
<a name="l00112"></a>00112 }
<a name="l00113"></a>00113 <a class="code" href="expr__manager_8cpp.html#ae7ac6263bf1137d9d09d24e72f3f0e11">registerKinds</a>(*<span class="keyword">this</span>);
<a name="l00114"></a>00114
<a name="l00115"></a>00115 <a class="code" href="classCVC3_1_1ExprManager.html#a8f6f7143ab2a62f58ed86d296fa23be4" title="Expr constants cached for fast access.">d_bool</a> = <a class="code" href="group__EM__Priv.html#gacd77df1dbcc429e06a75047e2f609822">newLeafExpr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba8a583f16e8d237a423c8c1d9087a4c72">BOOLEAN</a>);
<a name="l00116"></a>00116 <a class="code" href="classCVC3_1_1ExprManager.html#a4b0a44de15c4b3de63233d824a2058bd">d_false</a> = <a class="code" href="group__EM__Priv.html#gacd77df1dbcc429e06a75047e2f609822">newLeafExpr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5f71bd33a6528411ae681f5291de1d82">FALSE_EXPR</a>);
<a name="l00117"></a>00117 <a class="code" href="classCVC3_1_1ExprManager.html#a4b0a44de15c4b3de63233d824a2058bd">d_false</a>.<a class="code" href="group__ExprPkg.html#ga07d47f902598e00097086deabf04d9c5" title="Set the cached type.">setType</a>(<a class="code" href="classCVC3_1_1Type.html#a20b55d497b79ffc60b68ffe512dc2b56">Type::typeBool</a>(<span class="keyword">this</span>));
<a name="l00118"></a>00118 <a class="code" href="classCVC3_1_1ExprManager.html#a6c341a4de2d1e1189e9a1a67430a508c">d_true</a> = <a class="code" href="group__EM__Priv.html#gacd77df1dbcc429e06a75047e2f609822">newLeafExpr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba1fad76919fba496de21807e2beec533d">TRUE_EXPR</a>);
<a name="l00119"></a>00119 <a class="code" href="classCVC3_1_1ExprManager.html#a6c341a4de2d1e1189e9a1a67430a508c">d_true</a>.<a class="code" href="group__ExprPkg.html#ga07d47f902598e00097086deabf04d9c5" title="Set the cached type.">setType</a>(<a class="code" href="classCVC3_1_1Type.html#a20b55d497b79ffc60b68ffe512dc2b56">Type::typeBool</a>(<span class="keyword">this</span>));
<a name="l00120"></a>00120
<a name="l00121"></a>00121 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(d_inRebuild = <span class="keyword">false</span>;)
<a name="l00122"></a>00122 }
<a name="l00123"></a>00123
<a name="l00124"></a>00124 <span class="comment">// Destructor</span>
<a name="l00125"></a><a class="code" href="group__EM__Priv.html#ga318254064b65faf57e1657b680688bc7">00125</a> <a class="code" href="classCVC3_1_1ExprManager.html">ExprManager</a>::~<a class="code" href="group__EM__Priv.html#gaf3af8657f4b2c64f189f0a50147d3589" title="Constructor.">ExprManager</a>() {
<a name="l00126"></a>00126 <a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(<a class="code" href="classCVC3_1_1ExprManager.html#a20b3e13cca9564afd32e3df2537bdb24" title="Empty vector of Expr to return by reference as empty vector of children.">d_emptyVec</a>.size()==0, <span class="stringliteral">"~ExprManager()"</span>);
<a name="l00127"></a>00127 <span class="keyword">delete</span> <a class="code" href="classCVC3_1_1ExprManager.html#abf2f3e04c70fc71ba01170007e3a0831" title="Notification on pop()">d_notifyObj</a>;
<a name="l00128"></a>00128 <span class="comment">// Make sure garbage collector doesn't get in the way</span>
<a name="l00129"></a>00129 <a class="code" href="classCVC3_1_1ExprManager.html#a9c4e054fd961a0910bbf03b8bbccb04a" title="Disable garbage collection.">d_disableGC</a> = <span class="keyword">false</span>; <span class="comment">// clear() will assert this.</span>
<a name="l00130"></a>00130 <a class="code" href="group__EM__Priv.html#ga9bddd7eaf6f198476eda3cd55227f384" title="Free up all memory and delete all the expressions.">clear</a>();
<a name="l00131"></a>00131 <a class="code" href="classCVC3_1_1ExprManager.html#a9c4e054fd961a0910bbf03b8bbccb04a" title="Disable garbage collection.">d_disableGC</a> = <span class="keyword">true</span>;
<a name="l00132"></a>00132 <span class="comment">// Destroy memory managers</span>
<a name="l00133"></a>00133 <a class="code" href="debug_8h.html#ad64155edafde9f067f4868817cd04bdf">TRACE_MSG</a>(<span class="stringliteral">"delete"</span>, <span class="stringliteral">"~ExprManager: deleting d_mm's {"</span>);
<a name="l00134"></a>00134 <span class="keywordflow">for</span>(<span class="keywordtype">size_t</span> i=0; i<<a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>.size(); ++i)
<a name="l00135"></a>00135 <span class="keyword">delete</span> <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[i];
<a name="l00136"></a>00136
<a name="l00137"></a>00137 <a class="code" href="debug_8h.html#ad64155edafde9f067f4868817cd04bdf">TRACE_MSG</a>(<span class="stringliteral">"delete"</span>, <span class="stringliteral">"~ExprManager: finished deleting d_mm's }"</span>);
<a name="l00138"></a>00138 }
<a name="l00139"></a>00139
<a name="l00140"></a>00140
<a name="l00141"></a><a class="code" href="group__EM__Priv.html#ga9bddd7eaf6f198476eda3cd55227f384">00141</a> <span class="keywordtype">void</span> <a class="code" href="group__EM__Priv.html#ga9bddd7eaf6f198476eda3cd55227f384" title="Free up all memory and delete all the expressions.">ExprManager::clear</a>() {
<a name="l00142"></a>00142 <a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(<a class="code" href="group__EM__Priv.html#gaaec477005a23531fa15d27282658aab8" title="Check if the ExprManager is still active (clear() was not called)">isActive</a>(), <span class="stringliteral">"ExprManager::clear()"</span>);
<a name="l00143"></a>00143 <span class="comment">// Make ExprManager inactive, but keep all the Exprs intact</span>
<a name="l00144"></a>00144 <span class="comment">// Remove all internal expressions.</span>
<a name="l00145"></a>00145 <a class="code" href="classCVC3_1_1ExprManager.html#a9c4e054fd961a0910bbf03b8bbccb04a" title="Disable garbage collection.">d_disableGC</a> = <span class="keyword">true</span>;
<a name="l00146"></a>00146
<a name="l00147"></a>00147 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"delete"</span>, <span class="stringliteral">"clear: number of remaining Exprs: "</span>,
<a name="l00148"></a>00148 <a class="code" href="classCVC3_1_1ExprManager.html#a007da346931bbc8d2dafafaa81c4ea9c" title="Hash set for uniquifying expressions.">d_exprSet</a>.<a class="code" href="classHash_1_1hash__set.html#a8d883de7bd664d4cf8f4e440b711873f">size</a>(), flush);
<a name="l00149"></a>00149
<a name="l00150"></a>00150 <a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(<a class="code" href="classCVC3_1_1ExprManager.html#afd9f8cac32e3acbbf7bbb18506cb2350" title="Null Expr to return by reference, for efficiency.">d_nullExpr</a>.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>(), <span class="stringliteral">"ExprManager::clear()"</span>);
<a name="l00151"></a>00151
<a name="l00152"></a>00152 <span class="comment">// Set class-local Exprs to Null</span>
<a name="l00153"></a>00153 <a class="code" href="classCVC3_1_1ExprManager.html#a8f6f7143ab2a62f58ed86d296fa23be4" title="Expr constants cached for fast access.">d_bool</a> = <a class="code" href="classCVC3_1_1ExprManager.html#aa33520359f6cc0f51b476790d39ed869">Expr</a>();
<a name="l00154"></a>00154 <a class="code" href="classCVC3_1_1ExprManager.html#a4b0a44de15c4b3de63233d824a2058bd">d_false</a> = <a class="code" href="classCVC3_1_1ExprManager.html#aa33520359f6cc0f51b476790d39ed869">Expr</a>();
<a name="l00155"></a>00155 <a class="code" href="classCVC3_1_1ExprManager.html#a6c341a4de2d1e1189e9a1a67430a508c">d_true</a> = <a class="code" href="classCVC3_1_1ExprManager.html#aa33520359f6cc0f51b476790d39ed869">Expr</a>();
<a name="l00156"></a>00156
<a name="l00157"></a>00157 <span class="comment">// Save all the pointers, clear the hash set, then free the</span>
<a name="l00158"></a>00158 <span class="comment">// pointers. Erasing one pointer at a time requires rehashing,</span>
<a name="l00159"></a>00159 <span class="comment">// which will segfault if some pointers are already deleted.</span>
<a name="l00160"></a>00160 vector<ExprValue*> exprs;
<a name="l00161"></a>00161 exprs.reserve(<a class="code" href="classCVC3_1_1ExprManager.html#a007da346931bbc8d2dafafaa81c4ea9c" title="Hash set for uniquifying expressions.">d_exprSet</a>.<a class="code" href="classHash_1_1hash__set.html#a8d883de7bd664d4cf8f4e440b711873f">size</a>());
<a name="l00162"></a>00162 <a class="code" href="debug_8h.html#ad64155edafde9f067f4868817cd04bdf">TRACE_MSG</a>(<span class="stringliteral">"delete"</span>, <span class="stringliteral">"clear:() collecting exprs { "</span>);
<a name="l00163"></a>00163 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<span class="keywordtype">int</span> n(0);)
<a name="l00164"></a>00164 <span class="keywordflow">for</span>(<a class="code" href="classHash_1_1hash__set.html#a87a125f71dd85de65e662559bd5a66dc">ExprValueSet::iterator</a> i=<a class="code" href="classCVC3_1_1ExprManager.html#a007da346931bbc8d2dafafaa81c4ea9c" title="Hash set for uniquifying expressions.">d_exprSet</a>.<a class="code" href="classHash_1_1hash__set.html#a69de75543eb1e9fa3510bb5090ad61a6" title="iterators">begin</a>(), iend=<a class="code" href="classCVC3_1_1ExprManager.html#a007da346931bbc8d2dafafaa81c4ea9c" title="Hash set for uniquifying expressions.">d_exprSet</a>.<a class="code" href="classHash_1_1hash__set.html#ae3ee82665499970f29a93df9948a5757">end</a>();
<a name="l00165"></a>00165 i!=iend; ++i) {
<a name="l00166"></a>00166 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"delete"</span>, <span class="stringliteral">"expr["</span>, n++, <span class="stringliteral">"]"</span>);
<a name="l00167"></a>00167 exprs.push_back(*i);
<a name="l00168"></a>00168 }
<a name="l00169"></a>00169 <a class="code" href="debug_8h.html#ad64155edafde9f067f4868817cd04bdf">TRACE_MSG</a>(<span class="stringliteral">"delete"</span>, <span class="stringliteral">"clear(): finished collecting exprs }"</span>);
<a name="l00170"></a>00170 <a class="code" href="classCVC3_1_1ExprManager.html#a007da346931bbc8d2dafafaa81c4ea9c" title="Hash set for uniquifying expressions.">d_exprSet</a>.<a class="code" href="classHash_1_1hash__set.html#a2d699de2bb0dac0d1ea819fdc8acda96">clear</a>();
<a name="l00171"></a>00171 <a class="code" href="debug_8h.html#ad64155edafde9f067f4868817cd04bdf">TRACE_MSG</a>(<span class="stringliteral">"delete"</span>, <span class="stringliteral">"clear(): deleting exprs { "</span>);
<a name="l00172"></a>00172 <span class="keywordflow">for</span>(vector<ExprValue*>::iterator i=exprs.begin(), iend=exprs.end();
<a name="l00173"></a>00173 i!=iend; ++i) {
<a name="l00174"></a>00174 <a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a> *pExpr= *i;
<a name="l00175"></a>00175 <span class="keywordtype">size_t</span> tp(pExpr-><a class="code" href="classCVC3_1_1ExprValue.html#af4280c2539ba1dd4a089f0537f7ef3d4" title="Get unique memory manager ID.">getMMIndex</a>()); <span class="comment">// which memory manager to use</span>
<a name="l00176"></a>00176 <span class="keyword">delete</span> (pExpr);
<a name="l00177"></a>00177 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[tp]->deleteData(pExpr);
<a name="l00178"></a>00178 }
<a name="l00179"></a>00179 <a class="code" href="debug_8h.html#ad64155edafde9f067f4868817cd04bdf">TRACE_MSG</a>(<span class="stringliteral">"delete"</span>, <span class="stringliteral">"clear(): finished deleting exprs }"</span>);
<a name="l00180"></a>00180
<a name="l00181"></a>00181 }
<a name="l00182"></a>00182
<a name="l00183"></a>00183
<a name="l00184"></a><a class="code" href="group__EM__Priv.html#gaaec477005a23531fa15d27282658aab8">00184</a> <span class="keywordtype">bool</span> <a class="code" href="group__EM__Priv.html#gaaec477005a23531fa15d27282658aab8" title="Check if the ExprManager is still active (clear() was not called)">ExprManager::isActive</a>() { <span class="keywordflow">return</span> !<a class="code" href="classCVC3_1_1ExprManager.html#a9c4e054fd961a0910bbf03b8bbccb04a" title="Disable garbage collection.">d_disableGC</a>; }
<a name="l00185"></a>00185
<a name="l00186"></a>00186
<a name="l00187"></a>00187 <span class="comment">// Garbage collect the ExprValue pointer</span>
<a name="l00188"></a><a class="code" href="group__EM__Priv.html#ga5878c4fbe700243540dc835b965fd01b">00188</a> <span class="keywordtype">void</span> <a class="code" href="group__EM__Priv.html#ga5878c4fbe700243540dc835b965fd01b" title="Garbage collect the ExprValue pointer.">ExprManager::gc</a>(<a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* ev) {
<a name="l00189"></a>00189 <span class="keywordflow">if</span>(!<a class="code" href="classCVC3_1_1ExprManager.html#a9c4e054fd961a0910bbf03b8bbccb04a" title="Disable garbage collection.">d_disableGC</a>) {
<a name="l00190"></a>00190 <a class="code" href="classCVC3_1_1ExprManager.html#a007da346931bbc8d2dafafaa81c4ea9c" title="Hash set for uniquifying expressions.">d_exprSet</a>.<a class="code" href="classHash_1_1hash__set.html#a82dbe044048d8e25f0ffd148d726d1e4">erase</a>(ev);
<a name="l00191"></a>00191 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1ExprManager.html#a6ae99a5eb75cee11d7f638c1ea17a201" title="Flag for whether GC is already running.">d_inGC</a>) <a class="code" href="classCVC3_1_1ExprManager.html#a99533eeb3df944329cf62d97c86fc43c" title="Queue of pending exprs to GC.">d_pending</a>.push_back(ev);
<a name="l00192"></a>00192 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1ExprManager.html#a7ee8efeb3b86e7b044290ad543792db2" title="Postpone deleting garbage-collected expressions.">d_postponeGC</a>) <a class="code" href="classCVC3_1_1ExprManager.html#a679888b2e2e5cb92645ec6bd0701f7ec" title="Vector of postponed garbage-collected expressions.">d_postponed</a>.push_back(ev);
<a name="l00193"></a>00193 <span class="keywordflow">else</span> {
<a name="l00194"></a>00194 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(<a class="code" href="classCVC3_1_1ExprManager.html#a99533eeb3df944329cf62d97c86fc43c" title="Queue of pending exprs to GC.">d_pending</a>.size() == 0, <span class="stringliteral">"Expected size 1"</span>);)
<a name="l00195"></a>00195 <a class="code" href="classCVC3_1_1ExprManager.html#a6ae99a5eb75cee11d7f638c1ea17a201" title="Flag for whether GC is already running.">d_inGC</a> = <span class="keyword">true</span>;
<a name="l00196"></a>00196 <span class="keywordtype">size_t</span> tp = ev-><a class="code" href="classCVC3_1_1ExprValue.html#af4280c2539ba1dd4a089f0537f7ef3d4" title="Get unique memory manager ID.">getMMIndex</a>();
<a name="l00197"></a>00197 <span class="keyword">delete</span> ev;
<a name="l00198"></a>00198 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[tp]->deleteData(ev);
<a name="l00199"></a>00199 <span class="keywordflow">while</span> (<a class="code" href="classCVC3_1_1ExprManager.html#a99533eeb3df944329cf62d97c86fc43c" title="Queue of pending exprs to GC.">d_pending</a>.size() > 0) {
<a name="l00200"></a>00200 ev = <a class="code" href="classCVC3_1_1ExprManager.html#a99533eeb3df944329cf62d97c86fc43c" title="Queue of pending exprs to GC.">d_pending</a>.front();
<a name="l00201"></a>00201 <a class="code" href="classCVC3_1_1ExprManager.html#a99533eeb3df944329cf62d97c86fc43c" title="Queue of pending exprs to GC.">d_pending</a>.pop_front();
<a name="l00202"></a>00202 tp = ev-><a class="code" href="classCVC3_1_1ExprValue.html#af4280c2539ba1dd4a089f0537f7ef3d4" title="Get unique memory manager ID.">getMMIndex</a>();
<a name="l00203"></a>00203 <span class="keyword">delete</span> ev;
<a name="l00204"></a>00204 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[tp]->deleteData(ev);
<a name="l00205"></a>00205 }
<a name="l00206"></a>00206 <a class="code" href="classCVC3_1_1ExprManager.html#a6ae99a5eb75cee11d7f638c1ea17a201" title="Flag for whether GC is already running.">d_inGC</a> = <span class="keyword">false</span>;
<a name="l00207"></a>00207 }
<a name="l00208"></a>00208 }
<a name="l00209"></a>00209 }
<a name="l00210"></a>00210
<a name="l00211"></a>00211 <span class="keywordtype">void</span>
<a name="l00212"></a><a class="code" href="group__EM__Priv.html#gafd44d7be33c1111722aa7bb9f3b8b2e9">00212</a> <a class="code" href="group__EM__Priv.html#gafd44d7be33c1111722aa7bb9f3b8b2e9" title="Resume deletion of garbage-collected expressions.">ExprManager::resumeGC</a>() {
<a name="l00213"></a>00213 <a class="code" href="classCVC3_1_1ExprManager.html#a7ee8efeb3b86e7b044290ad543792db2" title="Postpone deleting garbage-collected expressions.">d_postponeGC</a> = <span class="keyword">false</span>;
<a name="l00214"></a>00214 <span class="keywordflow">while</span>(<a class="code" href="classCVC3_1_1ExprManager.html#a679888b2e2e5cb92645ec6bd0701f7ec" title="Vector of postponed garbage-collected expressions.">d_postponed</a>.size()>0) {
<a name="l00215"></a>00215 <a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* ev = <a class="code" href="classCVC3_1_1ExprManager.html#a679888b2e2e5cb92645ec6bd0701f7ec" title="Vector of postponed garbage-collected expressions.">d_postponed</a>.back();
<a name="l00216"></a>00216 <span class="keywordtype">size_t</span> tp(ev-><a class="code" href="classCVC3_1_1ExprValue.html#af4280c2539ba1dd4a089f0537f7ef3d4" title="Get unique memory manager ID.">getMMIndex</a>());
<a name="l00217"></a>00217 <a class="code" href="classCVC3_1_1ExprManager.html#a679888b2e2e5cb92645ec6bd0701f7ec" title="Vector of postponed garbage-collected expressions.">d_postponed</a>.pop_back();
<a name="l00218"></a>00218 <span class="keyword">delete</span> ev;
<a name="l00219"></a>00219 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>[tp]->deleteData(ev);
<a name="l00220"></a>00220 }
<a name="l00221"></a>00221 }
<a name="l00222"></a>00222
<a name="l00223"></a>00223
<a name="l00224"></a>00224 <span class="comment">// Rebuild the Expr with this ExprManager if it belongs to another</span>
<a name="l00225"></a>00225 <span class="comment">// ExprManager</span>
<a name="l00226"></a><a class="code" href="group__EM__Priv.html#gacaab5ccf5cf81d11185979051d301d5e">00226</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="group__EM__Priv.html#gacaab5ccf5cf81d11185979051d301d5e" title="Rebuild the Expr with this ExprManager if it belongs to another ExprManager.">ExprManager::rebuild</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 name="l00227"></a>00227 <span class="comment">// TRACE("expr", "rebuild(", e, ") {");</span>
<a name="l00228"></a>00228 <span class="comment">// Shouldn't rebuild a Null Expr (it's a bug)</span>
<a name="l00229"></a>00229 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!e.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>(), <span class="stringliteral">"ExprManager::rebuild called on Null Expr"</span>);
<a name="l00230"></a>00230 <span class="comment">// Both ExprManagers must be active</span>
<a name="l00231"></a>00231 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="group__EM__Priv.html#gaaec477005a23531fa15d27282658aab8" title="Check if the ExprManager is still active (clear() was not called)">isActive</a>() && e.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#gaaec477005a23531fa15d27282658aab8" title="Check if the ExprManager is still active (clear() was not called)">isActive</a>(),
<a name="l00232"></a>00232 <span class="stringliteral">"ExprManager::rebuild is called on inactive ExprManager"</span>);
<a name="l00233"></a>00233 <span class="comment">// If e has the same ExprManager, no rebuilding is necessary</span>
<a name="l00234"></a>00234 <span class="keywordflow">if</span>(e.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>() || (e.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>() == <span class="keyword">this</span>)) {
<a name="l00235"></a>00235 <span class="comment">// TRACE_MSG("expr", "rebuild (same EM) => }");</span>
<a name="l00236"></a>00236 <span class="keywordflow">return</span> e;
<a name="l00237"></a>00237 }
<a name="l00238"></a>00238 <span class="comment">// Gotta rebuild</span>
<a name="l00239"></a>00239 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!d_inRebuild, <span class="stringliteral">"ExprManager::rebuild()"</span>);
<a name="l00240"></a>00240 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<a class="code" href="classCVC3_1_1ScopeWatcher.html" title="A class which sets a boolean value to true when created, and resets to false when deleted...">ScopeWatcher</a> sw(&d_inRebuild);)
<a name="l00241"></a>00241 <span class="comment">// First, clear the cache</span>
<a name="l00242"></a>00242 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1ExprManager.html#a841b8a48adc1372b7d99e3f93dd9620a" title="Rebuild cache.">d_rebuildCache</a>.<a class="code" href="classCVC3_1_1ExprHashMap.html#a9d792cf5282604c376d329ae325c983e">size</a>() > 0) <a class="code" href="classCVC3_1_1ExprManager.html#a841b8a48adc1372b7d99e3f93dd9620a" title="Rebuild cache.">d_rebuildCache</a>.<a class="code" href="classCVC3_1_1ExprHashMap.html#aa20f14dba09537171af45bf479b99c66">clear</a>();
<a name="l00243"></a>00243 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> res = <a class="code" href="group__EM__Priv.html#gaa86d7ed7800549f1621d2d5ce64ce643" title="Cached recursive descent. Must be called only during rebuild()">rebuildRec</a>(e);
<a name="l00244"></a>00244 <span class="comment">// Leave no trail behind (free up Exprs)</span>
<a name="l00245"></a>00245 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1ExprManager.html#a841b8a48adc1372b7d99e3f93dd9620a" title="Rebuild cache.">d_rebuildCache</a>.<a class="code" href="classCVC3_1_1ExprHashMap.html#a9d792cf5282604c376d329ae325c983e">size</a>() > 0) <a class="code" href="classCVC3_1_1ExprManager.html#a841b8a48adc1372b7d99e3f93dd9620a" title="Rebuild cache.">d_rebuildCache</a>.<a class="code" href="classCVC3_1_1ExprHashMap.html#aa20f14dba09537171af45bf479b99c66">clear</a>();
<a name="l00246"></a>00246 <span class="comment">// TRACE("expr", "rebuild => ", e, " }");</span>
<a name="l00247"></a>00247 <span class="keywordflow">return</span> res;
<a name="l00248"></a>00248 }
<a name="l00249"></a>00249
<a name="l00250"></a>00250
<a name="l00251"></a><a class="code" href="group__EM__Priv.html#gaa86d7ed7800549f1621d2d5ce64ce643">00251</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="group__EM__Priv.html#gaa86d7ed7800549f1621d2d5ce64ce643" title="Cached recursive descent. Must be called only during rebuild()">ExprManager::rebuildRec</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 name="l00252"></a>00252 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(d_inRebuild, <span class="stringliteral">"ExprManager::rebuildRec("</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>()+<span class="stringliteral">")"</span>);
<a name="l00253"></a>00253 <span class="comment">// Check cache</span>
<a name="l00254"></a>00254 <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr>::iterator</a> j=<a class="code" href="classCVC3_1_1ExprManager.html#a841b8a48adc1372b7d99e3f93dd9620a" title="Rebuild cache.">d_rebuildCache</a>.<a class="code" href="classCVC3_1_1ExprHashMap.html#aeffd58f05fbeb8f381ba2050adef7a2d">find</a>(e),
<a name="l00255"></a>00255 jend=<a class="code" href="classCVC3_1_1ExprManager.html#a841b8a48adc1372b7d99e3f93dd9620a" title="Rebuild cache.">d_rebuildCache</a>.<a class="code" href="classCVC3_1_1ExprHashMap.html#a0ea2aa250fd1431c311d83f32862bba7">end</a>();
<a name="l00256"></a>00256 <span class="keywordflow">if</span>(j!=jend) <span class="keywordflow">return</span> (*j).second;
<a name="l00257"></a>00257
<a name="l00258"></a>00258 <a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* ev = e.<a class="code" href="group__ExprPkg.html#ga3a08bea4e8715a268083e1671e340a2e">d_expr</a>-><a class="code" href="classCVC3_1_1ExprValue.html#a2a5a87b2cdf0318ac9555ed82bd781c5" title="Make a clean copy of itself using the given ExprManager.">rebuild</a>(<span class="keyword">this</span>);
<a name="l00259"></a>00259 <span class="comment">// Uniquify the pointer</span>
<a name="l00260"></a>00260 <a class="code" href="classHash_1_1hash__set.html#a87a125f71dd85de65e662559bd5a66dc">ExprValueSet::iterator</a> i(<a class="code" href="classCVC3_1_1ExprManager.html#a007da346931bbc8d2dafafaa81c4ea9c" title="Hash set for uniquifying expressions.">d_exprSet</a>.<a class="code" href="classHash_1_1hash__set.html#a955279e5fd49f919bb6b0cd456d39c7b" title="operations">find</a>(ev)), iend(<a class="code" href="classCVC3_1_1ExprManager.html#a007da346931bbc8d2dafafaa81c4ea9c" title="Hash set for uniquifying expressions.">d_exprSet</a>.<a class="code" href="classHash_1_1hash__set.html#ae3ee82665499970f29a93df9948a5757">end</a>());
<a name="l00261"></a>00261 <span class="keywordflow">if</span>(i != iend) {
<a name="l00262"></a>00262 <a class="code" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* mm = <a class="code" href="group__EM__Priv.html#ga721fc26fe37460f80e6d614cfe0d6fd8" title="Return a MemoryManager for the given ExprValue type.">getMM</a>(ev->getMMIndex());
<a name="l00263"></a>00263 <span class="keyword">delete</span> ev;
<a name="l00264"></a>00264 mm-><a class="code" href="classCVC3_1_1MemoryManager.html#ad29fac88d3a07566d9a8f9dc8d8e059c">deleteData</a>(ev);
<a name="l00265"></a>00265 ev = *i;
<a name="l00266"></a>00266 } <span class="keywordflow">else</span> {
<a name="l00267"></a>00267 ev->setIndex(<a class="code" href="group__EM__Priv.html#ga212f07de6befabee47e4f9a1813e7c44" title="Return the next Expr index.">nextIndex</a>());
<a name="l00268"></a>00268 <a class="code" href="classCVC3_1_1ExprManager.html#a007da346931bbc8d2dafafaa81c4ea9c" title="Hash set for uniquifying expressions.">d_exprSet</a>.<a class="code" href="classHash_1_1hash__set.html#a156c40ba629d5aba7f7cacf4eeab1e2d">insert</a>(ev);
<a name="l00269"></a>00269 }
<a name="l00270"></a>00270 <span class="comment">// Use non-uniquifying Expr() constructor</span>
<a name="l00271"></a>00271 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> res(ev);
<a name="l00272"></a>00272 <span class="comment">// Cache the result</span>
<a name="l00273"></a>00273 <a class="code" href="classCVC3_1_1ExprManager.html#a841b8a48adc1372b7d99e3f93dd9620a" title="Rebuild cache.">d_rebuildCache</a>[e] = res;
<a name="l00274"></a>00274
<a name="l00275"></a>00275 <span class="comment">// Rebuild the type too</span>
<a name="l00276"></a>00276 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> t;
<a name="l00277"></a>00277 <span class="keywordflow">if</span> (!e.<a class="code" href="group__ExprPkg.html#ga3a08bea4e8715a268083e1671e340a2e">d_expr</a>-><a class="code" href="classCVC3_1_1ExprValue.html#a6c369e54e40d39696ff852e1013b7198" title="The cached type of the expression (may be Null)">d_type</a>.<a class="code" href="classCVC3_1_1Type.html#ab5fe00c99ee91f369e3339b26bab0bf7">isNull</a>()) {
<a name="l00278"></a>00278 t = <a class="code" href="classCVC3_1_1ExprManager.html#a18dba29b4f3e91d6d2bc53472a6bb7cc">Type</a>(<a class="code" href="group__EM__Priv.html#gaa86d7ed7800549f1621d2d5ce64ce643" title="Cached recursive descent. Must be called only during rebuild()">rebuildRec</a>(e.<a class="code" href="group__ExprPkg.html#ga3a08bea4e8715a268083e1671e340a2e">d_expr</a>-><a class="code" href="classCVC3_1_1ExprValue.html#a6c369e54e40d39696ff852e1013b7198" title="The cached type of the expression (may be Null)">d_type</a>.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>()));
<a name="l00279"></a>00279 <span class="keywordflow">if</span> (ev->d_type.isNull()) ev->d_type = t;
<a name="l00280"></a>00280 if (ev->d_type != t) {
<a name="l00281"></a>00281 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1Exception.html">Exception</a>(<span class="stringliteral">"Types don't match in rebuildRec"</span>);
<a name="l00282"></a>00282 }
<a name="l00283"></a>00283 }
<a name="l00284"></a>00284 <span class="keywordflow">return</span> res;
<a name="l00285"></a>00285 }
<a name="l00286"></a>00286
<a name="l00287"></a>00287
<a name="l00288"></a><a class="code" href="group__EM__Priv.html#ga3c693890e6e6e1610c44dda553dbf803">00288</a> <a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* <a class="code" href="group__EM__Priv.html#ga3c693890e6e6e1610c44dda553dbf803" title="Return either an existing or a new ExprValue matching ev.">ExprManager::newExprValue</a>(<a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* ev) {
<a name="l00289"></a>00289 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="group__EM__Priv.html#gaaec477005a23531fa15d27282658aab8" title="Check if the ExprManager is still active (clear() was not called)">isActive</a>(), <span class="stringliteral">"ExprManager::newExprValue(ExprValue*)"</span>);
<a name="l00290"></a>00290 <a class="code" href="classHash_1_1hash__set.html#a87a125f71dd85de65e662559bd5a66dc">ExprValueSet::iterator</a> i(<a class="code" href="classCVC3_1_1ExprManager.html#a007da346931bbc8d2dafafaa81c4ea9c" title="Hash set for uniquifying expressions.">d_exprSet</a>.<a class="code" href="classHash_1_1hash__set.html#a955279e5fd49f919bb6b0cd456d39c7b" title="operations">find</a>(ev)), iend(<a class="code" href="classCVC3_1_1ExprManager.html#a007da346931bbc8d2dafafaa81c4ea9c" title="Hash set for uniquifying expressions.">d_exprSet</a>.<a class="code" href="classHash_1_1hash__set.html#ae3ee82665499970f29a93df9948a5757">end</a>());
<a name="l00291"></a>00291 <span class="keywordflow">if</span>(i != iend) <span class="keywordflow">return</span> (*i);
<a name="l00292"></a>00292 <span class="comment">// No such ExprValue. Create a clean copy, insert it into the set</span>
<a name="l00293"></a>00293 <span class="comment">// and return the new pointer.</span>
<a name="l00294"></a>00294 <a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* p_ev = ev-><a class="code" href="classCVC3_1_1ExprValue.html#a2e152d0473e881c1eb47f5baeb546525" title="Make a clean copy of itself using the given ExprManager.">copy</a>(<span class="keyword">this</span>, <a class="code" href="group__EM__Priv.html#ga212f07de6befabee47e4f9a1813e7c44" title="Return the next Expr index.">nextIndex</a>());
<a name="l00295"></a>00295 <a class="code" href="classCVC3_1_1ExprManager.html#a007da346931bbc8d2dafafaa81c4ea9c" title="Hash set for uniquifying expressions.">d_exprSet</a>.<a class="code" href="classHash_1_1hash__set.html#a156c40ba629d5aba7f7cacf4eeab1e2d">insert</a>(p_ev);
<a name="l00296"></a>00296 <span class="keywordflow">return</span> p_ev;
<a name="l00297"></a>00297 }
<a name="l00298"></a>00298
<a name="l00299"></a>00299
<a name="l00300"></a>00300 <span class="comment">// ExprValue* ExprManager::newExprValue(const Expr& op,</span>
<a name="l00301"></a>00301 <span class="comment">// const vector<Expr>& kids) {</span>
<a name="l00302"></a>00302 <span class="comment">// // Check if op and kids have the same ExprManager</span>
<a name="l00303"></a>00303 <span class="comment">// DebugAssert(isActive(), "ExprManager::newExprValue(op, kids)");</span>
<a name="l00304"></a>00304 <span class="comment">// DebugAssert(this == op.getEM(),</span>
<a name="l00305"></a>00305 <span class="comment">// "ExprManager::newExprValue(op, kids): op is from a wrong "</span>
<a name="l00306"></a>00306 <span class="comment">// "ExprManager/ValidityChecker, call importExpr() first:\n"</span>
<a name="l00307"></a>00307 <span class="comment">// +op.toString());</span>
<a name="l00308"></a>00308 <span class="comment">// IF_DEBUG(</span>
<a name="l00309"></a>00309 <span class="comment">// for(vector<Expr>::const_iterator i=kids.begin(), iend=kids.end();</span>
<a name="l00310"></a>00310 <span class="comment">// i!=iend; ++i)</span>
<a name="l00311"></a>00311 <span class="comment">// DebugAssert(!i->isNull() && (i->getEM() == this),</span>
<a name="l00312"></a>00312 <span class="comment">// "ExprManager::newExprValue(op, kids): the child is"</span>
<a name="l00313"></a>00313 <span class="comment">// " from a wrong instance of ExprManager/ValidityChecker,"</span>
<a name="l00314"></a>00314 <span class="comment">// "call importExpr() first:\n"</span>
<a name="l00315"></a>00315 <span class="comment">// +i->toString());</span>
<a name="l00316"></a>00316 <span class="comment">// )</span>
<a name="l00317"></a>00317 <span class="comment">// ExprValue* res = op.d_expr->copy(this, kids);</span>
<a name="l00318"></a>00318 <span class="comment">// ExprValueSet::iterator i(d_exprSet.find(res)), iend(d_exprSet.end());</span>
<a name="l00319"></a>00319 <span class="comment">// if(i != iend) {</span>
<a name="l00320"></a>00320 <span class="comment">// MemoryManager* mm = getMM(res->getMMIndex());</span>
<a name="l00321"></a>00321 <span class="comment">// delete res;</span>
<a name="l00322"></a>00322 <span class="comment">// mm->deleteData(res);</span>
<a name="l00323"></a>00323 <span class="comment">// return (*i);</span>
<a name="l00324"></a>00324 <span class="comment">// } else {</span>
<a name="l00325"></a>00325 <span class="comment">// res->setIndex(nextIndex());</span>
<a name="l00326"></a>00326 <span class="comment">// installExprValue(res);</span>
<a name="l00327"></a>00327 <span class="comment">// return res;</span>
<a name="l00328"></a>00328 <span class="comment">// }</span>
<a name="l00329"></a>00329 <span class="comment">// }</span>
<a name="l00330"></a>00330
<a name="l00331"></a>00331 <span class="comment"></span>
<a name="l00332"></a>00332 <span class="comment">//! Set initial indentation. Returns the previous permanent value.</span>
<a name="l00333"></a>00333 <span class="comment"></span><span class="keywordtype">int</span>
<a name="l00334"></a><a class="code" href="group__EM__Priv.html#ga787e95a252f54b5fdb7c4d387ea49fae">00334</a> <a class="code" href="group__EM__Priv.html#ga54ddb950b6bd35316d1cefe3fd506149" title="Get initial indentation.">ExprManager::indent</a>(<span class="keywordtype">int</span> n, <span class="keywordtype">bool</span> permanent) {
<a name="l00335"></a>00335 <span class="keywordtype">int</span> ret(<a class="code" href="classCVC3_1_1ExprManager.html#a74ef690ec61d40be41b784246ecd32c4" title="Permanent indentation.">d_indent</a>);
<a name="l00336"></a>00336 <a class="code" href="classCVC3_1_1ExprManager.html#a84f7afd3443e0b6998db69cea8340b38" title="Transient indentation.">d_indentTransient</a> = n;
<a name="l00337"></a>00337 <span class="keywordflow">if</span>(permanent) <a class="code" href="classCVC3_1_1ExprManager.html#a74ef690ec61d40be41b784246ecd32c4" title="Permanent indentation.">d_indent</a> = n;
<a name="l00338"></a>00338 <span class="keywordflow">return</span> ret;
<a name="l00339"></a>00339 }
<a name="l00340"></a>00340 <span class="comment"></span>
<a name="l00341"></a>00341 <span class="comment">//! Increment the current transient indentation by n</span>
<a name="l00342"></a>00342 <span class="comment"></span><span class="comment">/*! If the second argument is true, sets the result as permanent.</span>
<a name="l00343"></a>00343 <span class="comment"> \return previous permanent value. */</span>
<a name="l00344"></a>00344 <span class="keywordtype">int</span>
<a name="l00345"></a><a class="code" href="group__EM__Priv.html#gaf1a5a30e0f0ed0a3e59201530d39d49a">00345</a> <a class="code" href="group__EM__Priv.html#gaf1a5a30e0f0ed0a3e59201530d39d49a" title="Increment the current transient indentation by n.">ExprManager::incIndent</a>(<span class="keywordtype">int</span> n, <span class="keywordtype">bool</span> permanent) {
<a name="l00346"></a>00346 <span class="keywordtype">int</span> ret(<a class="code" href="classCVC3_1_1ExprManager.html#a74ef690ec61d40be41b784246ecd32c4" title="Permanent indentation.">d_indent</a>);
<a name="l00347"></a>00347 <a class="code" href="classCVC3_1_1ExprManager.html#a84f7afd3443e0b6998db69cea8340b38" title="Transient indentation.">d_indentTransient</a> += n;
<a name="l00348"></a>00348 <span class="keywordflow">if</span>(permanent) <a class="code" href="classCVC3_1_1ExprManager.html#a74ef690ec61d40be41b784246ecd32c4" title="Permanent indentation.">d_indent</a> = <a class="code" href="classCVC3_1_1ExprManager.html#a84f7afd3443e0b6998db69cea8340b38" title="Transient indentation.">d_indentTransient</a>;
<a name="l00349"></a>00349 <span class="keywordflow">return</span> ret;
<a name="l00350"></a>00350 }
<a name="l00351"></a>00351
<a name="l00352"></a>00352 <span class="comment">// Various options</span>
<a name="l00353"></a>00353 <a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e" title="Different input languages.">InputLanguage</a>
<a name="l00354"></a><a class="code" href="group__EM__Priv.html#gae33e1c95930679cde944e2d2d5984db1">00354</a> <a class="code" href="group__EM__Priv.html#gae33e1c95930679cde944e2d2d5984db1" title="Get the input language for printing.">ExprManager::getInputLang</a>()<span class="keyword"> const </span>{
<a name="l00355"></a>00355 <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#aac47d390dde36b9c597d428cb149bee7">getLanguage</a>(*<a class="code" href="classCVC3_1_1ExprManager.html#ac323f030431b1f87c9201117486f2fd6" title="Input language (printing)">d_inputLang</a>);
<a name="l00356"></a>00356 }
<a name="l00357"></a>00357
<a name="l00358"></a>00358
<a name="l00359"></a>00359 <a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e" title="Different input languages.">InputLanguage</a>
<a name="l00360"></a><a class="code" href="group__EM__Priv.html#gaeef110905b00e6e89f54c082e3c4c1a3">00360</a> <a class="code" href="group__EM__Priv.html#gaeef110905b00e6e89f54c082e3c4c1a3" title="Get the output language for printing.">ExprManager::getOutputLang</a>()<span class="keyword"> const </span>{
<a name="l00361"></a>00361 <span class="keyword">const</span> std::string* langPtr
<a name="l00362"></a>00362 = (*<a class="code" href="classCVC3_1_1ExprManager.html#ac2d8f75464d06456fa0b2111df849d70" title="Output language (printing)">d_outputLang</a> == <span class="stringliteral">""</span>)? <a class="code" href="classCVC3_1_1ExprManager.html#ac323f030431b1f87c9201117486f2fd6" title="Input language (printing)">d_inputLang</a> : <a class="code" href="classCVC3_1_1ExprManager.html#ac2d8f75464d06456fa0b2111df849d70" title="Output language (printing)">d_outputLang</a>;
<a name="l00363"></a>00363 <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#aac47d390dde36b9c597d428cb149bee7">getLanguage</a>(*langPtr);
<a name="l00364"></a>00364 }
<a name="l00365"></a>00365
<a name="l00366"></a>00366
<a name="l00367"></a><a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1">00367</a> <span class="keywordtype">void</span> <a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">ExprManager::newKind</a>(<span class="keywordtype">int</span> kind, <span class="keyword">const</span> <span class="keywordtype">string</span> &name, <span class="keywordtype">bool</span> isType) {
<a name="l00368"></a>00368 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1ExprManager.html#a07ec9cfbc5aa8fbc09b7844a4a7ad34e" title="The database of registered kinds.">d_kindMap</a>.<a class="code" href="classHash_1_1hash__map.html#a3d52fe0d391d58e9573ce84472dfea24">count</a>(kind) == 0) {
<a name="l00369"></a>00369 <a class="code" href="classCVC3_1_1ExprManager.html#a07ec9cfbc5aa8fbc09b7844a4a7ad34e" title="The database of registered kinds.">d_kindMap</a>[kind] = name;
<a name="l00370"></a>00370 <span class="keywordflow">if</span>(isType) <a class="code" href="classCVC3_1_1ExprManager.html#a77f4cd27ea691329a3c01285c116eebd" title="The set of kinds representing a type.">d_typeKinds</a>.<a class="code" href="classHash_1_1hash__set.html#a156c40ba629d5aba7f7cacf4eeab1e2d">insert</a>(kind);
<a name="l00371"></a>00371 }
<a name="l00372"></a>00372 <span class="keywordflow">else</span> <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1ExprManager.html#a07ec9cfbc5aa8fbc09b7844a4a7ad34e" title="The database of registered kinds.">d_kindMap</a>[kind] != name) {
<a name="l00373"></a>00373 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"CVC3::ExprManager::newKind(kind = "</span>
<a name="l00374"></a>00374 + <a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(kind) + <span class="stringliteral">", name = "</span> + name
<a name="l00375"></a>00375 + <span class="stringliteral">"): \n"</span> +
<a name="l00376"></a>00376 <span class="stringliteral">"this kind is already registered with a different name: "</span>
<a name="l00377"></a>00377 + <a class="code" href="classCVC3_1_1ExprManager.html#a07ec9cfbc5aa8fbc09b7844a4a7ad34e" title="The database of registered kinds.">d_kindMap</a>[kind]);
<a name="l00378"></a>00378 }
<a name="l00379"></a>00379 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1ExprManager.html#aeab702ffe6838b75b285df2d1cd0f8fb" title="The reverse map of names to kinds.">d_kindMapByName</a>.<a class="code" href="classHash_1_1hash__map.html#a3d52fe0d391d58e9573ce84472dfea24">count</a>(name) == 0)
<a name="l00380"></a>00380 <a class="code" href="classCVC3_1_1ExprManager.html#aeab702ffe6838b75b285df2d1cd0f8fb" title="The reverse map of names to kinds.">d_kindMapByName</a>[name] = kind;
<a name="l00381"></a>00381 <span class="keywordflow">else</span> <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1ExprManager.html#aeab702ffe6838b75b285df2d1cd0f8fb" title="The reverse map of names to kinds.">d_kindMapByName</a>[name] != kind) {
<a name="l00382"></a>00382 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"CVC3::ExprManager::newKind(kind = "</span>
<a name="l00383"></a>00383 + <a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(kind) + <span class="stringliteral">", name = "</span> + name
<a name="l00384"></a>00384 + <span class="stringliteral">"): \n"</span> +
<a name="l00385"></a>00385 <span class="stringliteral">"this kind name is already registered with a different index: "</span>
<a name="l00386"></a>00386 + <a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(<a class="code" href="classCVC3_1_1ExprManager.html#aeab702ffe6838b75b285df2d1cd0f8fb" title="The reverse map of names to kinds.">d_kindMapByName</a>[name]));
<a name="l00387"></a>00387 }
<a name="l00388"></a>00388 }
<a name="l00389"></a>00389
<a name="l00390"></a>00390 <span class="comment">// Register a printer</span>
<a name="l00391"></a><a class="code" href="group__EM__Priv.html#gacd01e4de3a171218d0192a9450fb7605">00391</a> <span class="keywordtype">void</span> <a class="code" href="group__EM__Priv.html#gacd01e4de3a171218d0192a9450fb7605" title="Register the pretty-printer (can only do it if none registered)">ExprManager::registerPrettyPrinter</a>(<a class="code" href="classCVC3_1_1PrettyPrinter.html" title="Abstract API to a pretty-printer for Expr.">PrettyPrinter</a>& printer) {
<a name="l00392"></a>00392 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1ExprManager.html#a12e3e4bb896c10134908607b528512de" title="The registered pretty-printer, a connector to theory-specific pretty-printers.">d_prettyPrinter</a>==NULL, <span class="stringliteral">"ExprManager:registerPrettyPrinter():"</span>
<a name="l00393"></a>00393 <span class="stringliteral">" printer is already registered"</span>);
<a name="l00394"></a>00394 <a class="code" href="classCVC3_1_1ExprManager.html#a12e3e4bb896c10134908607b528512de" title="The registered pretty-printer, a connector to theory-specific pretty-printers.">d_prettyPrinter</a> = &printer;
<a name="l00395"></a>00395 }
<a name="l00396"></a>00396
<a name="l00397"></a>00397 <span class="comment">// Unregister a printer</span>
<a name="l00398"></a><a class="code" href="group__EM__Priv.html#ga4662ac518622beab3379f6da23380a75">00398</a> <span class="keywordtype">void</span> <a class="code" href="group__EM__Priv.html#ga4662ac518622beab3379f6da23380a75" title="Tell ExprManager that the printer is no longer valid.">ExprManager::unregisterPrettyPrinter</a>() {
<a name="l00399"></a>00399 <a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(<a class="code" href="classCVC3_1_1ExprManager.html#a12e3e4bb896c10134908607b528512de" title="The registered pretty-printer, a connector to theory-specific pretty-printers.">d_prettyPrinter</a>!=NULL, <span class="stringliteral">"ExprManager:unregisterPrettyPrinter():"</span>
<a name="l00400"></a>00400 <span class="stringliteral">" printer is not registered"</span>);
<a name="l00401"></a>00401 <a class="code" href="classCVC3_1_1ExprManager.html#a12e3e4bb896c10134908607b528512de" title="The registered pretty-printer, a connector to theory-specific pretty-printers.">d_prettyPrinter</a> = NULL;
<a name="l00402"></a>00402 }
<a name="l00403"></a>00403
<a name="l00404"></a>00404
<a name="l00405"></a><a class="code" href="group__EM__Priv.html#gad129f2ecc362f60ca43e06ff46b8521b">00405</a> <span class="keyword">const</span> <span class="keywordtype">string</span>& <a class="code" href="group__EM__Priv.html#gad129f2ecc362f60ca43e06ff46b8521b" title="Return the name associated with a kind. The kind must already be registered.">ExprManager::getKindName</a>(<span class="keywordtype">int</span> kind) {
<a name="l00406"></a>00406 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1ExprManager.html#a07ec9cfbc5aa8fbc09b7844a4a7ad34e" title="The database of registered kinds.">d_kindMap</a>.<a class="code" href="classHash_1_1hash__map.html#a3d52fe0d391d58e9573ce84472dfea24">count</a>(kind) > 0,
<a name="l00407"></a>00407 (<span class="stringliteral">"CVC3::ExprManager::getKindName(kind = "</span>
<a name="l00408"></a>00408 + <a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(kind) + <span class="stringliteral">"): kind is not registered."</span>).c_str());
<a name="l00409"></a>00409 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprManager.html#a07ec9cfbc5aa8fbc09b7844a4a7ad34e" title="The database of registered kinds.">d_kindMap</a>[kind];
<a name="l00410"></a>00410 }
<a name="l00411"></a>00411
<a name="l00412"></a><a class="code" href="group__EM__Priv.html#ga9e7929fab9329724812e74b066a3c90a">00412</a> <span class="keywordtype">int</span> <a class="code" href="group__EM__Priv.html#ga9e7929fab9329724812e74b066a3c90a" title="Return a kind associated with a name. Returns NULL_KIND if not found.">ExprManager::getKind</a>(<span class="keyword">const</span> <span class="keywordtype">string</span>& name) {
<a name="l00413"></a>00413 <a class="code" href="classHash_1_1hash__map.html">std::hash_map<std::string, int, HashString>::iterator</a>
<a name="l00414"></a>00414 i=<a class="code" href="classCVC3_1_1ExprManager.html#aeab702ffe6838b75b285df2d1cd0f8fb" title="The reverse map of names to kinds.">d_kindMapByName</a>.<a class="code" href="classHash_1_1hash__map.html#af3317f9087a35d09985b6513c45d2ab8" title="operations">find</a>(name),
<a name="l00415"></a>00415 iend=<a class="code" href="classCVC3_1_1ExprManager.html#aeab702ffe6838b75b285df2d1cd0f8fb" title="The reverse map of names to kinds.">d_kindMapByName</a>.<a class="code" href="classHash_1_1hash__map.html#a2c776e055f3d17226605157e1c37dbc9">end</a>();
<a name="l00416"></a>00416 <span class="keywordflow">if</span>(i==iend) <span class="keywordflow">return</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5bc05ce87fa69f660d39d0a4fa188c67">NULL_KIND</a>;
<a name="l00417"></a>00417 <span class="keywordflow">else</span> <span class="keywordflow">return</span> (*i).second;
<a name="l00418"></a>00418 }
<a name="l00419"></a>00419
<a name="l00420"></a>00420
<a name="l00421"></a><a class="code" href="group__EM__Priv.html#ga10284641fda307d52345f73e8ad5def0">00421</a> <span class="keywordtype">size_t</span> <a class="code" href="group__EM__Priv.html#ga10284641fda307d52345f73e8ad5def0" title="Register a new subclass of ExprValue.">ExprManager::registerSubclass</a>(<span class="keywordtype">size_t</span> sizeOfSubclass) {
<a name="l00422"></a>00422 <span class="keywordtype">size_t</span> idx(<a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>.size());
<a name="l00423"></a>00423 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1ExprManager.html#a5cfe801f6ae8f9fd7a51477a219685e8" title="Which memory manager to use (copy the flag value and keep it the same)">d_mmFlag</a> == <span class="stringliteral">"chunks"</span>)
<a name="l00424"></a>00424 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>.push_back(<span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerChunks.html">MemoryManagerChunks</a>(sizeOfSubclass));
<a name="l00425"></a>00425 <span class="keywordflow">else</span>
<a name="l00426"></a>00426 <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>.push_back(<span class="keyword">new</span> <a class="code" href="classCVC3_1_1MemoryManagerMalloc.html">MemoryManagerMalloc</a>());
<a name="l00427"></a>00427
<a name="l00428"></a>00428 <a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(<a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>.back() != NULL, <span class="stringliteral">"Out of memory"</span>);
<a name="l00429"></a>00429 <span class="keywordflow">return</span> idx;
<a name="l00430"></a>00430 }
<a name="l00431"></a>00431
<a name="l00432"></a>00432
<a name="l00433"></a><a class="code" href="group__EM__Priv.html#gaa4b16553ca47bb59c3978be771a5766b">00433</a> <span class="keywordtype">unsigned</span> <span class="keywordtype">long</span> <a class="code" href="group__EM__Priv.html#gaa4b16553ca47bb59c3978be771a5766b" title="Calculate memory usage.">ExprManager::getMemory</a>(<span class="keywordtype">int</span> verbosity)
<a name="l00434"></a>00434 {
<a name="l00435"></a>00435 <span class="keywordtype">unsigned</span> <span class="keywordtype">long</span> memSelf = <span class="keyword">sizeof</span>(<a class="code" href="group__EM__Priv.html#gaf3af8657f4b2c64f189f0a50147d3589" title="Constructor.">ExprManager</a>);
<a name="l00436"></a>00436 <span class="keywordtype">unsigned</span> <span class="keywordtype">long</span> mem = 0;
<a name="l00437"></a>00437
<a name="l00438"></a>00438 <span class="comment">// mem += MemoryTracker::getHashMap(verbosity - 1, d_kindMap);</span>
<a name="l00439"></a>00439
<a name="l00440"></a>00440 <span class="comment">// mem += d_typeKinds.getMemory(verbosity - 1);</span>
<a name="l00441"></a>00441 <span class="comment">// mem += d_kindMapByName.getMemory(verbosity - 1);</span>
<a name="l00442"></a>00442 <span class="comment">// mem += d_prettyPrinter->getMemory(verbosity - 1);</span>
<a name="l00443"></a>00443 mem += <a class="code" href="classCVC3_1_1MemoryTracker.html#add7e68c278aae046a5f5a4df50402114">MemoryTracker::getString</a>(verbosity - 1, <a class="code" href="classCVC3_1_1ExprManager.html#a5cfe801f6ae8f9fd7a51477a219685e8" title="Which memory manager to use (copy the flag value and keep it the same)">d_mmFlag</a>);
<a name="l00444"></a>00444
<a name="l00445"></a>00445 <span class="comment">// mem += d_exprSet.getMemory(verbosity - 1);</span>
<a name="l00446"></a>00446 <span class="comment">// mem += getMemoryVec(d_mm);</span>
<a name="l00447"></a>00447 <span class="comment">// for (i = 0; i < d_mm.size(); ++i) {</span>
<a name="l00448"></a>00448 <span class="comment">// mem += d_mm->getMemory(verbosity - 1);</span>
<a name="l00449"></a>00449 <span class="comment">// }</span>
<a name="l00450"></a>00450
<a name="l00451"></a>00451 <span class="comment">// mem += d_pointerHash.getMemory(verbosity - 1) - sizeof(hash<void*>);</span>
<a name="l00452"></a>00452
<a name="l00453"></a>00453 <span class="comment">// mem += getMemoryVec(d_emptyVec);</span>
<a name="l00454"></a>00454 <span class="comment">// mem += getMemoryVec(d_postponed);</span>
<a name="l00455"></a>00455 <span class="comment">// mem += d_rebuildCache.getMemory(verbosity - 1) - sizeof(ExprHashMap<Expr>);</span>
<a name="l00456"></a>00456
<a name="l00457"></a>00457 <span class="comment">// mem += d_typecomputer->getMemory(verbosity - 1);</span>
<a name="l00458"></a>00458
<a name="l00459"></a>00459 <a class="code" href="classCVC3_1_1MemoryTracker.html#a689b66f3be59b607f35a67238817b9d0">MemoryTracker::print</a>(<span class="stringliteral">"ExprManager"</span>, verbosity, memSelf, mem);
<a name="l00460"></a>00460
<a name="l00461"></a>00461 <span class="keywordflow">return</span> mem + memSelf;
<a name="l00462"></a>00462 }
<a name="l00463"></a>00463
<a name="l00464"></a>00464
<a name="l00465"></a><a class="code" href="group__EM__Priv.html#ga15e87e829f86a1dcf2c5e05be6f4d182">00465</a> <span class="keywordtype">void</span> <a class="code" href="group__EM__Priv.html#ga15e87e829f86a1dcf2c5e05be6f4d182" title="Compute the type of the Expr.">ExprManager::computeType</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 name="l00466"></a>00466 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1ExprManager.html#a3b4356ae8ebb7c1fc561188920ae7d03" title="Instance of TypeComputer: must be registered.">d_typeComputer</a>, <span class="stringliteral">"No type computer installed"</span>);
<a name="l00467"></a>00467 <a class="code" href="classCVC3_1_1ExprManager.html#a3b4356ae8ebb7c1fc561188920ae7d03" title="Instance of TypeComputer: must be registered.">d_typeComputer</a>-><a class="code" href="group__EM__Priv.html#ga670ca72899c66da598ea568af7389407" title="Compute the type of e.">computeType</a>(e);
<a name="l00468"></a>00468 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!e.<a class="code" href="group__ExprPkg.html#ga42929221eb172250697b72c28af6de07" title="Get the type. Recursively compute if necessary.">getType</a>().<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>().<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>(), <span class="stringliteral">"Type not set by computeType"</span>);
<a name="l00469"></a>00469 }
<a name="l00470"></a>00470
<a name="l00471"></a>00471
<a name="l00472"></a><a class="code" href="group__EM__Priv.html#ga51109c3e331615c510c964798b38ee95">00472</a> <span class="keywordtype">void</span> <a class="code" href="group__EM__Priv.html#ga51109c3e331615c510c964798b38ee95" title="Check well-formedness of a type Expr.">ExprManager::checkType</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 name="l00473"></a>00473 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1ExprManager.html#a3b4356ae8ebb7c1fc561188920ae7d03" title="Instance of TypeComputer: must be registered.">d_typeComputer</a>, <span class="stringliteral">"No type computer installed"</span>);
<a name="l00474"></a>00474 <span class="keywordflow">if</span> (!e.<a class="code" href="group__ExprPkg.html#gaed5d5a14a8089122a0e05a55e38fc37f">isValidType</a>()) <a class="code" href="classCVC3_1_1ExprManager.html#a3b4356ae8ebb7c1fc561188920ae7d03" title="Instance of TypeComputer: must be registered.">d_typeComputer</a>-><a class="code" href="group__EM__Priv.html#gae679c021fb433f86c28c5eec68e5b5ee" title="Check that e is a valid Type expr.">checkType</a>(e);
<a name="l00475"></a>00475 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e.<a class="code" href="group__ExprPkg.html#gaed5d5a14a8089122a0e05a55e38fc37f">isValidType</a>(), <span class="stringliteral">"Type not checked by checkType"</span>);
<a name="l00476"></a>00476 }
<a name="l00477"></a>00477
<a name="l00478"></a>00478
<a name="l00479"></a><a class="code" href="group__EM__Priv.html#gae5cc4c6a7dfcc718c7c931e6b160d9d1">00479</a> <a class="code" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54" title="Enum for cardinality of types.">Cardinality</a> <a class="code" href="group__EM__Priv.html#gae5cc4c6a7dfcc718c7c931e6b160d9d1" title="Get information related to finiteness of a type.">ExprManager::finiteTypeInfo</a>(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e,
<a name="l00480"></a>00480 <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a>& n,
<a name="l00481"></a>00481 <span class="keywordtype">bool</span> enumerate,
<a name="l00482"></a>00482 <span class="keywordtype">bool</span> computeSize)
<a name="l00483"></a>00483 {
<a name="l00484"></a>00484 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1ExprManager.html#a3b4356ae8ebb7c1fc561188920ae7d03" title="Instance of TypeComputer: must be registered.">d_typeComputer</a>, <span class="stringliteral">"No type computer installed"</span>);
<a name="l00485"></a>00485 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1ExprManager.html#a3b4356ae8ebb7c1fc561188920ae7d03" title="Instance of TypeComputer: must be registered.">d_typeComputer</a>-><a class="code" href="group__EM__Priv.html#ga13e9c0f4a23614e99705f60e3913c2b1" title="Get information related to finiteness of a type.">finiteTypeInfo</a>(e, n, enumerate, computeSize);
<a name="l00486"></a>00486 }
<a name="l00487"></a>00487
<a name="l00488"></a>00488
<a name="l00489"></a>00489 <span class="comment">// Kind registration macro</span>
<a name="l00490"></a><a class="code" href="expr__manager_8cpp.html#ad33da540eb3d11c1971c4a03d100013c">00490</a> <span class="preprocessor">#define REG(k) em.newKind(k, #k)</span>
<a name="l00491"></a><a class="code" href="expr__manager_8cpp.html#a7876b7f51ad3380f0bd237585f17672c">00491</a> <span class="preprocessor"></span><span class="preprocessor">#define REG_TYPE(k) em.newKind(k, #k, true)</span>
<a name="l00492"></a>00492 <span class="preprocessor"></span>
<a name="l00493"></a><a class="code" href="expr__manager_8cpp.html#ae7ac6263bf1137d9d09d24e72f3f0e11">00493</a> <span class="keyword">static</span> <span class="keywordtype">void</span> <a class="code" href="expr__manager_8cpp.html#ae7ac6263bf1137d9d09d24e72f3f0e11">registerKinds</a>(<a class="code" href="classCVC3_1_1ExprManager.html">ExprManager</a>& em) {
<a name="l00494"></a>00494 <span class="comment">// Register type kinds</span>
<a name="l00495"></a>00495 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba8a583f16e8d237a423c8c1d9087a4c72">BOOLEAN</a>, <span class="stringliteral">"_BOOLEAN"</span>, <span class="keyword">true</span>);
<a name="l00496"></a>00496 <span class="comment">// REG(TUPLE_TYPE);</span>
<a name="l00497"></a>00497 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba6245843ec0c376adc7b587ad82459846">ANY_TYPE</a>, <span class="stringliteral">"_ANY_TYPE"</span>, <span class="keyword">true</span>);
<a name="l00498"></a>00498 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba546eccfedc4dcc8623ed0668f77ef982">ARROW</a>, <span class="stringliteral">"_ARROW"</span>, <span class="keyword">true</span>);
<a name="l00499"></a>00499 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab47ea8bb955afd0adc0ef98517dd6084">TYPE</a>, <span class="stringliteral">"_TYPE"</span>, <span class="keyword">true</span>);
<a name="l00500"></a>00500 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3bcf72a59026c6765481b300b363ff59">TYPEDECL</a>, <span class="stringliteral">"_TYPEDECL"</span>, <span class="keyword">true</span>);
<a name="l00501"></a>00501 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba802d02227696a7c5b5420b28d8b82338">TYPEDEF</a>, <span class="stringliteral">"_TYPEDEF"</span>, <span class="keyword">true</span>);
<a name="l00502"></a>00502 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9ae776fb49b0eb32dd93f866492000b5">SUBTYPE</a>, <span class="stringliteral">"_SUBTYPE"</span>, <span class="keyword">true</span>);
<a name="l00503"></a>00503
<a name="l00504"></a>00504 <span class="comment">// Register expression (non-type) kinds</span>
<a name="l00505"></a>00505 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5bc05ce87fa69f660d39d0a4fa188c67">NULL_KIND</a>, <span class="stringliteral">"_NULL_KIND"</span>);
<a name="l00506"></a>00506
<a name="l00507"></a>00507 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a>, <span class="stringliteral">"_RAW_LIST"</span>);
<a name="l00508"></a>00508 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba354df7c2d2ec2e54317f07437dc7380b">STRING_EXPR</a>, <span class="stringliteral">"_STRING_EXPR"</span>);
<a name="l00509"></a>00509 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bae07a708ec52c578b62f8b0f701571d56">RATIONAL_EXPR</a>, <span class="stringliteral">"_RATIONAL_EXPR"</span>);
<a name="l00510"></a>00510 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba1fad76919fba496de21807e2beec533d">TRUE_EXPR</a>, <span class="stringliteral">"_TRUE_EXPR"</span>);
<a name="l00511"></a>00511 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5f71bd33a6528411ae681f5291de1d82">FALSE_EXPR</a>, <span class="stringliteral">"_FALSE_EXPR"</span>);
<a name="l00512"></a>00512
<a name="l00513"></a>00513 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>, <span class="stringliteral">"_EQ"</span>);
<a name="l00514"></a>00514 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab4ab8d2a8dc61f08e3cc919787c79cd8">NEQ</a>, <span class="stringliteral">"_NEQ"</span>);
<a name="l00515"></a>00515 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa23a9880eca693f679c969556249925f">DISTINCT</a>, <span class="stringliteral">"_DISTINCT"</span>);
<a name="l00516"></a>00516
<a name="l00517"></a>00517 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0378ebc895849163b249d0b330257dd6">NOT</a>, <span class="stringliteral">"_NOT"</span>);
<a name="l00518"></a>00518 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba865555c9f2e0458a7078486aa1b3254f">AND</a>, <span class="stringliteral">"_AND"</span>);
<a name="l00519"></a>00519 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>, <span class="stringliteral">"_OR"</span>);
<a name="l00520"></a>00520 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bac62338ffb5de22369c75caa565b5da1a">XOR</a>, <span class="stringliteral">"_XOR"</span>);
<a name="l00521"></a>00521 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, <span class="stringliteral">"_IFF"</span>);
<a name="l00522"></a>00522 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7338bb59b9aa936104a6d2f631d4d8db">IMPLIES</a>, <span class="stringliteral">"_IMPLIES"</span>);
<a name="l00523"></a>00523
<a name="l00524"></a>00524 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf18208f4921c8175373d32e4ce909d42">AND_R</a>, <span class="stringliteral">"_AND_R"</span>);
<a name="l00525"></a>00525 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab3535bf1f1c26490d56f63dc20696fa6">IFF_R</a>, <span class="stringliteral">"_IFF_R"</span>);
<a name="l00526"></a>00526 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba096c0758089b7d7d0a596b1b4c89a084">ITE_R</a>, <span class="stringliteral">"_ITE_R"</span>);
<a name="l00527"></a>00527
<a name="l00528"></a>00528 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc">ITE</a>, <span class="stringliteral">"_ITE"</span>);
<a name="l00529"></a>00529
<a name="l00530"></a>00530 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7b7b6f6e2b88589bd4656a14bcb7eb94">FORALL</a>, <span class="stringliteral">"_FORALL"</span>);
<a name="l00531"></a>00531 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3197625a1bb2264943f5a95f236d9973">EXISTS</a>, <span class="stringliteral">"_EXISTS"</span>);
<a name="l00532"></a>00532
<a name="l00533"></a>00533 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa677b4263f974f2ccfe7986cedf3988e">UFUNC</a>, <span class="stringliteral">"_UFUNC"</span>);
<a name="l00534"></a>00534 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5c41450c4e719ca40d8e734f6a2008f0">APPLY</a>, <span class="stringliteral">"_APPLY"</span>);
<a name="l00535"></a>00535
<a name="l00536"></a>00536 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba61d9e0e93eb9635173764c5ba45666f1">ASSERT</a>, <span class="stringliteral">"_ASSERT"</span>);
<a name="l00537"></a>00537 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba21043ddfa5289b4cf14cd4e3f5a89b62">QUERY</a>, <span class="stringliteral">"_QUERY"</span>);
<a name="l00538"></a>00538 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba97a3c2659984ba305c883c77e5d837be">CHECKSAT</a>, <span class="stringliteral">"_CHECKSAT"</span>);
<a name="l00539"></a>00539 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba49959dd441dcda75d6898cf2c68fb374">CONTINUE</a>, <span class="stringliteral">"_CONTINUE"</span>);
<a name="l00540"></a>00540 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba262553c759e1d1a9398bc406b1fadcb7">RESTART</a>, <span class="stringliteral">"_RESTART"</span>);
<a name="l00541"></a>00541 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba488607ea6c5f90b63a063b953af1e078">DBG</a>, <span class="stringliteral">"_DBG"</span>);
<a name="l00542"></a>00542 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>, <span class="stringliteral">"_TRACE"</span>);
<a name="l00543"></a>00543 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba4360655450c463532deae4a265852354">UNTRACE</a>, <span class="stringliteral">"_UNTRACE"</span>);
<a name="l00544"></a>00544 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa90a72437604db645f335d571993dade">OPTION</a>, <span class="stringliteral">"_OPTION"</span>);
<a name="l00545"></a>00545 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9f5cb747b2e1f0ea781d2b1f2a5b4824">HELP</a>, <span class="stringliteral">"_HELP"</span>);
<a name="l00546"></a>00546 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba25f73324dc93d9024c0c75b4e6815335">TRANSFORM</a>, <span class="stringliteral">"_TRANSFORM"</span>);
<a name="l00547"></a>00547 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab107229d44d042caa8ab8df4c8acaa1f">PRINT</a>, <span class="stringliteral">"_PRINT"</span>);
<a name="l00548"></a>00548 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5babd0ebc08c262bab82a1882256d2d66e8">CALL</a>, <span class="stringliteral">"_CALL"</span>);
<a name="l00549"></a>00549 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba6e074abc1ec6368da315a331ad35c00b">ECHO</a>, <span class="stringliteral">"_ECHO"</span>);
<a name="l00550"></a>00550 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2f6f94469432973066c534d9bd1d1a7c">INCLUDE</a>, <span class="stringliteral">"_INCLUDE"</span>);
<a name="l00551"></a>00551 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf2fb94d1fd1739ad68220e57882efa23">GET_VALUE</a>, <span class="stringliteral">"_GET_VALUE"</span>);
<a name="l00552"></a>00552 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba93ac551e3fa00bc3ba324544985e0e07">GET_ASSIGNMENT</a>, <span class="stringliteral">"_GET_ASSIGNMENT"</span>);
<a name="l00553"></a>00553 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baaa71d9f5a927e04c20c2fe5708f30be2">DUMP_PROOF</a>, <span class="stringliteral">"_DUMP_PROOF"</span>);
<a name="l00554"></a>00554 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab31d3b785074846671439597e155a473">DUMP_ASSUMPTIONS</a>, <span class="stringliteral">"_DUMP_ASSUMPTIONS"</span>);
<a name="l00555"></a>00555 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7d5922eb81555f9010561ea51e241313">DUMP_SIG</a>, <span class="stringliteral">"_DUMP_SIG"</span>);
<a name="l00556"></a>00556 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0f26f0a2b11e05637f9aede0c3c953a1">DUMP_TCC</a>, <span class="stringliteral">"_DUMP_TCC"</span>);
<a name="l00557"></a>00557 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba806bb6dde10ffd8d7e12b01cf8a04421">DUMP_TCC_ASSUMPTIONS</a>, <span class="stringliteral">"_DUMP_TCC_ASSUMPTIONS"</span>);
<a name="l00558"></a>00558 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba8d86d3a8550f33dfb735dc25813c5794">DUMP_TCC_PROOF</a>, <span class="stringliteral">"_DUMP_TCC_PROOF"</span>);
<a name="l00559"></a>00559 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5badbf9b8b24fc59b74bd2b2121aba21e75">DUMP_CLOSURE</a>, <span class="stringliteral">"_DUMP_CLOSURE"</span>);
<a name="l00560"></a>00560 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2322495bb9d482b215bc6b52df111415">DUMP_CLOSURE_PROOF</a>, <span class="stringliteral">"_DUMP_CLOSURE_PROOF"</span>);
<a name="l00561"></a>00561 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0116b78582fbf1fd6e069fde8dd308c4">WHERE</a>, <span class="stringliteral">"_WHERE"</span>);
<a name="l00562"></a>00562 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bafa9d306e675c3be077c2e0561e6e8e6d">ASSERTIONS</a>, <span class="stringliteral">"_ASSERTIONS"</span>);
<a name="l00563"></a>00563 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab65def84e41af84db85737a6eb8dc748">ASSUMPTIONS</a>, <span class="stringliteral">"_ASSUMPTIONS"</span>);
<a name="l00564"></a>00564 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba87ad730e285cf17f4eefb214236a2c7a">COUNTEREXAMPLE</a>, <span class="stringliteral">"_COUNTEREXAMPLE"</span>);
<a name="l00565"></a>00565 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baea3d2c8907d2df3f13c0866a7970baaa">COUNTERMODEL</a>, <span class="stringliteral">"_COUNTERMODEL"</span>);
<a name="l00566"></a>00566 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bad263caec619c4d99e4684ba0fabd9493">PUSH</a>, <span class="stringliteral">"_PUSH"</span>);
<a name="l00567"></a>00567 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba061dcf4785583d8653942f2d252174fa">POP</a>, <span class="stringliteral">"_POP"</span>);
<a name="l00568"></a>00568 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba908bcfbc13c7f414e83641bb9339f31f">POPTO</a>, <span class="stringliteral">"_POPTO"</span>);
<a name="l00569"></a>00569 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5b5b049bfd6cb81f552222a8aad0dd99">PUSH_SCOPE</a>, <span class="stringliteral">"_PUSH_SCOPE"</span>);
<a name="l00570"></a>00570 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0eb24f3375e74e8a42303dc0c6e7e952">POP_SCOPE</a>, <span class="stringliteral">"_POP_SCOPE"</span>);
<a name="l00571"></a>00571 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba577463735743ccd8d67d3549bdcbc5eb">POPTO_SCOPE</a>, <span class="stringliteral">"_POPTO_SCOPE"</span>);
<a name="l00572"></a>00572 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba589b7d94a3d91d145720e2fed0eb3a05">RESET</a>, <span class="stringliteral">"_RESET"</span>);
<a name="l00573"></a>00573 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7f06283f0d1a4d167be6c37a3d24fd11">CONTEXT</a>, <span class="stringliteral">"_CONTEXT"</span>);
<a name="l00574"></a>00574 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5badd6ce7bf1c9b230e53a39d09a7d6e002">FORGET</a>, <span class="stringliteral">"_FORGET"</span>);
<a name="l00575"></a>00575 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9d77c0f7e14e04b7ecc95a029f669d83">GET_TYPE</a>, <span class="stringliteral">"_GET_TYPE"</span>);
<a name="l00576"></a>00576 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba915f5acbb5f4374dd2c4e9a37a40d2ef">CHECK_TYPE</a>, <span class="stringliteral">"_CHECK_TYPE"</span>);
<a name="l00577"></a>00577 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf87d4fe879a908f02ae07de41fff425e">GET_CHILD</a>, <span class="stringliteral">"_GET_CHILD"</span>);
<a name="l00578"></a>00578 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf910b817eb56e0a5ce680b74a0e8dc84">SUBSTITUTE</a>, <span class="stringliteral">"_SUBSTITUTE"</span>);
<a name="l00579"></a>00579 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9985ac4cb7cda855d785a610e6a866a7">SEQ</a>, <span class="stringliteral">"_SEQ"</span>);
<a name="l00580"></a>00580 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba62e1f4af4ae37d9c8a7f60bf47e4e72c">ARITH_VAR_ORDER</a>, <span class="stringliteral">"_ARITH_VAR_ORDER"</span>);
<a name="l00581"></a>00581 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba6f0302a99e7b65b652008363069ad743">ANNOTATION</a>, <span class="stringliteral">"_ANNOTATION"</span>);
<a name="l00582"></a>00582
<a name="l00583"></a>00583 <span class="comment">// Kinds used mostly in the parser</span>
<a name="l00584"></a>00584
<a name="l00585"></a>00585 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa74ae94cd8d7d555f0ca4c85ef80ad08">TCC</a>, <span class="stringliteral">"_TCC"</span>);
<a name="l00586"></a>00586 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba001479a58fb44c39a29b20d565081a68" title="Identifier is (ID (STRING_EXPR "name"))">ID</a>, <span class="stringliteral">"_ID"</span>);
<a name="l00587"></a>00587 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5ccfef7d76eb43a61d00eb7129ffc562">VARDECL</a>, <span class="stringliteral">"_VARDECL"</span>);
<a name="l00588"></a>00588 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7266e0d07f5aabab9d0515ea50fafc7c">VARDECLS</a>, <span class="stringliteral">"_VARDECLS"</span>);
<a name="l00589"></a>00589
<a name="l00590"></a>00590
<a name="l00591"></a>00591 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba462c38186c36e12c2f38a6d0d43feddf">BOUND_VAR</a>, <span class="stringliteral">"_BOUND_VAR"</span>);
<a name="l00592"></a>00592 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2a1805dc0fcdef2abbf0c780ab1c47ae">BOUND_ID</a>, <span class="stringliteral">"_BOUND_ID"</span>);
<a name="l00593"></a>00593
<a name="l00594"></a>00594 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba73072b2c6fef896d006d6691e932cf37">SKOLEM_VAR</a>, <span class="stringliteral">"_SKOLEM_VAR"</span>);
<a name="l00595"></a>00595 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bada5edea8bbb7cfbd2500be6eca0d4151">THEOREM_KIND</a>, <span class="stringliteral">"_THEOREM_KIND"</span>);
<a name="l00596"></a>00596
<a name="l00597"></a>00597 <span class="comment">// em.newKind(UPDATE, "_UPDATE");</span>
<a name="l00598"></a>00598 <span class="comment">// em.newKind(UPDATE_SELECT, "_UPDATE_SELECT");</span>
<a name="l00599"></a>00599
<a name="l00600"></a>00600 <span class="comment">// em.newKind(RECORD_TYPE, "_RECORD_TYPE");</span>
<a name="l00601"></a>00601 <span class="comment">// em.newKind(RECORD, "_RECORD");</span>
<a name="l00602"></a>00602 <span class="comment">// em.newKind(RECORD_SELECT, "_RECORD_SELECT");</span>
<a name="l00603"></a>00603 <span class="comment">// em.newKind(RECORD_UPDATE, "_RECORD_UPDATE");</span>
<a name="l00604"></a>00604
<a name="l00605"></a>00605 <span class="comment">// em.newKind(TUPLE, "_TUPLE");</span>
<a name="l00606"></a>00606 <span class="comment">// em.newKind(TUPLE_SELECT, "_TUPLE_SELECT");</span>
<a name="l00607"></a>00607 <span class="comment">// em.newKind(TUPLE_UPDATE, "_TUPLE_UPDATE");</span>
<a name="l00608"></a>00608
<a name="l00609"></a>00609 <span class="comment">// em.newKind(SUBRANGE, "_SUBRANGE");</span>
<a name="l00610"></a>00610
<a name="l00611"></a>00611 <span class="comment">// em.newKind(SCALARTYPE, "_SCALARTYPE");</span>
<a name="l00612"></a>00612 <span class="comment">// em.newKind(DATATYPE, "_DATATYPE");</span>
<a name="l00613"></a>00613 <span class="comment">// em.newKind(THISTYPE, "_THISTYPE");</span>
<a name="l00614"></a>00614 <span class="comment">// em.newKind(CONSTRUCTOR, "_CONSTRUCTOR");</span>
<a name="l00615"></a>00615 <span class="comment">// em.newKind(SELECTOR, "_SELECTOR");</span>
<a name="l00616"></a>00616 <span class="comment">// em.newKind(TESTER, "_TESTER");</span>
<a name="l00617"></a>00617 <span class="comment">// em.newKind(DATATYPE_UPDATE, "_DATATYPE_UPDATE");</span>
<a name="l00618"></a>00618
<a name="l00619"></a>00619 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba252802eda493fb6b4a279c4452acb547">IF</a>, <span class="stringliteral">"_IF"</span>);
<a name="l00620"></a>00620 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5bd60ae173f903f6b202daf0c2118387">IFTHEN</a>, <span class="stringliteral">"_IFTHEN"</span>);
<a name="l00621"></a>00621 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba90d649d830ea440c8b8a56c7ef23c426">ELSE</a>, <span class="stringliteral">"_ELSE"</span>);
<a name="l00622"></a>00622 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2f577f27f1d0dcd6aa8f0a144138dc42">COND</a>, <span class="stringliteral">"_COND"</span>);
<a name="l00623"></a>00623
<a name="l00624"></a>00624 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bafb72619a5a922e816967c4aa49301754">LET</a>, <span class="stringliteral">"_LET"</span>);
<a name="l00625"></a>00625 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2cd77861cfba212beedbf4245c990f72">LETDECLS</a>, <span class="stringliteral">"_LETDECLS"</span>);
<a name="l00626"></a>00626 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9508dd8c8e7db280a5dacc19bd74d92d">LETDECL</a>, <span class="stringliteral">"_LETDECL"</span>);
<a name="l00627"></a>00627
<a name="l00628"></a>00628 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba40176493726a127184ca47ea6352dc1f">LAMBDA</a>, <span class="stringliteral">"_LAMBDA"</span>);
<a name="l00629"></a>00629 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa1022ff97dac8e2d5d80d53c4cecd132">SIMULATE</a>, <span class="stringliteral">"_SIMULATE"</span>);
<a name="l00630"></a>00630
<a name="l00631"></a>00631 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3d044162d972156d897cea80f216b9ca">CONST</a>, <span class="stringliteral">"_CONST"</span>);
<a name="l00632"></a>00632 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba197dcccceb8ad4d4bd3b914f73f2978a">VARLIST</a>, <span class="stringliteral">"_VARLIST"</span>);
<a name="l00633"></a>00633 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2efaeb22f8803588598706b73cec8bda">UCONST</a>, <span class="stringliteral">"_UCONST"</span>);
<a name="l00634"></a>00634 em.<a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5a9e497d7471e5d91bd097e5b80a830d">DEFUN</a>, <span class="stringliteral">"_DEFUN"</span>);
<a name="l00635"></a>00635
<a name="l00636"></a>00636 <span class="comment">// Arithmetic types and operators</span>
<a name="l00637"></a>00637 <span class="comment">// em.newKind(REAL, "_REAL");</span>
<a name="l00638"></a>00638 <span class="comment">// em.newKind(INT, "_INT");</span>
<a name="l00639"></a>00639
<a name="l00640"></a>00640 <span class="comment">// em.newKind(UMINUS, "_UMINUS");</span>
<a name="l00641"></a>00641 <span class="comment">// em.newKind(PLUS, "_PLUS");</span>
<a name="l00642"></a>00642 <span class="comment">// em.newKind(MINUS, "_MINUS");</span>
<a name="l00643"></a>00643 <span class="comment">// em.newKind(MULT, "_MULT");</span>
<a name="l00644"></a>00644 <span class="comment">// em.newKind(DIVIDE, "_DIVIDE");</span>
<a name="l00645"></a>00645 <span class="comment">// em.newKind(POW, "_POW");</span>
<a name="l00646"></a>00646 <span class="comment">// em.newKind(INTDIV, "_INTDIV");</span>
<a name="l00647"></a>00647 <span class="comment">// em.newKind(MOD, "_MOD");</span>
<a name="l00648"></a>00648 <span class="comment">// em.newKind(LT, "_LT");</span>
<a name="l00649"></a>00649 <span class="comment">// em.newKind(LE, "_LE");</span>
<a name="l00650"></a>00650 <span class="comment">// em.newKind(GT, "_GT");</span>
<a name="l00651"></a>00651 <span class="comment">// em.newKind(GE, "_GE");</span>
<a name="l00652"></a>00652 <span class="comment">// em.newKind(IS_INTEGER, "_IS_INTEGER");</span>
<a name="l00653"></a>00653 <span class="comment">// em.newKind(NEGINF, "_NEGINF");</span>
<a name="l00654"></a>00654 <span class="comment">// em.newKind(POSINF, "_POSINF");</span>
<a name="l00655"></a>00655 <span class="comment">// em.newKind(FLOOR, "_FLOOR");</span>
<a name="l00656"></a>00656 }
<a name="l00657"></a>00657
<a name="l00658"></a>00658
<a name="l00659"></a><a class="code" href="group__EM__Priv.html#gac681a5cd1f70dda8a7a391439d887c2d">00659</a> <span class="keywordtype">void</span> <a class="code" href="group__EM__Priv.html#gac681a5cd1f70dda8a7a391439d887c2d">ExprManagerNotifyObj::notifyPre</a>() {
<a name="l00660"></a>00660 d_em->postponeGC();
<a name="l00661"></a>00661 }
<a name="l00662"></a>00662
<a name="l00663"></a>00663
<a name="l00664"></a><a class="code" href="group__EM__Priv.html#gadd71c522283037f94526bda8f73a8bbd">00664</a> <span class="keywordtype">void</span> <a class="code" href="group__EM__Priv.html#gadd71c522283037f94526bda8f73a8bbd">ExprManagerNotifyObj::notify</a>() {
<a name="l00665"></a>00665 d_em->resumeGC();
<a name="l00666"></a>00666 }
</pre></div></div>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
