<!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: theory_simulate.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">theory_simulate.cpp</div> </div>
</div>
<div class="contents">
<a href="theory__simulate_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 theory_simulate.cpp</span>
<a name="l00004"></a>00004 <span class="comment"> *\brief Implementation of class TheorySimulate.</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: Tue Oct 7 10:28:14 2003</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="preprocessor">#include "<a class="code" href="theory__simulate_8h.html" title="Implementation of a symbolic simulator.">theory_simulate.h</a>"</span>
<a name="l00023"></a>00023 <span class="preprocessor">#include "<a class="code" href="simulate__proof__rules_8h.html" title="Abstract interface to the symbolic simulator proof rules.">simulate_proof_rules.h</a>"</span>
<a name="l00024"></a>00024 <span class="preprocessor">#include "<a class="code" href="typecheck__exception_8h.html" title="An exception to be thrown at typecheck error.">typecheck_exception.h</a>"</span>
<a name="l00025"></a>00025 <span class="preprocessor">#include "<a class="code" href="parser__exception_8h.html" title="An exception thrown by the parser.">parser_exception.h</a>"</span>
<a name="l00026"></a>00026 <span class="preprocessor">#include "<a class="code" href="smtlib__exception_8h.html" title="An exception to be thrown by the smtlib translator.">smtlib_exception.h</a>"</span>
<a name="l00027"></a>00027 <span class="comment">// For the type REAL</span>
<a name="l00028"></a>00028 <span class="preprocessor">#include "<a class="code" href="theory__arith_8h.html">theory_arith.h</a>"</span>
<a name="l00029"></a>00029
<a name="l00030"></a>00030
<a name="l00031"></a>00031 <span class="keyword">using namespace </span>std;
<a name="l00032"></a>00032 <span class="keyword">using namespace </span>CVC3;
<a name="l00033"></a>00033
<a name="l00034"></a>00034
<a name="l00035"></a><a class="code" href="classCVC3_1_1TheorySimulate.html#a55c7af5a378de8d5d5be49ba8f255b14">00035</a> TheorySimulate::TheorySimulate(<a class="code" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">TheoryCore</a>* core)
<a name="l00036"></a>00036 : <a class="code" href="classCVC3_1_1Theory.html" title="Base class for theories.">Theory</a>(core, <span class="stringliteral">"Simulate"</span>) {
<a name="l00037"></a>00037 <span class="comment">// Initialize the proof rules</span>
<a name="l00038"></a>00038 <a class="code" href="classCVC3_1_1TheorySimulate.html#a549f5a22dfdb58a6d22f48b09ecaec3e" title="Our local proof rules.">d_rules</a> = <a class="code" href="classCVC3_1_1TheorySimulate.html#a9d7b41e634335a8c3ed2636b88fd714e" title="Create proof rules for this theory.">createProofRules</a>();
<a name="l00039"></a>00039 <span class="comment">// Register the kinds</span>
<a name="l00040"></a>00040 vector<int> kinds;
<a name="l00041"></a>00041 kinds.push_back(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa1022ff97dac8e2d5d80d53c4cecd132">SIMULATE</a>);
<a name="l00042"></a>00042 <span class="comment">// Register the theory with the core</span>
<a name="l00043"></a>00043 <a class="code" href="classCVC3_1_1Theory.html#a97a6f8e09f71513da969fa7847346c6f" title="Register a new theory.">registerTheory</a>(<span class="keyword">this</span>, kinds, <span class="keyword">false</span> <span class="comment">/* no solver */</span>);
<a name="l00044"></a>00044 }
<a name="l00045"></a>00045
<a name="l00046"></a>00046
<a name="l00047"></a><a class="code" href="classCVC3_1_1TheorySimulate.html#a360c8619bf0719db8811a3efae77b832">00047</a> <a class="code" href="classCVC3_1_1TheorySimulate.html#a360c8619bf0719db8811a3efae77b832" title="Destructor.">TheorySimulate::~TheorySimulate</a>() {
<a name="l00048"></a>00048 <span class="keyword">delete</span> <a class="code" href="classCVC3_1_1TheorySimulate.html#a549f5a22dfdb58a6d22f48b09ecaec3e" title="Our local proof rules.">d_rules</a>;
<a name="l00049"></a>00049 }
<a name="l00050"></a>00050
<a name="l00051"></a>00051
<a name="l00052"></a>00052 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00053"></a><a class="code" href="classCVC3_1_1TheorySimulate.html#a7ffc512dc7ea5a3178445b904c7071e2">00053</a> <a class="code" href="classCVC3_1_1TheorySimulate.html#a7ffc512dc7ea5a3178445b904c7071e2" title="Theory-specific rewrite rules.">TheorySimulate::rewrite</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) {
<a name="l00054"></a>00054 <span class="keywordflow">switch</span> (e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()) {
<a name="l00055"></a>00055 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa1022ff97dac8e2d5d80d53c4cecd132">SIMULATE</a>:
<a name="l00056"></a>00056 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheorySimulate.html#a549f5a22dfdb58a6d22f48b09ecaec3e" title="Our local proof rules.">d_rules</a>-><a class="code" href="classCVC3_1_1SimulateProofRules.html#a521de66c40b56968a3765f8a23755a3a" title="SIMULATE(f, s_0, i_1, ..., i_k, N) <=> f(...f(f(s_0, i_1), i_2), ... i_k)">expandSimulate</a>(e);
<a name="l00057"></a>00057 <span class="keywordflow">break</span>;
<a name="l00058"></a>00058 <span class="keywordflow">default</span>:
<a name="l00059"></a>00059 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theory.html#af860f5d5e01423628c97c399606916ff" title="==> a == a">reflexivityRule</a>(e);
<a name="l00060"></a>00060 }
<a name="l00061"></a>00061 }
<a name="l00062"></a>00062
<a name="l00063"></a>00063
<a name="l00064"></a>00064 <span class="keywordtype">void</span>
<a name="l00065"></a><a class="code" href="classCVC3_1_1TheorySimulate.html#a7b967470cb0087ab5ed87ecb483a978d">00065</a> <a class="code" href="classCVC3_1_1TheorySimulate.html#a7b967470cb0087ab5ed87ecb483a978d" title="Compute and store the type of e.">TheorySimulate::computeType</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) {
<a name="l00066"></a>00066 <span class="keywordflow">switch</span> (e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()) {
<a name="l00067"></a>00067 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa1022ff97dac8e2d5d80d53c4cecd132">SIMULATE</a>: { <span class="comment">// SIMULATE(f, s0, i_1, ..., i_k, N)</span>
<a name="l00068"></a>00068 <span class="keyword">const</span> <span class="keywordtype">int</span> arity = e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>();
<a name="l00069"></a>00069 <span class="keywordflow">if</span> (!e[arity - 1].<a class="code" href="namespaceCVC3.html#ac0334a083d6782caa17ca0d337fddddf">isRational</a>() ||
<a name="l00070"></a>00070 !e[arity - 1].getRational().isInteger()) {
<a name="l00071"></a>00071 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>
<a name="l00072"></a>00072 (<span class="stringliteral">"Number of cycles in SIMULATE (last arg) "</span>
<a name="l00073"></a>00073 <span class="stringliteral">"must be an integer constant:\n\n "</span> + e[arity -1].toString()
<a name="l00074"></a>00074 +<span class="stringliteral">"\n\nIn the following expression:\n\n "</span>
<a name="l00075"></a>00075 +e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00076"></a>00076 }
<a name="l00077"></a>00077
<a name="l00078"></a>00078 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& fn(e[0]);
<a name="l00079"></a>00079 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> fnType(<a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(fn));
<a name="l00080"></a>00080 <span class="comment">// The arity of function is k+1, which is e.arity()-2.</span>
<a name="l00081"></a>00081 <span class="comment">// The arity of the type also includes the result type.</span>
<a name="l00082"></a>00082 <span class="keywordflow">if</span>(fnType.<a class="code" href="classCVC3_1_1Type.html#abd7ab3fcb112e27aa05da8981b56e02c">arity</a>() != e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-1)
<a name="l00083"></a>00083 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>
<a name="l00084"></a>00084 (<span class="stringliteral">"Wrong number of arguments in SIMULATE:\n\n"</span>
<a name="l00085"></a>00085 +e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>()
<a name="l00086"></a>00086 +<span class="stringliteral">"\n\nExpected "</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(fnType.<a class="code" href="classCVC3_1_1Type.html#abd7ab3fcb112e27aa05da8981b56e02c">arity</a>()+1)
<a name="l00087"></a>00087 +<span class="stringliteral">" arguments, but received "</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>())+<span class="stringliteral">"."</span>);
<a name="l00088"></a>00088 <span class="comment">// Build the function type that SIMULATE expects</span>
<a name="l00089"></a>00089 vector<Type> argTp;
<a name="l00090"></a>00090 <span class="comment">// The (initial) state type</span>
<a name="l00091"></a>00091 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> resType(<a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(e[1]));
<a name="l00092"></a>00092 argTp.push_back(resType);
<a name="l00093"></a>00093 <span class="keywordflow">for</span>(<span class="keywordtype">int</span> i=2, iend=e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-1; i<iend; ++i) {
<a name="l00094"></a>00094 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> iTp(e[i].getType());
<a name="l00095"></a>00095 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> iTpBase(<a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(e[i]));
<a name="l00096"></a>00096 <span class="keywordflow">if</span>(!iTp.<a class="code" href="classCVC3_1_1Type.html#a9c3be568546a63fb424e4cb49391dfa6">isFunction</a>() || iTp.<a class="code" href="classCVC3_1_1Type.html#abd7ab3fcb112e27aa05da8981b56e02c">arity</a>() != 2 || !<a class="code" href="namespaceCVC3.html#a6475c7ef78c59970a4525d5b3ff0ce86">isReal</a>(iTpBase[0]))
<a name="l00097"></a>00097 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>
<a name="l00098"></a>00098 (<span class="stringliteral">"Type mismatch in SIMULATE:\n\n "</span>
<a name="l00099"></a>00099 +e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>()
<a name="l00100"></a>00100 +<span class="stringliteral">"\n\nThe input #"</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(i-1)
<a name="l00101"></a>00101 +<span class="stringliteral">" is expected to be of type:\n\n REAL -> <something>"</span>
<a name="l00102"></a>00102 <span class="stringliteral">"\n\nBut the actual type is:\n\n "</span>
<a name="l00103"></a>00103 +iTp.<a class="code" href="classCVC3_1_1Type.html#a2f5ce4b1973ec02b2f2b2eba8ce3cc50">toString</a>());
<a name="l00104"></a>00104 argTp.push_back(iTpBase[1]);
<a name="l00105"></a>00105 }
<a name="l00106"></a>00106 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> expectedFnType(<a class="code" href="classCVC3_1_1Type.html#a3ebf8a1ba9d894c33df064ea37c5ead5">Type::funType</a>(argTp, resType));
<a name="l00107"></a>00107 <span class="keywordflow">if</span>(fnType != expectedFnType)
<a name="l00108"></a>00108 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>
<a name="l00109"></a>00109 (<span class="stringliteral">"Type mismatch in SIMULATE:\n\n "</span>
<a name="l00110"></a>00110 +e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>()
<a name="l00111"></a>00111 +<span class="stringliteral">"\n\nThe transition function is expected to be of type:\n\n "</span>
<a name="l00112"></a>00112 +expectedFnType.<a class="code" href="classCVC3_1_1Type.html#a2f5ce4b1973ec02b2f2b2eba8ce3cc50">toString</a>()
<a name="l00113"></a>00113 +<span class="stringliteral">"\n\nBut the actual type is:\n\n "</span>
<a name="l00114"></a>00114 +fnType.<a class="code" href="classCVC3_1_1Type.html#a2f5ce4b1973ec02b2f2b2eba8ce3cc50">toString</a>());
<a name="l00115"></a>00115
<a name="l00116"></a>00116 e.<a class="code" href="group__ExprPkg.html#ga07d47f902598e00097086deabf04d9c5" title="Set the cached type.">setType</a>(resType);
<a name="l00117"></a>00117 <span class="keywordflow">break</span>;
<a name="l00118"></a>00118 }
<a name="l00119"></a>00119 <span class="keywordflow">default</span>:
<a name="l00120"></a>00120 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>,<span class="stringliteral">"TheorySimulate::computeType: Unexpected expression: "</span>
<a name="l00121"></a>00121 +e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00122"></a>00122 }
<a name="l00123"></a>00123 }
<a name="l00124"></a>00124 <span class="comment"></span>
<a name="l00125"></a>00125 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00126"></a>00126 <span class="comment"></span><span class="comment">//parseExprOp:</span>
<a name="l00127"></a>00127 <span class="comment">//Recursive call of parseExpr defined in theory_ libaries based on kind of expr </span>
<a name="l00128"></a>00128 <span class="comment">//being built</span><span class="comment"></span>
<a name="l00129"></a>00129 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00130"></a>00130 <span class="comment"></span><a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>
<a name="l00131"></a><a class="code" href="classCVC3_1_1TheorySimulate.html#a888f05dd7da9aa30304f6b7016dbfe46">00131</a> <a class="code" href="classCVC3_1_1TheorySimulate.html#a888f05dd7da9aa30304f6b7016dbfe46" title="Theory-specific parsing implemented by the DP.">TheorySimulate::parseExprOp</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) {
<a name="l00132"></a>00132 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"parser"</span>, <span class="stringliteral">"TheorySimulate::parseExprOp("</span>, e, <span class="stringliteral">")"</span>);
<a name="l00133"></a>00133 <span class="comment">// If the expression is not a list, it must have been already</span>
<a name="l00134"></a>00134 <span class="comment">// parsed, so just return it as is.</span>
<a name="l00135"></a>00135 <span class="keywordflow">if</span>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a> != e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()) <span class="keywordflow">return</span> e;
<a name="l00136"></a>00136
<a name="l00137"></a>00137 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() > 0,
<a name="l00138"></a>00138 <span class="stringliteral">"TheorySimulate::parseExprOp:\n e = "</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00139"></a>00139 <span class="comment">/* The first element of the list (e[0] is an ID of the operator. </span>
<a name="l00140"></a>00140 <span class="comment"> ID string values are the dirst element of the expression */</span>
<a name="l00141"></a>00141 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& c1 = e[0][0];
<a name="l00142"></a>00142 <span class="keywordtype">int</span> kind = <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga9e7929fab9329724812e74b066a3c90a" title="Return a kind associated with a name. Returns NULL_KIND if not found.">getKind</a>(c1.getString());
<a name="l00143"></a>00143 <span class="keywordflow">switch</span>(kind) {
<a name="l00144"></a>00144 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa1022ff97dac8e2d5d80d53c4cecd132">SIMULATE</a>: { <span class="comment">// Application of SIMULATE to args</span>
<a name="l00145"></a>00145 vector<Expr> k;
<a name="l00146"></a>00146 <a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> i = e.<a class="code" href="group__ExprPkg.html#gac890e13db184610276fc533fa4b4fe99" title="Begin iterator.">begin</a>(), iend=e.<a class="code" href="group__ExprPkg.html#gaf6048a5030c8fa2511bf5dfee868e653" title="End iterator.">end</a>();
<a name="l00147"></a>00147 <span class="comment">// Skip first element of the vector of kids in 'e'.</span>
<a name="l00148"></a>00148 <span class="comment">// The first element is the operator.</span>
<a name="l00149"></a>00149 ++i;
<a name="l00150"></a>00150 <span class="comment">// Parse the kids of e and push them into the vector 'k'</span>
<a name="l00151"></a>00151 <span class="keywordflow">for</span>(; i!=iend; ++i)
<a name="l00152"></a>00152 k.push_back(<a class="code" href="classCVC3_1_1Theory.html#abd5a64ee867dda0c216a04e9fc7fbd6c" title="Parse the generic expression.">parseExpr</a>(*i));
<a name="l00153"></a>00153 <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#aa10c9e8951b8ccf714a59ec321bdac5baa1022ff97dac8e2d5d80d53c4cecd132">SIMULATE</a>, k, e.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>());
<a name="l00154"></a>00154 <span class="keywordflow">break</span>;
<a name="l00155"></a>00155 }
<a name="l00156"></a>00156 <span class="keywordflow">default</span>:
<a name="l00157"></a>00157 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"TheorySimulate::parseExprOp: Unexpected operator: "</span>
<a name="l00158"></a>00158 +e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00159"></a>00159 }
<a name="l00160"></a>00160 <span class="keywordflow">return</span> e;
<a name="l00161"></a>00161 }
<a name="l00162"></a>00162
<a name="l00163"></a>00163 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>
<a name="l00164"></a><a class="code" href="classCVC3_1_1TheorySimulate.html#a46b843eea802fa2a9b666552a58886eb">00164</a> <a class="code" href="classCVC3_1_1TheorySimulate.html#a46b843eea802fa2a9b666552a58886eb" title="Compute and cache the TCC of e.">TheorySimulate::computeTCC</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) {
<a name="l00165"></a>00165 <span class="keywordflow">switch</span> (e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()) {
<a name="l00166"></a>00166 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa1022ff97dac8e2d5d80d53c4cecd132">SIMULATE</a>: {
<a name="l00167"></a>00167 <span class="comment">// TCC(SIMULATE(f, s, i1, ..., ik, N)):</span>
<a name="l00168"></a>00168
<a name="l00169"></a>00169 <span class="comment">// First, we require that the type of the first argument of f is</span>
<a name="l00170"></a>00170 <span class="comment">// exactly the same as the type of f's result (otherwise we need</span>
<a name="l00171"></a>00171 <span class="comment">// to check subtyping relation, which might be undecidable), and</span>
<a name="l00172"></a>00172 <span class="comment">// whether f is defined on s.</span>
<a name="l00173"></a>00173 <span class="comment">//</span>
<a name="l00174"></a>00174 <span class="comment">// Then, we check that the result type of i_j exactly matches the</span>
<a name="l00175"></a>00175 <span class="comment">// type of the j+1-th argument of f (again, for efficiency and</span>
<a name="l00176"></a>00176 <span class="comment">// decidability reasons), and that each i_j is defined on every</span>
<a name="l00177"></a>00177 <span class="comment">// integer from 0..N-1.</span>
<a name="l00178"></a>00178 vector<Expr> tccs;
<a name="l00179"></a>00179 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> fnType(e[0].getType());
<a name="l00180"></a>00180 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(fnType.<a class="code" href="classCVC3_1_1Type.html#abd7ab3fcb112e27aa05da8981b56e02c">arity</a>() == e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-1,
<a name="l00181"></a>00181 <span class="stringliteral">"TheorySimulate::computeTCC: SIMULATE() doesn't typecheck: "</span>
<a name="l00182"></a>00182 +e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00183"></a>00183 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> resType(fnType[fnType.<a class="code" href="classCVC3_1_1Type.html#abd7ab3fcb112e27aa05da8981b56e02c">arity</a>()-1]);
<a name="l00184"></a>00184 <span class="comment">// Check that the state type matches the 1st arg and the result type in f</span>
<a name="l00185"></a>00185 <span class="keywordflow">if</span>(fnType[0] != resType)
<a name="l00186"></a>00186 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()-><a class="code" href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae" title="FALSE Expr.">falseExpr</a>();
<a name="l00187"></a>00187 <span class="comment">// Compute TCC for f on the initial state</span>
<a name="l00188"></a>00188 tccs.push_back(<a class="code" href="classCVC3_1_1Theory.html#a39539e895f8aade88ae5bc05bbcc9302" title="Calls the correct theory to compute a type predicate.">getTypePred</a>(fnType[0], e[1]));
<a name="l00189"></a>00189
<a name="l00190"></a>00190 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a>& N = e[e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-1].<a class="code" href="group__ExprPkg.html#gab0eee70e4a7f97c09954dc61b71b65e5" title="Get the Rational value out of RATIONAL_EXPR.">getRational</a>();
<a name="l00191"></a>00191 <span class="comment">// Now, iterate through the inputs</span>
<a name="l00192"></a>00192 <span class="keywordflow">for</span>(<span class="keywordtype">int</span> i=2, iend=e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-1; i<iend; ++i) {
<a name="l00193"></a>00193 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> iTp(e[i].getType());
<a name="l00194"></a>00194 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(iTp.<a class="code" href="classCVC3_1_1Type.html#a9c3be568546a63fb424e4cb49391dfa6">isFunction</a>() && iTp.<a class="code" href="classCVC3_1_1Type.html#abd7ab3fcb112e27aa05da8981b56e02c">arity</a>()==2,
<a name="l00195"></a>00195 <span class="stringliteral">"TheorySimulate::computeTCC: SIMULATE() doesn't typecheck: "</span>
<a name="l00196"></a>00196 +e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00197"></a>00197 <span class="comment">// Match the return type of i-th input with f's argument</span>
<a name="l00198"></a>00198 <span class="keywordflow">if</span>(iTp[1] != fnType[i-1])
<a name="l00199"></a>00199 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()-><a class="code" href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae" title="FALSE Expr.">falseExpr</a>();
<a name="l00200"></a>00200 <span class="comment">// Compute the TCC for i(0) ... i(N-1)</span>
<a name="l00201"></a>00201 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1Rational.html">Rational</a> j=0; j<N; j = j+1)
<a name="l00202"></a>00202 tccs.push_back(<a class="code" href="classCVC3_1_1Theory.html#a39539e895f8aade88ae5bc05bbcc9302" title="Calls the correct theory to compute a type predicate.">getTypePred</a>(iTp[0], <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()->newRatExpr(j)));
<a name="l00203"></a>00203 }
<a name="l00204"></a>00204 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theory.html#aba1822f2d985b50f6405c290c3814c1a" title="==> AND(e1,e2) IFF [simplified expr]">rewriteAnd</a>(<a class="code" href="namespaceCVC3.html#ad4258158bba138eb54b9080af7f8223a">andExpr</a>(tccs)).<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>();
<a name="l00205"></a>00205 }
<a name="l00206"></a>00206 <span class="keywordflow">default</span>:
<a name="l00207"></a>00207 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"TheorySimulate::computeTCC("</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>()
<a name="l00208"></a>00208 +<span class="stringliteral">")\n\nUnknown expression."</span>);
<a name="l00209"></a>00209 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4471fca49c2acbb7b4cf71e72bc55d6a" title="TRUE Expr.">trueExpr</a>();
<a name="l00210"></a>00210 }
<a name="l00211"></a>00211 }
<a name="l00212"></a>00212
<a name="l00213"></a>00213
<a name="l00214"></a>00214 <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>&
<a name="l00215"></a><a class="code" href="classCVC3_1_1TheorySimulate.html#a9d4451dfc3e6f6e1b9872761b4a974f2">00215</a> <a class="code" href="classCVC3_1_1TheorySimulate.html#a9d4451dfc3e6f6e1b9872761b4a974f2" title="Theory-specific pretty-printing.">TheorySimulate::print</a>(<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 class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e) {
<a name="l00216"></a>00216 <span class="keywordflow">switch</span>(os.<a class="code" href="classCVC3_1_1ExprStream.html#ac2b2872228aff3fd5d08bbd69c672543" title="Get the current output language.">lang</a>()) {
<a name="l00217"></a>00217 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0eaa315c228d5c3290ce37df81524ed8e9a" title="Nice SAL-like language for manually written specs.">PRESENTATION_LANG</a>:
<a name="l00218"></a>00218 <span class="keywordflow">switch</span>(e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()) {
<a name="l00219"></a>00219 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa1022ff97dac8e2d5d80d53c4cecd132">SIMULATE</a>:{
<a name="l00220"></a>00220 os << <span class="stringliteral">"SIMULATE"</span> << <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="l00221"></a>00221 <span class="keywordtype">bool</span> first(<span class="keyword">true</span>);
<a name="l00222"></a>00222 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i = 0; i < e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>(); i++) {
<a name="l00223"></a>00223 <span class="keywordflow">if</span> (first) first = <span class="keyword">false</span>;
<a name="l00224"></a>00224 <span class="keywordflow">else</span> 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#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a>;
<a name="l00225"></a>00225 os << e[i];
<a name="l00226"></a>00226 }
<a name="l00227"></a>00227 os << push << <span class="stringliteral">")"</span>;
<a name="l00228"></a>00228 <span class="keywordflow">break</span>;
<a name="l00229"></a>00229 }
<a name="l00230"></a>00230 <span class="keywordflow">default</span>:
<a name="l00231"></a>00231 <span class="comment">// Print the top node in the default LISP format, continue with</span>
<a name="l00232"></a>00232 <span class="comment">// pretty-printing for children.</span>
<a name="l00233"></a>00233 e.<a class="code" href="group__ExprPkg.html#ga092308b0a88e12a5c7ff2fc0a2eca818" title="Print the top node and then recurse through the children */.">printAST</a>(os);
<a name="l00234"></a>00234
<a name="l00235"></a>00235 <span class="keywordflow">break</span>;
<a name="l00236"></a>00236 }
<a name="l00237"></a>00237 <span class="keywordflow">break</span>;
<a name="l00238"></a>00238 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0ea548619427a4d459d859ccd041ced9bfa" title="SMT-LIB format.">SMTLIB_LANG</a>:
<a name="l00239"></a>00239 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0eaed2643c62e36b9b222804a1ab5b4809e" title="SMT-LIB v2 format.">SMTLIB_V2_LANG</a>:
<a name="l00240"></a>00240 <a class="code" href="classCVC3_1_1Theory.html#a262fdc338527489b376ec181ecc38ddc">d_theoryUsed</a> = <span class="keyword">true</span>;
<a name="l00241"></a>00241 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1SmtlibException.html">SmtlibException</a>(<span class="stringliteral">"TheorySimulate::print: SMTLIB not supported"</span>);
<a name="l00242"></a>00242 <span class="keywordflow">switch</span>(e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()) {
<a name="l00243"></a>00243 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa1022ff97dac8e2d5d80d53c4cecd132">SIMULATE</a>:{
<a name="l00244"></a>00244 os << <span class="stringliteral">"("</span> << <a class="code" href="group__ExprStream__Manip.html#ga2a0348c6d3f94f2f8febc6dd0a9c3218" title="Set the indentation to the current position.">push</a> << <span class="stringliteral">"SIMULATE"</span> << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a>;
<a name="l00245"></a>00245 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i = 0; i < e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>(); i++) {
<a name="l00246"></a>00246 os << space << e[i];
<a name="l00247"></a>00247 }
<a name="l00248"></a>00248 os << <a class="code" href="group__ExprStream__Manip.html#ga2a0348c6d3f94f2f8febc6dd0a9c3218" title="Set the indentation to the current position.">push</a> << <span class="stringliteral">")"</span>;
<a name="l00249"></a>00249 <span class="keywordflow">break</span>;
<a name="l00250"></a>00250 }
<a name="l00251"></a>00251 <span class="keywordflow">default</span>:
<a name="l00252"></a>00252 <span class="comment">// Print the top node in the default LISP format, continue with</span>
<a name="l00253"></a>00253 <span class="comment">// pretty-printing for children.</span>
<a name="l00254"></a>00254 e.<a class="code" href="group__ExprPkg.html#ga092308b0a88e12a5c7ff2fc0a2eca818" title="Print the top node and then recurse through the children */.">printAST</a>(os);
<a name="l00255"></a>00255
<a name="l00256"></a>00256 <span class="keywordflow">break</span>;
<a name="l00257"></a>00257 }
<a name="l00258"></a>00258 <span class="keywordflow">break</span>;
<a name="l00259"></a>00259 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0ea00df691ed79361b36910e60b49824c35" title="Lisp-like format for automatically generated specs.">LISP_LANG</a>:
<a name="l00260"></a>00260 <span class="keywordflow">switch</span>(e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()) {
<a name="l00261"></a>00261 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa1022ff97dac8e2d5d80d53c4cecd132">SIMULATE</a>:{
<a name="l00262"></a>00262 os << <span class="stringliteral">"("</span> << <a class="code" href="group__ExprStream__Manip.html#ga2a0348c6d3f94f2f8febc6dd0a9c3218" title="Set the indentation to the current position.">push</a> << <span class="stringliteral">"SIMULATE"</span> << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a>;
<a name="l00263"></a>00263 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i = 0; i < e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>(); i++) {
<a name="l00264"></a>00264 os << space << e[i];
<a name="l00265"></a>00265 }
<a name="l00266"></a>00266 os << <a class="code" href="group__ExprStream__Manip.html#ga2a0348c6d3f94f2f8febc6dd0a9c3218" title="Set the indentation to the current position.">push</a> << <span class="stringliteral">")"</span>;
<a name="l00267"></a>00267 <span class="keywordflow">break</span>;
<a name="l00268"></a>00268 }
<a name="l00269"></a>00269 <span class="keywordflow">default</span>:
<a name="l00270"></a>00270 <span class="comment">// Print the top node in the default LISP format, continue with</span>
<a name="l00271"></a>00271 <span class="comment">// pretty-printing for children.</span>
<a name="l00272"></a>00272 e.<a class="code" href="group__ExprPkg.html#ga092308b0a88e12a5c7ff2fc0a2eca818" title="Print the top node and then recurse through the children */.">printAST</a>(os);
<a name="l00273"></a>00273
<a name="l00274"></a>00274 <span class="keywordflow">break</span>;
<a name="l00275"></a>00275 }
<a name="l00276"></a>00276 <span class="keywordflow">break</span>;
<a name="l00277"></a>00277 <span class="keywordflow">default</span>: <span class="comment">// Not a known language</span>
<a name="l00278"></a>00278 e.<a class="code" href="group__ExprPkg.html#ga092308b0a88e12a5c7ff2fc0a2eca818" title="Print the top node and then recurse through the children */.">printAST</a>(os);
<a name="l00279"></a>00279 <span class="keywordflow">break</span>;
<a name="l00280"></a>00280 }
<a name="l00281"></a>00281 <span class="keywordflow">return</span> os;
<a name="l00282"></a>00282 }
</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>
