<!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.cpp Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div class="header">
<div class="headertitle">
<div class="title">expr.cpp</div> </div>
</div>
<div class="contents">
<a href="expr_8cpp.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00002"></a>00002 <span class="comment">/*!</span>
<a name="l00003"></a>00003 <span class="comment"> * \file expr.cpp</span>
<a name="l00004"></a>00004 <span class="comment"> * </span>
<a name="l00005"></a>00005 <span class="comment"> * Author: Sergey Berezin</span>
<a name="l00006"></a>00006 <span class="comment"> * </span>
<a name="l00007"></a>00007 <span class="comment"> * Created: Thu Dec 5 11:35:55 2002</span>
<a name="l00008"></a>00008 <span class="comment"> *</span>
<a name="l00009"></a>00009 <span class="comment"> * <hr></span>
<a name="l00010"></a>00010 <span class="comment"> *</span>
<a name="l00011"></a>00011 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00012"></a>00012 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00013"></a>00013 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00014"></a>00014 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00015"></a>00015 <span class="comment"> * </span>
<a name="l00016"></a>00016 <span class="comment"> * <hr></span>
<a name="l00017"></a>00017 <span class="comment"> * </span>
<a name="l00018"></a>00018 <span class="comment"> */</span>
<a name="l00019"></a>00019 <span class="comment">/*****************************************************************************/</span>
<a name="l00020"></a>00020
<a name="l00021"></a>00021
<a name="l00022"></a>00022 <span class="preprocessor">#include <algorithm></span>
<a name="l00023"></a>00023
<a name="l00024"></a>00024
<a name="l00025"></a>00025 <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">#include "<a class="code" href="pretty__printer_8h.html">pretty_printer.h</a>"</span>
<a name="l00027"></a>00027 <span class="preprocessor">#include "<a class="code" href="expr__stream_8h.html">expr_stream.h</a>"</span>
<a name="l00028"></a>00028 <span class="preprocessor">#include "<a class="code" href="notifylist_8h.html">notifylist.h</a>"</span>
<a name="l00029"></a>00029 <span class="preprocessor">#include "<a class="code" href="exception_8h.html">exception.h</a>"</span>
<a name="l00030"></a>00030
<a name="l00031"></a>00031
<a name="l00032"></a>00032 <span class="keyword">using namespace </span>std;
<a name="l00033"></a>00033
<a name="l00034"></a>00034
<a name="l00035"></a><a class="code" href="namespaceCVC3.html">00035</a> <span class="keyword">namespace </span>CVC3 {
<a name="l00036"></a>00036
<a name="l00037"></a>00037
<a name="l00038"></a>00038 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> Expr::s_null;
<a name="l00039"></a>00039 <span class="comment"></span>
<a name="l00040"></a>00040 <span class="comment">///////////////////////////////////////////////////////////////////////</span>
<a name="l00041"></a>00041 <span class="comment"></span><span class="comment">// Class Expr methods //</span><span class="comment"></span>
<a name="l00042"></a>00042 <span class="comment">///////////////////////////////////////////////////////////////////////</span>
<a name="l00043"></a>00043 <span class="comment"></span>
<a name="l00044"></a><a class="code" href="group__ExprPkg.html#ga2605b52bcaa9bf4c04115a63ea773c9c">00044</a> vector<vector<Expr> > Expr::substTriggers(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr></a> & subst,
<a name="l00045"></a>00045 <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr></a> & visited)<span class="keyword"> const </span>{
<a name="l00046"></a>00046 <span class="comment">/* Do the substitution in triggers */</span>
<a name="l00047"></a>00047 vector<vector<Expr> > vvOldTriggers(getTriggers());
<a name="l00048"></a>00048 vector<vector<Expr> > vvNewTriggers;
<a name="l00049"></a>00049 vector<vector<Expr> >::const_iterator i, iEnd;
<a name="l00050"></a>00050 <span class="keywordflow">for</span>( i = vvOldTriggers.begin(), iEnd = vvOldTriggers.end(); i != iEnd; ++i ) {
<a name="l00051"></a>00051 vector<Expr> vOldTriggers(*i);
<a name="l00052"></a>00052 vector<Expr> vNewTriggers;
<a name="l00053"></a>00053 vector<Expr>::const_iterator j, jEnd;
<a name="l00054"></a>00054 <span class="keywordflow">for</span>( j = vOldTriggers.begin(), jEnd = vOldTriggers.end(); j != jEnd; ++j ) {
<a name="l00055"></a>00055 vNewTriggers.push_back((*j).recursiveSubst(subst, visited));
<a name="l00056"></a>00056 }
<a name="l00057"></a>00057 vvNewTriggers.push_back(vNewTriggers);
<a name="l00058"></a>00058 }
<a name="l00059"></a>00059
<a name="l00060"></a>00060 <span class="keywordflow">return</span> vvNewTriggers;
<a name="l00061"></a>00061 }
<a name="l00062"></a>00062
<a name="l00063"></a><a class="code" href="group__ExprPkg.html#ga7ee0a2ffca952496e3f1d8c9c9d66aab">00063</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> Expr::recursiveSubst(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr></a>& subst,
<a name="l00064"></a>00064 <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr></a>& visited)<span class="keyword"> const </span>{
<a name="l00065"></a>00065 <span class="comment">// Check the cache.</span>
<a name="l00066"></a>00066 <span class="comment">// INVARIANT: visited contains all the flagged expressions, and only those</span>
<a name="l00067"></a>00067 <span class="keywordflow">if</span>(getFlag()) <span class="keywordflow">return</span> visited[*<span class="keyword">this</span>];
<a name="l00068"></a>00068
<a name="l00069"></a>00069 <a class="code" href="namespaceCVC3.html#a4233916514848331ee104548acbab912" title="Expression index type.">ExprIndex</a> minIndex = 0;
<a name="l00070"></a>00070 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr>::const_iterator</a> i = subst.<a class="code" href="classCVC3_1_1ExprHashMap.html#a1a0ea7ed7eb73e3f08ccce9f29e90c71">begin</a>(),iend=subst.<a class="code" href="classCVC3_1_1ExprHashMap.html#a0ea2aa250fd1431c311d83f32862bba7">end</a>();i!=iend;++i) {
<a name="l00071"></a>00071 <span class="keywordflow">if</span>(minIndex > (i->first).getIndex())
<a name="l00072"></a>00072 minIndex = (i->first).getIndex();
<a name="l00073"></a>00073 }
<a name="l00074"></a>00074
<a name="l00075"></a>00075 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> replaced;
<a name="l00076"></a>00076
<a name="l00077"></a>00077 <span class="keywordflow">if</span>(isClosure()) {
<a name="l00078"></a>00078 <span class="keyword">const</span> vector<Expr> & vars = getVars();
<a name="l00079"></a>00079 vector<Expr> common; <span class="comment">// Bound vars which occur in subst</span>
<a name="l00080"></a>00080
<a name="l00081"></a>00081 <span class="keywordflow">for</span>(vector<Expr>::const_iterator i = vars.begin(), iend=vars.end();
<a name="l00082"></a>00082 i!=iend; ++i) {
<a name="l00083"></a>00083 <span class="keywordflow">if</span>(subst.<a class="code" href="classCVC3_1_1ExprHashMap.html#a7819727fbff7291cd64e99511d730bf7">count</a>(*i) > 0) common.push_back(*i);
<a name="l00084"></a>00084 }
<a name="l00085"></a>00085
<a name="l00086"></a>00086 <span class="keywordflow">if</span>(common.size() > 0) {
<a name="l00087"></a>00087 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(debugger.counter(<span class="stringliteral">"substExpr: bound var clashes"</span>)++;)
<a name="l00088"></a>00088 <span class="comment">// Reduced substitution (without the common vars)</span>
<a name="l00089"></a>00089 <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr></a> newSubst(subst);
<a name="l00090"></a>00090 <span class="comment">// Remove variables in "common" from the substitution</span>
<a name="l00091"></a>00091 <span class="keywordflow">for</span>(vector<Expr>::iterator i=common.begin(), iend=common.end();
<a name="l00092"></a>00092 i!=iend; ++i)
<a name="l00093"></a>00093 newSubst.erase(*i);
<a name="l00094"></a>00094
<a name="l00095"></a>00095 <span class="comment">// Clear all the caches (important!)</span>
<a name="l00096"></a>00096 visited.<a class="code" href="classCVC3_1_1ExprHashMap.html#aa20f14dba09537171af45bf479b99c66">clear</a>();
<a name="l00097"></a>00097 clearFlags();
<a name="l00098"></a>00098 visited = newSubst;
<a name="l00099"></a>00099
<a name="l00100"></a>00100 <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr>::iterator</a> j = newSubst.<a class="code" href="classCVC3_1_1ExprHashMap.html#a1a0ea7ed7eb73e3f08ccce9f29e90c71">begin</a>();
<a name="l00101"></a>00101 <span class="keywordflow">for</span> (; j != newSubst.<a class="code" href="classCVC3_1_1ExprHashMap.html#a0ea2aa250fd1431c311d83f32862bba7">end</a>(); ++j) { <span class="comment">// old vars bound in e</span>
<a name="l00102"></a>00102 j->first.setFlag();
<a name="l00103"></a>00103 }
<a name="l00104"></a>00104
<a name="l00105"></a>00105 vector<vector<Expr> > vvNewTriggers = substTriggers(newSubst,visited);
<a name="l00106"></a>00106
<a name="l00107"></a>00107 replaced =
<a name="l00108"></a>00108 getEM()->newClosureExpr(getKind(), vars,
<a name="l00109"></a>00109 getBody().recursiveSubst(newSubst, visited),
<a name="l00110"></a>00110 vvNewTriggers);
<a name="l00111"></a>00111
<a name="l00112"></a>00112 <span class="comment">// Clear the flags again, as we restore the substitution</span>
<a name="l00113"></a>00113 visited.<a class="code" href="classCVC3_1_1ExprHashMap.html#aa20f14dba09537171af45bf479b99c66">clear</a>();
<a name="l00114"></a>00114 clearFlags();
<a name="l00115"></a>00115 visited = subst;
<a name="l00116"></a>00116 <span class="comment">// Restore the flags on the original substitutions</span>
<a name="l00117"></a>00117 <span class="keywordflow">for</span> (<a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr>::const_iterator</a> i = subst.<a class="code" href="classCVC3_1_1ExprHashMap.html#a1a0ea7ed7eb73e3f08ccce9f29e90c71">begin</a>(), iend=subst.<a class="code" href="classCVC3_1_1ExprHashMap.html#a0ea2aa250fd1431c311d83f32862bba7">end</a>();
<a name="l00118"></a>00118 i != iend; ++i)
<a name="l00119"></a>00119 i->first.setFlag();
<a name="l00120"></a>00120 } <span class="keywordflow">else</span> {
<a name="l00121"></a>00121 vector<vector<Expr> > vvNewTriggers = substTriggers(subst,visited);
<a name="l00122"></a>00122 replaced =
<a name="l00123"></a>00123 getEM()->newClosureExpr(getKind(), vars,
<a name="l00124"></a>00124 getBody().recursiveSubst(subst, visited),
<a name="l00125"></a>00125 vvNewTriggers);
<a name="l00126"></a>00126 }
<a name="l00127"></a>00127 } <span class="keywordflow">else</span> { <span class="comment">// Not a Closure</span>
<a name="l00128"></a>00128 <span class="keywordtype">int</span> changed=0;
<a name="l00129"></a>00129 vector<Expr> children;
<a name="l00130"></a>00130 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> i=begin(), iend=end(); i!=iend; ++i){
<a name="l00131"></a>00131 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> repChild = *i;
<a name="l00132"></a>00132 <span class="keywordflow">if</span>(repChild.<a class="code" href="group__ExprPkg.html#gadaddb9b0566ecddd4611a10e820dc544">getIndex</a>() >= minIndex)
<a name="l00133"></a>00133 repChild = (*i).<a class="code" href="group__ExprPkg.html#ga7ee0a2ffca952496e3f1d8c9c9d66aab">recursiveSubst</a>(subst, visited);
<a name="l00134"></a>00134 <span class="keywordflow">if</span>(repChild != *i)
<a name="l00135"></a>00135 changed++;
<a name="l00136"></a>00136 children.push_back(repChild);
<a name="l00137"></a>00137 }
<a name="l00138"></a>00138 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> opExpr;
<a name="l00139"></a>00139 <span class="keywordflow">if</span> (isApply()) {
<a name="l00140"></a>00140 opExpr = getOpExpr().<a class="code" href="group__ExprPkg.html#ga7ee0a2ffca952496e3f1d8c9c9d66aab">recursiveSubst</a>(subst, visited);
<a name="l00141"></a>00141 <span class="keywordflow">if</span> (opExpr != getOpExpr()) ++changed;
<a name="l00142"></a>00142 }
<a name="l00143"></a>00143 <span class="keywordflow">if</span>(changed > 0) {
<a name="l00144"></a>00144 <a class="code" href="classCVC3_1_1Op.html">Op</a> op = opExpr.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>() ? getOp() : opExpr.<a class="code" href="group__ExprPkg.html#ga3aefe2fb15c2d8e3a51dd92dbcc5cdc5" title="Make the expr into an operator.">mkOp</a>();
<a name="l00145"></a>00145 replaced = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(op, children);
<a name="l00146"></a>00146 }
<a name="l00147"></a>00147 <span class="keywordflow">else</span> replaced = *<span class="keyword">this</span>;
<a name="l00148"></a>00148 }
<a name="l00149"></a>00149 visited.<a class="code" href="classCVC3_1_1ExprHashMap.html#a7fb3e24bb67239243212af626cc2f976">insert</a>(*<span class="keyword">this</span>, replaced);
<a name="l00150"></a>00150 setFlag();
<a name="l00151"></a>00151 <span class="keywordflow">return</span> replaced;
<a name="l00152"></a>00152 }
<a name="l00153"></a>00153
<a name="l00154"></a>00154
<a name="l00155"></a><a class="code" href="namespaceCVC3.html#a71ce1d03bd881f18ed36104cfa093212">00155</a> <span class="keyword">static</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a71ce1d03bd881f18ed36104cfa093212">subExprRec</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e2) {
<a name="l00156"></a>00156 <span class="keywordflow">if</span>(e1 == e2) <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00157"></a>00157 <span class="keywordflow">if</span>(e2.<a class="code" href="group__ExprPkg.html#gab9779994b0bb78e555c4f9e2163571ed" title="Check if the generic flag is set.">getFlag</a>()) <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00158"></a>00158 <span class="comment">// e1 is created after e2, so e1 cannot be a subexpr of e2</span>
<a name="l00159"></a>00159 <span class="keywordflow">if</span>(e1 > e2) <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00160"></a>00160 e2.<a class="code" href="group__ExprPkg.html#ga4695a56a4bdc943174eda1f41cbcead4" title="Set the generic flag.">setFlag</a>();
<a name="l00161"></a>00161 <span class="keywordtype">bool</span> res(<span class="keyword">false</span>);
<a name="l00162"></a>00162 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> i=e2.<a class="code" href="group__ExprPkg.html#gac890e13db184610276fc533fa4b4fe99" title="Begin iterator.">begin</a>(), iend=e2.<a class="code" href="group__ExprPkg.html#gaf6048a5030c8fa2511bf5dfee868e653" title="End iterator.">end</a>(); !res && i!=iend; ++i)
<a name="l00163"></a>00163 res = <a class="code" href="namespaceCVC3.html#a71ce1d03bd881f18ed36104cfa093212">subExprRec</a>(e1, *i);
<a name="l00164"></a>00164 <span class="keywordflow">return</span> res;
<a name="l00165"></a>00165 }
<a name="l00166"></a>00166
<a name="l00167"></a>00167
<a name="l00168"></a>00168 <span class="keywordtype">bool</span>
<a name="l00169"></a><a class="code" href="group__ExprPkg.html#ga4b89f3d46b36f66acb191a4fb359d69f">00169</a> Expr::subExprOf(<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="l00170"></a>00170 <span class="keywordflow">if</span>(*<span class="keyword">this</span> == e) <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00171"></a>00171 <span class="comment">// "this" is created after e, so it cannot be e's subexpression</span>
<a name="l00172"></a>00172 <span class="keywordflow">if</span>(*<span class="keyword">this</span> > e) <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00173"></a>00173 clearFlags();
<a name="l00174"></a>00174 <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#a71ce1d03bd881f18ed36104cfa093212">subExprRec</a>(*<span class="keyword">this</span>, e);
<a name="l00175"></a>00175 }
<a name="l00176"></a>00176
<a name="l00177"></a>00177
<a name="l00178"></a><a class="code" href="group__ExprPkg.html#ga95e18015860195a80b317bf756055786">00178</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> Expr::substExpr(<span class="keyword">const</span> vector<Expr>& oldTerms,
<a name="l00179"></a>00179 <span class="keyword">const</span> vector<Expr>& newTerms)<span class="keyword"> const</span>
<a name="l00180"></a>00180 <span class="keyword"></span>{
<a name="l00181"></a>00181 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(oldTerms.size() == newTerms.size(), <span class="stringliteral">"substExpr: vectors"</span>
<a name="l00182"></a>00182 <span class="stringliteral">"don't match in size"</span>);
<a name="l00183"></a>00183 <span class="comment">// Catch the vacuous case</span>
<a name="l00184"></a>00184 <span class="keywordflow">if</span>(oldTerms.size() == 0) <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00185"></a>00185
<a name="l00186"></a>00186 <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr></a> oldToNew(10);
<a name="l00187"></a>00187 clearFlags();
<a name="l00188"></a>00188 <span class="keywordflow">for</span>(<span class="keywordtype">unsigned</span> <span class="keywordtype">int</span> i=0; i<oldTerms.size(); i++) {
<a name="l00189"></a>00189 oldToNew.<a class="code" href="classCVC3_1_1ExprHashMap.html#a7fb3e24bb67239243212af626cc2f976">insert</a>(oldTerms[i], newTerms[i]);
<a name="l00190"></a>00190 oldTerms[i].setFlag();
<a name="l00191"></a>00191 }
<a name="l00192"></a>00192 <span class="comment">// For cache, initialized by the substitution</span>
<a name="l00193"></a>00193 <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr></a> visited(oldToNew);
<a name="l00194"></a>00194 <span class="keywordflow">return</span> recursiveSubst(oldToNew, visited);
<a name="l00195"></a>00195
<a name="l00196"></a>00196 }
<a name="l00197"></a>00197
<a name="l00198"></a>00198
<a name="l00199"></a><a class="code" href="group__ExprPkg.html#ga266ba75d3cf61c772b26a36ef5909a52">00199</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> Expr::substExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr></a>& oldToNew)<span class="keyword"> const</span>
<a name="l00200"></a>00200 <span class="keyword"></span>{
<a name="l00201"></a>00201 <span class="comment">// Catch the vacuous case</span>
<a name="l00202"></a>00202 <span class="keywordflow">if</span>(oldToNew.<a class="code" href="classCVC3_1_1ExprHashMap.html#a9d792cf5282604c376d329ae325c983e">size</a>() == 0) <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00203"></a>00203 <span class="comment">// Rebuild the map: we'll be using it as a cache</span>
<a name="l00204"></a>00204 <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr></a> visited(oldToNew);
<a name="l00205"></a>00205 clearFlags();
<a name="l00206"></a>00206 <span class="comment">// Flag all the LHS expressions in oldToNew map. We'll be checking</span>
<a name="l00207"></a>00207 <span class="comment">// all flagged expressions (and only those) for substitution.</span>
<a name="l00208"></a>00208 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr>::const_iterator</a> i=oldToNew.<a class="code" href="classCVC3_1_1ExprHashMap.html#a1a0ea7ed7eb73e3f08ccce9f29e90c71">begin</a>(), iend=oldToNew.<a class="code" href="classCVC3_1_1ExprHashMap.html#a0ea2aa250fd1431c311d83f32862bba7">end</a>();
<a name="l00209"></a>00209 i!=iend; ++i) {
<a name="l00210"></a>00210 (*i).first.setFlag();
<a name="l00211"></a>00211 }
<a name="l00212"></a>00212 <span class="keywordflow">return</span> recursiveSubst(oldToNew, visited);
<a name="l00213"></a>00213 }
<a name="l00214"></a>00214
<a name="l00215"></a>00215
<a name="l00216"></a>00216
<a name="l00217"></a><a class="code" href="group__ExprPkg.html#ga7cbbc123771321651e176a346731d255">00217</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> Expr::substExprQuant(<span class="keyword">const</span> vector<Expr>& oldTerms,
<a name="l00218"></a>00218 <span class="keyword">const</span> vector<Expr>& newTerms)<span class="keyword"> const</span>
<a name="l00219"></a>00219 <span class="keyword"></span>{
<a name="l00220"></a>00220 <span class="comment">//let us disable this first yeting</span>
<a name="l00221"></a>00221 <span class="comment">// static ExprHashMap<Expr> substCache;</span>
<a name="l00222"></a>00222 <span class="comment">// Expr cacheIndex = Expr(RAW_LIST, *this, Expr(RAW_LIST, newTerms));</span>
<a name="l00223"></a>00223
<a name="l00224"></a>00224 <span class="comment">// ExprHashMap<Expr>::iterator i = substCache.find(cacheIndex);</span>
<a name="l00225"></a>00225 <span class="comment">// if (i != substCache.end()){</span>
<a name="l00226"></a>00226 <span class="comment">// return i->second;</span>
<a name="l00227"></a>00227 <span class="comment">// }</span>
<a name="l00228"></a>00228
<a name="l00229"></a>00229 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(oldTerms.size() == newTerms.size(), <span class="stringliteral">"substExpr: vectors"</span>
<a name="l00230"></a>00230 <span class="stringliteral">"don't match in size"</span>);
<a name="l00231"></a>00231 <span class="comment">// Catch the vacuous case</span>
<a name="l00232"></a>00232
<a name="l00233"></a>00233 <span class="keywordflow">if</span>(oldTerms.size() == 0) <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00234"></a>00234
<a name="l00235"></a>00235 <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr></a> oldToNew(oldTerms.size());
<a name="l00236"></a>00236
<a name="l00237"></a>00237 <span class="comment">// clearFlags();</span>
<a name="l00238"></a>00238 <span class="keywordflow">for</span>(<span class="keywordtype">unsigned</span> <span class="keywordtype">int</span> i=0; i<oldTerms.size(); i++) {
<a name="l00239"></a>00239 oldToNew.<a class="code" href="classCVC3_1_1ExprHashMap.html#a7fb3e24bb67239243212af626cc2f976">insert</a>(oldTerms[i], newTerms[i]);
<a name="l00240"></a>00240 <span class="comment">// oldTerms[i].setFlag();</span>
<a name="l00241"></a>00241 }
<a name="l00242"></a>00242
<a name="l00243"></a>00243 <span class="comment">// For cache, initialized by the substitution</span>
<a name="l00244"></a>00244 <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr></a> visited(oldToNew);
<a name="l00245"></a>00245 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> returnExpr = recursiveQuantSubst(oldToNew, visited);;
<a name="l00246"></a>00246
<a name="l00247"></a>00247 <span class="comment">// substCache[cacheIndex] = returnExpr;</span>
<a name="l00248"></a>00248 <span class="comment">// cout<<"pushed " << cacheIndex << endl << "RET " << returnExpr << endl;</span>
<a name="l00249"></a>00249
<a name="l00250"></a>00250 <span class="keywordflow">return</span> returnExpr;
<a name="l00251"></a>00251
<a name="l00252"></a>00252 }
<a name="l00253"></a>00253
<a name="l00254"></a><a class="code" href="group__ExprPkg.html#ga6d955aae7246b6e55c7de394fe7895d4">00254</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> Expr::substExprQuant(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr></a>& oldToNew)<span class="keyword"> const</span>
<a name="l00255"></a>00255 <span class="keyword"></span>{
<a name="l00256"></a>00256 <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr></a> visited(oldToNew);
<a name="l00257"></a>00257 <span class="keywordflow">return</span> recursiveQuantSubst(oldToNew,visited);
<a name="l00258"></a>00258 }
<a name="l00259"></a>00259
<a name="l00260"></a><a class="code" href="group__ExprPkg.html#ga644bfdf1ae59727d6626c764208483e8">00260</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> Expr::recursiveQuantSubst(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr></a>& substMap,
<a name="l00261"></a>00261 <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr></a>& visited)<span class="keyword"> const </span>{
<a name="l00262"></a>00262 <span class="comment">/* [chris 12/3/2009] It appears that visited is never used. */</span>
<a name="l00263"></a>00263
<a name="l00264"></a>00264 <span class="keywordflow">if</span> (!containsBoundVar()){
<a name="l00265"></a>00265 <span class="comment">// std::cout <<"no bound var " << *this << std::endl;</span>
<a name="l00266"></a>00266 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00267"></a>00267 }
<a name="l00268"></a>00268
<a name="l00269"></a>00269 <span class="comment">// Check the cache.</span>
<a name="l00270"></a>00270 <span class="comment">// INVARIANT: visited contains all the flagged expressions, and only those</span>
<a name="l00271"></a>00271 <span class="comment">// the above invariant is no longer true. yeting</span>
<a name="l00272"></a>00272
<a name="l00273"></a>00273 <span class="keywordflow">if</span>(getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba462c38186c36e12c2f38a6d0d43feddf">BOUND_VAR</a> ) {
<a name="l00274"></a>00274 <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr>::const_iterator</a> find = substMap.<a class="code" href="classCVC3_1_1ExprHashMap.html#aeffd58f05fbeb8f381ba2050adef7a2d">find</a>(*<span class="keyword">this</span>);
<a name="l00275"></a>00275 <span class="keywordflow">if</span> (find != substMap.<a class="code" href="classCVC3_1_1ExprHashMap.html#a0ea2aa250fd1431c311d83f32862bba7">end</a>()) {
<a name="l00276"></a>00276 <span class="keywordflow">return</span> find->second;
<a name="l00277"></a>00277 }
<a name="l00278"></a>00278 <span class="comment">/*</span>
<a name="l00279"></a>00279 <span class="comment"> // Expr ret = visited[*this];</span>
<a name="l00280"></a>00280 <span class="comment"> const Expr ret = substMap[*this];</span>
<a name="l00281"></a>00281 <span class="comment"> if (!ret.isNull()){</span>
<a name="l00282"></a>00282 <span class="comment"> return ret; </span>
<a name="l00283"></a>00283 <span class="comment"> }</span>
<a name="l00284"></a>00284 <span class="comment">*/</span>
<a name="l00285"></a>00285 }
<a name="l00286"></a>00286
<a name="l00287"></a>00287 <span class="comment">// if(getFlag()) return visited[*this];</span>
<a name="l00288"></a>00288
<a name="l00289"></a>00289 <span class="comment">// why we need this.</span>
<a name="l00290"></a>00290 <span class="comment">// ExprIndex minIndex = 0;</span>
<a name="l00291"></a>00291 <span class="comment">// for(ExprHashMap<Expr>::iterator i = substMap.begin(),iend=substMap.end();i!=iend;++i) {</span>
<a name="l00292"></a>00292 <span class="comment">// if(minIndex > (i->first).getIndex())</span>
<a name="l00293"></a>00293 <span class="comment">// minIndex = (i->first).getIndex();</span>
<a name="l00294"></a>00294 <span class="comment">// }</span>
<a name="l00295"></a>00295
<a name="l00296"></a>00296 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> replaced;
<a name="l00297"></a>00297
<a name="l00298"></a>00298 <span class="keywordflow">if</span>(isClosure()) {
<a name="l00299"></a>00299 <span class="comment">// for safety, we can wrap the following lines by if debug</span>
<a name="l00300"></a>00300
<a name="l00301"></a>00301 <span class="keyword">const</span> vector<Expr> & vars = getVars();
<a name="l00302"></a>00302 <span class="comment">// vector<Expr> common; // Bound vars which occur in subst</span>
<a name="l00303"></a>00303
<a name="l00304"></a>00304 <span class="comment">// for(vector<Expr>::const_iterator i = vars.begin(), iend=vars.end();</span>
<a name="l00305"></a>00305 <span class="comment">// i!=iend; ++i) {</span>
<a name="l00306"></a>00306 <span class="comment">// if(substMap.count(*i) > 0) common.push_back(*i);</span>
<a name="l00307"></a>00307 <span class="comment">// }</span>
<a name="l00308"></a>00308
<a name="l00309"></a>00309 <span class="comment">// if(common.size() > 0) {</span>
<a name="l00310"></a>00310 <span class="comment">// cout<<"error in quant subst" << endl;</span>
<a name="l00311"></a>00311 <span class="comment">// } else {</span>
<a name="l00312"></a>00312
<a name="l00313"></a>00313 <span class="comment">/* Perform substition on the triggers */</span>
<a name="l00314"></a>00314
<a name="l00315"></a>00315 vector<vector<Expr> > vvNewTriggers = substTriggers(substMap,visited);
<a name="l00316"></a>00316 replaced =
<a name="l00317"></a>00317 getEM()->newClosureExpr(getKind(), vars,
<a name="l00318"></a>00318 getBody().recursiveQuantSubst(substMap, visited),
<a name="l00319"></a>00319 vvNewTriggers );
<a name="l00320"></a>00320 <span class="comment">// }</span>
<a name="l00321"></a>00321 } <span class="keywordflow">else</span> { <span class="comment">// Not a Closure</span>
<a name="l00322"></a>00322 <span class="keywordtype">int</span> changed=0;
<a name="l00323"></a>00323 vector<Expr> children;
<a name="l00324"></a>00324 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> i=begin(), iend=end(); i!=iend; ++i){
<a name="l00325"></a>00325 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> repChild ;
<a name="l00326"></a>00326 repChild = (*i).<a class="code" href="group__ExprPkg.html#ga644bfdf1ae59727d6626c764208483e8">recursiveQuantSubst</a>(substMap, visited);
<a name="l00327"></a>00327 <span class="keywordflow">if</span>(repChild != *i)
<a name="l00328"></a>00328 changed++;
<a name="l00329"></a>00329 children.push_back(repChild);
<a name="l00330"></a>00330 }
<a name="l00331"></a>00331 <span class="keywordflow">if</span>(changed > 0)
<a name="l00332"></a>00332 replaced = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(getOp(), children);
<a name="l00333"></a>00333 <span class="keywordflow">else</span>
<a name="l00334"></a>00334 replaced = *<span class="keyword">this</span>;
<a name="l00335"></a>00335 }
<a name="l00336"></a>00336 <span class="comment">// visited.insert(*this, replaced);</span>
<a name="l00337"></a>00337 <span class="comment">// setFlag();</span>
<a name="l00338"></a>00338 <span class="keywordflow">return</span> replaced;
<a name="l00339"></a>00339 }
<a name="l00340"></a>00340
<a name="l00341"></a>00341
<a name="l00342"></a>00342
<a name="l00343"></a>00343
<a name="l00344"></a><a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54">00344</a> <span class="keywordtype">string</span> Expr::toString()<span class="keyword"> const </span>{
<a name="l00345"></a>00345 <span class="keywordflow">return</span> toString(<a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0eaa315c228d5c3290ce37df81524ed8e9a" title="Nice SAL-like language for manually written specs.">PRESENTATION_LANG</a>);
<a name="l00346"></a>00346 <span class="comment">// if(isNull()) return "Null";</span>
<a name="l00347"></a>00347 <span class="comment">// ostringstream ss;</span>
<a name="l00348"></a>00348 <span class="comment">// ss << (*this);</span>
<a name="l00349"></a>00349 <span class="comment">// return ss.str();</span>
<a name="l00350"></a>00350 }
<a name="l00351"></a>00351
<a name="l00352"></a><a class="code" href="group__ExprPkg.html#ga306e932ab9a486c9350d55e216ae0de5">00352</a> <span class="keywordtype">string</span> Expr::toString(<a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e" title="Different input languages.">InputLanguage</a> lang)<span class="keyword"> const </span>{
<a name="l00353"></a>00353 <span class="keywordflow">if</span>(isNull()) <span class="keywordflow">return</span> <span class="stringliteral">"Null"</span>;
<a name="l00354"></a>00354 ostringstream ss;
<a name="l00355"></a>00355 <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a> os(getEM());
<a name="l00356"></a>00356 os.<a class="code" href="classCVC3_1_1ExprStream.html#ac2b2872228aff3fd5d08bbd69c672543" title="Get the current output language.">lang</a>(lang);
<a name="l00357"></a>00357 os.<a class="code" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512" title="Set a new output stream.">os</a>(ss);
<a name="l00358"></a>00358 os << (*this);
<a name="l00359"></a>00359 <span class="keywordflow">return</span> ss.str();
<a name="l00360"></a>00360 }
<a name="l00361"></a>00361
<a name="l00362"></a><a class="code" href="group__ExprPkg.html#ga76180628bc1561af88e41be586973fac">00362</a> <span class="keywordtype">void</span> Expr::print(<a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e" title="Different input languages.">InputLanguage</a> lang, <span class="keywordtype">bool</span> dagify)<span class="keyword"> const </span>{
<a name="l00363"></a>00363 <span class="keywordflow">if</span>(isNull()) {
<a name="l00364"></a>00364 cout << <span class="stringliteral">"Null"</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>; <span class="keywordflow">return</span>;
<a name="l00365"></a>00365 }
<a name="l00366"></a>00366 <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a> os(getEM());
<a name="l00367"></a>00367 os.<a class="code" href="classCVC3_1_1ExprStream.html#ac2b2872228aff3fd5d08bbd69c672543" title="Get the current output language.">lang</a>(lang);
<a name="l00368"></a>00368 os.<a class="code" href="classCVC3_1_1ExprStream.html#a2d4ff13cb98b358eb02dfbf149ae03ae" title="Set the DAG flag (return previous value)">dagFlag</a>(dagify);
<a name="l00369"></a>00369 os << *<span class="keyword">this</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00370"></a>00370 }
<a name="l00371"></a>00371
<a name="l00372"></a>00372
<a name="l00373"></a><a class="code" href="group__ExprPkg.html#ga3aa47bf8af3f2c88b8bc27e0cd07554e">00373</a> <span class="keywordtype">void</span> Expr::pprint()<span class="keyword"> const</span>
<a name="l00374"></a>00374 <span class="keyword"></span>{
<a name="l00375"></a>00375 <span class="keywordflow">if</span>(isNull()) {
<a name="l00376"></a>00376 cout << <span class="stringliteral">"Null"</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>; <span class="keywordflow">return</span>;
<a name="l00377"></a>00377 }
<a name="l00378"></a>00378 <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a> os(getEM());
<a name="l00379"></a>00379 os << *<span class="keyword">this</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00380"></a>00380 }
<a name="l00381"></a>00381
<a name="l00382"></a>00382
<a name="l00383"></a><a class="code" href="group__ExprPkg.html#ga010ae48d41f33790c6b9bb10829105e3">00383</a> <span class="keywordtype">void</span> Expr::pprintnodag()<span class="keyword"> const</span>
<a name="l00384"></a>00384 <span class="keyword"></span>{
<a name="l00385"></a>00385 <span class="keywordflow">if</span>(isNull()) {
<a name="l00386"></a>00386 cout << <span class="stringliteral">"Null"</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>; <span class="keywordflow">return</span>;
<a name="l00387"></a>00387 }
<a name="l00388"></a>00388 <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a> os(getEM());
<a name="l00389"></a>00389 os.<a class="code" href="classCVC3_1_1ExprStream.html#a2d4ff13cb98b358eb02dfbf149ae03ae" title="Set the DAG flag (return previous value)">dagFlag</a>(<span class="keyword">false</span>);
<a name="l00390"></a>00390 os << *<span class="keyword">this</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00391"></a>00391 }
<a name="l00392"></a>00392
<a name="l00393"></a>00393
<a name="l00394"></a><a class="code" href="group__ExprPkg.html#ga974964d4dba5b50f35ee03e2418e7fe9">00394</a> <span class="keywordtype">void</span> Expr::printnodag()<span class="keyword"> const</span>
<a name="l00395"></a>00395 <span class="keyword"></span>{
<a name="l00396"></a>00396 print(<a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0ea0ee28952d729595b97a9e592975d1521">AST_LANG</a>, <span class="keyword">false</span>);
<a name="l00397"></a>00397 }
<a name="l00398"></a>00398
<a name="l00399"></a>00399
<a name="l00400"></a><a class="code" href="group__ExprPkg.html#ga092308b0a88e12a5c7ff2fc0a2eca818">00400</a> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& Expr::printAST(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os)<span class="keyword"> const </span>{
<a name="l00401"></a>00401 <span class="keywordflow">if</span>(isNull()) <span class="keywordflow">return</span> os << <span class="stringliteral">"Null"</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00402"></a>00402 <span class="keywordtype">bool</span> isLetDecl(getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9508dd8c8e7db280a5dacc19bd74d92d">LETDECL</a>);
<a name="l00403"></a>00403 os << <span class="stringliteral">"("</span> << <a class="code" href="group__ExprStream__Manip.html#ga2a0348c6d3f94f2f8febc6dd0a9c3218" title="Set the indentation to the current position.">push</a>;
<a name="l00404"></a>00404 os << getEM()->getKindName(getKind());
<a name="l00405"></a>00405 <span class="keywordflow">if</span> (isApply()) {
<a name="l00406"></a>00406 os << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a> << <span class="stringliteral">"{"</span> << getOp().getExpr() << push << <span class="stringliteral">"}"</span>;
<a name="l00407"></a>00407 }
<a name="l00408"></a>00408 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (isSymbol()) {
<a name="l00409"></a>00409 os << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a> << <span class="stringliteral">"{Symbol: "</span> << getName() << <span class="stringliteral">"}"</span>;
<a name="l00410"></a>00410 }
<a name="l00411"></a>00411 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (isClosure()) {
<a name="l00412"></a>00412 os << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a> << <span class="stringliteral">"{"</span> << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a> << <span class="stringliteral">"("</span> << <a class="code" href="group__ExprStream__Manip.html#ga2a0348c6d3f94f2f8febc6dd0a9c3218" title="Set the indentation to the current position.">push</a>;
<a name="l00413"></a>00413 <span class="keyword">const</span> vector<Expr>& vars = getVars();
<a name="l00414"></a>00414 vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
<a name="l00415"></a>00415 <span class="keywordflow">if</span>(i!=iend) { os << *i; ++i; }
<a name="l00416"></a>00416 <span class="keywordflow">for</span>(; i!=iend; ++i) os << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a> << *i;
<a name="l00417"></a>00417 os << push << <span class="stringliteral">") "</span> << <a class="code" href="group__ExprStream__Manip.html#gaddb050a787be87116afc51791293d3be" title="Restore the indentation.">pop</a> << <a class="code" href="group__ExprStream__Manip.html#gaddb050a787be87116afc51791293d3be" title="Restore the indentation.">pop</a>;
<a name="l00418"></a>00418 os << getBody() << push << <span class="stringliteral">"}"</span>;
<a name="l00419"></a>00419 }
<a name="l00420"></a>00420 <span class="keywordflow">else</span> {
<a name="l00421"></a>00421 <span class="keywordflow">switch</span>(getKind()) {
<a name="l00422"></a>00422 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba354df7c2d2ec2e54317f07437dc7380b">STRING_EXPR</a>:
<a name="l00423"></a>00423 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(isString(), <span class="stringliteral">"Expected String"</span>);
<a name="l00424"></a>00424 os << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a> << <span class="stringliteral">"{"</span> << <span class="charliteral">'"'</span>+ getString() + <span class="charliteral">'"'</span> << <span class="stringliteral">"}"</span>;
<a name="l00425"></a>00425 <span class="keywordflow">break</span>;
<a name="l00426"></a>00426 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba73072b2c6fef896d006d6691e932cf37">SKOLEM_VAR</a>:
<a name="l00427"></a>00427 getExistential();
<a name="l00428"></a>00428 os << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a> << <span class="stringliteral">"{SKOLEM_"</span> << (int)getIndex() << <span class="stringliteral">"}"</span>;
<a name="l00429"></a>00429 <span class="keywordflow">break</span>;
<a name="l00430"></a>00430 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bae07a708ec52c578b62f8b0f701571d56">RATIONAL_EXPR</a>:
<a name="l00431"></a>00431 os << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a> << <span class="stringliteral">"{"</span> << getRational() << <span class="stringliteral">"}"</span>;
<a name="l00432"></a>00432 <span class="keywordflow">break</span>;
<a name="l00433"></a>00433 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2efaeb22f8803588598706b73cec8bda">UCONST</a>:
<a name="l00434"></a>00434 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(isVar(), <span class="stringliteral">"Expected Var"</span>);
<a name="l00435"></a>00435 os << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a> << <span class="stringliteral">"{"</span> << getName() << <span class="stringliteral">"}"</span>;
<a name="l00436"></a>00436 <span class="keywordflow">break</span>;
<a name="l00437"></a>00437 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba462c38186c36e12c2f38a6d0d43feddf">BOUND_VAR</a>:
<a name="l00438"></a>00438 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(isVar(), <span class="stringliteral">"Expected Var"</span>);
<a name="l00439"></a>00439 os << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a> << <span class="stringliteral">"{"</span>+getName()+<span class="stringliteral">"_"</span>+getUid()+<span class="stringliteral">"}"</span>;
<a name="l00440"></a>00440 <span class="keywordflow">break</span>;
<a name="l00441"></a>00441 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bada5edea8bbb7cfbd2500be6eca0d4151">THEOREM_KIND</a>:
<a name="l00442"></a>00442 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(isTheorem(), <span class="stringliteral">"Expected Theorem"</span>);
<a name="l00443"></a>00443 os << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a> << <span class="stringliteral">"{Theorem: "</span> << getTheorem().toString() << <span class="stringliteral">"}"</span>;
<a name="l00444"></a>00444 <span class="keywordflow">default</span>: ; <span class="comment">// Don't do anything</span>
<a name="l00445"></a>00445 }
<a name="l00446"></a>00446 }
<a name="l00447"></a>00447
<a name="l00448"></a>00448 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> i=begin(), iend=end(); i!=iend; ++i) {
<a name="l00449"></a>00449 <span class="keywordflow">if</span>(isLetDecl) os << <a class="code" href="group__ExprStream__Manip.html#gab9909b3108229b630956179ebd71f3ef">nodag</a>;
<a name="l00450"></a>00450 os << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a> << *i;
<a name="l00451"></a>00451 }
<a name="l00452"></a>00452 os << push << <span class="stringliteral">")"</span>;
<a name="l00453"></a>00453 os.<a class="code" href="classCVC3_1_1ExprStream.html#a946110c3457868fe38ce8c1d4cdde916" title="Reset indentation to what it was at this level.">resetIndent</a>();
<a name="l00454"></a>00454 <span class="keywordflow">return</span> os;
<a name="l00455"></a>00455 }
<a name="l00456"></a>00456
<a name="l00457"></a>00457
<a name="l00458"></a><a class="code" href="group__ExprPkg.html#gaa26519c37fd631580f14664d83dcb4fa">00458</a> <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& Expr::print(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os)<span class="keyword"> const </span>{
<a name="l00459"></a>00459 <span class="keywordflow">if</span>(isNull()) <span class="keywordflow">return</span> os << <span class="stringliteral">"Null"</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00460"></a>00460 <span class="keywordflow">if</span> (isSymbol()) <span class="keywordflow">return</span> os << getName();
<a name="l00461"></a>00461 <span class="keywordflow">switch</span>(getKind()) {
<a name="l00462"></a>00462 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba1fad76919fba496de21807e2beec533d">TRUE_EXPR</a>: <span class="keywordflow">return</span> os << <span class="stringliteral">"TRUE"</span>;
<a name="l00463"></a>00463 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5f71bd33a6528411ae681f5291de1d82">FALSE_EXPR</a>: <span class="keywordflow">return</span> os << <span class="stringliteral">"FALSE"</span>;
<a name="l00464"></a>00464 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5bc05ce87fa69f660d39d0a4fa188c67">NULL_KIND</a>: <span class="keywordflow">return</span> os << <span class="stringliteral">"Null"</span>;
<a name="l00465"></a>00465 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba354df7c2d2ec2e54317f07437dc7380b">STRING_EXPR</a>: <span class="keywordflow">return</span> os << <span class="charliteral">'"'</span>+ getString() + <span class="charliteral">'"'</span>;
<a name="l00466"></a>00466 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bae07a708ec52c578b62f8b0f701571d56">RATIONAL_EXPR</a>: <span class="keywordflow">return</span> os << getRational();
<a name="l00467"></a>00467 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba73072b2c6fef896d006d6691e932cf37">SKOLEM_VAR</a>: <span class="keywordflow">return</span> os << <span class="stringliteral">"SKOLEM_"</span> << <a class="code" href="structHash_1_1hash.html">hash</a>();
<a name="l00468"></a>00468 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2efaeb22f8803588598706b73cec8bda">UCONST</a>: <span class="keywordflow">return</span> os << getName();
<a name="l00469"></a>00469 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba462c38186c36e12c2f38a6d0d43feddf">BOUND_VAR</a>: <span class="keywordflow">return</span> os << <span class="stringliteral">"(BOUND_VAR "</span>+getName()+<span class="stringliteral">"_"</span>+getUid()+<span class="stringliteral">")"</span>;
<a name="l00470"></a>00470 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a>: {
<a name="l00471"></a>00471 os << <span class="stringliteral">"("</span> << <a class="code" href="group__ExprStream__Manip.html#ga2a0348c6d3f94f2f8febc6dd0a9c3218" title="Set the indentation to the current position.">push</a>;
<a name="l00472"></a>00472 <span class="keywordtype">bool</span> firstTime(<span class="keyword">true</span>);
<a name="l00473"></a>00473 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> i=begin(), iend=end(); i!=iend; ++i) {
<a name="l00474"></a>00474 <span class="keywordflow">if</span>(firstTime) firstTime = <span class="keyword">false</span>;
<a name="l00475"></a>00475 <span class="keywordflow">else</span> os << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a>;
<a name="l00476"></a>00476 os << *i;
<a name="l00477"></a>00477 }
<a name="l00478"></a>00478 <span class="keywordflow">return</span> os << push << <span class="stringliteral">")"</span>;
<a name="l00479"></a>00479 }
<a name="l00480"></a>00480 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7b7b6f6e2b88589bd4656a14bcb7eb94">FORALL</a>:
<a name="l00481"></a>00481 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3197625a1bb2264943f5a95f236d9973">EXISTS</a>:
<a name="l00482"></a>00482 <span class="keywordflow">if</span>(isQuantifier()) {
<a name="l00483"></a>00483 os << <span class="stringliteral">"("</span> << <a class="code" href="group__ExprStream__Manip.html#ga2a0348c6d3f94f2f8febc6dd0a9c3218" title="Set the indentation to the current position.">push</a> << getEM()->getKindName(getKind())
<a name="l00484"></a>00484 << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a> << <span class="stringliteral">"("</span> << <a class="code" href="group__ExprStream__Manip.html#ga2a0348c6d3f94f2f8febc6dd0a9c3218" title="Set the indentation to the current position.">push</a>;
<a name="l00485"></a>00485 <span class="keyword">const</span> vector<Expr>& vars = getVars();
<a name="l00486"></a>00486 vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
<a name="l00487"></a>00487 <span class="keywordflow">if</span>(i!=iend) { os << *i; ++i; }
<a name="l00488"></a>00488 <span class="keywordflow">for</span>(; i!=iend; ++i) os << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a> << *i;
<a name="l00489"></a>00489 os << push << <span class="stringliteral">") "</span> << <a class="code" href="group__ExprStream__Manip.html#gaddb050a787be87116afc51791293d3be" title="Restore the indentation.">pop</a> << <a class="code" href="group__ExprStream__Manip.html#gaddb050a787be87116afc51791293d3be" title="Restore the indentation.">pop</a>;
<a name="l00490"></a>00490 <span class="keywordflow">return</span> os << getBody() << push << <span class="stringliteral">")"</span>;
<a name="l00491"></a>00491 }
<a name="l00492"></a>00492 <span class="comment">// If not an internal representation of quantifiers, it'll be</span>
<a name="l00493"></a>00493 <span class="comment">// printed as "normal" Expr with a kind and children</span>
<a name="l00494"></a>00494 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba262553c759e1d1a9398bc406b1fadcb7">RESTART</a>: <span class="keywordflow">return</span> os << <span class="stringliteral">"RESTART "</span> << (*this)[0] << <span class="stringliteral">";"</span>;
<a name="l00495"></a>00495 <span class="keywordflow">default</span>:
<a name="l00496"></a>00496 <span class="comment">// os << "(" << push;</span>
<a name="l00497"></a>00497 os << getEM()->getKindName(getKind());
<a name="l00498"></a>00498 <span class="comment">// os << push << ")";</span>
<a name="l00499"></a>00499 }
<a name="l00500"></a>00500 os.<a class="code" href="classCVC3_1_1ExprStream.html#a946110c3457868fe38ce8c1d4cdde916" title="Reset indentation to what it was at this level.">resetIndent</a>();
<a name="l00501"></a>00501 <span class="keywordflow">return</span> os;
<a name="l00502"></a>00502 }
<a name="l00503"></a>00503
<a name="l00504"></a>00504 <span class="comment"></span>
<a name="l00505"></a>00505 <span class="comment">//! Set initial indentation to n.</span>
<a name="l00506"></a>00506 <span class="comment"></span><span class="comment">/*! The indentation will be reset to default unless the second</span>
<a name="l00507"></a>00507 <span class="comment"> argument is true. This setting only takes effect when printing to</span>
<a name="l00508"></a>00508 <span class="comment"> std::ostream. When printing to ExprStream, the indentation can be</span>
<a name="l00509"></a>00509 <span class="comment"> set directly in the ExprStream. */</span>
<a name="l00510"></a><a class="code" href="group__ExprPkg.html#ga9050d11fa8e8ece11ab586a560081196">00510</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& Expr::indent(<span class="keywordtype">int</span> n, <span class="keywordtype">bool</span> permanent) {
<a name="l00511"></a>00511 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!isNull(), <span class="stringliteral">"Expr::indent called on Null Expr"</span>);
<a name="l00512"></a>00512 getEM()->indent(n, permanent);
<a name="l00513"></a>00513 <span class="keywordflow">return</span> *<span class="keyword">this</span>;
<a name="l00514"></a>00514 }
<a name="l00515"></a>00515
<a name="l00516"></a>00516
<a name="l00517"></a><a class="code" href="group__ExprPkg.html#ga159d60cb0f32e09df89a395b2680664a">00517</a> <span class="keywordtype">void</span> Expr::addToNotify(<a class="code" href="classCVC3_1_1Theory.html" title="Base class for theories.">Theory</a>* i, <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="l00518"></a>00518 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!isNull(), <span class="stringliteral">"Expr::addToNotify() on Null expr"</span>);
<a name="l00519"></a>00519 <span class="keywordflow">if</span>(getNotify() == NULL)
<a name="l00520"></a>00520 d_expr->d_notifyList = <span class="keyword">new</span> <a class="code" href="classCVC3_1_1NotifyList.html">NotifyList</a>(getEM()->getCurrentContext());
<a name="l00521"></a>00521 getNotify()->add(i, e);
<a name="l00522"></a>00522 }
<a name="l00523"></a>00523
<a name="l00524"></a>00524
<a name="l00525"></a><a class="code" href="group__ExprPkg.html#gaf53e6a6f9dc01481d2cf94673c5505ce">00525</a> <span class="keywordtype">bool</span> Expr::containsTermITE()<span class="keyword"> const</span>
<a name="l00526"></a>00526 <span class="keyword"></span>{
<a name="l00527"></a>00527 <span class="keywordflow">if</span> (getType().isBool()) {
<a name="l00528"></a>00528
<a name="l00529"></a>00529 <span class="comment">// We overload the isAtomicFlag to mean !containsTermITE for exprs</span>
<a name="l00530"></a>00530 <span class="comment">// of Boolean type</span>
<a name="l00531"></a>00531 <span class="keywordflow">if</span> (validIsAtomicFlag()) {
<a name="l00532"></a>00532 <span class="keywordflow">return</span> !getIsAtomicFlag();
<a name="l00533"></a>00533 }
<a name="l00534"></a>00534
<a name="l00535"></a>00535 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> k = 0; k < arity(); ++k) {
<a name="l00536"></a>00536 <span class="keywordflow">if</span> ((*<span class="keyword">this</span>)[k].containsTermITE()) {
<a name="l00537"></a>00537 setIsAtomicFlag(<span class="keyword">false</span>);
<a name="l00538"></a>00538 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00539"></a>00539 }
<a name="l00540"></a>00540 }
<a name="l00541"></a>00541
<a name="l00542"></a>00542 setIsAtomicFlag(<span class="keyword">true</span>);
<a name="l00543"></a>00543 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00544"></a>00544
<a name="l00545"></a>00545 }
<a name="l00546"></a>00546 <span class="keywordflow">else</span> <span class="keywordflow">return</span> !isAtomic();
<a name="l00547"></a>00547 }
<a name="l00548"></a>00548
<a name="l00549"></a>00549
<a name="l00550"></a><a class="code" href="group__ExprPkg.html#ga48a9219339b394280550069ac7b0474f">00550</a> <span class="keywordtype">bool</span> Expr::isAtomic()<span class="keyword"> const</span>
<a name="l00551"></a>00551 <span class="keyword"></span>{
<a name="l00552"></a>00552 <span class="keywordflow">if</span> (getType().isBool()) {
<a name="l00553"></a>00553 <span class="keywordflow">return</span> isBoolConst();
<a name="l00554"></a>00554 }
<a name="l00555"></a>00555
<a name="l00556"></a>00556 <span class="keywordflow">if</span> (validIsAtomicFlag()) {
<a name="l00557"></a>00557 <span class="keywordflow">return</span> getIsAtomicFlag();
<a name="l00558"></a>00558 }
<a name="l00559"></a>00559
<a name="l00560"></a>00560 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> k = 0; k < arity(); ++k) {
<a name="l00561"></a>00561 <span class="keywordflow">if</span> (!(*<span class="keyword">this</span>)[k].isAtomic()) {
<a name="l00562"></a>00562 setIsAtomicFlag(<span class="keyword">false</span>);
<a name="l00563"></a>00563 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00564"></a>00564 }
<a name="l00565"></a>00565 }
<a name="l00566"></a>00566 setIsAtomicFlag(<span class="keyword">true</span>);
<a name="l00567"></a>00567 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00568"></a>00568 }
<a name="l00569"></a>00569
<a name="l00570"></a>00570
<a name="l00571"></a><a class="code" href="group__ExprPkg.html#ga4b575e0a191cc42706ff5b5a169c3069">00571</a> <span class="keywordtype">bool</span> Expr::isAtomicFormula()<span class="keyword"> const</span>
<a name="l00572"></a>00572 <span class="keyword"></span>{
<a name="l00573"></a>00573 <span class="comment">// TRACE("isAtomic", "isAtomicFormula(", *this, ") {");</span>
<a name="l00574"></a>00574 <span class="keywordflow">if</span> (!getType().isBool()) {
<a name="l00575"></a>00575 <span class="comment">// TRACE_MSG("isAtomic", "isAtomicFormula[kid] => false }");</span>
<a name="l00576"></a>00576 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00577"></a>00577 }
<a name="l00578"></a>00578 <span class="keywordflow">switch</span>(getKind()) {
<a name="l00579"></a>00579 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7b7b6f6e2b88589bd4656a14bcb7eb94">FORALL</a>: <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3197625a1bb2264943f5a95f236d9973">EXISTS</a>: <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bac62338ffb5de22369c75caa565b5da1a">XOR</a>:
<a name="l00580"></a>00580 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0378ebc895849163b249d0b330257dd6">NOT</a>: <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba865555c9f2e0458a7078486aa1b3254f">AND</a>: <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>: <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc">ITE</a>: <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>: <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7338bb59b9aa936104a6d2f631d4d8db">IMPLIES</a>:
<a name="l00581"></a>00581 <span class="comment">// TRACE_MSG("isAtomic", "isAtomicFormula[connective] => false }");</span>
<a name="l00582"></a>00582 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00583"></a>00583 }
<a name="l00584"></a>00584 <span class="keywordflow">for</span> (<a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> k = begin(), kend=end(); k != kend; ++k) {
<a name="l00585"></a>00585 <span class="keywordflow">if</span> (!(*k).isAtomic()) {
<a name="l00586"></a>00586 <span class="comment">// TRACE_MSG("isAtomic", "isAtomicFormula[kid] => false }");</span>
<a name="l00587"></a>00587 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00588"></a>00588 }
<a name="l00589"></a>00589 }
<a name="l00590"></a>00590 <span class="comment">// TRACE_MSG("isAtomic", "isAtomicFormula => true }");</span>
<a name="l00591"></a>00591 <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00592"></a>00592 }
<a name="l00593"></a>00593
<a name="l00594"></a>00594
<a name="l00595"></a>00595 <span class="comment">// This is one of the most friequently called routines. Make it as</span>
<a name="l00596"></a>00596 <span class="comment">// efficient as possible.</span>
<a name="l00597"></a><a class="code" href="namespaceCVC3.html#ac06ac2fd4db699104b790f98b7abba71">00597</a> <span class="keywordtype">int</span> <a class="code" href="namespaceCVC3.html#ac06ac2fd4db699104b790f98b7abba71">compare</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e2) {
<a name="l00598"></a>00598 <span class="comment">// Quick equality check (operator== is implemented independently</span>
<a name="l00599"></a>00599 <span class="comment">// and more efficiently)</span>
<a name="l00600"></a>00600 <span class="keywordflow">if</span>(e1 == e2) <span class="keywordflow">return</span> 0;
<a name="l00601"></a>00601
<a name="l00602"></a>00602 <span class="keywordflow">if</span>(e1.<a class="code" href="group__ExprPkg.html#ga3a08bea4e8715a268083e1671e340a2e">d_expr</a> == NULL) <span class="keywordflow">return</span> -1;
<a name="l00603"></a>00603 <span class="keywordflow">if</span>(e2.<a class="code" href="group__ExprPkg.html#ga3a08bea4e8715a268083e1671e340a2e">d_expr</a> == NULL) <span class="keywordflow">return</span> 1;
<a name="l00604"></a>00604
<a name="l00605"></a>00605 <span class="comment">// Both are non-Null. Check for constant</span>
<a name="l00606"></a>00606 <span class="keywordtype">bool</span> e1c = e1.<a class="code" href="group__ExprPkg.html#ga3c3645e1962f6de72655c650639e7a2d">isConstant</a>();
<a name="l00607"></a>00607 <span class="keywordflow">if</span> (e1c != e2.<a class="code" href="group__ExprPkg.html#ga3c3645e1962f6de72655c650639e7a2d">isConstant</a>()) {
<a name="l00608"></a>00608 <span class="keywordflow">return</span> e1c ? -1 : 1;
<a name="l00609"></a>00609 }
<a name="l00610"></a>00610
<a name="l00611"></a>00611 <span class="comment">// Compare the indices</span>
<a name="l00612"></a>00612 <span class="keywordflow">return</span> (e1.<a class="code" href="group__ExprPkg.html#gadaddb9b0566ecddd4611a10e820dc544">getIndex</a>() < e2.<a class="code" href="group__ExprPkg.html#gadaddb9b0566ecddd4611a10e820dc544">getIndex</a>())? -1 : 1;
<a name="l00613"></a>00613 }
<a name="l00614"></a>00614
<a name="l00615"></a>00615 <span class="comment"></span>
<a name="l00616"></a>00616 <span class="comment">///////////////////////////////////////////////////////////////////////</span>
<a name="l00617"></a>00617 <span class="comment"></span><span class="comment">// Class Expr::iterator methods //</span><span class="comment"></span>
<a name="l00618"></a>00618 <span class="comment">///////////////////////////////////////////////////////////////////////</span>
<a name="l00619"></a>00619 <span class="comment"></span>
<a name="l00620"></a>00620
<a name="l00621"></a><a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">00621</a> ostream& <a class="code" href="namespaceCVC3.html#a6b7e38d3c97da1e91e12a6c9555b8163">operator<<</a>(ostream& os, <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="l00622"></a>00622 <span class="keywordflow">if</span>(e.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>()) <span class="keywordflow">return</span> os << <span class="stringliteral">"Null"</span>;
<a name="l00623"></a>00623 <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a> es(e.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>());
<a name="l00624"></a>00624 es.<a class="code" href="classCVC3_1_1ExprStream.html#a8316bdcfb3ea96317ce9f8b4ebd16512" title="Set a new output stream.">os</a>(os);
<a name="l00625"></a>00625 es << e;
<a name="l00626"></a>00626 e.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga3fe43b71bb148045c114e054934f5304" title="Set transient indentation to permanent.">restoreIndent</a>();
<a name="l00627"></a>00627 <span class="keywordflow">return</span> os;
<a name="l00628"></a>00628 }
<a name="l00629"></a>00629
<a name="l00630"></a>00630
<a name="l00631"></a>00631 <span class="comment">// Functions from class Type</span>
<a name="l00632"></a>00632
<a name="l00633"></a>00633
<a name="l00634"></a><a class="code" href="classCVC3_1_1Type.html#a6dbeaa3c209ebef10debb276963d29b9">00634</a> Type::Type(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> expr) : d_expr(expr)
<a name="l00635"></a>00635 {
<a name="l00636"></a>00636 <span class="keywordflow">if</span> (expr.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>()) <span class="keywordflow">return</span>;
<a name="l00637"></a>00637 expr.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga51109c3e331615c510c964798b38ee95" title="Check well-formedness of a type Expr.">checkType</a>(expr);
<a name="l00638"></a>00638 }
<a name="l00639"></a>00639
<a name="l00640"></a>00640
<a name="l00641"></a><a class="code" href="classCVC3_1_1Type.html#a3ebf8a1ba9d894c33df064ea37c5ead5">00641</a> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> <a class="code" href="classCVC3_1_1Type.html#a3ebf8a1ba9d894c33df064ea37c5ead5">Type::funType</a>(<span class="keyword">const</span> std::vector<Type>& typeDom, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& typeRan) {
<a name="l00642"></a>00642 vector<Expr> tmp;
<a name="l00643"></a>00643 <span class="keywordflow">for</span>(vector<Type>::const_iterator i=typeDom.begin(), iend=typeDom.end();
<a name="l00644"></a>00644 i!=iend; ++i)
<a name="l00645"></a>00645 tmp.push_back(i->getExpr());
<a name="l00646"></a>00646 tmp.push_back(typeRan.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>());
<a name="l00647"></a>00647 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Type.html#a0c0779105402ab3486650cfac3c97fd1">Type</a>(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba546eccfedc4dcc8623ed0668f77ef982">ARROW</a>, tmp));
<a name="l00648"></a>00648 }
<a name="l00649"></a>00649
<a name="l00650"></a>00650
<a name="l00651"></a>00651 } <span class="comment">// end of namespace CVC3</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>
