<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: kinds.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><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 id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="dir_68267d1309a1af8e8297ef4c3efbcdba.html">src</a></li><li class="navelem"><a class="el" href="dir_b0856f6b0d80ccb263b2f415c91f9e17.html">include</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">kinds.h</div> </div>
</div><!--header-->
<div class="contents">
<a href="kinds_8h.html">Go to the documentation of this file.</a><div class="fragment"><div class="line"><a name="l00001"></a><span class="lineno"> 1</span> <span class="comment">/*****************************************************************************/</span><span class="comment"></span></div>
<div class="line"><a name="l00002"></a><span class="lineno"> 2</span> <span class="comment">/*!</span></div>
<div class="line"><a name="l00003"></a><span class="lineno"> 3</span> <span class="comment"> * \file kinds.h</span></div>
<div class="line"><a name="l00004"></a><span class="lineno"> 4</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00005"></a><span class="lineno"> 5</span> <span class="comment"> * Author: Clark Barrett</span></div>
<div class="line"><a name="l00006"></a><span class="lineno"> 6</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00007"></a><span class="lineno"> 7</span> <span class="comment"> * Created: Mon Jan 20 13:38:52 2003</span></div>
<div class="line"><a name="l00008"></a><span class="lineno"> 8</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00009"></a><span class="lineno"> 9</span> <span class="comment"> * <hr></span></div>
<div class="line"><a name="l00010"></a><span class="lineno"> 10</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00011"></a><span class="lineno"> 11</span> <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span></div>
<div class="line"><a name="l00012"></a><span class="lineno"> 12</span> <span class="comment"> * and its documentation for any purpose is hereby granted without</span></div>
<div class="line"><a name="l00013"></a><span class="lineno"> 13</span> <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span></div>
<div class="line"><a name="l00014"></a><span class="lineno"> 14</span> <span class="comment"> * LICENSE file provided with this distribution.</span></div>
<div class="line"><a name="l00015"></a><span class="lineno"> 15</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00016"></a><span class="lineno"> 16</span> <span class="comment"> * <hr></span></div>
<div class="line"><a name="l00017"></a><span class="lineno"> 17</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00018"></a><span class="lineno"> 18</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00019"></a><span class="lineno"> 19</span> <span class="comment">/*****************************************************************************/</span></div>
<div class="line"><a name="l00020"></a><span class="lineno"> 20</span> </div>
<div class="line"><a name="l00021"></a><span class="lineno"> 21</span> <span class="preprocessor">#ifndef _cvc3__include__kinds_h_</span></div>
<div class="line"><a name="l00022"></a><span class="lineno"> 22</span> <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__kinds_h_</span></div>
<div class="line"><a name="l00023"></a><span class="lineno"> 23</span> <span class="preprocessor"></span></div>
<div class="line"><a name="l00024"></a><span class="lineno"> 24</span> <span class="preprocessor">#ifdef __cplusplus</span></div>
<div class="line"><a name="l00025"></a><span class="lineno"> 25</span> <span class="preprocessor"></span><span class="keyword">namespace </span>CVC3 {</div>
<div class="line"><a name="l00026"></a><span class="lineno"> 26</span> <span class="preprocessor">#endif </span><span class="comment">/* __cplusplus */</span><span class="preprocessor"></span></div>
<div class="line"><a name="l00027"></a><span class="lineno"> 27</span> <span class="preprocessor"></span></div>
<div class="line"><a name="l00028"></a><span class="lineno"> 28</span>  <span class="comment">// The commonly used kinds and the kinds needed by the parser. All</span></div>
<div class="line"><a name="l00029"></a><span class="lineno"> 29</span>  <span class="comment">// these kinds are registered by the ExprManager and are readily</span></div>
<div class="line"><a name="l00030"></a><span class="lineno"> 30</span>  <span class="comment">// available for everyone else.</span></div>
<div class="line"><a name="l00031"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5b"> 31</a></span> <span class="keyword">typedef</span> <span class="keyword">enum</span> {</div>
<div class="line"><a name="l00032"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5bc05ce87fa69f660d39d0a4fa188c67"> 32</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5bc05ce87fa69f660d39d0a4fa188c67">NULL_KIND</a> = 0,</div>
<div class="line"><a name="l00033"></a><span class="lineno"> 33</span> </div>
<div class="line"><a name="l00034"></a><span class="lineno"> 34</span>  <span class="comment">// Constant (Leaf) Exprs</span></div>
<div class="line"><a name="l00035"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba1fad76919fba496de21807e2beec533d"> 35</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba1fad76919fba496de21807e2beec533d">TRUE_EXPR</a> = 1,</div>
<div class="line"><a name="l00036"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5f71bd33a6528411ae681f5291de1d82"> 36</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5f71bd33a6528411ae681f5291de1d82">FALSE_EXPR</a> = 2,</div>
<div class="line"><a name="l00037"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bae07a708ec52c578b62f8b0f701571d56"> 37</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bae07a708ec52c578b62f8b0f701571d56">RATIONAL_EXPR</a> = 3,</div>
<div class="line"><a name="l00038"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba354df7c2d2ec2e54317f07437dc7380b"> 38</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba354df7c2d2ec2e54317f07437dc7380b">STRING_EXPR</a> = 4,</div>
<div class="line"><a name="l00039"></a><span class="lineno"> 39</span> </div>
<div class="line"><a name="l00040"></a><span class="lineno"> 40</span>  <span class="comment">// All constants should have kinds less than MAX_CONST</span></div>
<div class="line"><a name="l00041"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3618e875d4c212a43e224a8a8745e7eb"> 41</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3618e875d4c212a43e224a8a8745e7eb">MAX_CONST</a> = 100,</div>
<div class="line"><a name="l00042"></a><span class="lineno"> 42</span> </div>
<div class="line"><a name="l00043"></a><span class="lineno"> 43</span>  <span class="comment">// Generic LISP kinds for representing raw parsed expressions</span></div>
<div class="line"><a name="l00044"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2"> 44</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a>, <span class="comment">//!< May have any number of children >= 0</span></div>
<div class="line"><a name="l00045"></a><span class="lineno"> 45</span> <span class="comment"></span><span class="comment"> //! Identifier is (ID (STRING_EXPR "name"))</span></div>
<div class="line"><a name="l00046"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba001479a58fb44c39a29b20d565081a68"> 46</a></span> <span class="comment"></span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba001479a58fb44c39a29b20d565081a68" title="Identifier is (ID (STRING_EXPR "name"))">ID</a>,</div>
<div class="line"><a name="l00047"></a><span class="lineno"> 47</span>  <span class="comment">// Types</span></div>
<div class="line"><a name="l00048"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba8a583f16e8d237a423c8c1d9087a4c72"> 48</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba8a583f16e8d237a423c8c1d9087a4c72">BOOLEAN</a>,</div>
<div class="line"><a name="l00049"></a><span class="lineno"> 49</span> <span class="comment">// TUPLE_TYPE,</span></div>
<div class="line"><a name="l00050"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba6245843ec0c376adc7b587ad82459846"> 50</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba6245843ec0c376adc7b587ad82459846">ANY_TYPE</a>,</div>
<div class="line"><a name="l00051"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba546eccfedc4dcc8623ed0668f77ef982"> 51</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba546eccfedc4dcc8623ed0668f77ef982">ARROW</a>,</div>
<div class="line"><a name="l00052"></a><span class="lineno"> 52</span>  <span class="comment">// The "type" of any expression type (as in BOOLEAN : TYPE).</span></div>
<div class="line"><a name="l00053"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab47ea8bb955afd0adc0ef98517dd6084"> 53</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab47ea8bb955afd0adc0ef98517dd6084">TYPE</a>,</div>
<div class="line"><a name="l00054"></a><span class="lineno"> 54</span>  <span class="comment">// Declaration of new (uninterpreted) types: T1, T2, ... : TYPE</span></div>
<div class="line"><a name="l00055"></a><span class="lineno"> 55</span>  <span class="comment">// (TYPEDECL T1 T2 ...)</span></div>
<div class="line"><a name="l00056"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3bcf72a59026c6765481b300b363ff59"> 56</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3bcf72a59026c6765481b300b363ff59">TYPEDECL</a>,</div>
<div class="line"><a name="l00057"></a><span class="lineno"> 57</span>  <span class="comment">// Declaration of a defined type T : TYPE = type === (TYPEDEF T type)</span></div>
<div class="line"><a name="l00058"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba802d02227696a7c5b5420b28d8b82338"> 58</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba802d02227696a7c5b5420b28d8b82338">TYPEDEF</a>,</div>
<div class="line"><a name="l00059"></a><span class="lineno"> 59</span> </div>
<div class="line"><a name="l00060"></a><span class="lineno"> 60</span>  <span class="comment">// Equality</span></div>
<div class="line"><a name="l00061"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f"> 61</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>,</div>
<div class="line"><a name="l00062"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab4ab8d2a8dc61f08e3cc919787c79cd8"> 62</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab4ab8d2a8dc61f08e3cc919787c79cd8">NEQ</a>,</div>
<div class="line"><a name="l00063"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa23a9880eca693f679c969556249925f"> 63</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa23a9880eca693f679c969556249925f">DISTINCT</a>,</div>
<div class="line"><a name="l00064"></a><span class="lineno"> 64</span> </div>
<div class="line"><a name="l00065"></a><span class="lineno"> 65</span>  <span class="comment">// Propositional connectives</span></div>
<div class="line"><a name="l00066"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0378ebc895849163b249d0b330257dd6"> 66</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0378ebc895849163b249d0b330257dd6">NOT</a>,</div>
<div class="line"><a name="l00067"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba865555c9f2e0458a7078486aa1b3254f"> 67</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba865555c9f2e0458a7078486aa1b3254f">AND</a>,</div>
<div class="line"><a name="l00068"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074"> 68</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>,</div>
<div class="line"><a name="l00069"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bac62338ffb5de22369c75caa565b5da1a"> 69</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bac62338ffb5de22369c75caa565b5da1a">XOR</a>,</div>
<div class="line"><a name="l00070"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7"> 70</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>,</div>
<div class="line"><a name="l00071"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7338bb59b9aa936104a6d2f631d4d8db"> 71</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7338bb59b9aa936104a6d2f631d4d8db">IMPLIES</a>,</div>
<div class="line"><a name="l00072"></a><span class="lineno"> 72</span>  <span class="comment">// BOOL_VAR, //!< Boolean variables are treated as 0-ary predicates</span></div>
<div class="line"><a name="l00073"></a><span class="lineno"> 73</span> </div>
<div class="line"><a name="l00074"></a><span class="lineno"> 74</span>  <span class="comment">// Propositional relations (for circuit propagation)</span></div>
<div class="line"><a name="l00075"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf18208f4921c8175373d32e4ce909d42"> 75</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf18208f4921c8175373d32e4ce909d42">AND_R</a>,</div>
<div class="line"><a name="l00076"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab3535bf1f1c26490d56f63dc20696fa6"> 76</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab3535bf1f1c26490d56f63dc20696fa6">IFF_R</a>,</div>
<div class="line"><a name="l00077"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba096c0758089b7d7d0a596b1b4c89a084"> 77</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba096c0758089b7d7d0a596b1b4c89a084">ITE_R</a>,</div>
<div class="line"><a name="l00078"></a><span class="lineno"> 78</span> </div>
<div class="line"><a name="l00079"></a><span class="lineno"> 79</span>  <span class="comment">// (ITE c e1 e2) == IF c THEN e1 ELSE e2 ENDIF, the internal</span></div>
<div class="line"><a name="l00080"></a><span class="lineno"> 80</span>  <span class="comment">// representation of the conditional. Parser produces (IF ...).</span></div>
<div class="line"><a name="l00081"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc"> 81</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc">ITE</a>,</div>
<div class="line"><a name="l00082"></a><span class="lineno"> 82</span> </div>
<div class="line"><a name="l00083"></a><span class="lineno"> 83</span>  <span class="comment">// Quantifiers</span></div>
<div class="line"><a name="l00084"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7b7b6f6e2b88589bd4656a14bcb7eb94"> 84</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7b7b6f6e2b88589bd4656a14bcb7eb94">FORALL</a>,</div>
<div class="line"><a name="l00085"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3197625a1bb2264943f5a95f236d9973"> 85</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3197625a1bb2264943f5a95f236d9973">EXISTS</a>,</div>
<div class="line"><a name="l00086"></a><span class="lineno"> 86</span> </div>
<div class="line"><a name="l00087"></a><span class="lineno"> 87</span>  <span class="comment">// Uninterpreted function</span></div>
<div class="line"><a name="l00088"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa677b4263f974f2ccfe7986cedf3988e"> 88</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa677b4263f974f2ccfe7986cedf3988e">UFUNC</a>,</div>
<div class="line"><a name="l00089"></a><span class="lineno"> 89</span>  <span class="comment">// Application of a function</span></div>
<div class="line"><a name="l00090"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5c41450c4e719ca40d8e734f6a2008f0"> 90</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5c41450c4e719ca40d8e734f6a2008f0">APPLY</a>,</div>
<div class="line"><a name="l00091"></a><span class="lineno"> 91</span> </div>
<div class="line"><a name="l00092"></a><span class="lineno"> 92</span>  <span class="comment">// Top-level Commands</span></div>
<div class="line"><a name="l00093"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba61d9e0e93eb9635173764c5ba45666f1"> 93</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba61d9e0e93eb9635173764c5ba45666f1">ASSERT</a>,</div>
<div class="line"><a name="l00094"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba21043ddfa5289b4cf14cd4e3f5a89b62"> 94</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba21043ddfa5289b4cf14cd4e3f5a89b62">QUERY</a>,</div>
<div class="line"><a name="l00095"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba97a3c2659984ba305c883c77e5d837be"> 95</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba97a3c2659984ba305c883c77e5d837be">CHECKSAT</a>,</div>
<div class="line"><a name="l00096"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba49959dd441dcda75d6898cf2c68fb374"> 96</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba49959dd441dcda75d6898cf2c68fb374">CONTINUE</a>,</div>
<div class="line"><a name="l00097"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba262553c759e1d1a9398bc406b1fadcb7"> 97</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba262553c759e1d1a9398bc406b1fadcb7">RESTART</a>,</div>
<div class="line"><a name="l00098"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba488607ea6c5f90b63a063b953af1e078"> 98</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba488607ea6c5f90b63a063b953af1e078">DBG</a>,</div>
<div class="line"><a name="l00099"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e"> 99</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>,</div>
<div class="line"><a name="l00100"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba4360655450c463532deae4a265852354"> 100</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba4360655450c463532deae4a265852354">UNTRACE</a>,</div>
<div class="line"><a name="l00101"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa90a72437604db645f335d571993dade"> 101</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa90a72437604db645f335d571993dade">OPTION</a>,</div>
<div class="line"><a name="l00102"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9f5cb747b2e1f0ea781d2b1f2a5b4824"> 102</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9f5cb747b2e1f0ea781d2b1f2a5b4824">HELP</a>,</div>
<div class="line"><a name="l00103"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba25f73324dc93d9024c0c75b4e6815335"> 103</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba25f73324dc93d9024c0c75b4e6815335">TRANSFORM</a>,</div>
<div class="line"><a name="l00104"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab107229d44d042caa8ab8df4c8acaa1f"> 104</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab107229d44d042caa8ab8df4c8acaa1f">PRINT</a>,</div>
<div class="line"><a name="l00105"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5babd0ebc08c262bab82a1882256d2d66e8"> 105</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5babd0ebc08c262bab82a1882256d2d66e8">CALL</a>,</div>
<div class="line"><a name="l00106"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba6e074abc1ec6368da315a331ad35c00b"> 106</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba6e074abc1ec6368da315a331ad35c00b">ECHO</a>,</div>
<div class="line"><a name="l00107"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2f6f94469432973066c534d9bd1d1a7c"> 107</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2f6f94469432973066c534d9bd1d1a7c">INCLUDE</a>,</div>
<div class="line"><a name="l00108"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf2fb94d1fd1739ad68220e57882efa23"> 108</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf2fb94d1fd1739ad68220e57882efa23">GET_VALUE</a>,</div>
<div class="line"><a name="l00109"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba93ac551e3fa00bc3ba324544985e0e07"> 109</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba93ac551e3fa00bc3ba324544985e0e07">GET_ASSIGNMENT</a>,</div>
<div class="line"><a name="l00110"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baaa71d9f5a927e04c20c2fe5708f30be2"> 110</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baaa71d9f5a927e04c20c2fe5708f30be2">DUMP_PROOF</a>,</div>
<div class="line"><a name="l00111"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab31d3b785074846671439597e155a473"> 111</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab31d3b785074846671439597e155a473">DUMP_ASSUMPTIONS</a>,</div>
<div class="line"><a name="l00112"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7d5922eb81555f9010561ea51e241313"> 112</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7d5922eb81555f9010561ea51e241313">DUMP_SIG</a>,</div>
<div class="line"><a name="l00113"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0f26f0a2b11e05637f9aede0c3c953a1"> 113</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0f26f0a2b11e05637f9aede0c3c953a1">DUMP_TCC</a>,</div>
<div class="line"><a name="l00114"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba806bb6dde10ffd8d7e12b01cf8a04421"> 114</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba806bb6dde10ffd8d7e12b01cf8a04421">DUMP_TCC_ASSUMPTIONS</a>,</div>
<div class="line"><a name="l00115"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba8d86d3a8550f33dfb735dc25813c5794"> 115</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba8d86d3a8550f33dfb735dc25813c5794">DUMP_TCC_PROOF</a>,</div>
<div class="line"><a name="l00116"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5badbf9b8b24fc59b74bd2b2121aba21e75"> 116</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5badbf9b8b24fc59b74bd2b2121aba21e75">DUMP_CLOSURE</a>,</div>
<div class="line"><a name="l00117"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2322495bb9d482b215bc6b52df111415"> 117</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2322495bb9d482b215bc6b52df111415">DUMP_CLOSURE_PROOF</a>,</div>
<div class="line"><a name="l00118"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0116b78582fbf1fd6e069fde8dd308c4"> 118</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0116b78582fbf1fd6e069fde8dd308c4">WHERE</a>,</div>
<div class="line"><a name="l00119"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bafa9d306e675c3be077c2e0561e6e8e6d"> 119</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bafa9d306e675c3be077c2e0561e6e8e6d">ASSERTIONS</a>,</div>
<div class="line"><a name="l00120"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab65def84e41af84db85737a6eb8dc748"> 120</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab65def84e41af84db85737a6eb8dc748">ASSUMPTIONS</a>,</div>
<div class="line"><a name="l00121"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba87ad730e285cf17f4eefb214236a2c7a"> 121</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba87ad730e285cf17f4eefb214236a2c7a">COUNTEREXAMPLE</a>,</div>
<div class="line"><a name="l00122"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baea3d2c8907d2df3f13c0866a7970baaa"> 122</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baea3d2c8907d2df3f13c0866a7970baaa">COUNTERMODEL</a>,</div>
<div class="line"><a name="l00123"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bad263caec619c4d99e4684ba0fabd9493"> 123</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bad263caec619c4d99e4684ba0fabd9493">PUSH</a>,</div>
<div class="line"><a name="l00124"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba061dcf4785583d8653942f2d252174fa"> 124</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba061dcf4785583d8653942f2d252174fa">POP</a>,</div>
<div class="line"><a name="l00125"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba908bcfbc13c7f414e83641bb9339f31f"> 125</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba908bcfbc13c7f414e83641bb9339f31f">POPTO</a>,</div>
<div class="line"><a name="l00126"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5b5b049bfd6cb81f552222a8aad0dd99"> 126</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5b5b049bfd6cb81f552222a8aad0dd99">PUSH_SCOPE</a>,</div>
<div class="line"><a name="l00127"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0eb24f3375e74e8a42303dc0c6e7e952"> 127</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0eb24f3375e74e8a42303dc0c6e7e952">POP_SCOPE</a>,</div>
<div class="line"><a name="l00128"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba577463735743ccd8d67d3549bdcbc5eb"> 128</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba577463735743ccd8d67d3549bdcbc5eb">POPTO_SCOPE</a>,</div>
<div class="line"><a name="l00129"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba589b7d94a3d91d145720e2fed0eb3a05"> 129</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba589b7d94a3d91d145720e2fed0eb3a05">RESET</a>,</div>
<div class="line"><a name="l00130"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7f06283f0d1a4d167be6c37a3d24fd11"> 130</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7f06283f0d1a4d167be6c37a3d24fd11">CONTEXT</a>,</div>
<div class="line"><a name="l00131"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5badd6ce7bf1c9b230e53a39d09a7d6e002"> 131</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5badd6ce7bf1c9b230e53a39d09a7d6e002">FORGET</a>,</div>
<div class="line"><a name="l00132"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9d77c0f7e14e04b7ecc95a029f669d83"> 132</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9d77c0f7e14e04b7ecc95a029f669d83">GET_TYPE</a>,</div>
<div class="line"><a name="l00133"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba915f5acbb5f4374dd2c4e9a37a40d2ef"> 133</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba915f5acbb5f4374dd2c4e9a37a40d2ef">CHECK_TYPE</a>,</div>
<div class="line"><a name="l00134"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf87d4fe879a908f02ae07de41fff425e"> 134</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf87d4fe879a908f02ae07de41fff425e">GET_CHILD</a>,</div>
<div class="line"><a name="l00135"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf910b817eb56e0a5ce680b74a0e8dc84"> 135</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf910b817eb56e0a5ce680b74a0e8dc84">SUBSTITUTE</a>,</div>
<div class="line"><a name="l00136"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9985ac4cb7cda855d785a610e6a866a7"> 136</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9985ac4cb7cda855d785a610e6a866a7">SEQ</a>,</div>
<div class="line"><a name="l00137"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba62e1f4af4ae37d9c8a7f60bf47e4e72c"> 137</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba62e1f4af4ae37d9c8a7f60bf47e4e72c">ARITH_VAR_ORDER</a>,</div>
<div class="line"><a name="l00138"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba6f0302a99e7b65b652008363069ad743"> 138</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba6f0302a99e7b65b652008363069ad743">ANNOTATION</a>,</div>
<div class="line"><a name="l00139"></a><span class="lineno"> 139</span> </div>
<div class="line"><a name="l00140"></a><span class="lineno"> 140</span>  <span class="comment">// Kinds used mostly in the parser</span></div>
<div class="line"><a name="l00141"></a><span class="lineno"> 141</span> </div>
<div class="line"><a name="l00142"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa74ae94cd8d7d555f0ca4c85ef80ad08"> 142</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa74ae94cd8d7d555f0ca4c85ef80ad08">TCC</a>,</div>
<div class="line"><a name="l00143"></a><span class="lineno"> 143</span>  <span class="comment">// Variable declaration (VARDECL v1 v2 ... v_n type). A variable</span></div>
<div class="line"><a name="l00144"></a><span class="lineno"> 144</span>  <span class="comment">// can be an ID or a BOUNDVAR.</span></div>
<div class="line"><a name="l00145"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5ccfef7d76eb43a61d00eb7129ffc562"> 145</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5ccfef7d76eb43a61d00eb7129ffc562">VARDECL</a>,</div>
<div class="line"><a name="l00146"></a><span class="lineno"> 146</span>  <span class="comment">// A list of variable declarations (VARDECLS (VARDECL ...) (VARDECL ...) ...)</span></div>
<div class="line"><a name="l00147"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7266e0d07f5aabab9d0515ea50fafc7c"> 147</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7266e0d07f5aabab9d0515ea50fafc7c">VARDECLS</a>,</div>
<div class="line"><a name="l00148"></a><span class="lineno"> 148</span> </div>
<div class="line"><a name="l00149"></a><span class="lineno"> 149</span>  <span class="comment">// Bound variables have a "printable name", the one the user typed</span></div>
<div class="line"><a name="l00150"></a><span class="lineno"> 150</span>  <span class="comment">// in, and a uniqueID used to distinguish it from other bound</span></div>
<div class="line"><a name="l00151"></a><span class="lineno"> 151</span>  <span class="comment">// variables, which is effectively the alpha-renaming:</span></div>
<div class="line"><a name="l00152"></a><span class="lineno"> 152</span> </div>
<div class="line"><a name="l00153"></a><span class="lineno"> 153</span>  <span class="comment">// Op(BOUND_VAR (BOUND_ID "user_name" "uniqueID")). Note that</span></div>
<div class="line"><a name="l00154"></a><span class="lineno"> 154</span>  <span class="comment">// BOUND_VAR is an operator (Expr without children), just as UFUNC</span></div>
<div class="line"><a name="l00155"></a><span class="lineno"> 155</span>  <span class="comment">// and UCONST.</span></div>
<div class="line"><a name="l00156"></a><span class="lineno"> 156</span> </div>
<div class="line"><a name="l00157"></a><span class="lineno"> 157</span>  <span class="comment">// The uniqueID normally is just a number, so one can print a bound</span></div>
<div class="line"><a name="l00158"></a><span class="lineno"> 158</span>  <span class="comment">// variable X as X_17.</span></div>
<div class="line"><a name="l00159"></a><span class="lineno"> 159</span> </div>
<div class="line"><a name="l00160"></a><span class="lineno"> 160</span>  <span class="comment">// NOTE that in the parsed expressions like LET x: T = e IN foo(x),</span></div>
<div class="line"><a name="l00161"></a><span class="lineno"> 161</span>  <span class="comment">// the second instance of 'x' will be an ID, and *not* a BOUNDVAR.</span></div>
<div class="line"><a name="l00162"></a><span class="lineno"> 162</span>  <span class="comment">// The parser does not know how to resolve bound variables, and it</span></div>
<div class="line"><a name="l00163"></a><span class="lineno"> 163</span>  <span class="comment">// has to be resolved later.</span></div>
<div class="line"><a name="l00164"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba462c38186c36e12c2f38a6d0d43feddf"> 164</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba462c38186c36e12c2f38a6d0d43feddf">BOUND_VAR</a>,</div>
<div class="line"><a name="l00165"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2a1805dc0fcdef2abbf0c780ab1c47ae"> 165</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2a1805dc0fcdef2abbf0c780ab1c47ae">BOUND_ID</a>,</div>
<div class="line"><a name="l00166"></a><span class="lineno"> 166</span> </div>
<div class="line"><a name="l00167"></a><span class="lineno"> 167</span>  <span class="comment">// Updator "e1 WITH <bunch of stuff> := e2" is represented as</span></div>
<div class="line"><a name="l00168"></a><span class="lineno"> 168</span>  <span class="comment">// (UPDATE e1 (UPDATE_SELECT <bunch of stuff>) e2), where <bunch</span></div>
<div class="line"><a name="l00169"></a><span class="lineno"> 169</span>  <span class="comment">// of stuff> is the list of accessors:</span></div>
<div class="line"><a name="l00170"></a><span class="lineno"> 170</span>  <span class="comment">// (READ idx)</span></div>
<div class="line"><a name="l00171"></a><span class="lineno"> 171</span>  <span class="comment">// ID (what's that for?)</span></div>
<div class="line"><a name="l00172"></a><span class="lineno"> 172</span>  <span class="comment">// (REC_SELECT ID)</span></div>
<div class="line"><a name="l00173"></a><span class="lineno"> 173</span>  <span class="comment">// and (TUPLE_SELECT num).</span></div>
<div class="line"><a name="l00174"></a><span class="lineno"> 174</span> <span class="comment">// UPDATE,</span></div>
<div class="line"><a name="l00175"></a><span class="lineno"> 175</span> <span class="comment">// UPDATE_SELECT,</span></div>
<div class="line"><a name="l00176"></a><span class="lineno"> 176</span>  <span class="comment">// Record type [# f1 : t1, f2 : t2 ... #] is represented as</span></div>
<div class="line"><a name="l00177"></a><span class="lineno"> 177</span>  <span class="comment">// (RECORD_TYPE (f1 t1) (f2 t2) ... )</span></div>
<div class="line"><a name="l00178"></a><span class="lineno"> 178</span> <span class="comment">// RECORD_TYPE,</span></div>
<div class="line"><a name="l00179"></a><span class="lineno"> 179</span> <span class="comment">// // (# f1=e1, f2=e2, ...#) == (RECORD (f1 e1) ...)</span></div>
<div class="line"><a name="l00180"></a><span class="lineno"> 180</span> <span class="comment">// RECORD,</span></div>
<div class="line"><a name="l00181"></a><span class="lineno"> 181</span> <span class="comment">// RECORD_SELECT,</span></div>
<div class="line"><a name="l00182"></a><span class="lineno"> 182</span> <span class="comment">// RECORD_UPDATE,</span></div>
<div class="line"><a name="l00183"></a><span class="lineno"> 183</span> </div>
<div class="line"><a name="l00184"></a><span class="lineno"> 184</span> <span class="comment">// // (e1, e2, ...) == (TUPLE e1 e2 ...)</span></div>
<div class="line"><a name="l00185"></a><span class="lineno"> 185</span> <span class="comment">// TUPLE,</span></div>
<div class="line"><a name="l00186"></a><span class="lineno"> 186</span> <span class="comment">// TUPLE_SELECT,</span></div>
<div class="line"><a name="l00187"></a><span class="lineno"> 187</span> <span class="comment">// TUPLE_UPDATE,</span></div>
<div class="line"><a name="l00188"></a><span class="lineno"> 188</span> </div>
<div class="line"><a name="l00189"></a><span class="lineno"> 189</span> <span class="comment">// SUBRANGE,</span></div>
<div class="line"><a name="l00190"></a><span class="lineno"> 190</span>  <span class="comment">// Enumerated type (SCALARTYPE v1 v2 ...)</span></div>
<div class="line"><a name="l00191"></a><span class="lineno"> 191</span> <span class="comment">// SCALARTYPE,</span></div>
<div class="line"><a name="l00192"></a><span class="lineno"> 192</span>  <span class="comment">// Predicate subtype: the argument is the predicate (lambda-expression)</span></div>
<div class="line"><a name="l00193"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9ae776fb49b0eb32dd93f866492000b5"> 193</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9ae776fb49b0eb32dd93f866492000b5">SUBTYPE</a>,</div>
<div class="line"><a name="l00194"></a><span class="lineno"> 194</span>  <span class="comment">// Datatype is Expr(DATATYPE, Constructors), where Constructors is a</span></div>
<div class="line"><a name="l00195"></a><span class="lineno"> 195</span>  <span class="comment">// vector of Expr(CONSTRUCTOR, id [ , arg ]), where 'id' is an ID,</span></div>
<div class="line"><a name="l00196"></a><span class="lineno"> 196</span>  <span class="comment">// and 'arg' a VARDECL node (list of variable declarations with</span></div>
<div class="line"><a name="l00197"></a><span class="lineno"> 197</span>  <span class="comment">// types). If 'arg' is present, the constructor has arguments</span></div>
<div class="line"><a name="l00198"></a><span class="lineno"> 198</span>  <span class="comment">// corresponding to the declared variables.</span></div>
<div class="line"><a name="l00199"></a><span class="lineno"> 199</span> <span class="comment">// DATATYPE,</span></div>
<div class="line"><a name="l00200"></a><span class="lineno"> 200</span> <span class="comment">// THISTYPE, // Used to indicate recursion in recursive datatypes</span></div>
<div class="line"><a name="l00201"></a><span class="lineno"> 201</span> <span class="comment">// CONSTRUCTOR,</span></div>
<div class="line"><a name="l00202"></a><span class="lineno"> 202</span> <span class="comment">// SELECTOR,</span></div>
<div class="line"><a name="l00203"></a><span class="lineno"> 203</span> <span class="comment">// TESTER,</span></div>
<div class="line"><a name="l00204"></a><span class="lineno"> 204</span>  <span class="comment">// Expression e WITH accessor := e2 is transformed by the command</span></div>
<div class="line"><a name="l00205"></a><span class="lineno"> 205</span>  <span class="comment">// processor into (DATATYPE_UPDATE e accessor e2), where e is the</span></div>
<div class="line"><a name="l00206"></a><span class="lineno"> 206</span>  <span class="comment">// original datatype value C(a1, ..., an) (here C is the</span></div>
<div class="line"><a name="l00207"></a><span class="lineno"> 207</span>  <span class="comment">// constructor), and "accessor" is the name of one of the arguments</span></div>
<div class="line"><a name="l00208"></a><span class="lineno"> 208</span>  <span class="comment">// a_i of C.</span></div>
<div class="line"><a name="l00209"></a><span class="lineno"> 209</span>  <span class="comment">// DATATYPE_UPDATE,</span></div>
<div class="line"><a name="l00210"></a><span class="lineno"> 210</span>  <span class="comment">// Statement IF c1 THEN e1 ELSIF c2 THEN e2 ... ELSE e_n ENDIF is</span></div>
<div class="line"><a name="l00211"></a><span class="lineno"> 211</span>  <span class="comment">// represented as (IF (IFTHEN c1 e1) (IFTHEN c2 e2) ... (ELSE e_n))</span></div>
<div class="line"><a name="l00212"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba252802eda493fb6b4a279c4452acb547"> 212</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba252802eda493fb6b4a279c4452acb547">IF</a>,</div>
<div class="line"><a name="l00213"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5bd60ae173f903f6b202daf0c2118387"> 213</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5bd60ae173f903f6b202daf0c2118387">IFTHEN</a>,</div>
<div class="line"><a name="l00214"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba90d649d830ea440c8b8a56c7ef23c426"> 214</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba90d649d830ea440c8b8a56c7ef23c426">ELSE</a>,</div>
<div class="line"><a name="l00215"></a><span class="lineno"> 215</span>  <span class="comment">// Lisp version of multi-branch IF:</span></div>
<div class="line"><a name="l00216"></a><span class="lineno"> 216</span>  <span class="comment">// (COND (c1 e1) (c2 e2) ... (ELSE en))</span></div>
<div class="line"><a name="l00217"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2f577f27f1d0dcd6aa8f0a144138dc42"> 217</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2f577f27f1d0dcd6aa8f0a144138dc42">COND</a>,</div>
<div class="line"><a name="l00218"></a><span class="lineno"> 218</span> </div>
<div class="line"><a name="l00219"></a><span class="lineno"> 219</span>  <span class="comment">// LET x1: t1 = e1, x2: t2 = e2, ... IN e</span></div>
<div class="line"><a name="l00220"></a><span class="lineno"> 220</span>  <span class="comment">// Parser builds:</span></div>
<div class="line"><a name="l00221"></a><span class="lineno"> 221</span>  <span class="comment">// (LET (LETDECLS (LETDECL x1 t1 e1) (LETDECL x2 t2 e2) ... ) e)</span></div>
<div class="line"><a name="l00222"></a><span class="lineno"> 222</span>  <span class="comment">// where each x_i is a BOUNDVAR.</span></div>
<div class="line"><a name="l00223"></a><span class="lineno"> 223</span>  <span class="comment">// After processing, it is rebuilt to have (LETDECL var def); the</span></div>
<div class="line"><a name="l00224"></a><span class="lineno"> 224</span>  <span class="comment">// type is set as the attribute to var.</span></div>
<div class="line"><a name="l00225"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bafb72619a5a922e816967c4aa49301754"> 225</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bafb72619a5a922e816967c4aa49301754">LET</a>,</div>
<div class="line"><a name="l00226"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2cd77861cfba212beedbf4245c990f72"> 226</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2cd77861cfba212beedbf4245c990f72">LETDECLS</a>,</div>
<div class="line"><a name="l00227"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9508dd8c8e7db280a5dacc19bd74d92d"> 227</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9508dd8c8e7db280a5dacc19bd74d92d">LETDECL</a>,</div>
<div class="line"><a name="l00228"></a><span class="lineno"> 228</span>  <span class="comment">// Lambda-abstraction LAMBDA (<vars>) : e === (LAMBDA <vars> e)</span></div>
<div class="line"><a name="l00229"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba40176493726a127184ca47ea6352dc1f"> 229</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba40176493726a127184ca47ea6352dc1f">LAMBDA</a>,</div>
<div class="line"><a name="l00230"></a><span class="lineno"> 230</span>  <span class="comment">// Symbolic simulation operator</span></div>
<div class="line"><a name="l00231"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa1022ff97dac8e2d5d80d53c4cecd132"> 231</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa1022ff97dac8e2d5d80d53c4cecd132">SIMULATE</a>,</div>
<div class="line"><a name="l00232"></a><span class="lineno"> 232</span> </div>
<div class="line"><a name="l00233"></a><span class="lineno"> 233</span>  <span class="comment">// Uninterpreted constants (variables) x1, x2, ... , x_n : type</span></div>
<div class="line"><a name="l00234"></a><span class="lineno"> 234</span>  <span class="comment">// (CONST (VARLIST x1 x2 ... x_n) type)</span></div>
<div class="line"><a name="l00235"></a><span class="lineno"> 235</span>  <span class="comment">// Uninterpreted functions are declared as constants of functional type.</span></div>
<div class="line"><a name="l00236"></a><span class="lineno"> 236</span> </div>
<div class="line"><a name="l00237"></a><span class="lineno"> 237</span>  <span class="comment">// After processing, uninterpreted functions and constants</span></div>
<div class="line"><a name="l00238"></a><span class="lineno"> 238</span>  <span class="comment">// (a.k.a. variables) are represented as Op(UFUNC, (ID "name")) and</span></div>
<div class="line"><a name="l00239"></a><span class="lineno"> 239</span>  <span class="comment">// Op(UCONST, (ID "name")) with the appropriate type attribute.</span></div>
<div class="line"><a name="l00240"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3d044162d972156d897cea80f216b9ca"> 240</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3d044162d972156d897cea80f216b9ca">CONST</a>,</div>
<div class="line"><a name="l00241"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba197dcccceb8ad4d4bd3b914f73f2978a"> 241</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba197dcccceb8ad4d4bd3b914f73f2978a">VARLIST</a>,</div>
<div class="line"><a name="l00242"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2efaeb22f8803588598706b73cec8bda"> 242</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2efaeb22f8803588598706b73cec8bda">UCONST</a>,</div>
<div class="line"><a name="l00243"></a><span class="lineno"> 243</span> </div>
<div class="line"><a name="l00244"></a><span class="lineno"> 244</span>  <span class="comment">// User function definition f(args) : type = e === (DEFUN args type e)</span></div>
<div class="line"><a name="l00245"></a><span class="lineno"> 245</span>  <span class="comment">// Here 'args' are bound var declarations</span></div>
<div class="line"><a name="l00246"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5a9e497d7471e5d91bd097e5b80a830d"> 246</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5a9e497d7471e5d91bd097e5b80a830d">DEFUN</a>,</div>
<div class="line"><a name="l00247"></a><span class="lineno"> 247</span> </div>
<div class="line"><a name="l00248"></a><span class="lineno"> 248</span>  <span class="comment">// Arithmetic types and operators</span></div>
<div class="line"><a name="l00249"></a><span class="lineno"> 249</span> <span class="comment">// REAL,</span></div>
<div class="line"><a name="l00250"></a><span class="lineno"> 250</span> <span class="comment">// INT,</span></div>
<div class="line"><a name="l00251"></a><span class="lineno"> 251</span> </div>
<div class="line"><a name="l00252"></a><span class="lineno"> 252</span> <span class="comment">// UMINUS,</span></div>
<div class="line"><a name="l00253"></a><span class="lineno"> 253</span> <span class="comment">// PLUS,</span></div>
<div class="line"><a name="l00254"></a><span class="lineno"> 254</span> <span class="comment">// MINUS,</span></div>
<div class="line"><a name="l00255"></a><span class="lineno"> 255</span> <span class="comment">// MULT,</span></div>
<div class="line"><a name="l00256"></a><span class="lineno"> 256</span> <span class="comment">// DIVIDE,</span></div>
<div class="line"><a name="l00257"></a><span class="lineno"> 257</span> <span class="comment">// INTDIV,</span></div>
<div class="line"><a name="l00258"></a><span class="lineno"> 258</span> <span class="comment">// MOD,</span></div>
<div class="line"><a name="l00259"></a><span class="lineno"> 259</span> <span class="comment">// LT,</span></div>
<div class="line"><a name="l00260"></a><span class="lineno"> 260</span> <span class="comment">// LE,</span></div>
<div class="line"><a name="l00261"></a><span class="lineno"> 261</span> <span class="comment">// GT,</span></div>
<div class="line"><a name="l00262"></a><span class="lineno"> 262</span> <span class="comment">// GE,</span></div>
<div class="line"><a name="l00263"></a><span class="lineno"> 263</span> <span class="comment">// IS_INTEGER,</span></div>
<div class="line"><a name="l00264"></a><span class="lineno"> 264</span> <span class="comment">// NEGINF,</span></div>
<div class="line"><a name="l00265"></a><span class="lineno"> 265</span> <span class="comment">// POSINF,</span></div>
<div class="line"><a name="l00266"></a><span class="lineno"> 266</span> <span class="comment">// DARK_SHADOW,</span></div>
<div class="line"><a name="l00267"></a><span class="lineno"> 267</span> <span class="comment">// GRAY_SHADOW,</span></div>
<div class="line"><a name="l00268"></a><span class="lineno"> 268</span> </div>
<div class="line"><a name="l00269"></a><span class="lineno"> 269</span> <span class="comment">// //Floor theory operators</span></div>
<div class="line"><a name="l00270"></a><span class="lineno"> 270</span> <span class="comment">// FLOOR,</span></div>
<div class="line"><a name="l00271"></a><span class="lineno"> 271</span>  <span class="comment">// Kind for Extension to Non-linear Arithmetic</span></div>
<div class="line"><a name="l00272"></a><span class="lineno"> 272</span> <span class="comment">// POW,</span></div>
<div class="line"><a name="l00273"></a><span class="lineno"> 273</span> </div>
<div class="line"><a name="l00274"></a><span class="lineno"> 274</span>  <span class="comment">// Kinds for proof terms</span></div>
<div class="line"><a name="l00275"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baee1a6e6a0705cce09e48dbe8d3f26572"> 275</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baee1a6e6a0705cce09e48dbe8d3f26572">PF_APPLY</a>,</div>
<div class="line"><a name="l00276"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2656992cdd2e5b8fd78f595329c1f58f"> 276</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2656992cdd2e5b8fd78f595329c1f58f">PF_HOLE</a>,</div>
<div class="line"><a name="l00277"></a><span class="lineno"> 277</span> </div>
<div class="line"><a name="l00278"></a><span class="lineno"> 278</span> </div>
<div class="line"><a name="l00279"></a><span class="lineno"> 279</span> <span class="comment">// // Mlss</span></div>
<div class="line"><a name="l00280"></a><span class="lineno"> 280</span> <span class="comment">// EMPTY, // {}</span></div>
<div class="line"><a name="l00281"></a><span class="lineno"> 281</span> <span class="comment">// UNION, // +</span></div>
<div class="line"><a name="l00282"></a><span class="lineno"> 282</span> <span class="comment">// INTER, // *</span></div>
<div class="line"><a name="l00283"></a><span class="lineno"> 283</span> <span class="comment">// DIFF,</span></div>
<div class="line"><a name="l00284"></a><span class="lineno"> 284</span> <span class="comment">// SINGLETON,</span></div>
<div class="line"><a name="l00285"></a><span class="lineno"> 285</span> <span class="comment">// IN,</span></div>
<div class="line"><a name="l00286"></a><span class="lineno"> 286</span> <span class="comment">// INCS,</span></div>
<div class="line"><a name="l00287"></a><span class="lineno"> 287</span> <span class="comment">// INCIN,</span></div>
<div class="line"><a name="l00288"></a><span class="lineno"> 288</span> </div>
<div class="line"><a name="l00289"></a><span class="lineno"> 289</span>  <span class="comment">//Skolem variable</span></div>
<div class="line"><a name="l00290"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba73072b2c6fef896d006d6691e932cf37"> 290</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba73072b2c6fef896d006d6691e932cf37">SKOLEM_VAR</a>,</div>
<div class="line"><a name="l00291"></a><span class="lineno"> 291</span>  <span class="comment">// Expr that holds a theorem</span></div>
<div class="line"><a name="l00292"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bada5edea8bbb7cfbd2500be6eca0d4151"> 292</a></span>  <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bada5edea8bbb7cfbd2500be6eca0d4151">THEOREM_KIND</a>,<span class="comment"></span></div>
<div class="line"><a name="l00293"></a><span class="lineno"> 293</span> <span class="comment"> //! Must always be the last kind</span></div>
<div class="line"><a name="l00294"></a><span class="lineno"><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bac8e823433db1723711ac5685ba2e7f60"> 294</a></span> <span class="comment"></span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bac8e823433db1723711ac5685ba2e7f60" title="Must always be the last kind.">LAST_KIND</a></div>
<div class="line"><a name="l00295"></a><span class="lineno"> 295</span> } <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5b">Kind</a>;</div>
<div class="line"><a name="l00296"></a><span class="lineno"> 296</span> </div>
<div class="line"><a name="l00297"></a><span class="lineno"> 297</span> <span class="preprocessor">#ifdef __cplusplus</span></div>
<div class="line"><a name="l00298"></a><span class="lineno"> 298</span> <span class="preprocessor"></span>} <span class="comment">// end of namespace CVC3</span></div>
<div class="line"><a name="l00299"></a><span class="lineno"> 299</span> <span class="preprocessor">#endif </span><span class="comment">/* __cplusplus */</span><span class="preprocessor"></span></div>
<div class="line"><a name="l00300"></a><span class="lineno"> 300</span> <span class="preprocessor"></span></div>
<div class="line"><a name="l00301"></a><span class="lineno"> 301</span> <span class="preprocessor">#endif</span></div>
</div><!-- fragment --></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:14 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
