<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: theory_datatype.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">theory_datatype.h</div> </div>
</div>
<div class="contents">
<a href="theory__datatype_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 theory_datatype.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: Wed Dec 1 22:24:32 2004</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__theory_datatype_h_</span>
<a name="l00022"></a>00022 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__theory_datatype_h_</span>
<a name="l00023"></a>00023 <span class="preprocessor"></span>
<a name="l00024"></a>00024 <span class="preprocessor">#include "<a class="code" href="theory_8h.html" title="Generic API for Theories plus methods commonly used by theories.">theory.h</a>"</span>
<a name="l00025"></a>00025 <span class="preprocessor">#include "<a class="code" href="smartcdo_8h.html" title="Smart context-dependent object wrapper.">smartcdo.h</a>"</span>
<a name="l00026"></a>00026 <span class="preprocessor">#include "<a class="code" href="cdmap_8h.html">cdmap.h</a>"</span>
<a name="l00027"></a>00027
<a name="l00028"></a>00028 <span class="keyword">namespace </span>CVC3 {
<a name="l00029"></a>00029
<a name="l00030"></a>00030 <span class="keyword">class </span>DatatypeProofRules;
<a name="l00031"></a>00031 <span class="comment"></span>
<a name="l00032"></a>00032 <span class="comment">//! Local kinds for datatypes</span>
<a name="l00033"></a><a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089">00033</a> <span class="comment"></span> <span class="keyword">typedef</span> <span class="keyword">enum</span> {
<a name="l00034"></a><a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089a5cc02a3e0fe70ce33e5c3d450b38136c">00034</a> <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089a5cc02a3e0fe70ce33e5c3d450b38136c">DATATYPE_DECL</a> = 600,
<a name="l00035"></a><a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ad94b8e65b0abc98bb6b5729da9e3b40a">00035</a> <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ad94b8e65b0abc98bb6b5729da9e3b40a">DATATYPE</a>,
<a name="l00036"></a><a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ae3aa1eb89fb69c62d502b57c020ed789">00036</a> <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ae3aa1eb89fb69c62d502b57c020ed789">CONSTRUCTOR</a>,
<a name="l00037"></a><a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ac909f916e89d861b4a4e5eba782c5259">00037</a> <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ac909f916e89d861b4a4e5eba782c5259">SELECTOR</a>,
<a name="l00038"></a><a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089a4df0e72bf250adc8dd78e81fea2f281c">00038</a> <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089a4df0e72bf250adc8dd78e81fea2f281c">TESTER</a>
<a name="l00039"></a>00039 } <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089" title="Local kinds for datatypes.">DatatypeKinds</a>;
<a name="l00040"></a>00040
<a name="l00041"></a>00041 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00042"></a>00042 <span class="comment">/*!</span>
<a name="l00043"></a>00043 <span class="comment"> *\class TheoryDatatype</span>
<a name="l00044"></a>00044 <span class="comment"> *\ingroup Theories</span>
<a name="l00045"></a>00045 <span class="comment"> *\brief This theory handles datatypes.</span>
<a name="l00046"></a>00046 <span class="comment"> *</span>
<a name="l00047"></a>00047 <span class="comment"> * Author: Clark Barrett</span>
<a name="l00048"></a>00048 <span class="comment"> *</span>
<a name="l00049"></a>00049 <span class="comment"> * Created: Wed Dec 1 22:27:12 2004</span>
<a name="l00050"></a>00050 <span class="comment"> */</span>
<a name="l00051"></a>00051 <span class="comment">/*****************************************************************************/</span>
<a name="l00052"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html">00052</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1TheoryDatatype.html" title="This theory handles datatypes.">TheoryDatatype</a> :<span class="keyword">public</span> <a class="code" href="classCVC3_1_1Theory.html" title="Base class for theories.">Theory</a> {
<a name="l00053"></a>00053 <span class="keyword">protected</span>:
<a name="l00054"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#abcd88b0572b5751bddccd9210939f5d0">00054</a> <a class="code" href="classCVC3_1_1DatatypeProofRules.html">DatatypeProofRules</a>* <a class="code" href="classCVC3_1_1TheoryDatatype.html#abcd88b0572b5751bddccd9210939f5d0">d_rules</a>;
<a name="l00055"></a>00055
<a name="l00056"></a>00056 <span class="comment">// maps DATATYPE expressions to map containing constructors for that datatype</span>
<a name="l00057"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">00057</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<ExprMap<unsigned></a> > <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>;
<a name="l00058"></a>00058 <span class="comment">// maps constructor to its selectors</span>
<a name="l00059"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a1e8e2818f2f0dcf45743b42b3d9778b3">00059</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<std::vector<Expr></a> > <a class="code" href="classCVC3_1_1TheoryDatatype.html#a1e8e2818f2f0dcf45743b42b3d9778b3">d_constructorMap</a>;
<a name="l00060"></a>00060 <span class="comment">// maps selector to a pair containing the constructor and the position of the selctor for that constructor</span>
<a name="l00061"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a63dc7258a77b6e3cb172c1a38994a06b">00061</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<std::pair<Expr,unsigned></a> > <a class="code" href="classCVC3_1_1TheoryDatatype.html#a63dc7258a77b6e3cb172c1a38994a06b">d_selectorMap</a>;
<a name="l00062"></a>00062 <span class="comment">// maps tester to constructor that it matches</span>
<a name="l00063"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a6c428d8d15b377753c2154f4109604c8">00063</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6c428d8d15b377753c2154f4109604c8">d_testerMap</a>;
<a name="l00064"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a7aab890b7ccd92b61dafb89bcf9adc65">00064</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Op></a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a7aab890b7ccd92b61dafb89bcf9adc65">d_reach</a>;
<a name="l00065"></a>00065
<a name="l00066"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">00066</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, SmartCDO<Unsigned></a> > <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>;
<a name="l00067"></a>00067
<a name="l00068"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a64a98802daa8a6a7c4f683b60740961f">00068</a> <a class="code" href="classCVC3_1_1CDList.html">CDList<Theorem></a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a64a98802daa8a6a7c4f683b60740961f">d_facts</a>;
<a name="l00069"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a3b16dee83eb2df2c860c14752913a12e">00069</a> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a3b16dee83eb2df2c860c14752913a12e">d_splitters</a>;
<a name="l00070"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a1952cec9cef126b4c3d9611738f7169e">00070</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned></a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a1952cec9cef126b4c3d9611738f7169e">d_splittersIndex</a>;
<a name="l00071"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a73d20b00d4a702698ea0a9baea9c5bc2">00071</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<bool></a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a73d20b00d4a702698ea0a9baea9c5bc2">d_splitterAsserted</a>;
<a name="l00072"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a44dee8f4a9da185dcbac872295d342a4">00072</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>& <a class="code" href="classCVC3_1_1TheoryDatatype.html#a44dee8f4a9da185dcbac872295d342a4">d_smartSplits</a>;
<a name="l00073"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#ae5ebfda4bb10cae8a4a3c620731bfb51">00073</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#ae5ebfda4bb10cae8a4a3c620731bfb51">d_getConstantStack</a>;
<a name="l00074"></a>00074
<a name="l00075"></a>00075 <span class="keyword">protected</span>:
<a name="l00076"></a>00076 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a61b966ebd57ae1b2819f8d6ac73555f6">instantiate</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a>& u);
<a name="l00077"></a>00077 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a3915e378cdf3889e9776b7f0e8c7ee15">initializeLabels</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& t);
<a name="l00078"></a>00078 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a942fa3974b5c4bc2f44e202a6adc80c8">mergeLabels</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e2);
<a name="l00079"></a>00079 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a942fa3974b5c4bc2f44e202a6adc80c8">mergeLabels</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e,
<a name="l00080"></a>00080 <span class="keywordtype">unsigned</span> position, <span class="keywordtype">bool</span> positive);
<a name="l00081"></a>00081
<a name="l00082"></a>00082 <span class="keyword">public</span>:
<a name="l00083"></a>00083 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a9a9fd251c5310efadde13129eff997e1">TheoryDatatype</a>(<a class="code" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">TheoryCore</a>* <a class="code" href="classCVC3_1_1Theory.html#a90684d2a97738341c00f8f9c99af7b66" title="Get a pointer to theoryCore.">theoryCore</a>);
<a name="l00084"></a>00084 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a409850e0e05071bb71ac2494665729e3">~TheoryDatatype</a>();
<a name="l00085"></a>00085
<a name="l00086"></a>00086 <span class="comment">// Trusted method that creates the proof rules class (used in constructor).</span>
<a name="l00087"></a>00087 <span class="comment">// Implemented in datatype_theorem_producer.cpp</span>
<a name="l00088"></a>00088 <a class="code" href="classCVC3_1_1DatatypeProofRules.html">DatatypeProofRules</a>* <a class="code" href="classCVC3_1_1TheoryDatatype.html#a2c187b27067bc4d794cac14046216598">createProofRules</a>();
<a name="l00089"></a>00089
<a name="l00090"></a>00090 <span class="comment">// Theory interface</span>
<a name="l00091"></a>00091 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a998e0cd18f7d41f9e7df014d7f86edbc" title="Notify theory of a new shared term.">addSharedTerm</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00092"></a>00092 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a640ba909d9c6470c40600a82cdb65417" title="Assert a new fact to the decision procedure.">assertFact</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e);
<a name="l00093"></a>00093 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a50136aaaf32b6b42751290cb2ccfedf6" title="Check for satisfiability in the theory.">checkSat</a>(<span class="keywordtype">bool</span> fullEffort);
<a name="l00094"></a>00094 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a5fea4f3ab06825c2df409082095f7d96" title="Theory-specific rewrite rules.">rewrite</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00095"></a>00095 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a8825c26c5b357ec4a6fde28aaceeea44" title="Set up the term e for call-backs when e or its children change.">setup</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00096"></a>00096 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a4d1da766acf310b425f564027c70b8b9" title="Notify a theory of a new equality.">update</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& d);
<a name="l00097"></a>00097 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#ab5f431756db284b50c011774862f9f16" title="An optional solver.">solve</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e);
<a name="l00098"></a>00098 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#acf535107486ee65ec245d080c48c277f" title="Check that e is a valid Type expr.">checkType</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00099"></a>00099 <a class="code" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54" title="Enum for cardinality of types.">Cardinality</a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#ad370efc075c3da6b8b081020cd56a55e" title="Compute information related to finiteness of types.">finiteTypeInfo</a>(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a>& n,
<a name="l00100"></a>00100 <span class="keywordtype">bool</span> enumerate, <span class="keywordtype">bool</span> computeSize);
<a name="l00101"></a>00101 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#af1237546f5860ded939958b0c31c6669" title="Compute and store the type of e.">computeType</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00102"></a>00102 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a8fa2a50fe50ccfda4b557783f566dbfc" title="Add variables from 'e' to 'v' for constructing a concrete model.">computeModelTerm</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, std::vector<Expr>& v);
<a name="l00103"></a>00103 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#ae50ed74ea28aae7d5919a3461302a83e" title="Compute and cache the TCC of e.">computeTCC</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00104"></a>00104 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a464a093b6247645cf10c1bb8aa9a03a4" title="Theory-specific parsing implemented by the DP.">parseExprOp</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00105"></a>00105 <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="classCVC3_1_1TheoryDatatype.html#a1d17495677079120272ec4073cd777db" title="Theory-specific pretty-printing.">print</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00106"></a>00106
<a name="l00107"></a>00107 <span class="comment">// Returns Expr(DATATYPE_DECL datatype)</span>
<a name="l00108"></a>00108 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#ab31831ed547432e2a83f74c83a82e982">dataType</a>(<span class="keyword">const</span> std::string& name,
<a name="l00109"></a>00109 <span class="keyword">const</span> std::vector<std::string>& constructors,
<a name="l00110"></a>00110 <span class="keyword">const</span> std::vector<std::vector<std::string> >& selectors,
<a name="l00111"></a>00111 <span class="keyword">const</span> std::vector<std::vector<Expr> >& types);
<a name="l00112"></a>00112
<a name="l00113"></a>00113 <span class="comment">// Returns Expr(DATATYPE_DECL type_1, type_2, ...)</span>
<a name="l00114"></a>00114 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#ab31831ed547432e2a83f74c83a82e982">dataType</a>(<span class="keyword">const</span> std::vector<std::string>& names,
<a name="l00115"></a>00115 <span class="keyword">const</span> std::vector<std::vector<std::string> >& constructors,
<a name="l00116"></a>00116 <span class="keyword">const</span> std::vector<std::vector<std::vector<std::string> > >& selectors,
<a name="l00117"></a>00117 <span class="keyword">const</span> std::vector<std::vector<std::vector<Expr> > >& types);
<a name="l00118"></a>00118
<a name="l00119"></a>00119 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a12a7bb383d9780f84484de597892809b">datatypeConsExpr</a>(<span class="keyword">const</span> std::string& constructor,
<a name="l00120"></a>00120 <span class="keyword">const</span> std::vector<Expr>& args);
<a name="l00121"></a>00121 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#ac38281a765aa4e57af9a2c6ff4c3686c">datatypeSelExpr</a>(<span class="keyword">const</span> std::string& selector, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& arg);
<a name="l00122"></a>00122 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a51372d26e89b189c8a5f42d18dd2eedc">datatypeTestExpr</a>(<span class="keyword">const</span> std::string& constructor, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& arg);
<a name="l00123"></a>00123
<a name="l00124"></a>00124 <span class="keyword">const</span> std::pair<Expr,unsigned>& <a class="code" href="classCVC3_1_1TheoryDatatype.html#a5ae1a2fe60c6e2af77cf098340cabd53">getSelectorInfo</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00125"></a>00125 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#af39a46bc360e9f7c91bf0d85cc3908ca">getConsForTester</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00126"></a>00126 <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d93ab7a39a1eb3e82cb67f0425ffee">getConsPos</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00127"></a>00127 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a60d3e5400ca66acaf39a1365bd378c7e">getConstant</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& t);
<a name="l00128"></a>00128 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Op.html">Op</a>& <a class="code" href="classCVC3_1_1TheoryDatatype.html#a53246e5e620d363d47497792573ea970">getReachablePredicate</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& t);
<a name="l00129"></a>00129 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a513d221b48500cf4bc91393293d9b2f2">canCollapse</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00130"></a>00130
<a name="l00131"></a>00131 };
<a name="l00132"></a>00132
<a name="l00133"></a><a class="code" href="namespaceCVC3.html#a88890c6bdae30ff688fd2ea5bd799676">00133</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a88890c6bdae30ff688fd2ea5bd799676">isDatatype</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& t)
<a name="l00134"></a>00134 { <span class="keywordflow">return</span> t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>().<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ad94b8e65b0abc98bb6b5729da9e3b40a">DATATYPE</a>; }
<a name="l00135"></a>00135
<a name="l00136"></a><a class="code" href="namespaceCVC3.html#a91840d293c43120244ce5b5165bdacc4">00136</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a91840d293c43120244ce5b5165bdacc4">isConstructor</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e)
<a name="l00137"></a>00137 { <span class="keywordflow">return</span> (e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ae3aa1eb89fb69c62d502b57c020ed789">CONSTRUCTOR</a> && e.<a class="code" href="group__ExprPkg.html#ga42929221eb172250697b72c28af6de07" title="Get the type. Recursively compute if necessary.">getType</a>().<a class="code" href="classCVC3_1_1Type.html#abd7ab3fcb112e27aa05da8981b56e02c">arity</a>()==1) ||
<a name="l00138"></a>00138 (e.<a class="code" href="group__ExprPkg.html#ga1d6a6b4a9ce81b0dd8fd74870ff4284b">isApply</a>() && e.<a class="code" href="group__ExprPkg.html#gad036a3a3597d590ca6ee694505c6e1cd" title="Get kind of operator (for APPLY Exprs only)">getOpKind</a>() == <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ae3aa1eb89fb69c62d502b57c020ed789">CONSTRUCTOR</a>); }
<a name="l00139"></a>00139
<a name="l00140"></a><a class="code" href="namespaceCVC3.html#afdcf0b93fc0d1b03a5a14c4988443c7a">00140</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#afdcf0b93fc0d1b03a5a14c4988443c7a">isSelector</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e)
<a name="l00141"></a>00141 { <span class="keywordflow">return</span> e.<a class="code" href="group__ExprPkg.html#ga1d6a6b4a9ce81b0dd8fd74870ff4284b">isApply</a>() && e.<a class="code" href="group__ExprPkg.html#gad036a3a3597d590ca6ee694505c6e1cd" title="Get kind of operator (for APPLY Exprs only)">getOpKind</a>() == <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ac909f916e89d861b4a4e5eba782c5259">SELECTOR</a>; }
<a name="l00142"></a>00142
<a name="l00143"></a><a class="code" href="namespaceCVC3.html#a8297278831bf83882f7c6a1e3c84fa98">00143</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#a8297278831bf83882f7c6a1e3c84fa98">isTester</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e)
<a name="l00144"></a>00144 { <span class="keywordflow">return</span> e.<a class="code" href="group__ExprPkg.html#ga1d6a6b4a9ce81b0dd8fd74870ff4284b">isApply</a>() && e.<a class="code" href="group__ExprPkg.html#gad036a3a3597d590ca6ee694505c6e1cd" title="Get kind of operator (for APPLY Exprs only)">getOpKind</a>() == <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089a4df0e72bf250adc8dd78e81fea2f281c">TESTER</a>; }
<a name="l00145"></a>00145
<a name="l00146"></a><a class="code" href="namespaceCVC3.html#ac1eec763ed1ae5d0f52c4bed47d6fee5">00146</a> <span class="keyword">inline</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="namespaceCVC3.html#ac1eec763ed1ae5d0f52c4bed47d6fee5">getConstructor</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e)
<a name="l00147"></a>00147 { <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="namespaceCVC3.html#a91840d293c43120244ce5b5165bdacc4">isConstructor</a>(e), <span class="stringliteral">"Constructor expected"</span>);
<a name="l00148"></a>00148 <span class="keywordflow">return</span> e.<a class="code" href="group__ExprPkg.html#ga1d6a6b4a9ce81b0dd8fd74870ff4284b">isApply</a>() ? e.<a class="code" href="group__ExprPkg.html#ga9f3328fe077191803a780cfd6566ff9b" title="Get expression of operator (for APPLY Exprs only)">getOpExpr</a>() : e; }
<a name="l00149"></a>00149
<a name="l00150"></a>00150 }
<a name="l00151"></a>00151
<a name="l00152"></a>00152 <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>
