<!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: kinds.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div class="header">
<div class="headertitle">
<div class="title">kinds.h</div> </div>
</div>
<div class="contents">
<a href="kinds_8h.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00002"></a>00002 <span class="comment">/*!</span>
<a name="l00003"></a>00003 <span class="comment"> * \file kinds.h</span>
<a name="l00004"></a>00004 <span class="comment"> *</span>
<a name="l00005"></a>00005 <span class="comment"> * Author: Clark Barrett</span>
<a name="l00006"></a>00006 <span class="comment"> *</span>
<a name="l00007"></a>00007 <span class="comment"> * Created: Mon Jan 20 13:38:52 2003</span>
<a name="l00008"></a>00008 <span class="comment"> *</span>
<a name="l00009"></a>00009 <span class="comment"> * <hr></span>
<a name="l00010"></a>00010 <span class="comment"> *</span>
<a name="l00011"></a>00011 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00012"></a>00012 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00013"></a>00013 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00014"></a>00014 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00015"></a>00015 <span class="comment"> *</span>
<a name="l00016"></a>00016 <span class="comment"> * <hr></span>
<a name="l00017"></a>00017 <span class="comment"> *</span>
<a name="l00018"></a>00018 <span class="comment"> */</span>
<a name="l00019"></a>00019 <span class="comment">/*****************************************************************************/</span>
<a name="l00020"></a>00020
<a name="l00021"></a>00021 <span class="preprocessor">#ifndef _cvc3__include__kinds_h_</span>
<a name="l00022"></a>00022 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__kinds_h_</span>
<a name="l00023"></a>00023 <span class="preprocessor"></span>
<a name="l00024"></a>00024 <span class="preprocessor">#ifdef __cplusplus</span>
<a name="l00025"></a>00025 <span class="preprocessor"></span><span class="keyword">namespace </span>CVC3 {
<a name="l00026"></a>00026 <span class="preprocessor">#endif </span><span class="comment">/* __cplusplus */</span>
<a name="l00027"></a>00027
<a name="l00028"></a>00028 <span class="comment">// The commonly used kinds and the kinds needed by the parser. All</span>
<a name="l00029"></a>00029 <span class="comment">// these kinds are registered by the ExprManager and are readily</span>
<a name="l00030"></a>00030 <span class="comment">// available for everyone else.</span>
<a name="l00031"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5b">00031</a> <span class="keyword">typedef</span> <span class="keyword">enum</span> {
<a name="l00032"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5bc05ce87fa69f660d39d0a4fa188c67">00032</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5bc05ce87fa69f660d39d0a4fa188c67">NULL_KIND</a> = 0,
<a name="l00033"></a>00033
<a name="l00034"></a>00034 <span class="comment">// Constant (Leaf) Exprs</span>
<a name="l00035"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba1fad76919fba496de21807e2beec533d">00035</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba1fad76919fba496de21807e2beec533d">TRUE_EXPR</a> = 1,
<a name="l00036"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5f71bd33a6528411ae681f5291de1d82">00036</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5f71bd33a6528411ae681f5291de1d82">FALSE_EXPR</a> = 2,
<a name="l00037"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bae07a708ec52c578b62f8b0f701571d56">00037</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bae07a708ec52c578b62f8b0f701571d56">RATIONAL_EXPR</a> = 3,
<a name="l00038"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba354df7c2d2ec2e54317f07437dc7380b">00038</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba354df7c2d2ec2e54317f07437dc7380b">STRING_EXPR</a> = 4,
<a name="l00039"></a>00039
<a name="l00040"></a>00040 <span class="comment">// All constants should have kinds less than MAX_CONST</span>
<a name="l00041"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3618e875d4c212a43e224a8a8745e7eb">00041</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3618e875d4c212a43e224a8a8745e7eb">MAX_CONST</a> = 100,
<a name="l00042"></a>00042
<a name="l00043"></a>00043 <span class="comment">// Generic LISP kinds for representing raw parsed expressions</span>
<a name="l00044"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">00044</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a>, <span class="comment">//!< May have any number of children >= 0</span>
<a name="l00045"></a>00045 <span class="comment"></span><span class="comment"> //! Identifier is (ID (STRING_EXPR "name"))</span>
<a name="l00046"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba001479a58fb44c39a29b20d565081a68">00046</a> <span class="comment"></span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba001479a58fb44c39a29b20d565081a68" title="Identifier is (ID (STRING_EXPR "name"))">ID</a>,
<a name="l00047"></a>00047 <span class="comment">// Types</span>
<a name="l00048"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba8a583f16e8d237a423c8c1d9087a4c72">00048</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba8a583f16e8d237a423c8c1d9087a4c72">BOOLEAN</a>,
<a name="l00049"></a>00049 <span class="comment">// TUPLE_TYPE,</span>
<a name="l00050"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba6245843ec0c376adc7b587ad82459846">00050</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba6245843ec0c376adc7b587ad82459846">ANY_TYPE</a>,
<a name="l00051"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba546eccfedc4dcc8623ed0668f77ef982">00051</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba546eccfedc4dcc8623ed0668f77ef982">ARROW</a>,
<a name="l00052"></a>00052 <span class="comment">// The "type" of any expression type (as in BOOLEAN : TYPE).</span>
<a name="l00053"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab47ea8bb955afd0adc0ef98517dd6084">00053</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab47ea8bb955afd0adc0ef98517dd6084">TYPE</a>,
<a name="l00054"></a>00054 <span class="comment">// Declaration of new (uninterpreted) types: T1, T2, ... : TYPE</span>
<a name="l00055"></a>00055 <span class="comment">// (TYPEDECL T1 T2 ...)</span>
<a name="l00056"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3bcf72a59026c6765481b300b363ff59">00056</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3bcf72a59026c6765481b300b363ff59">TYPEDECL</a>,
<a name="l00057"></a>00057 <span class="comment">// Declaration of a defined type T : TYPE = type === (TYPEDEF T type)</span>
<a name="l00058"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba802d02227696a7c5b5420b28d8b82338">00058</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba802d02227696a7c5b5420b28d8b82338">TYPEDEF</a>,
<a name="l00059"></a>00059
<a name="l00060"></a>00060 <span class="comment">// Equality</span>
<a name="l00061"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">00061</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9efdc855f3c1477957fb50affec07f8f">EQ</a>,
<a name="l00062"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab4ab8d2a8dc61f08e3cc919787c79cd8">00062</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab4ab8d2a8dc61f08e3cc919787c79cd8">NEQ</a>,
<a name="l00063"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa23a9880eca693f679c969556249925f">00063</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa23a9880eca693f679c969556249925f">DISTINCT</a>,
<a name="l00064"></a>00064
<a name="l00065"></a>00065 <span class="comment">// Propositional connectives</span>
<a name="l00066"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0378ebc895849163b249d0b330257dd6">00066</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0378ebc895849163b249d0b330257dd6">NOT</a>,
<a name="l00067"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba865555c9f2e0458a7078486aa1b3254f">00067</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba865555c9f2e0458a7078486aa1b3254f">AND</a>,
<a name="l00068"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">00068</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>,
<a name="l00069"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bac62338ffb5de22369c75caa565b5da1a">00069</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bac62338ffb5de22369c75caa565b5da1a">XOR</a>,
<a name="l00070"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">00070</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>,
<a name="l00071"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7338bb59b9aa936104a6d2f631d4d8db">00071</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7338bb59b9aa936104a6d2f631d4d8db">IMPLIES</a>,
<a name="l00072"></a>00072 <span class="comment">// BOOL_VAR, //!< Boolean variables are treated as 0-ary predicates</span>
<a name="l00073"></a>00073
<a name="l00074"></a>00074 <span class="comment">// Propositional relations (for circuit propagation)</span>
<a name="l00075"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf18208f4921c8175373d32e4ce909d42">00075</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf18208f4921c8175373d32e4ce909d42">AND_R</a>,
<a name="l00076"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab3535bf1f1c26490d56f63dc20696fa6">00076</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab3535bf1f1c26490d56f63dc20696fa6">IFF_R</a>,
<a name="l00077"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba096c0758089b7d7d0a596b1b4c89a084">00077</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba096c0758089b7d7d0a596b1b4c89a084">ITE_R</a>,
<a name="l00078"></a>00078
<a name="l00079"></a>00079 <span class="comment">// (ITE c e1 e2) == IF c THEN e1 ELSE e2 ENDIF, the internal</span>
<a name="l00080"></a>00080 <span class="comment">// representation of the conditional. Parser produces (IF ...).</span>
<a name="l00081"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc">00081</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc">ITE</a>,
<a name="l00082"></a>00082
<a name="l00083"></a>00083 <span class="comment">// Quantifiers</span>
<a name="l00084"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7b7b6f6e2b88589bd4656a14bcb7eb94">00084</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7b7b6f6e2b88589bd4656a14bcb7eb94">FORALL</a>,
<a name="l00085"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3197625a1bb2264943f5a95f236d9973">00085</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3197625a1bb2264943f5a95f236d9973">EXISTS</a>,
<a name="l00086"></a>00086
<a name="l00087"></a>00087 <span class="comment">// Uninterpreted function</span>
<a name="l00088"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa677b4263f974f2ccfe7986cedf3988e">00088</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa677b4263f974f2ccfe7986cedf3988e">UFUNC</a>,
<a name="l00089"></a>00089 <span class="comment">// Application of a function</span>
<a name="l00090"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5c41450c4e719ca40d8e734f6a2008f0">00090</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5c41450c4e719ca40d8e734f6a2008f0">APPLY</a>,
<a name="l00091"></a>00091
<a name="l00092"></a>00092 <span class="comment">// Top-level Commands</span>
<a name="l00093"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba61d9e0e93eb9635173764c5ba45666f1">00093</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba61d9e0e93eb9635173764c5ba45666f1">ASSERT</a>,
<a name="l00094"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba21043ddfa5289b4cf14cd4e3f5a89b62">00094</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba21043ddfa5289b4cf14cd4e3f5a89b62">QUERY</a>,
<a name="l00095"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba97a3c2659984ba305c883c77e5d837be">00095</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba97a3c2659984ba305c883c77e5d837be">CHECKSAT</a>,
<a name="l00096"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba49959dd441dcda75d6898cf2c68fb374">00096</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba49959dd441dcda75d6898cf2c68fb374">CONTINUE</a>,
<a name="l00097"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba262553c759e1d1a9398bc406b1fadcb7">00097</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba262553c759e1d1a9398bc406b1fadcb7">RESTART</a>,
<a name="l00098"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba488607ea6c5f90b63a063b953af1e078">00098</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba488607ea6c5f90b63a063b953af1e078">DBG</a>,
<a name="l00099"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">00099</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>,
<a name="l00100"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba4360655450c463532deae4a265852354">00100</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba4360655450c463532deae4a265852354">UNTRACE</a>,
<a name="l00101"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa90a72437604db645f335d571993dade">00101</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa90a72437604db645f335d571993dade">OPTION</a>,
<a name="l00102"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9f5cb747b2e1f0ea781d2b1f2a5b4824">00102</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9f5cb747b2e1f0ea781d2b1f2a5b4824">HELP</a>,
<a name="l00103"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba25f73324dc93d9024c0c75b4e6815335">00103</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba25f73324dc93d9024c0c75b4e6815335">TRANSFORM</a>,
<a name="l00104"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab107229d44d042caa8ab8df4c8acaa1f">00104</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab107229d44d042caa8ab8df4c8acaa1f">PRINT</a>,
<a name="l00105"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5babd0ebc08c262bab82a1882256d2d66e8">00105</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5babd0ebc08c262bab82a1882256d2d66e8">CALL</a>,
<a name="l00106"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba6e074abc1ec6368da315a331ad35c00b">00106</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba6e074abc1ec6368da315a331ad35c00b">ECHO</a>,
<a name="l00107"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2f6f94469432973066c534d9bd1d1a7c">00107</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2f6f94469432973066c534d9bd1d1a7c">INCLUDE</a>,
<a name="l00108"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf2fb94d1fd1739ad68220e57882efa23">00108</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf2fb94d1fd1739ad68220e57882efa23">GET_VALUE</a>,
<a name="l00109"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba93ac551e3fa00bc3ba324544985e0e07">00109</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba93ac551e3fa00bc3ba324544985e0e07">GET_ASSIGNMENT</a>,
<a name="l00110"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baaa71d9f5a927e04c20c2fe5708f30be2">00110</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baaa71d9f5a927e04c20c2fe5708f30be2">DUMP_PROOF</a>,
<a name="l00111"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab31d3b785074846671439597e155a473">00111</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab31d3b785074846671439597e155a473">DUMP_ASSUMPTIONS</a>,
<a name="l00112"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7d5922eb81555f9010561ea51e241313">00112</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7d5922eb81555f9010561ea51e241313">DUMP_SIG</a>,
<a name="l00113"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0f26f0a2b11e05637f9aede0c3c953a1">00113</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0f26f0a2b11e05637f9aede0c3c953a1">DUMP_TCC</a>,
<a name="l00114"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba806bb6dde10ffd8d7e12b01cf8a04421">00114</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba806bb6dde10ffd8d7e12b01cf8a04421">DUMP_TCC_ASSUMPTIONS</a>,
<a name="l00115"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba8d86d3a8550f33dfb735dc25813c5794">00115</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba8d86d3a8550f33dfb735dc25813c5794">DUMP_TCC_PROOF</a>,
<a name="l00116"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5badbf9b8b24fc59b74bd2b2121aba21e75">00116</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5badbf9b8b24fc59b74bd2b2121aba21e75">DUMP_CLOSURE</a>,
<a name="l00117"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2322495bb9d482b215bc6b52df111415">00117</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2322495bb9d482b215bc6b52df111415">DUMP_CLOSURE_PROOF</a>,
<a name="l00118"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0116b78582fbf1fd6e069fde8dd308c4">00118</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0116b78582fbf1fd6e069fde8dd308c4">WHERE</a>,
<a name="l00119"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bafa9d306e675c3be077c2e0561e6e8e6d">00119</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bafa9d306e675c3be077c2e0561e6e8e6d">ASSERTIONS</a>,
<a name="l00120"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab65def84e41af84db85737a6eb8dc748">00120</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab65def84e41af84db85737a6eb8dc748">ASSUMPTIONS</a>,
<a name="l00121"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba87ad730e285cf17f4eefb214236a2c7a">00121</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba87ad730e285cf17f4eefb214236a2c7a">COUNTEREXAMPLE</a>,
<a name="l00122"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baea3d2c8907d2df3f13c0866a7970baaa">00122</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baea3d2c8907d2df3f13c0866a7970baaa">COUNTERMODEL</a>,
<a name="l00123"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bad263caec619c4d99e4684ba0fabd9493">00123</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bad263caec619c4d99e4684ba0fabd9493">PUSH</a>,
<a name="l00124"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba061dcf4785583d8653942f2d252174fa">00124</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba061dcf4785583d8653942f2d252174fa">POP</a>,
<a name="l00125"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba908bcfbc13c7f414e83641bb9339f31f">00125</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba908bcfbc13c7f414e83641bb9339f31f">POPTO</a>,
<a name="l00126"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5b5b049bfd6cb81f552222a8aad0dd99">00126</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5b5b049bfd6cb81f552222a8aad0dd99">PUSH_SCOPE</a>,
<a name="l00127"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0eb24f3375e74e8a42303dc0c6e7e952">00127</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba0eb24f3375e74e8a42303dc0c6e7e952">POP_SCOPE</a>,
<a name="l00128"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba577463735743ccd8d67d3549bdcbc5eb">00128</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba577463735743ccd8d67d3549bdcbc5eb">POPTO_SCOPE</a>,
<a name="l00129"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba589b7d94a3d91d145720e2fed0eb3a05">00129</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba589b7d94a3d91d145720e2fed0eb3a05">RESET</a>,
<a name="l00130"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7f06283f0d1a4d167be6c37a3d24fd11">00130</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7f06283f0d1a4d167be6c37a3d24fd11">CONTEXT</a>,
<a name="l00131"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5badd6ce7bf1c9b230e53a39d09a7d6e002">00131</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5badd6ce7bf1c9b230e53a39d09a7d6e002">FORGET</a>,
<a name="l00132"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9d77c0f7e14e04b7ecc95a029f669d83">00132</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9d77c0f7e14e04b7ecc95a029f669d83">GET_TYPE</a>,
<a name="l00133"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba915f5acbb5f4374dd2c4e9a37a40d2ef">00133</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba915f5acbb5f4374dd2c4e9a37a40d2ef">CHECK_TYPE</a>,
<a name="l00134"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf87d4fe879a908f02ae07de41fff425e">00134</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf87d4fe879a908f02ae07de41fff425e">GET_CHILD</a>,
<a name="l00135"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf910b817eb56e0a5ce680b74a0e8dc84">00135</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf910b817eb56e0a5ce680b74a0e8dc84">SUBSTITUTE</a>,
<a name="l00136"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9985ac4cb7cda855d785a610e6a866a7">00136</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9985ac4cb7cda855d785a610e6a866a7">SEQ</a>,
<a name="l00137"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba62e1f4af4ae37d9c8a7f60bf47e4e72c">00137</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba62e1f4af4ae37d9c8a7f60bf47e4e72c">ARITH_VAR_ORDER</a>,
<a name="l00138"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba6f0302a99e7b65b652008363069ad743">00138</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba6f0302a99e7b65b652008363069ad743">ANNOTATION</a>,
<a name="l00139"></a>00139
<a name="l00140"></a>00140 <span class="comment">// Kinds used mostly in the parser</span>
<a name="l00141"></a>00141
<a name="l00142"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa74ae94cd8d7d555f0ca4c85ef80ad08">00142</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa74ae94cd8d7d555f0ca4c85ef80ad08">TCC</a>,
<a name="l00143"></a>00143 <span class="comment">// Variable declaration (VARDECL v1 v2 ... v_n type). A variable</span>
<a name="l00144"></a>00144 <span class="comment">// can be an ID or a BOUNDVAR.</span>
<a name="l00145"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5ccfef7d76eb43a61d00eb7129ffc562">00145</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5ccfef7d76eb43a61d00eb7129ffc562">VARDECL</a>,
<a name="l00146"></a>00146 <span class="comment">// A list of variable declarations (VARDECLS (VARDECL ...) (VARDECL ...) ...)</span>
<a name="l00147"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7266e0d07f5aabab9d0515ea50fafc7c">00147</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7266e0d07f5aabab9d0515ea50fafc7c">VARDECLS</a>,
<a name="l00148"></a>00148
<a name="l00149"></a>00149 <span class="comment">// Bound variables have a "printable name", the one the user typed</span>
<a name="l00150"></a>00150 <span class="comment">// in, and a uniqueID used to distinguish it from other bound</span>
<a name="l00151"></a>00151 <span class="comment">// variables, which is effectively the alpha-renaming:</span>
<a name="l00152"></a>00152
<a name="l00153"></a>00153 <span class="comment">// Op(BOUND_VAR (BOUND_ID "user_name" "uniqueID")). Note that</span>
<a name="l00154"></a>00154 <span class="comment">// BOUND_VAR is an operator (Expr without children), just as UFUNC</span>
<a name="l00155"></a>00155 <span class="comment">// and UCONST.</span>
<a name="l00156"></a>00156
<a name="l00157"></a>00157 <span class="comment">// The uniqueID normally is just a number, so one can print a bound</span>
<a name="l00158"></a>00158 <span class="comment">// variable X as X_17.</span>
<a name="l00159"></a>00159
<a name="l00160"></a>00160 <span class="comment">// NOTE that in the parsed expressions like LET x: T = e IN foo(x),</span>
<a name="l00161"></a>00161 <span class="comment">// the second instance of 'x' will be an ID, and *not* a BOUNDVAR.</span>
<a name="l00162"></a>00162 <span class="comment">// The parser does not know how to resolve bound variables, and it</span>
<a name="l00163"></a>00163 <span class="comment">// has to be resolved later.</span>
<a name="l00164"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba462c38186c36e12c2f38a6d0d43feddf">00164</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba462c38186c36e12c2f38a6d0d43feddf">BOUND_VAR</a>,
<a name="l00165"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2a1805dc0fcdef2abbf0c780ab1c47ae">00165</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2a1805dc0fcdef2abbf0c780ab1c47ae">BOUND_ID</a>,
<a name="l00166"></a>00166
<a name="l00167"></a>00167 <span class="comment">// Updator "e1 WITH <bunch of stuff> := e2" is represented as</span>
<a name="l00168"></a>00168 <span class="comment">// (UPDATE e1 (UPDATE_SELECT <bunch of stuff>) e2), where <bunch</span>
<a name="l00169"></a>00169 <span class="comment">// of stuff> is the list of accessors:</span>
<a name="l00170"></a>00170 <span class="comment">// (READ idx)</span>
<a name="l00171"></a>00171 <span class="comment">// ID (what's that for?)</span>
<a name="l00172"></a>00172 <span class="comment">// (REC_SELECT ID)</span>
<a name="l00173"></a>00173 <span class="comment">// and (TUPLE_SELECT num).</span>
<a name="l00174"></a>00174 <span class="comment">// UPDATE,</span>
<a name="l00175"></a>00175 <span class="comment">// UPDATE_SELECT,</span>
<a name="l00176"></a>00176 <span class="comment">// Record type [# f1 : t1, f2 : t2 ... #] is represented as</span>
<a name="l00177"></a>00177 <span class="comment">// (RECORD_TYPE (f1 t1) (f2 t2) ... )</span>
<a name="l00178"></a>00178 <span class="comment">// RECORD_TYPE,</span>
<a name="l00179"></a>00179 <span class="comment">// // (# f1=e1, f2=e2, ...#) == (RECORD (f1 e1) ...)</span>
<a name="l00180"></a>00180 <span class="comment">// RECORD,</span>
<a name="l00181"></a>00181 <span class="comment">// RECORD_SELECT,</span>
<a name="l00182"></a>00182 <span class="comment">// RECORD_UPDATE,</span>
<a name="l00183"></a>00183
<a name="l00184"></a>00184 <span class="comment">// // (e1, e2, ...) == (TUPLE e1 e2 ...)</span>
<a name="l00185"></a>00185 <span class="comment">// TUPLE,</span>
<a name="l00186"></a>00186 <span class="comment">// TUPLE_SELECT,</span>
<a name="l00187"></a>00187 <span class="comment">// TUPLE_UPDATE,</span>
<a name="l00188"></a>00188
<a name="l00189"></a>00189 <span class="comment">// SUBRANGE,</span>
<a name="l00190"></a>00190 <span class="comment">// Enumerated type (SCALARTYPE v1 v2 ...)</span>
<a name="l00191"></a>00191 <span class="comment">// SCALARTYPE,</span>
<a name="l00192"></a>00192 <span class="comment">// Predicate subtype: the argument is the predicate (lambda-expression)</span>
<a name="l00193"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9ae776fb49b0eb32dd93f866492000b5">00193</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9ae776fb49b0eb32dd93f866492000b5">SUBTYPE</a>,
<a name="l00194"></a>00194 <span class="comment">// Datatype is Expr(DATATYPE, Constructors), where Constructors is a</span>
<a name="l00195"></a>00195 <span class="comment">// vector of Expr(CONSTRUCTOR, id [ , arg ]), where 'id' is an ID,</span>
<a name="l00196"></a>00196 <span class="comment">// and 'arg' a VARDECL node (list of variable declarations with</span>
<a name="l00197"></a>00197 <span class="comment">// types). If 'arg' is present, the constructor has arguments</span>
<a name="l00198"></a>00198 <span class="comment">// corresponding to the declared variables.</span>
<a name="l00199"></a>00199 <span class="comment">// DATATYPE,</span>
<a name="l00200"></a>00200 <span class="comment">// THISTYPE, // Used to indicate recursion in recursive datatypes</span>
<a name="l00201"></a>00201 <span class="comment">// CONSTRUCTOR,</span>
<a name="l00202"></a>00202 <span class="comment">// SELECTOR,</span>
<a name="l00203"></a>00203 <span class="comment">// TESTER,</span>
<a name="l00204"></a>00204 <span class="comment">// Expression e WITH accessor := e2 is transformed by the command</span>
<a name="l00205"></a>00205 <span class="comment">// processor into (DATATYPE_UPDATE e accessor e2), where e is the</span>
<a name="l00206"></a>00206 <span class="comment">// original datatype value C(a1, ..., an) (here C is the</span>
<a name="l00207"></a>00207 <span class="comment">// constructor), and "accessor" is the name of one of the arguments</span>
<a name="l00208"></a>00208 <span class="comment">// a_i of C.</span>
<a name="l00209"></a>00209 <span class="comment">// DATATYPE_UPDATE,</span>
<a name="l00210"></a>00210 <span class="comment">// Statement IF c1 THEN e1 ELSIF c2 THEN e2 ... ELSE e_n ENDIF is</span>
<a name="l00211"></a>00211 <span class="comment">// represented as (IF (IFTHEN c1 e1) (IFTHEN c2 e2) ... (ELSE e_n))</span>
<a name="l00212"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba252802eda493fb6b4a279c4452acb547">00212</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba252802eda493fb6b4a279c4452acb547">IF</a>,
<a name="l00213"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5bd60ae173f903f6b202daf0c2118387">00213</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5bd60ae173f903f6b202daf0c2118387">IFTHEN</a>,
<a name="l00214"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba90d649d830ea440c8b8a56c7ef23c426">00214</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba90d649d830ea440c8b8a56c7ef23c426">ELSE</a>,
<a name="l00215"></a>00215 <span class="comment">// Lisp version of multi-branch IF:</span>
<a name="l00216"></a>00216 <span class="comment">// (COND (c1 e1) (c2 e2) ... (ELSE en))</span>
<a name="l00217"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2f577f27f1d0dcd6aa8f0a144138dc42">00217</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2f577f27f1d0dcd6aa8f0a144138dc42">COND</a>,
<a name="l00218"></a>00218
<a name="l00219"></a>00219 <span class="comment">// LET x1: t1 = e1, x2: t2 = e2, ... IN e</span>
<a name="l00220"></a>00220 <span class="comment">// Parser builds:</span>
<a name="l00221"></a>00221 <span class="comment">// (LET (LETDECLS (LETDECL x1 t1 e1) (LETDECL x2 t2 e2) ... ) e)</span>
<a name="l00222"></a>00222 <span class="comment">// where each x_i is a BOUNDVAR.</span>
<a name="l00223"></a>00223 <span class="comment">// After processing, it is rebuilt to have (LETDECL var def); the</span>
<a name="l00224"></a>00224 <span class="comment">// type is set as the attribute to var.</span>
<a name="l00225"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bafb72619a5a922e816967c4aa49301754">00225</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bafb72619a5a922e816967c4aa49301754">LET</a>,
<a name="l00226"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2cd77861cfba212beedbf4245c990f72">00226</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2cd77861cfba212beedbf4245c990f72">LETDECLS</a>,
<a name="l00227"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9508dd8c8e7db280a5dacc19bd74d92d">00227</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba9508dd8c8e7db280a5dacc19bd74d92d">LETDECL</a>,
<a name="l00228"></a>00228 <span class="comment">// Lambda-abstraction LAMBDA (<vars>) : e === (LAMBDA <vars> e)</span>
<a name="l00229"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba40176493726a127184ca47ea6352dc1f">00229</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba40176493726a127184ca47ea6352dc1f">LAMBDA</a>,
<a name="l00230"></a>00230 <span class="comment">// Symbolic simulation operator</span>
<a name="l00231"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa1022ff97dac8e2d5d80d53c4cecd132">00231</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baa1022ff97dac8e2d5d80d53c4cecd132">SIMULATE</a>,
<a name="l00232"></a>00232
<a name="l00233"></a>00233 <span class="comment">// Uninterpreted constants (variables) x1, x2, ... , x_n : type</span>
<a name="l00234"></a>00234 <span class="comment">// (CONST (VARLIST x1 x2 ... x_n) type)</span>
<a name="l00235"></a>00235 <span class="comment">// Uninterpreted functions are declared as constants of functional type.</span>
<a name="l00236"></a>00236
<a name="l00237"></a>00237 <span class="comment">// After processing, uninterpreted functions and constants</span>
<a name="l00238"></a>00238 <span class="comment">// (a.k.a. variables) are represented as Op(UFUNC, (ID "name")) and</span>
<a name="l00239"></a>00239 <span class="comment">// Op(UCONST, (ID "name")) with the appropriate type attribute.</span>
<a name="l00240"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3d044162d972156d897cea80f216b9ca">00240</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3d044162d972156d897cea80f216b9ca">CONST</a>,
<a name="l00241"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba197dcccceb8ad4d4bd3b914f73f2978a">00241</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba197dcccceb8ad4d4bd3b914f73f2978a">VARLIST</a>,
<a name="l00242"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2efaeb22f8803588598706b73cec8bda">00242</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2efaeb22f8803588598706b73cec8bda">UCONST</a>,
<a name="l00243"></a>00243
<a name="l00244"></a>00244 <span class="comment">// User function definition f(args) : type = e === (DEFUN args type e)</span>
<a name="l00245"></a>00245 <span class="comment">// Here 'args' are bound var declarations</span>
<a name="l00246"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5a9e497d7471e5d91bd097e5b80a830d">00246</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5a9e497d7471e5d91bd097e5b80a830d">DEFUN</a>,
<a name="l00247"></a>00247
<a name="l00248"></a>00248 <span class="comment">// Arithmetic types and operators</span>
<a name="l00249"></a>00249 <span class="comment">// REAL,</span>
<a name="l00250"></a>00250 <span class="comment">// INT,</span>
<a name="l00251"></a>00251
<a name="l00252"></a>00252 <span class="comment">// UMINUS,</span>
<a name="l00253"></a>00253 <span class="comment">// PLUS,</span>
<a name="l00254"></a>00254 <span class="comment">// MINUS,</span>
<a name="l00255"></a>00255 <span class="comment">// MULT,</span>
<a name="l00256"></a>00256 <span class="comment">// DIVIDE,</span>
<a name="l00257"></a>00257 <span class="comment">// INTDIV,</span>
<a name="l00258"></a>00258 <span class="comment">// MOD,</span>
<a name="l00259"></a>00259 <span class="comment">// LT,</span>
<a name="l00260"></a>00260 <span class="comment">// LE,</span>
<a name="l00261"></a>00261 <span class="comment">// GT,</span>
<a name="l00262"></a>00262 <span class="comment">// GE,</span>
<a name="l00263"></a>00263 <span class="comment">// IS_INTEGER,</span>
<a name="l00264"></a>00264 <span class="comment">// NEGINF,</span>
<a name="l00265"></a>00265 <span class="comment">// POSINF,</span>
<a name="l00266"></a>00266 <span class="comment">// DARK_SHADOW,</span>
<a name="l00267"></a>00267 <span class="comment">// GRAY_SHADOW,</span>
<a name="l00268"></a>00268
<a name="l00269"></a>00269 <span class="comment">// //Floor theory operators</span>
<a name="l00270"></a>00270 <span class="comment">// FLOOR,</span>
<a name="l00271"></a>00271 <span class="comment">// Kind for Extension to Non-linear Arithmetic</span>
<a name="l00272"></a>00272 <span class="comment">// POW,</span>
<a name="l00273"></a>00273
<a name="l00274"></a>00274 <span class="comment">// Kinds for proof terms</span>
<a name="l00275"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baee1a6e6a0705cce09e48dbe8d3f26572">00275</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baee1a6e6a0705cce09e48dbe8d3f26572">PF_APPLY</a>,
<a name="l00276"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2656992cdd2e5b8fd78f595329c1f58f">00276</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba2656992cdd2e5b8fd78f595329c1f58f">PF_HOLE</a>,
<a name="l00277"></a>00277
<a name="l00278"></a>00278
<a name="l00279"></a>00279 <span class="comment">// // Mlss</span>
<a name="l00280"></a>00280 <span class="comment">// EMPTY, // {}</span>
<a name="l00281"></a>00281 <span class="comment">// UNION, // +</span>
<a name="l00282"></a>00282 <span class="comment">// INTER, // *</span>
<a name="l00283"></a>00283 <span class="comment">// DIFF,</span>
<a name="l00284"></a>00284 <span class="comment">// SINGLETON,</span>
<a name="l00285"></a>00285 <span class="comment">// IN,</span>
<a name="l00286"></a>00286 <span class="comment">// INCS,</span>
<a name="l00287"></a>00287 <span class="comment">// INCIN,</span>
<a name="l00288"></a>00288
<a name="l00289"></a>00289 <span class="comment">//Skolem variable</span>
<a name="l00290"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba73072b2c6fef896d006d6691e932cf37">00290</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba73072b2c6fef896d006d6691e932cf37">SKOLEM_VAR</a>,
<a name="l00291"></a>00291 <span class="comment">// Expr that holds a theorem</span>
<a name="l00292"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bada5edea8bbb7cfbd2500be6eca0d4151">00292</a> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bada5edea8bbb7cfbd2500be6eca0d4151">THEOREM_KIND</a>,<span class="comment"></span>
<a name="l00293"></a>00293 <span class="comment"> //! Must always be the last kind</span>
<a name="l00294"></a><a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bac8e823433db1723711ac5685ba2e7f60">00294</a> <span class="comment"></span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bac8e823433db1723711ac5685ba2e7f60" title="Must always be the last kind.">LAST_KIND</a>
<a name="l00295"></a>00295 } <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5b">Kind</a>;
<a name="l00296"></a>00296
<a name="l00297"></a>00297 <span class="preprocessor">#ifdef __cplusplus</span>
<a name="l00298"></a>00298 <span class="preprocessor"></span>} <span class="comment">// end of namespace CVC3</span>
<a name="l00299"></a>00299 <span class="preprocessor">#endif </span><span class="comment">/* __cplusplus */</span>
<a name="l00300"></a>00300
<a name="l00301"></a>00301 <span class="preprocessor">#endif</span>
</pre></div></div>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
