<!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.h 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.h</div> </div>
</div>
<div class="contents">
<a href="expr__manager_8h.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.h</span>
<a name="l00004"></a>00004 <span class="comment"> * \brief Expression manager API</span>
<a name="l00005"></a>00005 <span class="comment"> * </span>
<a name="l00006"></a>00006 <span class="comment"> * Author: Sergey Berezin</span>
<a name="l00007"></a>00007 <span class="comment"> * </span>
<a name="l00008"></a>00008 <span class="comment"> * Created: Wed Dec 4 14:20:56 2002</span>
<a name="l00009"></a>00009 <span class="comment"> *</span>
<a name="l00010"></a>00010 <span class="comment"> * <hr></span>
<a name="l00011"></a>00011 <span class="comment"> *</span>
<a name="l00012"></a>00012 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00013"></a>00013 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00014"></a>00014 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00015"></a>00015 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00016"></a>00016 <span class="comment"> * </span>
<a name="l00017"></a>00017 <span class="comment"> * <hr></span>
<a name="l00018"></a>00018 <span class="comment"> * </span>
<a name="l00019"></a>00019 <span class="comment"> */</span>
<a name="l00020"></a>00020 <span class="comment">/*****************************************************************************/</span>
<a name="l00021"></a>00021
<a name="l00022"></a>00022 <span class="comment">// Must be before #ifndef, since expr.h also includes this file (see</span>
<a name="l00023"></a>00023 <span class="comment">// comments in expr_value.h)</span>
<a name="l00024"></a>00024 <span class="preprocessor">#ifndef _cvc3__expr_h_</span>
<a name="l00025"></a>00025 <span class="preprocessor"></span><span class="preprocessor">#include "<a class="code" href="expr_8h.html" title="Definition of the API to expression package. See class Expr for details.">expr.h</a>"</span>
<a name="l00026"></a>00026 <span class="preprocessor">#endif</span>
<a name="l00027"></a>00027 <span class="preprocessor"></span>
<a name="l00028"></a>00028 <span class="preprocessor">#ifndef _cvc3__include__expr_manager_h_</span>
<a name="l00029"></a>00029 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__expr_manager_h_</span>
<a name="l00030"></a>00030 <span class="preprocessor"></span>
<a name="l00031"></a>00031 <span class="preprocessor">#include "<a class="code" href="os_8h.html" title="Abstraction over different operating systems.">os.h</a>"</span>
<a name="l00032"></a>00032 <span class="preprocessor">#include "<a class="code" href="expr__map_8h.html">expr_map.h</a>"</span>
<a name="l00033"></a>00033 <span class="preprocessor">#include <deque></span>
<a name="l00034"></a>00034
<a name="l00035"></a>00035 <span class="keyword">namespace </span>CVC3 {
<a name="l00036"></a>00036 <span class="comment">// Command line flags</span>
<a name="l00037"></a>00037 <span class="keyword">class </span>CLFlags;
<a name="l00038"></a>00038 <span class="keyword">class </span>PrettyPrinter;
<a name="l00039"></a>00039 <span class="keyword">class </span>MemoryManager;
<a name="l00040"></a>00040 <span class="keyword">class </span>ExprManagerNotifyObj;
<a name="l00041"></a>00041 <span class="keyword">class </span>TheoremManager;
<a name="l00042"></a>00042 <span class="comment"></span>
<a name="l00043"></a>00043 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00044"></a>00044 <span class="comment">//! Expression Manager</span>
<a name="l00045"></a>00045 <span class="comment"></span><span class="comment">/*!</span>
<a name="l00046"></a>00046 <span class="comment"> Class: ExprManager</span>
<a name="l00047"></a>00047 <span class="comment"> </span>
<a name="l00048"></a>00048 <span class="comment"> Author: Sergey Berezin</span>
<a name="l00049"></a>00049 <span class="comment"> </span>
<a name="l00050"></a>00050 <span class="comment"> Created: Wed Dec 4 14:26:35 2002</span>
<a name="l00051"></a>00051 <span class="comment"></span>
<a name="l00052"></a>00052 <span class="comment"> Description: Global state of the Expr package for a particular</span>
<a name="l00053"></a>00053 <span class="comment"> instance of CVC3. Each instance of the CVC3 library has</span>
<a name="l00054"></a>00054 <span class="comment"> its own expression manager, for thread-safety.</span>
<a name="l00055"></a>00055 <span class="comment">*/</span><span class="comment"></span>
<a name="l00056"></a>00056 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00057"></a>00057 <span class="comment"></span>
<a name="l00058"></a><a class="code" href="classCVC3_1_1ExprManager.html">00058</a> <span class="keyword">class </span><a class="code" href="os_8h.html#a0035aac6379df39aa69feba98b2751ba">CVC_DLL</a> <a class="code" href="classCVC3_1_1ExprManager.html">ExprManager</a> {
<a name="l00059"></a><a class="code" href="classCVC3_1_1ExprManager.html#aa33520359f6cc0f51b476790d39ed869">00059</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>;
<a name="l00060"></a><a class="code" href="classCVC3_1_1ExprManager.html#a6b4e0ce748563841be8fe35c34ee7975">00060</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>;
<a name="l00061"></a><a class="code" href="classCVC3_1_1ExprManager.html#a2c31e8a3c11caeb061d69db14ebb0e95">00061</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Op.html">Op</a>; <span class="comment">// It wants to call rebuildExpr</span>
<a name="l00062"></a><a class="code" href="classCVC3_1_1ExprManager.html#a5027bd09c010f0a1fdc060a3064b1c7c">00062</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprManager_1_1HashEV.html" title="Private class for d_exprSet.">HashEV</a>; <span class="comment">// Our own private class</span>
<a name="l00063"></a><a class="code" href="classCVC3_1_1ExprManager.html#a18dba29b4f3e91d6d2bc53472a6bb7cc">00063</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>;
<a name="l00064"></a>00064
<a name="l00065"></a><a class="code" href="classCVC3_1_1ExprManager.html#ab4503774f636c29f72d680289f2783dc">00065</a> <a class="code" href="classCVC3_1_1ContextManager.html" title="Manager for multiple contexts. Also holds current context.">ContextManager</a>* <a class="code" href="classCVC3_1_1ExprManager.html#ab4503774f636c29f72d680289f2783dc" title="For backtracking attributes.">d_cm</a>; <span class="comment">//!< For backtracking attributes</span>
<a name="l00066"></a><a class="code" href="classCVC3_1_1ExprManager.html#a144ee6ab8333d5a1c79b304abe296e89">00066</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>* <a class="code" href="classCVC3_1_1ExprManager.html#a144ee6ab8333d5a1c79b304abe296e89" title="Needed for Refl Theorems.">d_tm</a>; <span class="comment">//!< Needed for Refl Theorems</span>
<a name="l00067"></a><a class="code" href="classCVC3_1_1ExprManager.html#abf2f3e04c70fc71ba01170007e3a0831">00067</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ExprManagerNotifyObj.html" title="Notifies ExprManager before and after each pop()">ExprManagerNotifyObj</a>* <a class="code" href="classCVC3_1_1ExprManager.html#abf2f3e04c70fc71ba01170007e3a0831" title="Notification on pop()">d_notifyObj</a>; <span class="comment">//!< Notification on pop()</span>
<a name="l00068"></a><a class="code" href="classCVC3_1_1ExprManager.html#abc472a0164e86abb54806342ce2020fd">00068</a> <span class="comment"></span> <a class="code" href="namespaceCVC3.html#a4233916514848331ee104548acbab912" title="Expression index type.">ExprIndex</a> <a class="code" href="classCVC3_1_1ExprManager.html#abc472a0164e86abb54806342ce2020fd" title="Index counter for Expr compare()">d_index</a>; <span class="comment">//!< Index counter for Expr compare()</span>
<a name="l00069"></a><a class="code" href="classCVC3_1_1ExprManager.html#a0e8b6ba08f3b0cdf44457240da091100">00069</a> <span class="comment"></span> <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1ExprManager.html#a0e8b6ba08f3b0cdf44457240da091100" title="Counter for a generic Expr flag.">d_flagCounter</a>; <span class="comment">//!< Counter for a generic Expr flag</span>
<a name="l00070"></a>00070 <span class="comment"></span><span class="comment"></span>
<a name="l00071"></a>00071 <span class="comment"> //! The database of registered kinds</span>
<a name="l00072"></a><a class="code" href="classCVC3_1_1ExprManager.html#a07ec9cfbc5aa8fbc09b7844a4a7ad34e">00072</a> <span class="comment"></span> <a class="code" href="classHash_1_1hash__map.html">std::hash_map<int, std::string></a> <a class="code" href="classCVC3_1_1ExprManager.html#a07ec9cfbc5aa8fbc09b7844a4a7ad34e" title="The database of registered kinds.">d_kindMap</a>;<span class="comment"></span>
<a name="l00073"></a>00073 <span class="comment"> //! The set of kinds representing a type</span>
<a name="l00074"></a><a class="code" href="classCVC3_1_1ExprManager.html#a77f4cd27ea691329a3c01285c116eebd">00074</a> <span class="comment"></span> <a class="code" href="classHash_1_1hash__set.html">std::hash_set<int></a> <a class="code" href="classCVC3_1_1ExprManager.html#a77f4cd27ea691329a3c01285c116eebd" title="The set of kinds representing a type.">d_typeKinds</a>;<span class="comment"></span>
<a name="l00075"></a>00075 <span class="comment"> //! Private class for hashing strings</span>
<a name="l00076"></a><a class="code" href="classCVC3_1_1ExprManager_1_1HashString.html">00076</a> <span class="comment"></span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprManager_1_1HashString.html" title="Private class for hashing strings.">HashString</a> {
<a name="l00077"></a><a class="code" href="classCVC3_1_1ExprManager_1_1HashString.html#a727d1263f81f01e526042f38ec668caa">00077</a> <a class="code" href="structHash_1_1hash_3_01char_01_5_01_4.html">std::hash<char*></a> <a class="code" href="classCVC3_1_1ExprManager_1_1HashString.html#a727d1263f81f01e526042f38ec668caa">h</a>;
<a name="l00078"></a>00078 <span class="keyword">public</span>:
<a name="l00079"></a><a class="code" href="group__EM__Priv.html#ga9fe970ca9a02174a617bce9797d41815">00079</a> <span class="keywordtype">size_t</span> <a class="code" href="group__EM__Priv.html#ga9fe970ca9a02174a617bce9797d41815">operator()</a>(<span class="keyword">const</span> std::string& s)<span class="keyword"> const </span>{
<a name="l00080"></a>00080 <span class="keywordflow">return</span> h(const_cast<char*>(s.c_str()));
<a name="l00081"></a>00081 }
<a name="l00082"></a>00082 };<span class="comment"></span>
<a name="l00083"></a>00083 <span class="comment"> //! The reverse map of names to kinds</span>
<a name="l00084"></a><a class="code" href="classCVC3_1_1ExprManager.html#aeab702ffe6838b75b285df2d1cd0f8fb">00084</a> <span class="comment"></span> <a class="code" href="classHash_1_1hash__map.html">std::hash_map<std::string, int, HashString></a> <a class="code" href="classCVC3_1_1ExprManager.html#aeab702ffe6838b75b285df2d1cd0f8fb" title="The reverse map of names to kinds.">d_kindMapByName</a>;<span class="comment"></span>
<a name="l00085"></a>00085 <span class="comment"> /*! @brief The registered pretty-printer, a connector to</span>
<a name="l00086"></a>00086 <span class="comment"> theory-specific pretty-printers */</span>
<a name="l00087"></a><a class="code" href="classCVC3_1_1ExprManager.html#a12e3e4bb896c10134908607b528512de">00087</a> <a class="code" href="classCVC3_1_1PrettyPrinter.html" title="Abstract API to a pretty-printer for Expr.">PrettyPrinter</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>;
<a name="l00088"></a>00088
<a name="l00089"></a>00089 <span class="keywordtype">size_t</span> <a class="code" href="structHash_1_1hash.html">hash</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* ev) <span class="keyword">const</span>;
<a name="l00090"></a>00090
<a name="l00091"></a>00091 <span class="comment">// Printing and other options </span>
<a name="l00092"></a>00092 <span class="comment"></span>
<a name="l00093"></a>00093 <span class="comment"> /*! @brief Print upto the given depth, replace the rest with</span>
<a name="l00094"></a>00094 <span class="comment"> "...". -1==unlimited depth. */</span>
<a name="l00095"></a><a class="code" href="classCVC3_1_1ExprManager.html#ac51aa6e1a689046daae9591ffdf7a6fe">00095</a> <span class="keyword">const</span> <span class="keywordtype">int</span>* <a class="code" href="classCVC3_1_1ExprManager.html#ac51aa6e1a689046daae9591ffdf7a6fe" title="Print upto the given depth, replace the rest with "...". -1==unlimited depth.">d_printDepth</a>;<span class="comment"></span>
<a name="l00096"></a>00096 <span class="comment"> //! Whether to print with indentation</span>
<a name="l00097"></a><a class="code" href="classCVC3_1_1ExprManager.html#ad6daa0d62357b8c7b8e17e9cbe627936">00097</a> <span class="comment"></span> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1ExprManager.html#ad6daa0d62357b8c7b8e17e9cbe627936" title="Whether to print with indentation.">d_withIndentation</a>;<span class="comment"></span>
<a name="l00098"></a>00098 <span class="comment"> //! Permanent indentation</span>
<a name="l00099"></a><a class="code" href="classCVC3_1_1ExprManager.html#a74ef690ec61d40be41b784246ecd32c4">00099</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1ExprManager.html#a74ef690ec61d40be41b784246ecd32c4" title="Permanent indentation.">d_indent</a>;<span class="comment"></span>
<a name="l00100"></a>00100 <span class="comment"> //! Transient indentation</span>
<a name="l00101"></a>00101 <span class="comment"></span><span class="comment"> /*! Normally is the same as d_indent, but may temporarily be</span>
<a name="l00102"></a>00102 <span class="comment"> different for printing one single Expr */</span>
<a name="l00103"></a><a class="code" href="classCVC3_1_1ExprManager.html#a84f7afd3443e0b6998db69cea8340b38">00103</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1ExprManager.html#a84f7afd3443e0b6998db69cea8340b38" title="Transient indentation.">d_indentTransient</a>;<span class="comment"></span>
<a name="l00104"></a>00104 <span class="comment"> //! Suggested line width for printing with indentation</span>
<a name="l00105"></a><a class="code" href="classCVC3_1_1ExprManager.html#acc7d0bb165528fd61ae7a1015cd28dfe">00105</a> <span class="comment"></span> <span class="keyword">const</span> <span class="keywordtype">int</span>* <a class="code" href="classCVC3_1_1ExprManager.html#acc7d0bb165528fd61ae7a1015cd28dfe" title="Suggested line width for printing with indentation.">d_lineWidth</a>;<span class="comment"></span>
<a name="l00106"></a>00106 <span class="comment"> //! Input language (printing)</span>
<a name="l00107"></a><a class="code" href="classCVC3_1_1ExprManager.html#ac323f030431b1f87c9201117486f2fd6">00107</a> <span class="comment"></span> <span class="keyword">const</span> std::string* <a class="code" href="classCVC3_1_1ExprManager.html#ac323f030431b1f87c9201117486f2fd6" title="Input language (printing)">d_inputLang</a>;<span class="comment"></span>
<a name="l00108"></a>00108 <span class="comment"> //! Output language (printing)</span>
<a name="l00109"></a><a class="code" href="classCVC3_1_1ExprManager.html#ac2d8f75464d06456fa0b2111df849d70">00109</a> <span class="comment"></span> <span class="keyword">const</span> std::string* <a class="code" href="classCVC3_1_1ExprManager.html#ac2d8f75464d06456fa0b2111df849d70" title="Output language (printing)">d_outputLang</a>;<span class="comment"></span>
<a name="l00110"></a>00110 <span class="comment"> //! Whether to print Expr's as DAGs</span>
<a name="l00111"></a><a class="code" href="classCVC3_1_1ExprManager.html#a002213c66d24e953c75d7f1238849c87">00111</a> <span class="comment"></span> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1ExprManager.html#a002213c66d24e953c75d7f1238849c87" title="Whether to print Expr's as DAGs.">d_dagPrinting</a>;<span class="comment"></span>
<a name="l00112"></a>00112 <span class="comment"> //! Which memory manager to use (copy the flag value and keep it the same)</span>
<a name="l00113"></a><a class="code" href="classCVC3_1_1ExprManager.html#a5cfe801f6ae8f9fd7a51477a219685e8">00113</a> <span class="comment"></span> <span class="keyword">const</span> std::string <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="l00114"></a>00114 <span class="comment"></span>
<a name="l00115"></a>00115 <span class="comment"> //! Private class for d_exprSet</span>
<a name="l00116"></a><a class="code" href="classCVC3_1_1ExprManager_1_1HashEV.html">00116</a> <span class="comment"></span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprManager_1_1HashEV.html" title="Private class for d_exprSet.">HashEV</a> {
<a name="l00117"></a><a class="code" href="classCVC3_1_1ExprManager_1_1HashEV.html#aa8b0387e58616954916858e296de4449">00117</a> <a class="code" href="classCVC3_1_1ExprManager.html">ExprManager</a>* <a class="code" href="classCVC3_1_1ExprManager_1_1HashEV.html#aa8b0387e58616954916858e296de4449">d_em</a>;
<a name="l00118"></a>00118 <span class="keyword">public</span>:
<a name="l00119"></a><a class="code" href="group__EM__Priv.html#gaabb82d3abf0072c71761ca599ba9a8fa">00119</a> <a class="code" href="group__EM__Priv.html#gaabb82d3abf0072c71761ca599ba9a8fa">HashEV</a>(<a class="code" href="classCVC3_1_1ExprManager.html">ExprManager</a>* em): d_em(em) { }
<a name="l00120"></a><a class="code" href="group__EM__Priv.html#gac8adf717113c11ce0bc84160d17bea7a">00120</a> <span class="keywordtype">size_t</span> <a class="code" href="group__EM__Priv.html#gac8adf717113c11ce0bc84160d17bea7a">operator()</a>(<a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* ev)<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_em->hash(ev); }
<a name="l00121"></a>00121 };<span class="comment"></span>
<a name="l00122"></a>00122 <span class="comment"> //! Private class for d_exprSet</span>
<a name="l00123"></a><a class="code" href="classCVC3_1_1ExprManager_1_1EqEV.html">00123</a> <span class="comment"></span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprManager_1_1EqEV.html" title="Private class for d_exprSet.">EqEV</a> {
<a name="l00124"></a>00124 <span class="keyword">public</span>:
<a name="l00125"></a>00125 <span class="keywordtype">bool</span> operator()(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* ev1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* ev2) <span class="keyword">const</span>;
<a name="l00126"></a>00126 };
<a name="l00127"></a>00127 <span class="comment"></span>
<a name="l00128"></a>00128 <span class="comment"> //! Hash set type for uniquifying expressions</span>
<a name="l00129"></a><a class="code" href="classCVC3_1_1ExprManager.html#ac77431b2fe56b930edd5961b1f6eb14d">00129</a> <span class="comment"></span> <span class="keyword">typedef</span> <a class="code" href="classHash_1_1hash__set.html">std::hash_set<ExprValue*, HashEV, EqEV></a> <a class="code" href="classCVC3_1_1ExprManager.html#ac77431b2fe56b930edd5961b1f6eb14d" title="Hash set type for uniquifying expressions.">ExprValueSet</a>;<span class="comment"></span>
<a name="l00130"></a>00130 <span class="comment"> //! Hash set for uniquifying expressions</span>
<a name="l00131"></a><a class="code" href="classCVC3_1_1ExprManager.html#a007da346931bbc8d2dafafaa81c4ea9c">00131</a> <span class="comment"></span> <a class="code" href="classHash_1_1hash__set.html">ExprValueSet</a> <a class="code" href="classCVC3_1_1ExprManager.html#a007da346931bbc8d2dafafaa81c4ea9c" title="Hash set for uniquifying expressions.">d_exprSet</a>;<span class="comment"></span>
<a name="l00132"></a>00132 <span class="comment"> //! Array of memory managers for subclasses of ExprValue</span>
<a name="l00133"></a><a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d">00133</a> <span class="comment"></span> std::vector<MemoryManager*> <a class="code" href="classCVC3_1_1ExprManager.html#aa5eefdcd1d9d304dec3553908c76f10d" title="Array of memory managers for subclasses of ExprValue.">d_mm</a>;
<a name="l00134"></a>00134 <span class="comment"></span>
<a name="l00135"></a>00135 <span class="comment"> //! A hash function for hashing pointers</span>
<a name="l00136"></a><a class="code" href="classCVC3_1_1ExprManager.html#a5ab1d84efde75b4ed4d5c1f4b47c2601">00136</a> <span class="comment"></span> <a class="code" href="structHash_1_1hash.html">std::hash<void*></a> <a class="code" href="classCVC3_1_1ExprManager.html#a5ab1d84efde75b4ed4d5c1f4b47c2601" title="A hash function for hashing pointers.">d_pointerHash</a>;
<a name="l00137"></a>00137 <span class="comment"></span>
<a name="l00138"></a>00138 <span class="comment"> //! Expr constants cached for fast access</span>
<a name="l00139"></a><a class="code" href="classCVC3_1_1ExprManager.html#a8f6f7143ab2a62f58ed86d296fa23be4">00139</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1ExprManager.html#a8f6f7143ab2a62f58ed86d296fa23be4" title="Expr constants cached for fast access.">d_bool</a>;
<a name="l00140"></a><a class="code" href="classCVC3_1_1ExprManager.html#a4b0a44de15c4b3de63233d824a2058bd">00140</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1ExprManager.html#a4b0a44de15c4b3de63233d824a2058bd">d_false</a>;
<a name="l00141"></a><a class="code" href="classCVC3_1_1ExprManager.html#a6c341a4de2d1e1189e9a1a67430a508c">00141</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1ExprManager.html#a6c341a4de2d1e1189e9a1a67430a508c">d_true</a>;<span class="comment"></span>
<a name="l00142"></a>00142 <span class="comment"> //! Empty vector of Expr to return by reference as empty vector of children</span>
<a name="l00143"></a><a class="code" href="classCVC3_1_1ExprManager.html#a20b3e13cca9564afd32e3df2537bdb24">00143</a> <span class="comment"></span> std::vector<Expr> <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>;<span class="comment"></span>
<a name="l00144"></a>00144 <span class="comment"> //! Null Expr to return by reference, for efficiency</span>
<a name="l00145"></a><a class="code" href="classCVC3_1_1ExprManager.html#afd9f8cac32e3acbbf7bbb18506cb2350">00145</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1ExprManager.html#afd9f8cac32e3acbbf7bbb18506cb2350" title="Null Expr to return by reference, for efficiency.">d_nullExpr</a>;
<a name="l00146"></a>00146
<a name="l00147"></a>00147 <span class="keywordtype">void</span> installExprValue(<a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* ev);
<a name="l00148"></a>00148 <span class="comment"></span>
<a name="l00149"></a>00149 <span class="comment"> //! Current value of the simplifier cache tag</span>
<a name="l00150"></a>00150 <span class="comment"></span><span class="comment"> /*! The cached values of calls to Simplify are valid as long as</span>
<a name="l00151"></a>00151 <span class="comment"> their cache tag matches this tag. Caches can then be</span>
<a name="l00152"></a>00152 <span class="comment"> invalidated by incrementing this tag. */</span>
<a name="l00153"></a><a class="code" href="classCVC3_1_1ExprManager.html#a8770381a9e54320b15897ad4757d6c5e">00153</a> <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1ExprManager.html#a8770381a9e54320b15897ad4757d6c5e" title="Current value of the simplifier cache tag.">d_simpCacheTagCurrent</a>;
<a name="l00154"></a>00154 <span class="comment"></span>
<a name="l00155"></a>00155 <span class="comment"> //! Disable garbage collection</span>
<a name="l00156"></a>00156 <span class="comment"></span><span class="comment"> /*! This flag disables the garbage collection. Normally, it's set</span>
<a name="l00157"></a>00157 <span class="comment"> in the destructor, so that we can delete all remaining</span>
<a name="l00158"></a>00158 <span class="comment"> expressions without GC getting in the way. */</span>
<a name="l00159"></a><a class="code" href="classCVC3_1_1ExprManager.html#a9c4e054fd961a0910bbf03b8bbccb04a">00159</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprManager.html#a9c4e054fd961a0910bbf03b8bbccb04a" title="Disable garbage collection.">d_disableGC</a>;<span class="comment"></span>
<a name="l00160"></a>00160 <span class="comment"> //! Postpone deleting garbage-collected expressions.</span>
<a name="l00161"></a>00161 <span class="comment"></span><span class="comment"> /*! Useful during manipulation of context, especially at the time</span>
<a name="l00162"></a>00162 <span class="comment"> * of backtracking, since we may have objects with circular</span>
<a name="l00163"></a>00163 <span class="comment"> * dependencies (like find pointers).</span>
<a name="l00164"></a>00164 <span class="comment"> *</span>
<a name="l00165"></a>00165 <span class="comment"> * The postponed expressions will be deleted the next time the</span>
<a name="l00166"></a>00166 <span class="comment"> * garbage collector is called after this flag is cleared.</span>
<a name="l00167"></a>00167 <span class="comment"> */</span>
<a name="l00168"></a><a class="code" href="classCVC3_1_1ExprManager.html#a7ee8efeb3b86e7b044290ad543792db2">00168</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprManager.html#a7ee8efeb3b86e7b044290ad543792db2" title="Postpone deleting garbage-collected expressions.">d_postponeGC</a>;<span class="comment"></span>
<a name="l00169"></a>00169 <span class="comment"> //! Vector of postponed garbage-collected expressions</span>
<a name="l00170"></a><a class="code" href="classCVC3_1_1ExprManager.html#a679888b2e2e5cb92645ec6bd0701f7ec">00170</a> <span class="comment"></span> std::vector<ExprValue*> <a class="code" href="classCVC3_1_1ExprManager.html#a679888b2e2e5cb92645ec6bd0701f7ec" title="Vector of postponed garbage-collected expressions.">d_postponed</a>;
<a name="l00171"></a>00171 <span class="comment"></span>
<a name="l00172"></a>00172 <span class="comment"> //! Flag for whether GC is already running</span>
<a name="l00173"></a><a class="code" href="classCVC3_1_1ExprManager.html#a6ae99a5eb75cee11d7f638c1ea17a201">00173</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1ExprManager.html#a6ae99a5eb75cee11d7f638c1ea17a201" title="Flag for whether GC is already running.">d_inGC</a>;<span class="comment"></span>
<a name="l00174"></a>00174 <span class="comment"> //! Queue of pending exprs to GC</span>
<a name="l00175"></a><a class="code" href="classCVC3_1_1ExprManager.html#a99533eeb3df944329cf62d97c86fc43c">00175</a> <span class="comment"></span> std::deque<ExprValue*> <a class="code" href="classCVC3_1_1ExprManager.html#a99533eeb3df944329cf62d97c86fc43c" title="Queue of pending exprs to GC.">d_pending</a>;
<a name="l00176"></a>00176 <span class="comment"></span>
<a name="l00177"></a>00177 <span class="comment"> //! Rebuild cache</span>
<a name="l00178"></a><a class="code" href="classCVC3_1_1ExprManager.html#a841b8a48adc1372b7d99e3f93dd9620a">00178</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr></a> <a class="code" href="classCVC3_1_1ExprManager.html#a841b8a48adc1372b7d99e3f93dd9620a" title="Rebuild cache.">d_rebuildCache</a>;
<a name="l00179"></a>00179 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<span class="keywordtype">bool</span> d_inRebuild;)
<a name="l00180"></a>00180
<a name="l00181"></a>00181 <span class="keyword">public</span>:<span class="comment"></span>
<a name="l00182"></a>00182 <span class="comment"> //! Abstract class for computing expr type</span>
<a name="l00183"></a><a class="code" href="classCVC3_1_1ExprManager_1_1TypeComputer.html">00183</a> <span class="comment"></span> <span class="keyword">class</span> <a class="code" href="classCVC3_1_1ExprManager_1_1TypeComputer.html" title="Abstract class for computing expr type.">TypeComputer</a> {
<a name="l00184"></a>00184 <span class="keyword">public</span>:
<a name="l00185"></a><a class="code" href="classCVC3_1_1ExprManager_1_1TypeComputer.html#af4397d9b6d23d0e4b9112b509d9dfad4">00185</a> <a class="code" href="classCVC3_1_1ExprManager_1_1TypeComputer.html#af4397d9b6d23d0e4b9112b509d9dfad4">TypeComputer</a>() {}
<a name="l00186"></a><a class="code" href="group__EM__Priv.html#gaee11e07336c1b8704409d42c0aaeafad">00186</a> <span class="keyword">virtual</span> <a class="code" href="group__EM__Priv.html#gaee11e07336c1b8704409d42c0aaeafad">~TypeComputer</a>() {}<span class="comment"></span>
<a name="l00187"></a>00187 <span class="comment"> //! Compute the type of e</span>
<a name="l00188"></a>00188 <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">void</span> computeType(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;<span class="comment"></span>
<a name="l00189"></a>00189 <span class="comment"> //! Check that e is a valid Type expr</span>
<a name="l00190"></a>00190 <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">void</span> checkType(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) = 0;<span class="comment"></span>
<a name="l00191"></a>00191 <span class="comment"> //! Get information related to finiteness of a type</span>
<a name="l00192"></a>00192 <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54" title="Enum for cardinality of types.">Cardinality</a> finiteTypeInfo(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a>& n,
<a name="l00193"></a>00193 <span class="keywordtype">bool</span> enumerate, <span class="keywordtype">bool</span> computeSize) = 0;
<a name="l00194"></a>00194 };
<a name="l00195"></a>00195 <span class="keyword">private</span>:<span class="comment"></span>
<a name="l00196"></a>00196 <span class="comment"> //! Instance of TypeComputer: must be registered</span>
<a name="l00197"></a><a class="code" href="classCVC3_1_1ExprManager.html#a3b4356ae8ebb7c1fc561188920ae7d03">00197</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ExprManager_1_1TypeComputer.html" title="Abstract class for computing expr type.">TypeComputer</a>* <a class="code" href="classCVC3_1_1ExprManager.html#a3b4356ae8ebb7c1fc561188920ae7d03" title="Instance of TypeComputer: must be registered.">d_typeComputer</a>;
<a name="l00198"></a>00198 <span class="comment"></span>
<a name="l00199"></a>00199 <span class="comment"> /////////////////////////////////////////////////////////////////////////</span>
<a name="l00200"></a>00200 <span class="comment"></span><span class="comment"> /*! \defgroup EM_Priv Private methods</span>
<a name="l00201"></a>00201 <span class="comment"> * \ingroup ExprPkg</span>
<a name="l00202"></a>00202 <span class="comment"> * @{</span>
<a name="l00203"></a>00203 <span class="comment"> */</span><span class="comment"></span>
<a name="l00204"></a>00204 <span class="comment"> /////////////////////////////////////////////////////////////////////////</span>
<a name="l00205"></a>00205 <span class="comment"></span><span class="comment"></span>
<a name="l00206"></a>00206 <span class="comment"> //! Cached recursive descent. Must be called only during rebuild()</span>
<a name="l00207"></a>00207 <span class="comment"></span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> rebuildRec(<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="l00208"></a>00208 <span class="comment"></span>
<a name="l00209"></a>00209 <span class="comment"> //! Return either an existing or a new ExprValue matching ev</span>
<a name="l00210"></a>00210 <span class="comment"></span> <a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* newExprValue(<a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* ev);
<a name="l00211"></a>00211 <span class="comment"></span>
<a name="l00212"></a>00212 <span class="comment"> //! Return the current Expr flag counter</span>
<a name="l00213"></a><a class="code" href="group__EM__Priv.html#gacaa71017958e2e9d069c055248c8dd78">00213</a> <span class="comment"></span> <span class="keywordtype">unsigned</span> <a class="code" href="group__EM__Priv.html#gacaa71017958e2e9d069c055248c8dd78" title="Return the current Expr flag counter.">getFlag</a>() { <span class="keywordflow">return</span> d_flagCounter; }<span class="comment"></span>
<a name="l00214"></a>00214 <span class="comment"> //! Increment and return the Expr flag counter (this clears all the flags)</span>
<a name="l00215"></a><a class="code" href="group__EM__Priv.html#gab5336831e8006e69a57f9c1b728138f6">00215</a> <span class="comment"></span> <span class="keywordtype">unsigned</span> nextFlag()
<a name="l00216"></a>00216 { <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>(++d_flagCounter, <span class="stringliteral">"flag overflow"</span>); <span class="keywordflow">return</span> d_flagCounter; }
<a name="l00217"></a>00217 <span class="comment"></span>
<a name="l00218"></a>00218 <span class="comment"> //! Compute the type of the Expr</span>
<a name="l00219"></a>00219 <span class="comment"></span> <span class="keywordtype">void</span> computeType(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span>
<a name="l00220"></a>00220 <span class="comment"> //! Check well-formedness of a type Expr</span>
<a name="l00221"></a>00221 <span class="comment"></span> <span class="keywordtype">void</span> checkType(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span>
<a name="l00222"></a>00222 <span class="comment"> //! Get information related to finiteness of a type</span>
<a name="l00223"></a>00223 <span class="comment"></span> <span class="comment">// 1. Returns Cardinality of the type (finite, infinite, or unknown)</span>
<a name="l00224"></a>00224 <span class="comment">// 2. If cardinality = finite and enumerate is true,</span>
<a name="l00225"></a>00225 <span class="comment">// sets e to the nth element of the type if it can</span>
<a name="l00226"></a>00226 <span class="comment">// sets e to NULL if n is out of bounds or if unable to compute nth element</span>
<a name="l00227"></a>00227 <span class="comment">// 3. If cardinality = finite and computeSize is true,</span>
<a name="l00228"></a>00228 <span class="comment">// sets n to the size of the type if it can</span>
<a name="l00229"></a>00229 <span class="comment">// sets n to 0 otherwise</span>
<a name="l00230"></a>00230 <a class="code" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54" title="Enum for cardinality of types.">Cardinality</a> finiteTypeInfo(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a>& n,
<a name="l00231"></a>00231 <span class="keywordtype">bool</span> enumerate, <span class="keywordtype">bool</span> computeSize);
<a name="l00232"></a>00232
<a name="l00233"></a>00233 <span class="keyword">public</span>:<span class="comment"></span>
<a name="l00234"></a>00234 <span class="comment"> //! Constructor</span>
<a name="l00235"></a>00235 <span class="comment"></span> <a class="code" href="classCVC3_1_1ExprManager.html">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);<span class="comment"></span>
<a name="l00236"></a>00236 <span class="comment"> //! Destructor</span>
<a name="l00237"></a>00237 <span class="comment"></span> ~<a class="code" href="classCVC3_1_1ExprManager.html">ExprManager</a>();<span class="comment"></span>
<a name="l00238"></a>00238 <span class="comment"> //! Free up all memory and delete all the expressions.</span>
<a name="l00239"></a>00239 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00240"></a>00240 <span class="comment"> * No more expressions can be created after this point, only</span>
<a name="l00241"></a>00241 <span class="comment"> * destructors ~Expr() can be called.</span>
<a name="l00242"></a>00242 <span class="comment"> *</span>
<a name="l00243"></a>00243 <span class="comment"> * This method is needed to dis-entangle the mutual dependency of</span>
<a name="l00244"></a>00244 <span class="comment"> * ExprManager and ContextManager, when destructors of ExprValue</span>
<a name="l00245"></a>00245 <span class="comment"> * (sub)classes need to delete backtracking objects, and deleting</span>
<a name="l00246"></a>00246 <span class="comment"> * the ContextManager requires destruction of some remaining Exprs.</span>
<a name="l00247"></a>00247 <span class="comment"> */</span>
<a name="l00248"></a>00248 <span class="keywordtype">void</span> clear();<span class="comment"></span>
<a name="l00249"></a>00249 <span class="comment"> //! Check if the ExprManager is still active (clear() was not called)</span>
<a name="l00250"></a>00250 <span class="comment"></span> <span class="keywordtype">bool</span> isActive();
<a name="l00251"></a>00251 <span class="comment"></span>
<a name="l00252"></a>00252 <span class="comment"> //! Garbage collect the ExprValue pointer </span>
<a name="l00253"></a>00253 <span class="comment"></span><span class="comment"> /*! \ingroup EM_Priv */</span>
<a name="l00254"></a>00254 <span class="keywordtype">void</span> gc(<a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* ev);<span class="comment"></span>
<a name="l00255"></a>00255 <span class="comment"> //! Postpone deletion of garbage-collected expressions.</span>
<a name="l00256"></a>00256 <span class="comment"></span><span class="comment"> /*! \sa resumeGC() */</span>
<a name="l00257"></a><a class="code" href="group__EM__Priv.html#ga9c35426ab6885b609e84a4be9b30effc">00257</a> <span class="keywordtype">void</span> <a class="code" href="group__EM__Priv.html#ga9c35426ab6885b609e84a4be9b30effc" title="Postpone deletion of garbage-collected expressions.">postponeGC</a>() { d_postponeGC = <span class="keyword">true</span>; }<span class="comment"></span>
<a name="l00258"></a>00258 <span class="comment"> //! Resume deletion of garbage-collected expressions.</span>
<a name="l00259"></a>00259 <span class="comment"></span><span class="comment"> /*! \sa postponeGC() */</span>
<a name="l00260"></a>00260 <span class="keywordtype">void</span> resumeGC();
<a name="l00261"></a>00261 <span class="comment"></span>
<a name="l00262"></a>00262 <span class="comment"> /*! @brief Rebuild the Expr with this ExprManager if it belongs to</span>
<a name="l00263"></a>00263 <span class="comment"> another ExprManager */</span>
<a name="l00264"></a>00264 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> rebuild(<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="l00265"></a>00265 <span class="comment"></span>
<a name="l00266"></a>00266 <span class="comment"> //! Return the next Expr index</span>
<a name="l00267"></a>00267 <span class="comment"></span><span class="comment"> /*! It should be used only by ExprValue() constructor */</span>
<a name="l00268"></a><a class="code" href="group__EM__Priv.html#ga212f07de6befabee47e4f9a1813e7c44">00268</a> <a class="code" href="namespaceCVC3.html#a4233916514848331ee104548acbab912" title="Expression index type.">ExprIndex</a> <a class="code" href="group__EM__Priv.html#ga212f07de6befabee47e4f9a1813e7c44" title="Return the next Expr index.">nextIndex</a>() { <span class="keywordflow">return</span> d_index++; }
<a name="l00269"></a><a class="code" href="group__EM__Priv.html#gac64badd3988c01f34e43f227902e80f1">00269</a> <a class="code" href="namespaceCVC3.html#a4233916514848331ee104548acbab912" title="Expression index type.">ExprIndex</a> <a class="code" href="group__EM__Priv.html#gac64badd3988c01f34e43f227902e80f1">lastIndex</a>() { <span class="keywordflow">return</span> d_index - 1; }
<a name="l00270"></a>00270 <span class="comment"></span>
<a name="l00271"></a>00271 <span class="comment"> //! Clears the generic Expr flag in all Exprs</span>
<a name="l00272"></a><a class="code" href="group__EM__Priv.html#gab4b3f2259b5c0af2251741139ea9d952">00272</a> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__EM__Priv.html#gab4b3f2259b5c0af2251741139ea9d952" title="Clears the generic Expr flag in all Exprs.">clearFlags</a>() { nextFlag(); }
<a name="l00273"></a>00273
<a name="l00274"></a>00274 <span class="comment">// Core leaf exprs</span><span class="comment"></span>
<a name="l00275"></a>00275 <span class="comment"> //! BOOLEAN Expr</span>
<a name="l00276"></a><a class="code" href="group__EM__Priv.html#gab01fe102500e6b4e266299bf4bbb8a20">00276</a> <span class="comment"></span> <span class="keyword">const</span> <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#gab01fe102500e6b4e266299bf4bbb8a20" title="BOOLEAN Expr.">boolExpr</a>() { <span class="keywordflow">return</span> d_bool; }<span class="comment"></span>
<a name="l00277"></a>00277 <span class="comment"> //! FALSE Expr</span>
<a name="l00278"></a><a class="code" href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae">00278</a> <span class="comment"></span> <span class="keyword">const</span> <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#gaae9db4c93c67cbf8bbf5d1e60e94f1ae" title="FALSE Expr.">falseExpr</a>() { <span class="keywordflow">return</span> d_false; }<span class="comment"></span>
<a name="l00279"></a>00279 <span class="comment"> //! TRUE Expr</span>
<a name="l00280"></a><a class="code" href="group__EM__Priv.html#ga4471fca49c2acbb7b4cf71e72bc55d6a">00280</a> <span class="comment"></span> <span class="keyword">const</span> <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#ga4471fca49c2acbb7b4cf71e72bc55d6a" title="TRUE Expr.">trueExpr</a>() { <span class="keywordflow">return</span> d_true; }<span class="comment"></span>
<a name="l00281"></a>00281 <span class="comment"> //! References to empty objects (used in ExprValue)</span>
<a name="l00282"></a><a class="code" href="group__EM__Priv.html#ga4619bc6e35a273b89d30908c45d73348">00282</a> <span class="comment"></span> <span class="keyword">const</span> std::vector<Expr>& <a class="code" href="group__EM__Priv.html#ga4619bc6e35a273b89d30908c45d73348" title="References to empty objects (used in ExprValue)">getEmptyVector</a>() { <span class="keywordflow">return</span> d_emptyVec; }<span class="comment"></span>
<a name="l00283"></a>00283 <span class="comment"> //! References to empty objects (used in ExprValue)</span>
<a name="l00284"></a><a class="code" href="group__EM__Priv.html#ga5b9a6dbadfbed96662a5b5d72e6001e2">00284</a> <span class="comment"></span> <span class="keyword">const</span> <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#ga5b9a6dbadfbed96662a5b5d72e6001e2" title="References to empty objects (used in ExprValue)">getNullExpr</a>() { <span class="keywordflow">return</span> d_nullExpr; }
<a name="l00285"></a>00285
<a name="l00286"></a>00286 <span class="comment">// Expr constructors</span>
<a name="l00287"></a>00287 <span class="comment"></span>
<a name="l00288"></a>00288 <span class="comment"> //! Return either an existing or a new Expr matching ev</span>
<a name="l00289"></a><a class="code" href="group__EM__Priv.html#ga603f0df90a7c9695e010355f8ad8df43">00289</a> <span class="comment"></span> <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#ga603f0df90a7c9695e010355f8ad8df43" title="Return either an existing or a new Expr matching ev.">newExpr</a>(<a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* ev) { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(newExprValue(ev)); }
<a name="l00290"></a>00290
<a name="l00291"></a>00291 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newLeafExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Op.html">Op</a>& op);
<a name="l00292"></a>00292 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newStringExpr(<span class="keyword">const</span> std::string &s);
<a name="l00293"></a>00293 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newRatExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a>& r);
<a name="l00294"></a>00294 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newSkolemExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keywordtype">int</span> i);
<a name="l00295"></a>00295 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newVarExpr(<span class="keyword">const</span> std::string &s);
<a name="l00296"></a>00296 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newSymbolExpr(<span class="keyword">const</span> std::string &s, <span class="keywordtype">int</span> kind);
<a name="l00297"></a>00297 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBoundVarExpr(<span class="keyword">const</span> std::string &name, <span class="keyword">const</span> std::string& uid);
<a name="l00298"></a>00298 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBoundVarExpr(<span class="keyword">const</span> std::string &name, <span class="keyword">const</span> std::string& uid,
<a name="l00299"></a>00299 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type);
<a name="l00300"></a>00300 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBoundVarExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type);
<a name="l00301"></a>00301 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newClosureExpr(<span class="keywordtype">int</span> kind, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& var, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& body);
<a name="l00302"></a>00302 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newClosureExpr(<span class="keywordtype">int</span> kind, <span class="keyword">const</span> std::vector<Expr>& vars,
<a name="l00303"></a>00303 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& body);
<a name="l00304"></a>00304 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newClosureExpr(<span class="keywordtype">int</span> kind, <span class="keyword">const</span> std::vector<Expr>& vars,
<a name="l00305"></a>00305 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& body, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& trigger);
<a name="l00306"></a>00306 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newClosureExpr(<span class="keywordtype">int</span> kind, <span class="keyword">const</span> std::vector<Expr>& vars,
<a name="l00307"></a>00307 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& body, <span class="keyword">const</span> std::vector<Expr>& triggers);
<a name="l00308"></a>00308 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newClosureExpr(<span class="keywordtype">int</span> kind, <span class="keyword">const</span> std::vector<Expr>& vars,
<a name="l00309"></a>00309 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& body, <span class="keyword">const</span> std::vector<std::vector<Expr> >& triggers);
<a name="l00310"></a>00310
<a name="l00311"></a>00311 <span class="comment">// Vector of children constructors (vector may be empty)</span>
<a name="l00312"></a><a class="code" href="group__EM__Priv.html#ga305b349b572c311b55a121e28392a714">00312</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="namespaceCVC3.html#ad4258158bba138eb54b9080af7f8223a">andExpr</a>(<span class="keyword">const</span> std::vector <Expr>& children)
<a name="l00313"></a>00313 { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba865555c9f2e0458a7078486aa1b3254f">AND</a>, children, <span class="keyword">this</span>); }
<a name="l00314"></a><a class="code" href="group__EM__Priv.html#ga65c227873c06b36c509832506d690aaa">00314</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="namespaceCVC3.html#a30f30b6e20c174f21ae63acea8618294">orExpr</a>(<span class="keyword">const</span> std::vector <Expr>& children)
<a name="l00315"></a>00315 { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>, children, <span class="keyword">this</span>); }
<a name="l00316"></a>00316
<a name="l00317"></a>00317 <span class="comment">// Public methods</span>
<a name="l00318"></a>00318 <span class="comment"></span>
<a name="l00319"></a>00319 <span class="comment"> //! Hash function for a single Expr</span>
<a name="l00320"></a>00320 <span class="comment"></span> <span class="keywordtype">size_t</span> <a class="code" href="structHash_1_1hash.html">hash</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) <span class="keyword">const</span>;<span class="comment"></span>
<a name="l00321"></a>00321 <span class="comment"> //! Fetch our ContextManager</span>
<a name="l00322"></a><a class="code" href="group__EM__Priv.html#ga50b20f4e775e01da9045fbea0762855b">00322</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ContextManager.html" title="Manager for multiple contexts. Also holds current context.">ContextManager</a>* <a class="code" href="group__EM__Priv.html#ga50b20f4e775e01da9045fbea0762855b" title="Fetch our ContextManager.">getCM</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_cm; }<span class="comment"></span>
<a name="l00323"></a>00323 <span class="comment"> //! Get the current context from our ContextManager</span>
<a name="l00324"></a><a class="code" href="group__EM__Priv.html#ga5f8daa1f01a0b3f30a3a147243411e5a">00324</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Context.html">Context</a>* <a class="code" href="group__EM__Priv.html#ga5f8daa1f01a0b3f30a3a147243411e5a" title="Get the current context from our ContextManager.">getCurrentContext</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_cm->getCurrentContext(); }<span class="comment"></span>
<a name="l00325"></a>00325 <span class="comment"> //! Get current scope level</span>
<a name="l00326"></a><a class="code" href="group__EM__Priv.html#gafd98497270fdbd403d52b09cf95d0839">00326</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="group__EM__Priv.html#gafd98497270fdbd403d52b09cf95d0839" title="Get current scope level.">scopelevel</a>() { <span class="keywordflow">return</span> d_cm->scopeLevel(); }
<a name="l00327"></a>00327 <span class="comment"></span>
<a name="l00328"></a>00328 <span class="comment"> //! Set the TheoremManager</span>
<a name="l00329"></a><a class="code" href="group__EM__Priv.html#ga3a3060cbeb64eb97ac935f8f05a60f9b">00329</a> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__EM__Priv.html#ga3a3060cbeb64eb97ac935f8f05a60f9b" title="Set the TheoremManager.">setTM</a>(<a class="code" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>* tm) { d_tm = tm; }<span class="comment"></span>
<a name="l00330"></a>00330 <span class="comment"> //! Fetch the TheoremManager</span>
<a name="l00331"></a><a class="code" href="group__EM__Priv.html#ga4aa1269ec9df849a4b7654742408d2ca">00331</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>* <a class="code" href="group__EM__Priv.html#ga4aa1269ec9df849a4b7654742408d2ca" title="Fetch the TheoremManager.">getTM</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_tm; }
<a name="l00332"></a>00332 <span class="comment"></span>
<a name="l00333"></a>00333 <span class="comment"> //! Return a MemoryManager for the given ExprValue type</span>
<a name="l00334"></a><a class="code" href="group__EM__Priv.html#ga721fc26fe37460f80e6d614cfe0d6fd8">00334</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1MemoryManager.html">MemoryManager</a>* <a class="code" href="group__EM__Priv.html#ga721fc26fe37460f80e6d614cfe0d6fd8" title="Return a MemoryManager for the given ExprValue type.">getMM</a>(<span class="keywordtype">size_t</span> MMIndex) {
<a name="l00335"></a>00335 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(MMIndex < d_mm.size(), <span class="stringliteral">"ExprManager::getMM()"</span>);
<a name="l00336"></a>00336 <span class="keywordflow">return</span> d_mm[MMIndex];
<a name="l00337"></a>00337 }<span class="comment"></span>
<a name="l00338"></a>00338 <span class="comment"> //! Get the simplifier's cache tag</span>
<a name="l00339"></a><a class="code" href="group__EM__Priv.html#gacacaaf5083e198a6014c2407c7f09cc0">00339</a> <span class="comment"></span> <span class="keywordtype">unsigned</span> <a class="code" href="group__EM__Priv.html#gacacaaf5083e198a6014c2407c7f09cc0" title="Get the simplifier's cache tag.">getSimpCacheTag</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_simpCacheTagCurrent; }<span class="comment"></span>
<a name="l00340"></a>00340 <span class="comment"> //! Invalidate the simplifier's cache tag</span>
<a name="l00341"></a><a class="code" href="group__EM__Priv.html#gaba358e1731ad9309e52e64eb9ce60755">00341</a> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__EM__Priv.html#gaba358e1731ad9309e52e64eb9ce60755" title="Invalidate the simplifier's cache tag.">invalidateSimpCache</a>() { d_simpCacheTagCurrent++; }
<a name="l00342"></a>00342 <span class="comment"></span>
<a name="l00343"></a>00343 <span class="comment"> //! Register type computer</span>
<a name="l00344"></a><a class="code" href="group__EM__Priv.html#ga39c8449d567e83ccd711cb2ff1a91dbf">00344</a> <span class="comment"></span> <span class="keywordtype">void</span> registerTypeComputer(<a class="code" href="classCVC3_1_1ExprManager_1_1TypeComputer.html" title="Abstract class for computing expr type.">TypeComputer</a>* typeComputer)
<a name="l00345"></a>00345 { d_typeComputer = typeComputer; }
<a name="l00346"></a>00346 <span class="comment"></span>
<a name="l00347"></a>00347 <span class="comment"> //! Get printing depth</span>
<a name="l00348"></a><a class="code" href="group__EM__Priv.html#ga56fe351db38c3cc509ae6b1b9c2de000">00348</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="group__EM__Priv.html#ga56fe351db38c3cc509ae6b1b9c2de000" title="Get printing depth.">printDepth</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> *d_printDepth; }<span class="comment"></span>
<a name="l00349"></a>00349 <span class="comment"> //! Whether to print with indentation</span>
<a name="l00350"></a><a class="code" href="group__EM__Priv.html#ga3576f0cdcb0ab043d0612c7d9aff7ba1">00350</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="group__EM__Priv.html#ga3576f0cdcb0ab043d0612c7d9aff7ba1" title="Whether to print with indentation.">withIndentation</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> *d_withIndentation; }<span class="comment"></span>
<a name="l00351"></a>00351 <span class="comment"> //! Suggested line width for printing with indentation</span>
<a name="l00352"></a><a class="code" href="group__EM__Priv.html#gab624bd63ef4b189802f1708a41b2b3da">00352</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="group__EM__Priv.html#gab624bd63ef4b189802f1708a41b2b3da" title="Suggested line width for printing with indentation.">lineWidth</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> *d_lineWidth; }<span class="comment"></span>
<a name="l00353"></a>00353 <span class="comment"> //! Get initial indentation</span>
<a name="l00354"></a><a class="code" href="group__EM__Priv.html#ga54ddb950b6bd35316d1cefe3fd506149">00354</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="group__EM__Priv.html#ga54ddb950b6bd35316d1cefe3fd506149" title="Get initial indentation.">indent</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_indentTransient; }<span class="comment"></span>
<a name="l00355"></a>00355 <span class="comment"> //! Set initial indentation. Returns the previous permanent value.</span>
<a name="l00356"></a>00356 <span class="comment"></span> <span class="keywordtype">int</span> indent(<span class="keywordtype">int</span> n, <span class="keywordtype">bool</span> permanent = <span class="keyword">false</span>);<span class="comment"></span>
<a name="l00357"></a>00357 <span class="comment"> //! Increment the current transient indentation by n</span>
<a name="l00358"></a>00358 <span class="comment"></span><span class="comment"> /*! If the second argument is true, sets the result as permanent.</span>
<a name="l00359"></a>00359 <span class="comment"> \return previous permanent value. */</span>
<a name="l00360"></a>00360 <span class="keywordtype">int</span> incIndent(<span class="keywordtype">int</span> n, <span class="keywordtype">bool</span> permanent = <span class="keyword">false</span>);<span class="comment"></span>
<a name="l00361"></a>00361 <span class="comment"> //! Set transient indentation to permanent</span>
<a name="l00362"></a><a class="code" href="group__EM__Priv.html#ga3fe43b71bb148045c114e054934f5304">00362</a> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__EM__Priv.html#ga3fe43b71bb148045c114e054934f5304" title="Set transient indentation to permanent.">restoreIndent</a>() { d_indentTransient = d_indent; }<span class="comment"></span>
<a name="l00363"></a>00363 <span class="comment"> //! Get the input language for printing</span>
<a name="l00364"></a>00364 <span class="comment"></span> <a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e" title="Different input languages.">InputLanguage</a> getInputLang() <span class="keyword">const</span>;<span class="comment"></span>
<a name="l00365"></a>00365 <span class="comment"> //! Get the output language for printing</span>
<a name="l00366"></a>00366 <span class="comment"></span> <a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e" title="Different input languages.">InputLanguage</a> getOutputLang() <span class="keyword">const</span>;<span class="comment"></span>
<a name="l00367"></a>00367 <span class="comment"> //! Whether to print Expr's as DAGs</span>
<a name="l00368"></a><a class="code" href="group__EM__Priv.html#gab24afcec7ae8e33808eebf608193efd9">00368</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="group__EM__Priv.html#gab24afcec7ae8e33808eebf608193efd9" title="Whether to print Expr's as DAGs.">dagPrinting</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> *d_dagPrinting; }<span class="comment"></span>
<a name="l00369"></a>00369 <span class="comment"> /*! @brief Return the pretty-printer if there is one; otherwise</span>
<a name="l00370"></a>00370 <span class="comment"> return NULL. */</span>
<a name="l00371"></a><a class="code" href="group__EM__Priv.html#ga3762b5bfe4264bd35b4e887084835fa6">00371</a> <a class="code" href="classCVC3_1_1PrettyPrinter.html" title="Abstract API to a pretty-printer for Expr.">PrettyPrinter</a>* <a class="code" href="group__EM__Priv.html#ga3762b5bfe4264bd35b4e887084835fa6" title="Return the pretty-printer if there is one; otherwise return NULL.">getPrinter</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_prettyPrinter; }
<a name="l00372"></a>00372 <span class="comment"></span>
<a name="l00373"></a>00373 <span class="comment"> /////////////////////////////////////////////////////////////////////////////</span>
<a name="l00374"></a>00374 <span class="comment"></span> <span class="comment">// Kind registration //</span><span class="comment"></span>
<a name="l00375"></a>00375 <span class="comment"> /////////////////////////////////////////////////////////////////////////////</span>
<a name="l00376"></a>00376 <span class="comment"></span><span class="comment"></span>
<a name="l00377"></a>00377 <span class="comment"> //! Register a new kind.</span>
<a name="l00378"></a>00378 <span class="comment"></span><span class="comment"> /*! The kind may already be registered under the same name, but if</span>
<a name="l00379"></a>00379 <span class="comment"> * the name is different, it's an error.</span>
<a name="l00380"></a>00380 <span class="comment"> * </span>
<a name="l00381"></a>00381 <span class="comment"> * If the new kind is supposed to represent a type, set isType to true.</span>
<a name="l00382"></a>00382 <span class="comment"> */</span>
<a name="l00383"></a>00383 <span class="keywordtype">void</span> newKind(<span class="keywordtype">int</span> kind, <span class="keyword">const</span> std::string &name, <span class="keywordtype">bool</span> isType = <span class="keyword">false</span>);<span class="comment"></span>
<a name="l00384"></a>00384 <span class="comment"> //! Register the pretty-printer (can only do it if none registered)</span>
<a name="l00385"></a>00385 <span class="comment"></span><span class="comment"> /*! The pointer is NOT owned by ExprManager. Delete it yourself.</span>
<a name="l00386"></a>00386 <span class="comment"> */</span>
<a name="l00387"></a>00387 <span class="keywordtype">void</span> registerPrettyPrinter(<a class="code" href="classCVC3_1_1PrettyPrinter.html" title="Abstract API to a pretty-printer for Expr.">PrettyPrinter</a>& printer);<span class="comment"></span>
<a name="l00388"></a>00388 <span class="comment"> //! Tell ExprManager that the printer is no longer valid</span>
<a name="l00389"></a>00389 <span class="comment"></span> <span class="keywordtype">void</span> unregisterPrettyPrinter();<span class="comment"></span>
<a name="l00390"></a>00390 <span class="comment"> /*! @brief Returns true if kind is built into CVC or has been registered</span>
<a name="l00391"></a>00391 <span class="comment"> via newKind. */</span>
<a name="l00392"></a><a class="code" href="group__EM__Priv.html#gae9e4de0bea1c6f2b5ef2e6c8a59b2b7c">00392</a> <span class="keywordtype">bool</span> <a class="code" href="group__EM__Priv.html#gae9e4de0bea1c6f2b5ef2e6c8a59b2b7c" title="Returns true if kind is built into CVC or has been registered via newKind.">isKindRegistered</a>(<span class="keywordtype">int</span> kind) { <span class="keywordflow">return</span> d_kindMap.count(kind) > 0; }<span class="comment"></span>
<a name="l00393"></a>00393 <span class="comment"> //! Check if a kind represents a type</span>
<a name="l00394"></a><a class="code" href="group__EM__Priv.html#ga8e91326852cd6030a390fa3a29f6c8f9">00394</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="group__EM__Priv.html#ga8e91326852cd6030a390fa3a29f6c8f9" title="Check if a kind represents a type.">isTypeKind</a>(<span class="keywordtype">int</span> kind) { <span class="keywordflow">return</span> d_typeKinds.count(kind) > 0; }
<a name="l00395"></a>00395 <span class="comment"></span>
<a name="l00396"></a>00396 <span class="comment"> /*! @brief Return the name associated with a kind. The kind must</span>
<a name="l00397"></a>00397 <span class="comment"> already be registered. */</span>
<a name="l00398"></a>00398 <span class="keyword">const</span> std::string& getKindName(<span class="keywordtype">int</span> kind);<span class="comment"></span>
<a name="l00399"></a>00399 <span class="comment"> //! Return a kind associated with a name. Returns NULL_KIND if not found.</span>
<a name="l00400"></a>00400 <span class="comment"></span> <span class="keywordtype">int</span> getKind(<span class="keyword">const</span> std::string& name);<span class="comment"></span>
<a name="l00401"></a>00401 <span class="comment"> //! Register a new subclass of ExprValue</span>
<a name="l00402"></a>00402 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00403"></a>00403 <span class="comment"> * Takes the size (in bytes) of the new subclass and returns the</span>
<a name="l00404"></a>00404 <span class="comment"> * unique index of that subclass. Subsequent calls to the</span>
<a name="l00405"></a>00405 <span class="comment"> * subclass's getMMIndex() must return that index.</span>
<a name="l00406"></a>00406 <span class="comment"> */</span>
<a name="l00407"></a>00407 <span class="keywordtype">size_t</span> registerSubclass(<span class="keywordtype">size_t</span> sizeOfSubclass);
<a name="l00408"></a>00408 <span class="comment"></span>
<a name="l00409"></a>00409 <span class="comment"> //! Calculate memory usage</span>
<a name="l00410"></a>00410 <span class="comment"></span> <span class="keywordtype">unsigned</span> <span class="keywordtype">long</span> getMemory(<span class="keywordtype">int</span> verbosity);
<a name="l00411"></a>00411
<a name="l00412"></a>00412 }; <span class="comment">// end of class ExprManager</span>
<a name="l00413"></a>00413
<a name="l00414"></a>00414
<a name="l00415"></a>00415 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00416"></a>00416 <span class="comment">/*!</span>
<a name="l00417"></a>00417 <span class="comment"> *\class ExprManagerNotifyObj</span>
<a name="l00418"></a>00418 <span class="comment"> *\brief Notifies ExprManager before and after each pop()</span>
<a name="l00419"></a>00419 <span class="comment"> *</span>
<a name="l00420"></a>00420 <span class="comment"> * Author: Sergey Berezin</span>
<a name="l00421"></a>00421 <span class="comment"> *</span>
<a name="l00422"></a>00422 <span class="comment"> * Created: Tue Mar 1 12:29:14 2005</span>
<a name="l00423"></a>00423 <span class="comment"> *</span>
<a name="l00424"></a>00424 <span class="comment"> * Disables the deletion of Exprs during context restoration</span>
<a name="l00425"></a>00425 <span class="comment"> * (backtracking). This solves the problem of circular dependencies,</span>
<a name="l00426"></a>00426 <span class="comment"> * e.g. in find pointers.</span>
<a name="l00427"></a>00427 <span class="comment"> */</span>
<a name="l00428"></a>00428 <span class="comment">/*****************************************************************************/</span>
<a name="l00429"></a><a class="code" href="classCVC3_1_1ExprManagerNotifyObj.html">00429</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1ExprManagerNotifyObj.html" title="Notifies ExprManager before and after each pop()">ExprManagerNotifyObj</a>: <span class="keyword">public</span> <a class="code" href="classCVC3_1_1ContextNotifyObj.html">ContextNotifyObj</a> {
<a name="l00430"></a><a class="code" href="classCVC3_1_1ExprManagerNotifyObj.html#a5b95d2473f4230b72cc27b090500552f">00430</a> <a class="code" href="classCVC3_1_1ExprManager.html">ExprManager</a>* <a class="code" href="classCVC3_1_1ExprManagerNotifyObj.html#a5b95d2473f4230b72cc27b090500552f">d_em</a>;
<a name="l00431"></a>00431 <span class="keyword">public</span>:<span class="comment"></span>
<a name="l00432"></a>00432 <span class="comment"> //! Constructor</span>
<a name="l00433"></a><a class="code" href="group__EM__Priv.html#ga8150de408f4d5aec9ceddabf86b30cf3">00433</a> <span class="comment"></span> <a class="code" href="group__EM__Priv.html#ga8150de408f4d5aec9ceddabf86b30cf3" title="Constructor.">ExprManagerNotifyObj</a>(<a class="code" href="classCVC3_1_1ExprManager.html">ExprManager</a>* em, <a class="code" href="classCVC3_1_1Context.html">Context</a>* cxt)
<a name="l00434"></a>00434 : <a class="code" href="classCVC3_1_1ContextNotifyObj.html">ContextNotifyObj</a>(cxt), <a class="code" href="classCVC3_1_1ExprManagerNotifyObj.html#a5b95d2473f4230b72cc27b090500552f">d_em</a>(em) { }
<a name="l00435"></a>00435
<a name="l00436"></a>00436 <span class="keywordtype">void</span> <a class="code" href="group__EM__Priv.html#gac681a5cd1f70dda8a7a391439d887c2d">notifyPre</a>(<span class="keywordtype">void</span>);
<a name="l00437"></a>00437 <span class="keywordtype">void</span> <a class="code" href="group__EM__Priv.html#gadd71c522283037f94526bda8f73a8bbd">notify</a>(<span class="keywordtype">void</span>);
<a name="l00438"></a><a class="code" href="group__EM__Priv.html#ga083141d49f93f86b917f6a99f239d2c8">00438</a> <span class="keywordtype">unsigned</span> <span class="keywordtype">long</span> <a class="code" href="group__EM__Priv.html#ga083141d49f93f86b917f6a99f239d2c8">getMemory</a>(<span class="keywordtype">int</span> verbosity) { <span class="keywordflow">return</span> <span class="keyword">sizeof</span>(<a class="code" href="group__EM__Priv.html#ga8150de408f4d5aec9ceddabf86b30cf3" title="Constructor.">ExprManagerNotifyObj</a>); }
<a name="l00439"></a>00439 };
<a name="l00440"></a>00440
<a name="l00441"></a>00441
<a name="l00442"></a>00442 } <span class="comment">// end of namespace CVC3</span>
<a name="l00443"></a>00443
<a name="l00444"></a>00444 <span class="comment">// Include expr_value here for inline definitions</span>
<a name="l00445"></a>00445 <span class="preprocessor">#include "<a class="code" href="expr__value_8h.html">expr_value.h</a>"</span>
<a name="l00446"></a>00446
<a name="l00447"></a>00447 <span class="keyword">namespace </span>CVC3 {
<a name="l00448"></a>00448
<a name="l00449"></a><a class="code" href="classCVC3_1_1ExprManager.html#ac4a0d5785aa3427b482ab07dff8b5609">00449</a> <span class="keyword">inline</span> <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1ExprManager.html#ac4a0d5785aa3427b482ab07dff8b5609">ExprManager::hash</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* ev)<span class="keyword"> const </span>{
<a name="l00450"></a>00450 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(ev!=NULL, <span class="stringliteral">"ExprManager::hash() called on a NULL ExprValue"</span>);
<a name="l00451"></a>00451 <span class="keywordflow">return</span> ev-><a class="code" href="classCVC3_1_1ExprValue.html#af56c36f0f7e4aab1a37cf35272d66198" title="Caching hash function.">hash</a>();
<a name="l00452"></a>00452 }
<a name="l00453"></a>00453
<a name="l00454"></a><a class="code" href="group__EM__Priv.html#gacd77df1dbcc429e06a75047e2f609822">00454</a> <span class="keyword">inline</span> <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#gacd77df1dbcc429e06a75047e2f609822">ExprManager::newLeafExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Op.html">Op</a>& op)
<a name="l00455"></a>00455 {
<a name="l00456"></a>00456 <span class="keywordflow">if</span> (op.<a class="code" href="classCVC3_1_1Op.html#a7fdaa9877edff1d7a32440a9400a81fd">getKind</a>() != <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5c41450c4e719ca40d8e734f6a2008f0">APPLY</a>) {
<a name="l00457"></a>00457 <a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a> ev(<span class="keyword">this</span>, op.<a class="code" href="classCVC3_1_1Op.html#a7fdaa9877edff1d7a32440a9400a81fd">getKind</a>());
<a name="l00458"></a>00458 <span class="keywordflow">return</span> <a class="code" href="group__EM__Priv.html#ga603f0df90a7c9695e010355f8ad8df43" title="Return either an existing or a new Expr matching ev.">newExpr</a>(&ev);
<a name="l00459"></a>00459 }
<a name="l00460"></a>00460 <span class="keywordflow">else</span> {
<a name="l00461"></a>00461 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(op.<a class="code" href="classCVC3_1_1Op.html#a4a38071541d1e863583f12e9d81de3a2">getExpr</a>().<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>() == <span class="keyword">this</span>, <span class="stringliteral">"ExprManager mismatch"</span>);
<a name="l00462"></a>00462 std::vector<Expr> kids;
<a name="l00463"></a>00463 <a class="code" href="classCVC3_1_1ExprApply.html">ExprApply</a> ev(<span class="keyword">this</span>, op, kids);
<a name="l00464"></a>00464 <span class="keywordflow">return</span> <a class="code" href="group__EM__Priv.html#ga603f0df90a7c9695e010355f8ad8df43" title="Return either an existing or a new Expr matching ev.">newExpr</a>(&ev);
<a name="l00465"></a>00465 }
<a name="l00466"></a>00466 }
<a name="l00467"></a>00467
<a name="l00468"></a><a class="code" href="group__EM__Priv.html#ga3c1f298d2fdd7aaba48d000ca27df636">00468</a> <span class="keyword">inline</span> <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#ga3c1f298d2fdd7aaba48d000ca27df636">ExprManager::newStringExpr</a>(<span class="keyword">const</span> std::string &s)
<a name="l00469"></a>00469 { <a class="code" href="classCVC3_1_1ExprString.html">ExprString</a> ev(<span class="keyword">this</span>, s); <span class="keywordflow">return</span> <a class="code" href="group__EM__Priv.html#ga603f0df90a7c9695e010355f8ad8df43" title="Return either an existing or a new Expr matching ev.">newExpr</a>(&ev); }
<a name="l00470"></a>00470
<a name="l00471"></a><a class="code" href="group__EM__Priv.html#ga18423a42ce6557dc33287d3979ccc3c6">00471</a> <span class="keyword">inline</span> <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#ga18423a42ce6557dc33287d3979ccc3c6">ExprManager::newRatExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a>& r)
<a name="l00472"></a>00472 { <a class="code" href="classCVC3_1_1ExprRational.html">ExprRational</a> ev(<span class="keyword">this</span>, r); <span class="keywordflow">return</span> <a class="code" href="group__EM__Priv.html#ga603f0df90a7c9695e010355f8ad8df43" title="Return either an existing or a new Expr matching ev.">newExpr</a>(&ev); }
<a name="l00473"></a>00473
<a name="l00474"></a><a class="code" href="group__EM__Priv.html#gaf392ed0e07e505e56e551ce9cdaa76fe">00474</a> <span class="keyword">inline</span> <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#gaf392ed0e07e505e56e551ce9cdaa76fe">ExprManager::newSkolemExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keywordtype">int</span> i)
<a name="l00475"></a>00475 { <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>() == <span class="keyword">this</span>, <span class="stringliteral">"ExprManager mismatch"</span>);
<a name="l00476"></a>00476 <a class="code" href="classCVC3_1_1ExprSkolem.html">ExprSkolem</a> ev(<span class="keyword">this</span>, i, e); <span class="keywordflow">return</span> <a class="code" href="group__EM__Priv.html#ga603f0df90a7c9695e010355f8ad8df43" title="Return either an existing or a new Expr matching ev.">newExpr</a>(&ev); }
<a name="l00477"></a>00477
<a name="l00478"></a><a class="code" href="group__EM__Priv.html#ga4d52ed373636679c2dd651d10822a3ee">00478</a> <span class="keyword">inline</span> <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#ga4d52ed373636679c2dd651d10822a3ee">ExprManager::newVarExpr</a>(<span class="keyword">const</span> std::string &s)
<a name="l00479"></a>00479 { <a class="code" href="classCVC3_1_1ExprVar.html">ExprVar</a> ev(<span class="keyword">this</span>, s); <span class="keywordflow">return</span> <a class="code" href="group__EM__Priv.html#ga603f0df90a7c9695e010355f8ad8df43" title="Return either an existing or a new Expr matching ev.">newExpr</a>(&ev); }
<a name="l00480"></a>00480
<a name="l00481"></a><a class="code" href="group__EM__Priv.html#gafddb4551e9dbb163823b1162248e58f0">00481</a> <span class="keyword">inline</span> <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#gafddb4551e9dbb163823b1162248e58f0">ExprManager::newSymbolExpr</a>(<span class="keyword">const</span> std::string &s, <span class="keywordtype">int</span> kind)
<a name="l00482"></a>00482 { <a class="code" href="classCVC3_1_1ExprSymbol.html">ExprSymbol</a> ev(<span class="keyword">this</span>, kind, s); <span class="keywordflow">return</span> <a class="code" href="group__EM__Priv.html#ga603f0df90a7c9695e010355f8ad8df43" title="Return either an existing or a new Expr matching ev.">newExpr</a>(&ev); }
<a name="l00483"></a>00483
<a name="l00484"></a><a class="code" href="group__EM__Priv.html#ga22dbb23f716cc73378d4c69d564e38dd">00484</a> <span class="keyword">inline</span> <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#ga22dbb23f716cc73378d4c69d564e38dd">ExprManager::newBoundVarExpr</a>(<span class="keyword">const</span> std::string &name,
<a name="l00485"></a>00485 <span class="keyword">const</span> std::string& uid)
<a name="l00486"></a>00486 { <a class="code" href="classCVC3_1_1ExprBoundVar.html">ExprBoundVar</a> ev(<span class="keyword">this</span>, name, uid); <span class="keywordflow">return</span> <a class="code" href="group__EM__Priv.html#ga603f0df90a7c9695e010355f8ad8df43" title="Return either an existing or a new Expr matching ev.">newExpr</a>(&ev); }
<a name="l00487"></a>00487
<a name="l00488"></a><a class="code" href="group__EM__Priv.html#ga53f1a8180e8fcfead2537dd876c80682">00488</a> <span class="keyword">inline</span> <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#ga22dbb23f716cc73378d4c69d564e38dd">ExprManager::newBoundVarExpr</a>(<span class="keyword">const</span> std::string& name,
<a name="l00489"></a>00489 <span class="keyword">const</span> std::string& uid,
<a name="l00490"></a>00490 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type) {
<a name="l00491"></a>00491 <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#ga22dbb23f716cc73378d4c69d564e38dd">newBoundVarExpr</a>(name, uid);
<a name="l00492"></a>00492 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(type.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>().<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() != <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba546eccfedc4dcc8623ed0668f77ef982">ARROW</a>,<span class="stringliteral">""</span>);
<a name="l00493"></a>00493 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(res.<a class="code" href="group__ExprPkg.html#ga801d77a373d26549c735dbd8a7fda1a5" title="Look up the current type. Do not recursively compute (i.e. may be NULL)">lookupType</a>().<a class="code" href="classCVC3_1_1Type.html#ab5fe00c99ee91f369e3339b26bab0bf7">isNull</a>(),
<a name="l00494"></a>00494 <span class="stringliteral">"newBoundVarExpr: redefining a variable "</span> + name);
<a name="l00495"></a>00495 res.<a class="code" href="group__ExprPkg.html#ga07d47f902598e00097086deabf04d9c5" title="Set the cached type.">setType</a>(type);
<a name="l00496"></a>00496 <span class="keywordflow">return</span> res;
<a name="l00497"></a>00497 }
<a name="l00498"></a>00498
<a name="l00499"></a><a class="code" href="group__EM__Priv.html#ga4a47e11b69e5a197d0437be8a632fa08">00499</a> <span class="keyword">inline</span> <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#ga22dbb23f716cc73378d4c69d564e38dd">ExprManager::newBoundVarExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type) {
<a name="l00500"></a>00500 <span class="keyword">static</span> <span class="keywordtype">int</span> nextNum = 0;
<a name="l00501"></a>00501 std::string name(<span class="stringliteral">"_cvc3_"</span>);
<a name="l00502"></a>00502 std::string uid = <a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(nextNum++);
<a name="l00503"></a>00503 <span class="keywordflow">return</span> <a class="code" href="group__EM__Priv.html#ga22dbb23f716cc73378d4c69d564e38dd">newBoundVarExpr</a>(name, uid, type);
<a name="l00504"></a>00504 }
<a name="l00505"></a>00505
<a name="l00506"></a><a class="code" href="group__EM__Priv.html#ga0d2ff7603a249b30b2df4e549607ad6e">00506</a> <span class="keyword">inline</span> <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#ga0d2ff7603a249b30b2df4e549607ad6e">ExprManager::newClosureExpr</a>(<span class="keywordtype">int</span> kind,
<a name="l00507"></a>00507 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& var,
<a name="l00508"></a>00508 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& body)
<a name="l00509"></a>00509 { <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> ev(<span class="keyword">this</span>, kind, var, body); <span class="keywordflow">return</span> <a class="code" href="group__EM__Priv.html#ga603f0df90a7c9695e010355f8ad8df43" title="Return either an existing or a new Expr matching ev.">newExpr</a>(&ev); }
<a name="l00510"></a>00510
<a name="l00511"></a><a class="code" href="group__EM__Priv.html#ga349cd5c632090f97d1f03effcbb3ebe4">00511</a> <span class="keyword">inline</span> <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#ga0d2ff7603a249b30b2df4e549607ad6e">ExprManager::newClosureExpr</a>(<span class="keywordtype">int</span> kind,
<a name="l00512"></a>00512 <span class="keyword">const</span> std::vector<Expr>& vars,
<a name="l00513"></a>00513 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& body)
<a name="l00514"></a>00514 { <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> ev(<span class="keyword">this</span>, kind, vars, body); <span class="keywordflow">return</span> <a class="code" href="group__EM__Priv.html#ga603f0df90a7c9695e010355f8ad8df43" title="Return either an existing or a new Expr matching ev.">newExpr</a>(&ev); }
<a name="l00515"></a>00515
<a name="l00516"></a><a class="code" href="group__EM__Priv.html#ga9793cd1d6b44062a5ae5b8bd5e5f548d">00516</a> <span class="keyword">inline</span> <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#ga0d2ff7603a249b30b2df4e549607ad6e">ExprManager::newClosureExpr</a>(<span class="keywordtype">int</span> kind,
<a name="l00517"></a>00517 <span class="keyword">const</span> std::vector<Expr>& vars,
<a name="l00518"></a>00518 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& body,
<a name="l00519"></a>00519 <span class="keyword">const</span> std::vector<Expr>& triggers)
<a name="l00520"></a>00520 { <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> ev(<span class="keyword">this</span>, kind, vars, body);
<a name="l00521"></a>00521 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> ret = <a class="code" href="group__EM__Priv.html#ga603f0df90a7c9695e010355f8ad8df43" title="Return either an existing or a new Expr matching ev.">newExpr</a>(&ev); ret.<a class="code" href="group__ExprPkg.html#gad15dc19335e0f59dddbb75d1d27579e7" title="Set the triggers for a closure Expr.">setTriggers</a>(triggers); <span class="keywordflow">return</span> ret; }
<a name="l00522"></a>00522
<a name="l00523"></a><a class="code" href="group__EM__Priv.html#ga47dd127b6737e1c0163fdf34cb5f1f15">00523</a> <span class="keyword">inline</span> <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#ga0d2ff7603a249b30b2df4e549607ad6e">ExprManager::newClosureExpr</a>(<span class="keywordtype">int</span> kind,
<a name="l00524"></a>00524 <span class="keyword">const</span> std::vector<Expr>& vars,
<a name="l00525"></a>00525 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& body,
<a name="l00526"></a>00526 <span class="keyword">const</span> std::vector<std::vector<Expr> >& triggers)
<a name="l00527"></a>00527 { <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> ev(<span class="keyword">this</span>, kind, vars, body);
<a name="l00528"></a>00528 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> ret = <a class="code" href="group__EM__Priv.html#ga603f0df90a7c9695e010355f8ad8df43" title="Return either an existing or a new Expr matching ev.">newExpr</a>(&ev); ret.<a class="code" href="group__ExprPkg.html#gad15dc19335e0f59dddbb75d1d27579e7" title="Set the triggers for a closure Expr.">setTriggers</a>(triggers); <span class="keywordflow">return</span> ret; }
<a name="l00529"></a>00529
<a name="l00530"></a><a class="code" href="group__EM__Priv.html#ga99ccea65cb5a86a0ac3f671777f8812d">00530</a> <span class="keyword">inline</span> <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#ga0d2ff7603a249b30b2df4e549607ad6e">ExprManager::newClosureExpr</a>(<span class="keywordtype">int</span> kind,
<a name="l00531"></a>00531 <span class="keyword">const</span> std::vector<Expr>& vars,
<a name="l00532"></a>00532 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& body,
<a name="l00533"></a>00533 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& trigger)
<a name="l00534"></a>00534 { <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> ev(<span class="keyword">this</span>, kind, vars, body);
<a name="l00535"></a>00535 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> ret = <a class="code" href="group__EM__Priv.html#ga603f0df90a7c9695e010355f8ad8df43" title="Return either an existing or a new Expr matching ev.">newExpr</a>(&ev); ret.<a class="code" href="group__ExprPkg.html#ga4e0dcc7b987305b845414ce0a7089381">setTrigger</a>(trigger); <span class="keywordflow">return</span> ret; }
<a name="l00536"></a>00536
<a name="l00537"></a><a class="code" href="group__EM__Priv.html#ga4a8fa9169728473cc4db3f96d467544f">00537</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="group__EM__Priv.html#ga4a8fa9169728473cc4db3f96d467544f">ExprManager::EqEV::operator()</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* ev1,
<a name="l00538"></a>00538 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a>* ev2)<span class="keyword"> const </span>{
<a name="l00539"></a>00539 <span class="keywordflow">return</span> (*ev1) == (*ev2);
<a name="l00540"></a>00540 }
<a name="l00541"></a>00541
<a name="l00542"></a><a class="code" href="group__EM__Priv.html#gaa6b885e5372d6072b670831c4e577eff">00542</a> <span class="keyword">inline</span> <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1ExprManager.html#ac4a0d5785aa3427b482ab07dff8b5609">ExprManager::hash</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e)<span class="keyword"> const </span>{
<a name="l00543"></a>00543 <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::hash() called on a Null Expr"</span>);
<a name="l00544"></a>00544 <span class="keywordflow">return</span> e.<a class="code" href="group__ExprPkg.html#ga3a08bea4e8715a268083e1671e340a2e">d_expr</a>-><a class="code" href="classCVC3_1_1ExprValue.html#af56c36f0f7e4aab1a37cf35272d66198" title="Caching hash function.">hash</a>();
<a name="l00545"></a>00545 }
<a name="l00546"></a>00546
<a name="l00547"></a>00547 } <span class="comment">// end of namespace CVC3</span>
<a name="l00548"></a>00548
<a name="l00549"></a>00549 <span class="preprocessor">#endif</span>
<a name="l00550"></a>00550 <span class="preprocessor"></span>
</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>
