<!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.cpp Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div class="header">
<div class="headertitle">
<div class="title">theory_datatype.cpp</div> </div>
</div>
<div class="contents">
<a href="theory__datatype_8cpp.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00002"></a>00002 <span class="comment">/*!</span>
<a name="l00003"></a>00003 <span class="comment"> *\file theory_datatype.cpp</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:32:26 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
<a name="l00022"></a>00022 <span class="preprocessor">#include "<a class="code" href="theory__datatype_8h.html">theory_datatype.h</a>"</span>
<a name="l00023"></a>00023 <span class="preprocessor">#include "<a class="code" href="datatype__proof__rules_8h.html" title="Abstract interface for recursive datatype proof rules.">datatype_proof_rules.h</a>"</span>
<a name="l00024"></a>00024 <span class="preprocessor">#include "<a class="code" href="typecheck__exception_8h.html" title="An exception to be thrown at typecheck error.">typecheck_exception.h</a>"</span>
<a name="l00025"></a>00025 <span class="preprocessor">#include "<a class="code" href="parser__exception_8h.html" title="An exception thrown by the parser.">parser_exception.h</a>"</span>
<a name="l00026"></a>00026 <span class="preprocessor">#include "<a class="code" href="smtlib__exception_8h.html" title="An exception to be thrown by the smtlib translator.">smtlib_exception.h</a>"</span>
<a name="l00027"></a>00027 <span class="preprocessor">#include "<a class="code" href="theory__core_8h.html">theory_core.h</a>"</span>
<a name="l00028"></a>00028 <span class="preprocessor">#include "<a class="code" href="theory__uf_8h.html">theory_uf.h</a>"</span>
<a name="l00029"></a>00029 <span class="preprocessor">#include "<a class="code" href="command__line__flags_8h.html">command_line_flags.h</a>"</span>
<a name="l00030"></a>00030
<a name="l00031"></a>00031
<a name="l00032"></a>00032 <span class="keyword">using namespace </span>std;
<a name="l00033"></a>00033 <span class="keyword">using namespace </span>CVC3;
<a name="l00034"></a>00034
<a name="l00035"></a>00035 <span class="comment"></span>
<a name="l00036"></a>00036 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00037"></a>00037 <span class="comment"></span><span class="comment">// TheoryDatatype Public Methods //</span><span class="comment"></span>
<a name="l00038"></a>00038 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00039"></a>00039 <span class="comment"></span>
<a name="l00040"></a>00040
<a name="l00041"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a9a9fd251c5310efadde13129eff997e1">00041</a> TheoryDatatype::TheoryDatatype(<a class="code" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">TheoryCore</a>* core)
<a name="l00042"></a>00042 : <a class="code" href="classCVC3_1_1Theory.html" title="Base class for theories.">Theory</a>(core, <span class="stringliteral">"Datatypes"</span>),
<a name="l00043"></a>00043 d_labels(core->getCM()->getCurrentContext()),
<a name="l00044"></a>00044 d_facts(core->getCM()->getCurrentContext()),
<a name="l00045"></a>00045 d_splitters(core->getCM()->getCurrentContext()),
<a name="l00046"></a>00046 d_splittersIndex(core->getCM()->getCurrentContext(), 0),
<a name="l00047"></a>00047 d_splitterAsserted(core->getCM()->getCurrentContext(), false),
<a name="l00048"></a>00048 d_smartSplits(core->getFlags()[<span class="stringliteral">"dt-smartsplits"</span>].getBool())
<a name="l00049"></a>00049 {
<a name="l00050"></a>00050 <a class="code" href="classCVC3_1_1TheoryDatatype.html#abcd88b0572b5751bddccd9210939f5d0">d_rules</a> = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a2c187b27067bc4d794cac14046216598">createProofRules</a>();
<a name="l00051"></a>00051
<a name="l00052"></a>00052 <span class="comment">// Register new local kinds with ExprManager</span>
<a name="l00053"></a>00053 <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089a5cc02a3e0fe70ce33e5c3d450b38136c">DATATYPE_DECL</a>, <span class="stringliteral">"_DATATYPE_DECL"</span>);
<a name="l00054"></a>00054 <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ad94b8e65b0abc98bb6b5729da9e3b40a">DATATYPE</a>, <span class="stringliteral">"_DATATYPE"</span>, <span class="keyword">true</span>);
<a name="l00055"></a>00055 <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ae3aa1eb89fb69c62d502b57c020ed789">CONSTRUCTOR</a>, <span class="stringliteral">"_CONSTRUCTOR"</span>);
<a name="l00056"></a>00056 <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ac909f916e89d861b4a4e5eba782c5259">SELECTOR</a>, <span class="stringliteral">"_SELECTOR"</span>);
<a name="l00057"></a>00057 <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga2b0c6f8e83135e82ebe084188e390da1" title="Register a new kind.">newKind</a>(<a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089a4df0e72bf250adc8dd78e81fea2f281c">TESTER</a>, <span class="stringliteral">"_TESTER"</span>);
<a name="l00058"></a>00058
<a name="l00059"></a>00059 vector<int> kinds;
<a name="l00060"></a>00060 kinds.push_back(<a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089a5cc02a3e0fe70ce33e5c3d450b38136c">DATATYPE_DECL</a>);
<a name="l00061"></a>00061 kinds.push_back(<a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ad94b8e65b0abc98bb6b5729da9e3b40a">DATATYPE</a>);
<a name="l00062"></a>00062 kinds.push_back(<a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089a4df0e72bf250adc8dd78e81fea2f281c">TESTER</a>);
<a name="l00063"></a>00063 kinds.push_back(<a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ae3aa1eb89fb69c62d502b57c020ed789">CONSTRUCTOR</a>);
<a name="l00064"></a>00064 kinds.push_back(<a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ac909f916e89d861b4a4e5eba782c5259">SELECTOR</a>);
<a name="l00065"></a>00065
<a name="l00066"></a>00066 <a class="code" href="classCVC3_1_1Theory.html#a97a6f8e09f71513da969fa7847346c6f" title="Register a new theory.">registerTheory</a>(<span class="keyword">this</span>, kinds);
<a name="l00067"></a>00067 }
<a name="l00068"></a>00068
<a name="l00069"></a>00069
<a name="l00070"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a409850e0e05071bb71ac2494665729e3">00070</a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a409850e0e05071bb71ac2494665729e3">TheoryDatatype::~TheoryDatatype</a>() {
<a name="l00071"></a>00071 <span class="keyword">delete</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#abcd88b0572b5751bddccd9210939f5d0">d_rules</a>;
<a name="l00072"></a>00072 }
<a name="l00073"></a>00073
<a name="l00074"></a>00074
<a name="l00075"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a61b966ebd57ae1b2819f8d6ac73555f6">00075</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a61b966ebd57ae1b2819f8d6ac73555f6">TheoryDatatype::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="l00076"></a>00076 {
<a name="l00077"></a>00077 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!e.<a class="code" href="group__ExprPkg.html#ga4dc94c33ae308ff8d9d004f49df8f42b">hasFind</a>() || <a class="code" href="classCVC3_1_1Theory.html#a08412b310cb743536f7edd9fccd60e46" title="Return the find of e, or e if it has no find.">findExpr</a>(e) == e,
<a name="l00078"></a>00078 <span class="stringliteral">"datatype: instantiate: Expected find(e)=e"</span>);
<a name="l00079"></a>00079 <span class="keywordflow">if</span> (<a class="code" href="namespaceCVC3.html#a91840d293c43120244ce5b5165bdacc4">isConstructor</a>(e)) <span class="keywordflow">return</span>;
<a name="l00080"></a>00080 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(u != 0 && (u & (u-1)) == 0,
<a name="l00081"></a>00081 <span class="stringliteral">"datatype: instantiate: Expected single label in u"</span>);
<a name="l00082"></a>00082 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>.<a class="code" href="classCVC3_1_1ExprMap.html#ae50ab1874dd63b575553e7db769abe28">find</a>(<a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(e).getExpr()) != <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>.<a class="code" href="classCVC3_1_1ExprMap.html#a283ae6c44308cbdda0d82da5a16e52c8">end</a>(),
<a name="l00083"></a>00083 <span class="stringliteral">"datatype: instantiate: Unexpected type: "</span>+<a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(e).<a class="code" href="classCVC3_1_1Type.html#a2f5ce4b1973ec02b2f2b2eba8ce3cc50">toString</a>()
<a name="l00084"></a>00084 +<span class="stringliteral">"\n\n for expression: "</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00085"></a>00085 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<unsigned></a>& c = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>[<a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(e).<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>()];
<a name="l00086"></a>00086 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<unsigned>::iterator</a> c_it = c.<a class="code" href="classCVC3_1_1ExprMap.html#a3db85401f8535daf4054fde531cd46b1">begin</a>(), c_end = c.end();
<a name="l00087"></a>00087 <span class="keywordflow">for</span> (; c_it != c_end; ++c_it) {
<a name="l00088"></a>00088 <span class="keywordflow">if</span> ((u & (<a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a>(1) << (<span class="keywordtype">unsigned</span>)(*c_it).second)) != 0) <span class="keywordflow">break</span>;
<a name="l00089"></a>00089 }
<a name="l00090"></a>00090 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(c_it != c_end,
<a name="l00091"></a>00091 <span class="stringliteral">"datatype: instantiate: couldn't find constructor"</span>);
<a name="l00092"></a>00092 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& cons = (*c_it).first;
<a name="l00093"></a>00093
<a name="l00094"></a>00094 <span class="keywordflow">if</span> (!cons.<a class="code" href="group__ExprPkg.html#gacf628bd70fc2c4766afa268ed22ea947">isFinite</a>() && !e.<a class="code" href="group__ExprPkg.html#ga3292a2d664355dd3246479f21e6f26cb">isSelected</a>()) <span class="keywordflow">return</span>;
<a name="l00095"></a>00095
<a name="l00096"></a>00096 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> consType = <a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(cons);
<a name="l00097"></a>00097 <span class="keywordflow">if</span> (consType.<a class="code" href="classCVC3_1_1Type.html#abd7ab3fcb112e27aa05da8981b56e02c">arity</a>() == 1) {
<a name="l00098"></a>00098 <a class="code" href="classCVC3_1_1Theory.html#a93856c9af82b2c25c51b3c36bafb71f4" title="Submit a derived fact to the core from a decision procedure.">enqueueFact</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#abcd88b0572b5751bddccd9210939f5d0">d_rules</a>-><a class="code" href="classCVC3_1_1DatatypeProofRules.html#a1f1fede903939b996f001baf43ec1f17">dummyTheorem</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a64a98802daa8a6a7c4f683b60740961f">d_facts</a>, e.<a class="code" href="group__ExprPkg.html#gacb48495ca445c895f95d0c3c1ae2070b">eqExpr</a>(cons)));
<a name="l00099"></a>00099 <span class="keywordflow">return</span>;
<a name="l00100"></a>00100 }
<a name="l00101"></a>00101 <span class="comment">// create vars</span>
<a name="l00102"></a>00102 vector<Expr> vars;
<a name="l00103"></a>00103 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i = 0; i < consType.<a class="code" href="classCVC3_1_1Type.html#abd7ab3fcb112e27aa05da8981b56e02c">arity</a>()-1; ++i) {
<a name="l00104"></a>00104 vars.push_back(<a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()->newBoundVarExpr(consType[i]));
<a name="l00105"></a>00105 }
<a name="l00106"></a>00106 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e2 = <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga0d2ff7603a249b30b2df4e549607ad6e">newClosureExpr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3197625a1bb2264943f5a95f236d9973">EXISTS</a>, vars,
<a name="l00107"></a>00107 e.<a class="code" href="group__ExprPkg.html#gacb48495ca445c895f95d0c3c1ae2070b">eqExpr</a>(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(cons.<a class="code" href="group__ExprPkg.html#ga3aefe2fb15c2d8e3a51dd92dbcc5cdc5" title="Make the expr into an operator.">mkOp</a>(), vars)));
<a name="l00108"></a>00108 <a class="code" href="classCVC3_1_1Theory.html#a93856c9af82b2c25c51b3c36bafb71f4" title="Submit a derived fact to the core from a decision procedure.">enqueueFact</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#abcd88b0572b5751bddccd9210939f5d0">d_rules</a>-><a class="code" href="classCVC3_1_1DatatypeProofRules.html#a1f1fede903939b996f001baf43ec1f17">dummyTheorem</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a64a98802daa8a6a7c4f683b60740961f">d_facts</a>, e2));
<a name="l00109"></a>00109 }
<a name="l00110"></a>00110
<a name="l00111"></a>00111
<a name="l00112"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a3915e378cdf3889e9776b7f0e8c7ee15">00112</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a3915e378cdf3889e9776b7f0e8c7ee15">TheoryDatatype::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="l00113"></a>00113 {
<a name="l00114"></a>00114 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1Theory.html#a08412b310cb743536f7edd9fccd60e46" title="Return the find of e, or e if it has no find.">findExpr</a>(e) == e,
<a name="l00115"></a>00115 <span class="stringliteral">"datatype: initializeLabels: Expected find(e)=e"</span>);
<a name="l00116"></a>00116 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>.<a class="code" href="classCVC3_1_1ExprMap.html#ae50ab1874dd63b575553e7db769abe28">find</a>(t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>()) != <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>.<a class="code" href="classCVC3_1_1ExprMap.html#a283ae6c44308cbdda0d82da5a16e52c8">end</a>(),
<a name="l00117"></a>00117 <span class="stringliteral">"Unknown datatype: "</span>+t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00118"></a>00118 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<unsigned></a>& c = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>[t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>()];
<a name="l00119"></a>00119 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a1cadecbd2d6fa614a2f2e9419aa43f33">find</a>(e) == <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a2a26c7cc4db12cb17d273db5cfa5a890">end</a>(),
<a name="l00120"></a>00120 <span class="stringliteral">"datatype: initializeLabels: expected unlabeled expr"</span>);
<a name="l00121"></a>00121 <span class="keywordflow">if</span> (<a class="code" href="namespaceCVC3.html#a91840d293c43120244ce5b5165bdacc4">isConstructor</a>(e)) {
<a name="l00122"></a>00122 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> cons = <a class="code" href="namespaceCVC3.html#ac1eec763ed1ae5d0f52c4bed47d6fee5">getConstructor</a>(e);
<a name="l00123"></a>00123 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(c.find(cons) != c.end(),
<a name="l00124"></a>00124 <span class="stringliteral">"datatype: initializeLabels: Couldn't find constructor "</span>
<a name="l00125"></a>00125 +cons.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00126"></a>00126 <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a664a15046de83b0af599f488cb420022">insert</a>(e,
<a name="l00127"></a>00127 <a class="code" href="classCVC3_1_1SmartCDO.html">SmartCDO<Unsigned></a>(<a class="code" href="classCVC3_1_1Theory.html#a90684d2a97738341c00f8f9c99af7b66" title="Get a pointer to theoryCore.">theoryCore</a>()->getCM()->getCurrentContext(),
<a name="l00128"></a>00128 (<a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a>)1 << c[cons], 0));
<a name="l00129"></a>00129 }
<a name="l00130"></a>00130 <span class="keywordflow">else</span> {
<a name="l00131"></a>00131 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(c.size() > 0, <span class="stringliteral">"No constructors?"</span>);
<a name="l00132"></a>00132 <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a> value = ((<a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a>)1 << c.size()) - 1;
<a name="l00133"></a>00133 <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a664a15046de83b0af599f488cb420022">insert</a>(e,
<a name="l00134"></a>00134 <a class="code" href="classCVC3_1_1SmartCDO.html">SmartCDO<Unsigned></a>(<a class="code" href="classCVC3_1_1Theory.html#a90684d2a97738341c00f8f9c99af7b66" title="Get a pointer to theoryCore.">theoryCore</a>()->getCM()->getCurrentContext(),
<a name="l00135"></a>00135 value, 0));
<a name="l00136"></a>00136 <span class="keywordflow">if</span> (value == 1) <a class="code" href="classCVC3_1_1TheoryDatatype.html#a61b966ebd57ae1b2819f8d6ac73555f6">instantiate</a>(e, 1);
<a name="l00137"></a>00137 <span class="keywordflow">else</span> {
<a name="l00138"></a>00138 <span class="keywordflow">if</span> (!<a class="code" href="classCVC3_1_1TheoryDatatype.html#a44dee8f4a9da185dcbac872295d342a4">d_smartSplits</a> || t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>().<a class="code" href="group__ExprPkg.html#gacf628bd70fc2c4766afa268ed22ea947">isFinite</a>()) <a class="code" href="classCVC3_1_1TheoryDatatype.html#a3b16dee83eb2df2c860c14752913a12e">d_splitters</a>.<a class="code" href="classCVC3_1_1CDList.html#aa1e8d3591c596d1b9c585dec955b519b">push_back</a>(e);
<a name="l00139"></a>00139 }
<a name="l00140"></a>00140 }
<a name="l00141"></a>00141 }
<a name="l00142"></a>00142
<a name="l00143"></a>00143
<a name="l00144"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a942fa3974b5c4bc2f44e202a6adc80c8">00144</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a942fa3974b5c4bc2f44e202a6adc80c8">TheoryDatatype::mergeLabels</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm,
<a name="l00145"></a>00145 <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="l00146"></a>00146 {
<a name="l00147"></a>00147 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e2.<a class="code" href="group__ExprPkg.html#ga4dc94c33ae308ff8d9d004f49df8f42b">hasFind</a>() && <a class="code" href="classCVC3_1_1Theory.html#a08412b310cb743536f7edd9fccd60e46" title="Return the find of e, or e if it has no find.">findExpr</a>(e2) == e2,
<a name="l00148"></a>00148 <span class="stringliteral">"datatype: mergeLabels: Expected find(e2)=e2"</span>);
<a name="l00149"></a>00149 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a1cadecbd2d6fa614a2f2e9419aa43f33">find</a>(e1) != <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a2a26c7cc4db12cb17d273db5cfa5a890">end</a>() &&
<a name="l00150"></a>00150 <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a1cadecbd2d6fa614a2f2e9419aa43f33">find</a>(e2) != <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a2a26c7cc4db12cb17d273db5cfa5a890">end</a>(),
<a name="l00151"></a>00151 <span class="stringliteral">"mergeLabels: expr is not labeled"</span>);
<a name="l00152"></a>00152 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(e1) == <a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(e2), <span class="stringliteral">"Expected same type"</span>);
<a name="l00153"></a>00153 <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a> u = <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>[e2].get().get();
<a name="l00154"></a>00154 <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a> uNew = u & <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>[e1].get().get();
<a name="l00155"></a>00155 <span class="keywordflow">if</span> (u != uNew) {
<a name="l00156"></a>00156 <span class="keywordflow">if</span> (!thm.<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>()) <a class="code" href="classCVC3_1_1TheoryDatatype.html#a64a98802daa8a6a7c4f683b60740961f">d_facts</a>.<a class="code" href="classCVC3_1_1CDList.html#aa1e8d3591c596d1b9c585dec955b519b">push_back</a>(thm);
<a name="l00157"></a>00157 <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>[e2].get().set(uNew);
<a name="l00158"></a>00158 <span class="keywordflow">if</span> (uNew == 0)
<a name="l00159"></a>00159 <a class="code" href="classCVC3_1_1Theory.html#a89f8e1e02e22ef524c286ce8b87bdea4" title="Make the context inconsistent; The formula proved by e must FALSE.">setInconsistent</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#abcd88b0572b5751bddccd9210939f5d0">d_rules</a>-><a class="code" href="classCVC3_1_1DatatypeProofRules.html#a1f1fede903939b996f001baf43ec1f17">dummyTheorem</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a64a98802daa8a6a7c4f683b60740961f">d_facts</a>, <a class="code" href="classCVC3_1_1Theory.html#a0bbf7c5b6079fc99a0f759e5809fe6f5" title="Return FALSE Expr.">falseExpr</a>()));
<a name="l00160"></a>00160 }
<a name="l00161"></a>00161 <span class="keywordflow">if</span> (uNew != 0 && ((uNew - 1) & uNew) == 0) {
<a name="l00162"></a>00162 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a61b966ebd57ae1b2819f8d6ac73555f6">instantiate</a>(e2, uNew);
<a name="l00163"></a>00163 }
<a name="l00164"></a>00164 }
<a name="l00165"></a>00165
<a name="l00166"></a>00166
<a name="l00167"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a602556d54fd1ad24a04437416613c7a4">00167</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a942fa3974b5c4bc2f44e202a6adc80c8">TheoryDatatype::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="l00168"></a>00168 <span class="keywordtype">unsigned</span> position, <span class="keywordtype">bool</span> positive)
<a name="l00169"></a>00169 {
<a name="l00170"></a>00170 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e.<a class="code" href="group__ExprPkg.html#ga4dc94c33ae308ff8d9d004f49df8f42b">hasFind</a>() && <a class="code" href="classCVC3_1_1Theory.html#a08412b310cb743536f7edd9fccd60e46" title="Return the find of e, or e if it has no find.">findExpr</a>(e) == e,
<a name="l00171"></a>00171 <span class="stringliteral">"datatype: mergeLabels2: Expected find(e)=e"</span>);
<a name="l00172"></a>00172 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a1cadecbd2d6fa614a2f2e9419aa43f33">find</a>(e) != <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a2a26c7cc4db12cb17d273db5cfa5a890">end</a>(),
<a name="l00173"></a>00173 <span class="stringliteral">"mergeLabels2: expr is not labeled"</span>);
<a name="l00174"></a>00174 <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a> u = <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>[e].get().get();
<a name="l00175"></a>00175 <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a> uNew = (<a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a>)1 << position;
<a name="l00176"></a>00176 <span class="keywordflow">if</span> (positive) {
<a name="l00177"></a>00177 uNew = u & uNew;
<a name="l00178"></a>00178 <span class="keywordflow">if</span> (u == uNew) <span class="keywordflow">return</span>;
<a name="l00179"></a>00179 } <span class="keywordflow">else</span> <span class="keywordflow">if</span> ((u & uNew) != 0) uNew = u - uNew;
<a name="l00180"></a>00180 <span class="keywordflow">else</span> <span class="keywordflow">return</span>;
<a name="l00181"></a>00181 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a64a98802daa8a6a7c4f683b60740961f">d_facts</a>.<a class="code" href="classCVC3_1_1CDList.html#aa1e8d3591c596d1b9c585dec955b519b">push_back</a>(thm);
<a name="l00182"></a>00182 <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>[e].get().set(uNew);
<a name="l00183"></a>00183 <span class="keywordflow">if</span> (uNew == 0)
<a name="l00184"></a>00184 <a class="code" href="classCVC3_1_1Theory.html#a89f8e1e02e22ef524c286ce8b87bdea4" title="Make the context inconsistent; The formula proved by e must FALSE.">setInconsistent</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#abcd88b0572b5751bddccd9210939f5d0">d_rules</a>-><a class="code" href="classCVC3_1_1DatatypeProofRules.html#a1f1fede903939b996f001baf43ec1f17">dummyTheorem</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a64a98802daa8a6a7c4f683b60740961f">d_facts</a>, <a class="code" href="classCVC3_1_1Theory.html#a0bbf7c5b6079fc99a0f759e5809fe6f5" title="Return FALSE Expr.">falseExpr</a>()));
<a name="l00185"></a>00185 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (((uNew - 1) & uNew) == 0) {
<a name="l00186"></a>00186 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a61b966ebd57ae1b2819f8d6ac73555f6">instantiate</a>(e, uNew);
<a name="l00187"></a>00187 }
<a name="l00188"></a>00188 }
<a name="l00189"></a>00189
<a name="l00190"></a>00190
<a name="l00191"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a998e0cd18f7d41f9e7df014d7f86edbc">00191</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a998e0cd18f7d41f9e7df014d7f86edbc" title="Notify theory of a new shared term.">TheoryDatatype::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="l00192"></a>00192 {
<a name="l00193"></a>00193 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(e).getExpr().getKind() == <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ad94b8e65b0abc98bb6b5729da9e3b40a">DATATYPE</a> &&
<a name="l00194"></a>00194 <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a1cadecbd2d6fa614a2f2e9419aa43f33">find</a>(e) == <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a2a26c7cc4db12cb17d273db5cfa5a890">end</a>()) {
<a name="l00195"></a>00195 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a3915e378cdf3889e9776b7f0e8c7ee15">initializeLabels</a>(e, <a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(e));
<a name="l00196"></a>00196 e.<a class="code" href="group__ExprPkg.html#ga159d60cb0f32e09df89a395b2680664a" title="Add (e,i) to the notify list of this expression.">addToNotify</a>(<span class="keyword">this</span>, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>());
<a name="l00197"></a>00197 }
<a name="l00198"></a>00198 }
<a name="l00199"></a>00199
<a name="l00200"></a>00200
<a name="l00201"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a640ba909d9c6470c40600a82cdb65417">00201</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a640ba909d9c6470c40600a82cdb65417" title="Assert a new fact to the decision procedure.">TheoryDatatype::assertFact</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e)
<a name="l00202"></a>00202 {
<a name="l00203"></a>00203 <span class="keywordflow">if</span> (!e.<a class="code" href="classCVC3_1_1Theorem.html#a362c1d70e03803d804bbe300e5f6dc87">isRewrite</a>()) {
<a name="l00204"></a>00204 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& expr = e.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>();
<a name="l00205"></a>00205 <span class="keywordflow">if</span> (expr.<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="l00206"></a>00206 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a942fa3974b5c4bc2f44e202a6adc80c8">mergeLabels</a>(e, expr[0],
<a name="l00207"></a>00207 <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d93ab7a39a1eb3e82cb67f0425ffee">getConsPos</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#af39a46bc360e9f7c91bf0d85cc3908ca">getConsForTester</a>(expr.<a class="code" href="group__ExprPkg.html#ga9f3328fe077191803a780cfd6566ff9b" title="Get expression of operator (for APPLY Exprs only)">getOpExpr</a>())),
<a name="l00208"></a>00208 <span class="keyword">true</span>);
<a name="l00209"></a>00209 }
<a name="l00210"></a>00210 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (expr.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>()) {
<a name="l00211"></a>00211 <span class="keywordflow">if</span> (expr[0].getOpKind() == <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089a4df0e72bf250adc8dd78e81fea2f281c">TESTER</a>) {
<a name="l00212"></a>00212 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a942fa3974b5c4bc2f44e202a6adc80c8">mergeLabels</a>(e, expr[0][0],
<a name="l00213"></a>00213 <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d93ab7a39a1eb3e82cb67f0425ffee">getConsPos</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#af39a46bc360e9f7c91bf0d85cc3908ca">getConsForTester</a>(expr[0].getOpExpr())),
<a name="l00214"></a>00214 <span class="keyword">false</span>);
<a name="l00215"></a>00215 }
<a name="l00216"></a>00216 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (expr[0].isEq() &&
<a name="l00217"></a>00217 <a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(expr[0][0]).getExpr().getKind() == <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ad94b8e65b0abc98bb6b5729da9e3b40a">DATATYPE</a>) {
<a name="l00218"></a>00218 <span class="comment">// Propagate disequality down</span>
<a name="l00219"></a>00219 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a1cadecbd2d6fa614a2f2e9419aa43f33">find</a>(expr[0][0]) == <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a2a26c7cc4db12cb17d273db5cfa5a890">end</a>()) {
<a name="l00220"></a>00220 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a3915e378cdf3889e9776b7f0e8c7ee15">initializeLabels</a>(expr[0][0], <a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(expr[0][0]));
<a name="l00221"></a>00221 expr[0][0].<a class="code" href="group__ExprPkg.html#ga159d60cb0f32e09df89a395b2680664a" title="Add (e,i) to the notify list of this expression.">addToNotify</a>(<span class="keyword">this</span>, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>());
<a name="l00222"></a>00222 }
<a name="l00223"></a>00223 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a1cadecbd2d6fa614a2f2e9419aa43f33">find</a>(expr[0][1]) == <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a2a26c7cc4db12cb17d273db5cfa5a890">end</a>()) {
<a name="l00224"></a>00224 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a3915e378cdf3889e9776b7f0e8c7ee15">initializeLabels</a>(expr[0][1], <a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(expr[0][1]));
<a name="l00225"></a>00225 expr[0][1].<a class="code" href="group__ExprPkg.html#ga159d60cb0f32e09df89a395b2680664a" title="Add (e,i) to the notify list of this expression.">addToNotify</a>(<span class="keyword">this</span>, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>());
<a name="l00226"></a>00226 }
<a name="l00227"></a>00227 <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a> u1 = <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>[expr[0][0]].get().get();
<a name="l00228"></a>00228 <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a> u2 = <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>[expr[0][1]].get().get();
<a name="l00229"></a>00229 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<unsigned></a>& c = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>[<a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(expr[0][0]).<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>()];
<a name="l00230"></a>00230 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<unsigned>::iterator</a> c_it = c.<a class="code" href="classCVC3_1_1ExprMap.html#a3db85401f8535daf4054fde531cd46b1">begin</a>(), c_end = c.<a class="code" href="classCVC3_1_1ExprMap.html#a283ae6c44308cbdda0d82da5a16e52c8">end</a>();
<a name="l00231"></a>00231 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> bigConj;
<a name="l00232"></a>00232 <span class="keywordflow">for</span> (; c_it != c_end; ++c_it) {
<a name="l00233"></a>00233 <span class="keywordflow">if</span> ((u1 & u2 & ((<a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a>)1 << <span class="keywordtype">unsigned</span>((*c_it).second))) != 0) {
<a name="l00234"></a>00234 vector<Expr>& selectors = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a1e8e2818f2f0dcf45743b42b3d9778b3">d_constructorMap</a>[(*c_it).first];
<a name="l00235"></a>00235 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> conj;
<a name="l00236"></a>00236 <span class="keywordflow">for</span> (<span class="keywordtype">unsigned</span> i = 0; i < selectors.size(); ++i) {
<a name="l00237"></a>00237 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e1 = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(selectors[i].mkOp(), expr[0][0]);
<a name="l00238"></a>00238 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e2 = e1.<a class="code" href="group__ExprPkg.html#gacb48495ca445c895f95d0c3c1ae2070b">eqExpr</a>(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(selectors[i].mkOp(), expr[0][1]));
<a name="l00239"></a>00239 <span class="keywordflow">if</span> (conj.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>()) conj = e2;
<a name="l00240"></a>00240 <span class="keywordflow">else</span> conj = conj.<a class="code" href="group__ExprPkg.html#ga6c3651465ce69ed5f4e6fd461b9acf3c">andExpr</a>(e2);
<a name="l00241"></a>00241 }
<a name="l00242"></a>00242 <span class="keywordflow">if</span> (!conj.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>()) {
<a name="l00243"></a>00243 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e1 = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a51372d26e89b189c8a5f42d18dd2eedc">datatypeTestExpr</a>((*c_it).first.getName(), expr[0][0]);
<a name="l00244"></a>00244 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e2 = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a51372d26e89b189c8a5f42d18dd2eedc">datatypeTestExpr</a>((*c_it).first.getName(), expr[0][1]);
<a name="l00245"></a>00245 conj = (e1 && e2).impExpr(!conj);
<a name="l00246"></a>00246 <span class="keywordflow">if</span> (bigConj.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>()) bigConj = conj;
<a name="l00247"></a>00247 <span class="keywordflow">else</span> bigConj = bigConj.<a class="code" href="group__ExprPkg.html#ga6c3651465ce69ed5f4e6fd461b9acf3c">andExpr</a>(conj);
<a name="l00248"></a>00248 }
<a name="l00249"></a>00249 }
<a name="l00250"></a>00250 }
<a name="l00251"></a>00251 <span class="keywordflow">if</span> (!bigConj.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>()) {
<a name="l00252"></a>00252 <a class="code" href="classCVC3_1_1Theory.html#a93856c9af82b2c25c51b3c36bafb71f4" title="Submit a derived fact to the core from a decision procedure.">enqueueFact</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#abcd88b0572b5751bddccd9210939f5d0">d_rules</a>-><a class="code" href="classCVC3_1_1DatatypeProofRules.html#a1f1fede903939b996f001baf43ec1f17">dummyTheorem</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a64a98802daa8a6a7c4f683b60740961f">d_facts</a>, expr.<a class="code" href="group__ExprPkg.html#ga8dd97bcdeb9d8870238f94a263fd083b">impExpr</a>(bigConj)));
<a name="l00253"></a>00253 }
<a name="l00254"></a>00254 }
<a name="l00255"></a>00255 }
<a name="l00256"></a>00256 }
<a name="l00257"></a>00257 }
<a name="l00258"></a>00258
<a name="l00259"></a>00259
<a name="l00260"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a50136aaaf32b6b42751290cb2ccfedf6">00260</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a50136aaaf32b6b42751290cb2ccfedf6" title="Check for satisfiability in the theory.">TheoryDatatype::checkSat</a>(<span class="keywordtype">bool</span> fullEffort)
<a name="l00261"></a>00261 {
<a name="l00262"></a>00262 <span class="keywordtype">bool</span> done = <span class="keyword">false</span>;
<a name="l00263"></a>00263 <span class="keywordflow">while</span> (!done && <a class="code" href="classCVC3_1_1TheoryDatatype.html#a1952cec9cef126b4c3d9611738f7169e">d_splittersIndex</a> < <a class="code" href="classCVC3_1_1TheoryDatatype.html#a3b16dee83eb2df2c860c14752913a12e">d_splitters</a>.<a class="code" href="classCVC3_1_1CDList.html#adf92d0f391d73e7ac70da57db135af27">size</a>()) {
<a name="l00264"></a>00264 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a3b16dee83eb2df2c860c14752913a12e">d_splitters</a>[<a class="code" href="classCVC3_1_1TheoryDatatype.html#a1952cec9cef126b4c3d9611738f7169e">d_splittersIndex</a>];
<a name="l00265"></a>00265 <span class="keywordflow">if</span> ((!<a class="code" href="classCVC3_1_1TheoryDatatype.html#a44dee8f4a9da185dcbac872295d342a4">d_smartSplits</a> || <a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(e).getExpr().isFinite()) &&
<a name="l00266"></a>00266 <a class="code" href="classCVC3_1_1Theory.html#a08412b310cb743536f7edd9fccd60e46" title="Return the find of e, or e if it has no find.">findExpr</a>(e) == e) {
<a name="l00267"></a>00267 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a1cadecbd2d6fa614a2f2e9419aa43f33">find</a>(e) != <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a2a26c7cc4db12cb17d273db5cfa5a890">end</a>(),
<a name="l00268"></a>00268 <span class="stringliteral">"checkSat: expr is not labeled"</span>);
<a name="l00269"></a>00269 <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a> u = <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>[e].get().get();
<a name="l00270"></a>00270 <span class="keywordflow">if</span> ((u & (u-1)) != 0) {
<a name="l00271"></a>00271 done = <span class="keyword">true</span>;
<a name="l00272"></a>00272 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!<a class="code" href="classCVC3_1_1TheoryDatatype.html#a73d20b00d4a702698ea0a9baea9c5bc2">d_splitterAsserted</a> || !fullEffort,
<a name="l00273"></a>00273 <span class="stringliteral">"splitter should have been resolved"</span>);
<a name="l00274"></a>00274 <span class="keywordflow">if</span> (!<a class="code" href="classCVC3_1_1TheoryDatatype.html#a73d20b00d4a702698ea0a9baea9c5bc2">d_splitterAsserted</a>) {
<a name="l00275"></a>00275 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>
<a name="l00276"></a>00276 (<a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>.<a class="code" href="classCVC3_1_1ExprMap.html#ae50ab1874dd63b575553e7db769abe28">find</a>(<a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(e).getExpr()) != <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>.<a class="code" href="classCVC3_1_1ExprMap.html#a283ae6c44308cbdda0d82da5a16e52c8">end</a>(),
<a name="l00277"></a>00277 <span class="stringliteral">"datatype: checkSat: Unexpected type: "</span>+<a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(e).<a class="code" href="classCVC3_1_1Type.html#a2f5ce4b1973ec02b2f2b2eba8ce3cc50">toString</a>()
<a name="l00278"></a>00278 +<span class="stringliteral">"\n\n for expression: "</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00279"></a>00279 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<unsigned></a>& c = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>[<a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(e).<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>()];
<a name="l00280"></a>00280 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<unsigned>::iterator</a> c_it = c.<a class="code" href="classCVC3_1_1ExprMap.html#a3db85401f8535daf4054fde531cd46b1">begin</a>(), c_end = c.end();
<a name="l00281"></a>00281 vector<Expr> vec;
<a name="l00282"></a>00282 <span class="keywordflow">for</span> (; c_it != c_end; ++c_it) {
<a name="l00283"></a>00283 <span class="keywordflow">if</span> ((u & ((<a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a>)1 << <span class="keywordtype">unsigned</span>((*c_it).second))) != 0) {
<a name="l00284"></a>00284 vec.push_back(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a51372d26e89b189c8a5f42d18dd2eedc">datatypeTestExpr</a>((*c_it).first.getName(), e));
<a name="l00285"></a>00285 }
<a name="l00286"></a>00286 }
<a name="l00287"></a>00287 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(vec.size() > 1, <span class="stringliteral">"datatype: checkSat: expected 2 or more possible constructors"</span>);
<a name="l00288"></a>00288 <a class="code" href="classCVC3_1_1Theory.html#a93856c9af82b2c25c51b3c36bafb71f4" title="Submit a derived fact to the core from a decision procedure.">enqueueFact</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#abcd88b0572b5751bddccd9210939f5d0">d_rules</a>-><a class="code" href="classCVC3_1_1DatatypeProofRules.html#a1f1fede903939b996f001baf43ec1f17">dummyTheorem</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a64a98802daa8a6a7c4f683b60740961f">d_facts</a>, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>, vec)));
<a name="l00289"></a>00289 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a73d20b00d4a702698ea0a9baea9c5bc2">d_splitterAsserted</a> = <span class="keyword">true</span>;
<a name="l00290"></a>00290 }
<a name="l00291"></a>00291 }
<a name="l00292"></a>00292 }
<a name="l00293"></a>00293 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoryDatatype.html#a44dee8f4a9da185dcbac872295d342a4">d_smartSplits</a> && !done && <a class="code" href="namespaceCVC3.html#afdcf0b93fc0d1b03a5a14c4988443c7a">isSelector</a>(e)) {
<a name="l00294"></a>00294 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> f = <a class="code" href="classCVC3_1_1Theory.html#a08412b310cb743536f7edd9fccd60e46" title="Return the find of e, or e if it has no find.">findExpr</a>(e[0]);
<a name="l00295"></a>00295 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a1cadecbd2d6fa614a2f2e9419aa43f33">find</a>(f) != <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a2a26c7cc4db12cb17d273db5cfa5a890">end</a>(),
<a name="l00296"></a>00296 <span class="stringliteral">"checkSat: expr is not labeled"</span>);
<a name="l00297"></a>00297 <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a> u = <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>[f].get().get();
<a name="l00298"></a>00298 <span class="keywordflow">if</span> ((u & (u-1)) != 0) {
<a name="l00299"></a>00299 pair<Expr, unsigned> selectorInfo = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a5ae1a2fe60c6e2af77cf098340cabd53">getSelectorInfo</a>(e.<a class="code" href="group__ExprPkg.html#ga9f3328fe077191803a780cfd6566ff9b" title="Get expression of operator (for APPLY Exprs only)">getOpExpr</a>());
<a name="l00300"></a>00300 <span class="keywordtype">unsigned</span> pos = <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d93ab7a39a1eb3e82cb67f0425ffee">getConsPos</a>(selectorInfo.first);
<a name="l00301"></a>00301 <span class="keywordflow">if</span> ((u & ((<a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a>)1 << pos)) != 0) {
<a name="l00302"></a>00302 done = <span class="keyword">true</span>;
<a name="l00303"></a>00303 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!<a class="code" href="classCVC3_1_1TheoryDatatype.html#a73d20b00d4a702698ea0a9baea9c5bc2">d_splitterAsserted</a> || !fullEffort,
<a name="l00304"></a>00304 <span class="stringliteral">"splitter should have been resolved"</span>);
<a name="l00305"></a>00305 <span class="keywordflow">if</span> (!<a class="code" href="classCVC3_1_1TheoryDatatype.html#a73d20b00d4a702698ea0a9baea9c5bc2">d_splitterAsserted</a>) {
<a name="l00306"></a>00306 <a class="code" href="classCVC3_1_1Theory.html#a605e960d2442b587046c562723b7f03a" title="Suggest a splitter to the SearchEngine.">addSplitter</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a51372d26e89b189c8a5f42d18dd2eedc">datatypeTestExpr</a>(selectorInfo.first.getName(), f));
<a name="l00307"></a>00307 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a73d20b00d4a702698ea0a9baea9c5bc2">d_splitterAsserted</a> = <span class="keyword">true</span>;
<a name="l00308"></a>00308 }
<a name="l00309"></a>00309 }
<a name="l00310"></a>00310 }
<a name="l00311"></a>00311 }
<a name="l00312"></a>00312 <span class="keywordflow">if</span> (!done) {
<a name="l00313"></a>00313 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a73d20b00d4a702698ea0a9baea9c5bc2">d_splitterAsserted</a> = <span class="keyword">false</span>;
<a name="l00314"></a>00314 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a1952cec9cef126b4c3d9611738f7169e">d_splittersIndex</a> = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a1952cec9cef126b4c3d9611738f7169e">d_splittersIndex</a> + 1;
<a name="l00315"></a>00315 }
<a name="l00316"></a>00316 }
<a name="l00317"></a>00317 }
<a name="l00318"></a>00318
<a name="l00319"></a>00319
<a name="l00320"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a5fea4f3ab06825c2df409082095f7d96">00320</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a5fea4f3ab06825c2df409082095f7d96" title="Theory-specific rewrite rules.">TheoryDatatype::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="l00321"></a>00321 {
<a name="l00322"></a>00322 <span class="comment">// TODO: UF rewrite?</span>
<a name="l00323"></a>00323 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm;
<a name="l00324"></a>00324 <span class="keywordflow">if</span> (<a class="code" href="namespaceCVC3.html#afdcf0b93fc0d1b03a5a14c4988443c7a">isSelector</a>(e)) {
<a name="l00325"></a>00325 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoryDatatype.html#a513d221b48500cf4bc91393293d9b2f2">canCollapse</a>(e)) {
<a name="l00326"></a>00326 thm = <a class="code" href="classCVC3_1_1TheoryDatatype.html#abcd88b0572b5751bddccd9210939f5d0">d_rules</a>-><a class="code" href="classCVC3_1_1DatatypeProofRules.html#a8ecc9e0e858ab2da52632df61ee8a44e">rewriteSelCons</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a64a98802daa8a6a7c4f683b60740961f">d_facts</a>, e);
<a name="l00327"></a>00327 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theory.html#a76f6507116e36f46dab074781fb9bf2d" title="(a1 == a2) & (a2 == a3) ==> (a1 == a3)">transitivityRule</a>(thm, <a class="code" href="classCVC3_1_1Theory.html#a52158688456f8605b064fbbf7a46039c" title="Simplify a term e and return a Theorem(e==e')">simplify</a>(thm.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>()));
<a name="l00328"></a>00328 }
<a name="l00329"></a>00329 }
<a name="l00330"></a>00330 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (<a class="code" href="namespaceCVC3.html#a8297278831bf83882f7c6a1e3c84fa98">isTester</a>(e)) {
<a name="l00331"></a>00331 <span class="keywordflow">if</span> (<a class="code" href="namespaceCVC3.html#a91840d293c43120244ce5b5165bdacc4">isConstructor</a>(e[0])) {
<a name="l00332"></a>00332 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#abcd88b0572b5751bddccd9210939f5d0">d_rules</a>-><a class="code" href="classCVC3_1_1DatatypeProofRules.html#ad6df2a8a8c661ed1a1be34ce66910a36">rewriteTestCons</a>(e);
<a name="l00333"></a>00333 }
<a name="l00334"></a>00334 }
<a name="l00335"></a>00335 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theory.html#af860f5d5e01423628c97c399606916ff" title="==> a == a">reflexivityRule</a>(e);
<a name="l00336"></a>00336 }
<a name="l00337"></a>00337
<a name="l00338"></a>00338
<a name="l00339"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a8825c26c5b357ec4a6fde28aaceeea44">00339</a> <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.">TheoryDatatype::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="l00340"></a>00340 {
<a name="l00341"></a>00341 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(e).getExpr().getKind() == <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ad94b8e65b0abc98bb6b5729da9e3b40a">DATATYPE</a> &&
<a name="l00342"></a>00342 <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a1cadecbd2d6fa614a2f2e9419aa43f33">find</a>(e) == <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a2a26c7cc4db12cb17d273db5cfa5a890">end</a>()) {
<a name="l00343"></a>00343 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a3915e378cdf3889e9776b7f0e8c7ee15">initializeLabels</a>(e, <a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(e));
<a name="l00344"></a>00344 e.<a class="code" href="group__ExprPkg.html#ga159d60cb0f32e09df89a395b2680664a" title="Add (e,i) to the notify list of this expression.">addToNotify</a>(<span class="keyword">this</span>, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>());
<a name="l00345"></a>00345 }
<a name="l00346"></a>00346 <span class="keywordflow">if</span> (e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() != <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5c41450c4e719ca40d8e734f6a2008f0">APPLY</a>) <span class="keywordflow">return</span>;
<a name="l00347"></a>00347 <span class="keywordflow">if</span> (<a class="code" href="namespaceCVC3.html#a91840d293c43120244ce5b5165bdacc4">isConstructor</a>(e) && e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() > 0) {
<a name="l00348"></a>00348 <a class="code" href="classCVC3_1_1Theory.html#a93856c9af82b2c25c51b3c36bafb71f4" title="Submit a derived fact to the core from a decision procedure.">enqueueFact</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#abcd88b0572b5751bddccd9210939f5d0">d_rules</a>-><a class="code" href="classCVC3_1_1DatatypeProofRules.html#acbe824de0e366b711db6d23e23b72509">noCycle</a>(e));
<a name="l00349"></a>00349 }
<a name="l00350"></a>00350 <span class="keywordflow">if</span> (<a class="code" href="namespaceCVC3.html#afdcf0b93fc0d1b03a5a14c4988443c7a">isSelector</a>(e)) {
<a name="l00351"></a>00351 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoryDatatype.html#a44dee8f4a9da185dcbac872295d342a4">d_smartSplits</a>) <a class="code" href="classCVC3_1_1TheoryDatatype.html#a3b16dee83eb2df2c860c14752913a12e">d_splitters</a>.<a class="code" href="classCVC3_1_1CDList.html#aa1e8d3591c596d1b9c585dec955b519b">push_back</a>(e);
<a name="l00352"></a>00352 e[0].<a class="code" href="group__ExprPkg.html#ga50ebe7a6fa50064b2d01e0eaa25f931a" title="Set the Selected flag for this Expr.">setSelected</a>();
<a name="l00353"></a>00353 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a942fa3974b5c4bc2f44e202a6adc80c8">mergeLabels</a>(<a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>(), e[0], e[0]);
<a name="l00354"></a>00354 }
<a name="l00355"></a>00355 <a class="code" href="classCVC3_1_1Theory.html#a29cc343040a52a299a4f20123edf4c75" title="Setup a term for congruence closure (must have sig and rep attributes)">setupCC</a>(e);
<a name="l00356"></a>00356 }
<a name="l00357"></a>00357
<a name="l00358"></a>00358
<a name="l00359"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a4d1da766acf310b425f564027c70b8b9">00359</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a4d1da766acf310b425f564027c70b8b9" title="Notify a theory of a new equality.">TheoryDatatype::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="l00360"></a>00360 {
<a name="l00361"></a>00361 <span class="keywordflow">if</span> (d.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>()) {
<a name="l00362"></a>00362 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& lhs = e.<a class="code" href="classCVC3_1_1Theorem.html#a206c04f39fbbcacef2337148675553f4">getLHS</a>();
<a name="l00363"></a>00363 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& rhs = e.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>();
<a name="l00364"></a>00364 <span class="keywordflow">if</span> (<a class="code" href="namespaceCVC3.html#a91840d293c43120244ce5b5165bdacc4">isConstructor</a>(lhs) && <a class="code" href="namespaceCVC3.html#a91840d293c43120244ce5b5165bdacc4">isConstructor</a>(rhs) &&
<a name="l00365"></a>00365 lhs.<a class="code" href="group__ExprPkg.html#ga1d6a6b4a9ce81b0dd8fd74870ff4284b">isApply</a>() && rhs.<a class="code" href="group__ExprPkg.html#ga1d6a6b4a9ce81b0dd8fd74870ff4284b">isApply</a>() &&
<a name="l00366"></a>00366 lhs.<a class="code" href="group__ExprPkg.html#ga9f3328fe077191803a780cfd6566ff9b" title="Get expression of operator (for APPLY Exprs only)">getOpExpr</a>() == rhs.<a class="code" href="group__ExprPkg.html#ga9f3328fe077191803a780cfd6566ff9b" title="Get expression of operator (for APPLY Exprs only)">getOpExpr</a>()) {
<a name="l00367"></a>00367 <a class="code" href="classCVC3_1_1Theory.html#a93856c9af82b2c25c51b3c36bafb71f4" title="Submit a derived fact to the core from a decision procedure.">enqueueFact</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#abcd88b0572b5751bddccd9210939f5d0">d_rules</a>-><a class="code" href="classCVC3_1_1DatatypeProofRules.html#a0ae4bc02188f1115e9ba2a44185b1d16">decompose</a>(e));
<a name="l00368"></a>00368 }
<a name="l00369"></a>00369 <span class="keywordflow">else</span> {
<a name="l00370"></a>00370 <span class="comment">// Possible for rhs to never have been seen: initialize it here</span>
<a name="l00371"></a>00371 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(rhs).getExpr().getKind() == <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ad94b8e65b0abc98bb6b5729da9e3b40a">DATATYPE</a>,
<a name="l00372"></a>00372 <span class="stringliteral">"Expected datatype"</span>);
<a name="l00373"></a>00373 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a1cadecbd2d6fa614a2f2e9419aa43f33">find</a>(rhs) == <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a2a26c7cc4db12cb17d273db5cfa5a890">end</a>()) {
<a name="l00374"></a>00374 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a3915e378cdf3889e9776b7f0e8c7ee15">initializeLabels</a>(rhs, <a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(rhs));
<a name="l00375"></a>00375 rhs.<a class="code" href="group__ExprPkg.html#ga159d60cb0f32e09df89a395b2680664a" title="Add (e,i) to the notify list of this expression.">addToNotify</a>(<span class="keyword">this</span>, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>());
<a name="l00376"></a>00376 }
<a name="l00377"></a>00377 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm(e);
<a name="l00378"></a>00378 <span class="keywordflow">if</span> (lhs.<a class="code" href="group__ExprPkg.html#ga3292a2d664355dd3246479f21e6f26cb">isSelected</a>() && !rhs.<a class="code" href="group__ExprPkg.html#ga3292a2d664355dd3246479f21e6f26cb">isSelected</a>()) {
<a name="l00379"></a>00379 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a64a98802daa8a6a7c4f683b60740961f">d_facts</a>.<a class="code" href="classCVC3_1_1CDList.html#aa1e8d3591c596d1b9c585dec955b519b">push_back</a>(e);
<a name="l00380"></a>00380 rhs.<a class="code" href="group__ExprPkg.html#ga50ebe7a6fa50064b2d01e0eaa25f931a" title="Set the Selected flag for this Expr.">setSelected</a>();
<a name="l00381"></a>00381 thm = <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>();
<a name="l00382"></a>00382 }
<a name="l00383"></a>00383 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a942fa3974b5c4bc2f44e202a6adc80c8">mergeLabels</a>(thm, lhs, rhs);
<a name="l00384"></a>00384 }
<a name="l00385"></a>00385 }
<a name="l00386"></a>00386 <span class="keywordflow">else</span> {
<a name="l00387"></a>00387 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& dEQdsig = d.<a class="code" href="group__ExprPkg.html#gae281b04465cc1bf24b5797c8b5e9cbb4">getSig</a>();
<a name="l00388"></a>00388 <span class="keywordflow">if</span> (!dEQdsig.<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>()) {
<a name="l00389"></a>00389 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& dsig = dEQdsig.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>();
<a name="l00390"></a>00390 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm = <a class="code" href="classCVC3_1_1Theory.html#ad6cb45844df7f1b08a53e41e40a362e3" title="Update the children of the term e.">updateHelper</a>(d);
<a name="l00391"></a>00391 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& sigNew = thm.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>();
<a name="l00392"></a>00392 <span class="keywordflow">if</span> (sigNew == dsig) <span class="keywordflow">return</span>;
<a name="l00393"></a>00393 dsig.<a class="code" href="group__ExprPkg.html#ga7b85677789c5a03e1a5dc2c93f0b6288">setRep</a>(<a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>());
<a name="l00394"></a>00394 <span class="keywordflow">if</span> (<a class="code" href="namespaceCVC3.html#afdcf0b93fc0d1b03a5a14c4988443c7a">isSelector</a>(sigNew) && <a class="code" href="classCVC3_1_1TheoryDatatype.html#a513d221b48500cf4bc91393293d9b2f2">canCollapse</a>(sigNew)) {
<a name="l00395"></a>00395 d.<a class="code" href="group__ExprPkg.html#gaaaba7ddaccd58bd37e3259fe9b949645">setSig</a>(<a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>());
<a name="l00396"></a>00396 <a class="code" href="classCVC3_1_1Theory.html#a93856c9af82b2c25c51b3c36bafb71f4" title="Submit a derived fact to the core from a decision procedure.">enqueueFact</a>(<a class="code" href="classCVC3_1_1Theory.html#a76f6507116e36f46dab074781fb9bf2d" title="(a1 == a2) & (a2 == a3) ==> (a1 == a3)">transitivityRule</a>(thm, <a class="code" href="classCVC3_1_1TheoryDatatype.html#abcd88b0572b5751bddccd9210939f5d0">d_rules</a>-><a class="code" href="classCVC3_1_1DatatypeProofRules.html#a8ecc9e0e858ab2da52632df61ee8a44e">rewriteSelCons</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a64a98802daa8a6a7c4f683b60740961f">d_facts</a>, sigNew)));
<a name="l00397"></a>00397 }
<a name="l00398"></a>00398 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (<a class="code" href="namespaceCVC3.html#a8297278831bf83882f7c6a1e3c84fa98">isTester</a>(sigNew) && <a class="code" href="namespaceCVC3.html#a91840d293c43120244ce5b5165bdacc4">isConstructor</a>(sigNew[0])) {
<a name="l00399"></a>00399 d.<a class="code" href="group__ExprPkg.html#gaaaba7ddaccd58bd37e3259fe9b949645">setSig</a>(<a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>());
<a name="l00400"></a>00400 <a class="code" href="classCVC3_1_1Theory.html#a93856c9af82b2c25c51b3c36bafb71f4" title="Submit a derived fact to the core from a decision procedure.">enqueueFact</a>(<a class="code" href="classCVC3_1_1Theory.html#a76f6507116e36f46dab074781fb9bf2d" title="(a1 == a2) & (a2 == a3) ==> (a1 == a3)">transitivityRule</a>(thm, <a class="code" href="classCVC3_1_1TheoryDatatype.html#abcd88b0572b5751bddccd9210939f5d0">d_rules</a>-><a class="code" href="classCVC3_1_1DatatypeProofRules.html#ad6df2a8a8c661ed1a1be34ce66910a36">rewriteTestCons</a>(sigNew)));
<a name="l00401"></a>00401 }
<a name="l00402"></a>00402 <span class="keywordflow">else</span> {
<a name="l00403"></a>00403 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& repEQsigNew = sigNew.<a class="code" href="group__ExprPkg.html#gaa4b5652980861e593ab8a741b5521779">getRep</a>();
<a name="l00404"></a>00404 <span class="keywordflow">if</span> (!repEQsigNew.<a class="code" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>()) {
<a name="l00405"></a>00405 d.<a class="code" href="group__ExprPkg.html#gaaaba7ddaccd58bd37e3259fe9b949645">setSig</a>(<a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>());
<a name="l00406"></a>00406 <a class="code" href="classCVC3_1_1Theory.html#a93856c9af82b2c25c51b3c36bafb71f4" title="Submit a derived fact to the core from a decision procedure.">enqueueFact</a>(<a class="code" href="classCVC3_1_1Theory.html#a76f6507116e36f46dab074781fb9bf2d" title="(a1 == a2) & (a2 == a3) ==> (a1 == a3)">transitivityRule</a>(repEQsigNew, <a class="code" href="classCVC3_1_1Theory.html#a7440711981ac1bba2bed7476c0fa4e0b" title="a1 == a2 ==> a2 == a1">symmetryRule</a>(thm)));
<a name="l00407"></a>00407 }
<a name="l00408"></a>00408 <span class="keywordflow">else</span> {
<a name="l00409"></a>00409 <span class="keywordtype">int</span> k, ar(d.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>());
<a name="l00410"></a>00410 <span class="keywordflow">for</span> (k = 0; k < ar; ++k) {
<a name="l00411"></a>00411 <span class="keywordflow">if</span> (sigNew[k] != dsig[k]) {
<a name="l00412"></a>00412 sigNew[k].<a class="code" href="group__ExprPkg.html#ga159d60cb0f32e09df89a395b2680664a" title="Add (e,i) to the notify list of this expression.">addToNotify</a>(<span class="keyword">this</span>, d);
<a name="l00413"></a>00413 }
<a name="l00414"></a>00414 }
<a name="l00415"></a>00415 d.<a class="code" href="group__ExprPkg.html#gaaaba7ddaccd58bd37e3259fe9b949645">setSig</a>(thm);
<a name="l00416"></a>00416 sigNew.<a class="code" href="group__ExprPkg.html#ga7b85677789c5a03e1a5dc2c93f0b6288">setRep</a>(thm);
<a name="l00417"></a>00417 <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()-><a class="code" href="group__EM__Priv.html#gaba358e1731ad9309e52e64eb9ce60755" title="Invalidate the simplifier's cache tag.">invalidateSimpCache</a>();
<a name="l00418"></a>00418 }
<a name="l00419"></a>00419 }
<a name="l00420"></a>00420 }
<a name="l00421"></a>00421 }
<a name="l00422"></a>00422 }
<a name="l00423"></a>00423
<a name="l00424"></a>00424
<a name="l00425"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#ab5f431756db284b50c011774862f9f16">00425</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryDatatype.html#ab5f431756db284b50c011774862f9f16" title="An optional solver.">TheoryDatatype::solve</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e)
<a name="l00426"></a>00426 {
<a name="l00427"></a>00427 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e.<a class="code" href="classCVC3_1_1Theorem.html#a362c1d70e03803d804bbe300e5f6dc87">isRewrite</a>() && e.<a class="code" href="classCVC3_1_1Theorem.html#a206c04f39fbbcacef2337148675553f4">getLHS</a>().<a class="code" href="group__ExprPkg.html#gad527acb49daef3591b78c748746e7eef" title="Test if e is a term (as opposed to a predicate/formula)">isTerm</a>(), <span class="stringliteral">"Expected equality"</span>);
<a name="l00428"></a>00428 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& lhs = e.<a class="code" href="classCVC3_1_1Theorem.html#a206c04f39fbbcacef2337148675553f4">getLHS</a>();
<a name="l00429"></a>00429 <span class="keywordflow">if</span> (<a class="code" href="namespaceCVC3.html#a91840d293c43120244ce5b5165bdacc4">isConstructor</a>(lhs) && !<a class="code" href="namespaceCVC3.html#a91840d293c43120244ce5b5165bdacc4">isConstructor</a>(e.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>())) {
<a name="l00430"></a>00430 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theory.html#a7440711981ac1bba2bed7476c0fa4e0b" title="a1 == a2 ==> a2 == a1">symmetryRule</a>(e);
<a name="l00431"></a>00431 }
<a name="l00432"></a>00432 <span class="keywordflow">return</span> e;
<a name="l00433"></a>00433 }
<a name="l00434"></a>00434
<a name="l00435"></a>00435
<a name="l00436"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#acf535107486ee65ec245d080c48c277f">00436</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#acf535107486ee65ec245d080c48c277f" title="Check that e is a valid Type expr.">TheoryDatatype::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="l00437"></a>00437 {
<a name="l00438"></a>00438 <span class="keywordflow">switch</span> (e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()) {
<a name="l00439"></a>00439 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ad94b8e65b0abc98bb6b5729da9e3b40a">DATATYPE</a>: {
<a name="l00440"></a>00440 <span class="keywordflow">if</span> (e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() != 1 || !e[0].<a class="code" href="group__ExprPkg.html#ga72034a21a6bcbd4d5d2085aa23c8f290">isString</a>())
<a name="l00441"></a>00441 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1Exception.html">Exception</a>(<span class="stringliteral">"Ill-formed datatype"</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00442"></a>00442 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1Theory.html#a07b326cd94b2bb8bafa39faf07caaec5" title="Resolve an identifier, for use in parseExprOp()">resolveID</a>(e[0].getString()) != e)
<a name="l00443"></a>00443 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1Exception.html">Exception</a>(<span class="stringliteral">"Unknown datatype"</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00444"></a>00444 <span class="keywordflow">break</span>;
<a name="l00445"></a>00445 }
<a name="l00446"></a>00446 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ae3aa1eb89fb69c62d502b57c020ed789">CONSTRUCTOR</a>:
<a name="l00447"></a>00447 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ac909f916e89d861b4a4e5eba782c5259">SELECTOR</a>:
<a name="l00448"></a>00448 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089a4df0e72bf250adc8dd78e81fea2f281c">TESTER</a>:
<a name="l00449"></a>00449 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1Exception.html">Exception</a>(<span class="stringliteral">"Non-type: "</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00450"></a>00450 <span class="keywordflow">default</span>:
<a name="l00451"></a>00451 <a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"Unexpected kind in TheoryDatatype::checkType"</span>
<a name="l00452"></a>00452 +<a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()->getKindName(e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()));
<a name="l00453"></a>00453 }
<a name="l00454"></a>00454 }
<a name="l00455"></a>00455
<a name="l00456"></a>00456
<a name="l00457"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#ad370efc075c3da6b8b081020cd56a55e">00457</a> <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.">TheoryDatatype::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="l00458"></a>00458 <span class="keywordtype">bool</span> enumerate, <span class="keywordtype">bool</span> computeSize)
<a name="l00459"></a>00459 {
<a name="l00460"></a>00460 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ad94b8e65b0abc98bb6b5729da9e3b40a">DATATYPE</a>,
<a name="l00461"></a>00461 <span class="stringliteral">"Unexpected kind in TheoryDatatype::finiteTypeInfo"</span>);
<a name="l00462"></a>00462 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoryDatatype.html#ae5ebfda4bb10cae8a4a3c620731bfb51">d_getConstantStack</a>.<a class="code" href="classCVC3_1_1ExprMap.html#aa96dfa3a54a131cdb0964ef4b80e324f">count</a>(e) != 0) {
<a name="l00463"></a>00463 <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54ad4a45eb68b0ebb32f0c805f6d2abf6d6">CARD_INFINITE</a>;
<a name="l00464"></a>00464 }
<a name="l00465"></a>00465 <a class="code" href="classCVC3_1_1TheoryDatatype.html#ae5ebfda4bb10cae8a4a3c620731bfb51">d_getConstantStack</a>[e] = <span class="keyword">true</span>;
<a name="l00466"></a>00466
<a name="l00467"></a>00467 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> typeExpr = e;
<a name="l00468"></a>00468 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<unsigned></a>& c = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>[typeExpr];
<a name="l00469"></a>00469 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<unsigned>::iterator</a> c_it = c.<a class="code" href="classCVC3_1_1ExprMap.html#a3db85401f8535daf4054fde531cd46b1">begin</a>(), c_end = c.<a class="code" href="classCVC3_1_1ExprMap.html#a283ae6c44308cbdda0d82da5a16e52c8">end</a>();
<a name="l00470"></a>00470 <a class="code" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54" title="Enum for cardinality of types.">Cardinality</a> card = <a class="code" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54ac1ba3119b0fd85d3e54c69601ec1ccca">CARD_FINITE</a>, cardTmp;
<a name="l00471"></a>00471 <span class="keywordtype">bool</span> getSize = enumerate || computeSize;
<a name="l00472"></a>00472 <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a> totalSize = 0, thisSize, size;
<a name="l00473"></a>00473 vector<Unsigned> sizes;
<a name="l00474"></a>00474 <span class="keywordtype">int</span> j;
<a name="l00475"></a>00475
<a name="l00476"></a>00476 <span class="comment">// Loop through constructors, and check if each one only has a finite number</span>
<a name="l00477"></a>00477 <span class="comment">// of possibilities</span>
<a name="l00478"></a>00478 <span class="keywordflow">for</span> (; c_it != c_end; ++c_it) {
<a name="l00479"></a>00479 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& cons = (*c_it).first;
<a name="l00480"></a>00480 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> funType = cons.<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#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>();
<a name="l00481"></a>00481 thisSize = 1;
<a name="l00482"></a>00482 <span class="keywordflow">for</span> (j = 0; j < funType.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-1; ++j) {
<a name="l00483"></a>00483 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e2 = funType[j];
<a name="l00484"></a>00484 cardTmp = <a class="code" href="classCVC3_1_1Theory.html#a01fa8047ed1f649dc98831cb536187e4" title="Return the theory associated with a kind.">theoryOf</a>(e2)-><a class="code" href="group__Theory__API.html#ga166b2a0c7ec3b09e079c2f84bb6087bc" title="Compute information related to finiteness of types.">finiteTypeInfo</a>(e2, size, <span class="keyword">false</span>, getSize);
<a name="l00485"></a>00485 <span class="keywordflow">if</span> (cardTmp == <a class="code" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54ad4a45eb68b0ebb32f0c805f6d2abf6d6">CARD_INFINITE</a>) {
<a name="l00486"></a>00486 card = <a class="code" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54ad4a45eb68b0ebb32f0c805f6d2abf6d6">CARD_INFINITE</a>;
<a name="l00487"></a>00487 <span class="keywordflow">break</span>;
<a name="l00488"></a>00488 }
<a name="l00489"></a>00489 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (cardTmp == <a class="code" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54a61454dbfa122fc961909dfd151695807">CARD_UNKNOWN</a>) {
<a name="l00490"></a>00490 card = <a class="code" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54a61454dbfa122fc961909dfd151695807">CARD_UNKNOWN</a>;
<a name="l00491"></a>00491 getSize = <span class="keyword">false</span>;
<a name="l00492"></a>00492 <span class="comment">// Keep looking to see if we can determine it is infinite</span>
<a name="l00493"></a>00493 }
<a name="l00494"></a>00494 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (getSize) {
<a name="l00495"></a>00495 thisSize = thisSize * size;
<a name="l00496"></a>00496 <span class="comment">// Give up if it gets too big</span>
<a name="l00497"></a>00497 <span class="keywordflow">if</span> (thisSize > 1000000) thisSize = 0;
<a name="l00498"></a>00498 <span class="keywordflow">if</span> (thisSize == 0) {
<a name="l00499"></a>00499 totalSize = 0;
<a name="l00500"></a>00500 getSize = <span class="keyword">false</span>;
<a name="l00501"></a>00501 }
<a name="l00502"></a>00502 }
<a name="l00503"></a>00503 }
<a name="l00504"></a>00504 <span class="keywordflow">if</span> (card == <a class="code" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54ad4a45eb68b0ebb32f0c805f6d2abf6d6">CARD_INFINITE</a>) <span class="keywordflow">break</span>;
<a name="l00505"></a>00505 <span class="keywordflow">if</span> (getSize) {
<a name="l00506"></a>00506 sizes.push_back(thisSize);
<a name="l00507"></a>00507 totalSize = totalSize + thisSize;
<a name="l00508"></a>00508 }
<a name="l00509"></a>00509 }
<a name="l00510"></a>00510
<a name="l00511"></a>00511 <span class="keywordflow">if</span> (card == <a class="code" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54ac1ba3119b0fd85d3e54c69601ec1ccca">CARD_FINITE</a>) {
<a name="l00512"></a>00512
<a name="l00513"></a>00513 <span class="keywordflow">if</span> (enumerate) {
<a name="l00514"></a>00514 c_it = c.<a class="code" href="classCVC3_1_1ExprMap.html#a3db85401f8535daf4054fde531cd46b1">begin</a>();
<a name="l00515"></a>00515 <span class="keywordtype">unsigned</span> i = 0;
<a name="l00516"></a>00516 <span class="keywordflow">for</span> (; i < sizes.size(); ++i, ++c_it) {
<a name="l00517"></a>00517 <span class="keywordflow">if</span> (n < sizes[i]) {
<a name="l00518"></a>00518 <span class="keywordflow">break</span>;
<a name="l00519"></a>00519 }
<a name="l00520"></a>00520 <span class="keywordflow">else</span> n = n - sizes[i];
<a name="l00521"></a>00521 }
<a name="l00522"></a>00522 <span class="keywordflow">if</span> (i == sizes.size() && n != 0) {
<a name="l00523"></a>00523 e = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>();
<a name="l00524"></a>00524 }
<a name="l00525"></a>00525 <span class="keywordflow">else</span> {
<a name="l00526"></a>00526 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& cons = (*c_it).first;
<a name="l00527"></a>00527 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> funType = cons.<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#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>();
<a name="l00528"></a>00528 <span class="keywordflow">if</span> (funType.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() == 1) {
<a name="l00529"></a>00529 e = cons;
<a name="l00530"></a>00530 }
<a name="l00531"></a>00531 <span class="keywordflow">else</span> {
<a name="l00532"></a>00532 vector<Expr> kids(funType.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-1);
<a name="l00533"></a>00533 <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a> thisSize;
<a name="l00534"></a>00534 <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a> elem;
<a name="l00535"></a>00535 <span class="keywordflow">for</span> (<span class="keywordtype">int</span> j = funType.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-2; j >= 0; --j) {
<a name="l00536"></a>00536 <span class="keywordflow">if</span> (n == 0) {
<a name="l00537"></a>00537 elem = 0;
<a name="l00538"></a>00538 }
<a name="l00539"></a>00539 <span class="keywordflow">else</span> {
<a name="l00540"></a>00540 thisSize = funType[j].<a class="code" href="group__ExprPkg.html#gaefc32b444057849c6364e63b7d4c3cf3" title="Return size of a finite type; returns 0 if size cannot be determined.">typeSizeFinite</a>();
<a name="l00541"></a>00541 elem = n % thisSize;
<a name="l00542"></a>00542 n = n - elem;
<a name="l00543"></a>00543 n = n / thisSize;
<a name="l00544"></a>00544 }
<a name="l00545"></a>00545 kids[j] = funType[j].<a class="code" href="group__ExprPkg.html#ga9abac5907964bb1ca7d6ad7d1280791c" title="Return nth (starting with 0) element in a finite type.">typeEnumerateFinite</a>(elem);
<a name="l00546"></a>00546 }
<a name="l00547"></a>00547 e = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(cons.<a class="code" href="group__ExprPkg.html#ga3aefe2fb15c2d8e3a51dd92dbcc5cdc5" title="Make the expr into an operator.">mkOp</a>(), kids);
<a name="l00548"></a>00548 }
<a name="l00549"></a>00549 }
<a name="l00550"></a>00550 }
<a name="l00551"></a>00551
<a name="l00552"></a>00552 <span class="keywordflow">if</span> (computeSize) {
<a name="l00553"></a>00553 n = totalSize;
<a name="l00554"></a>00554 }
<a name="l00555"></a>00555
<a name="l00556"></a>00556 }
<a name="l00557"></a>00557 <a class="code" href="classCVC3_1_1TheoryDatatype.html#ae5ebfda4bb10cae8a4a3c620731bfb51">d_getConstantStack</a>.<a class="code" href="classCVC3_1_1ExprMap.html#a2997aa3f20d09f6bf49b09da9a177003">erase</a>(typeExpr);
<a name="l00558"></a>00558 <span class="keywordflow">return</span> card;
<a name="l00559"></a>00559 }
<a name="l00560"></a>00560
<a name="l00561"></a>00561
<a name="l00562"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#af1237546f5860ded939958b0c31c6669">00562</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#af1237546f5860ded939958b0c31c6669" title="Compute and store the type of e.">TheoryDatatype::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="l00563"></a>00563 {
<a name="l00564"></a>00564 <span class="keywordflow">switch</span> (e.<a class="code" href="group__ExprPkg.html#gad036a3a3597d590ca6ee694505c6e1cd" title="Get kind of operator (for APPLY Exprs only)">getOpKind</a>()) {
<a name="l00565"></a>00565 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ae3aa1eb89fb69c62d502b57c020ed789">CONSTRUCTOR</a>:
<a name="l00566"></a>00566 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ac909f916e89d861b4a4e5eba782c5259">SELECTOR</a>:
<a name="l00567"></a>00567 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089a4df0e72bf250adc8dd78e81fea2f281c">TESTER</a>: {
<a name="l00568"></a>00568 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e.<a class="code" href="group__ExprPkg.html#ga1d6a6b4a9ce81b0dd8fd74870ff4284b">isApply</a>(), <span class="stringliteral">"Expected application"</span>);
<a name="l00569"></a>00569 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> op = e.<a class="code" href="group__ExprPkg.html#gace479f04faca399219496195152f7806" title="Get operator from expression.">getOp</a>().<a class="code" href="classCVC3_1_1Op.html#a4a38071541d1e863583f12e9d81de3a2">getExpr</a>();
<a name="l00570"></a>00570 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> t = op.lookupType();
<a name="l00571"></a>00571 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!t.<a class="code" href="classCVC3_1_1Type.html#ab5fe00c99ee91f369e3339b26bab0bf7">isNull</a>(), <span class="stringliteral">"Expected operator to be well-typed"</span>);
<a name="l00572"></a>00572 <span class="keywordflow">if</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="l00573"></a>00573 <span class="keywordflow">if</span> (e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() != 0)
<a name="l00574"></a>00574 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>(<span class="stringliteral">"Expected no children: "</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00575"></a>00575 e.<a class="code" href="group__ExprPkg.html#ga07d47f902598e00097086deabf04d9c5" title="Set the cached type.">setType</a>(t);
<a name="l00576"></a>00576 <span class="keywordflow">break</span>;
<a name="l00577"></a>00577 }
<a name="l00578"></a>00578 <span class="keywordflow">else</span> {
<a name="l00579"></a>00579 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(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="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba546eccfedc4dcc8623ed0668f77ef982">ARROW</a>, <span class="stringliteral">"Expected function type"</span>);
<a name="l00580"></a>00580 <span class="keywordflow">if</span> (e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() != t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>().<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-1)
<a name="l00581"></a>00581 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>(<span class="stringliteral">"Wrong number of children:\n"</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00582"></a>00582 <a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> i = e.<a class="code" href="group__ExprPkg.html#gac890e13db184610276fc533fa4b4fe99" title="Begin iterator.">begin</a>(), iend = e.<a class="code" href="group__ExprPkg.html#gaf6048a5030c8fa2511bf5dfee868e653" title="End iterator.">end</a>();
<a name="l00583"></a>00583 <a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> j = t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>().<a class="code" href="group__ExprPkg.html#gac890e13db184610276fc533fa4b4fe99" title="Begin iterator.">begin</a>();
<a name="l00584"></a>00584 <span class="keywordflow">for</span> (; i != iend; ++i, ++j) {
<a name="l00585"></a>00585 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(*i) != <a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(<a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>(*j))) {
<a name="l00586"></a>00586 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>(<span class="stringliteral">"Type mismatch for expression:\n\n "</span>
<a name="l00587"></a>00587 + (*i).toString()
<a name="l00588"></a>00588 + <span class="stringliteral">"\n\nhas the following type:\n\n "</span>
<a name="l00589"></a>00589 + (*i).getType().getExpr().toString()
<a name="l00590"></a>00590 + <span class="stringliteral">"\n\nbut the expected type is:\n\n "</span>
<a name="l00591"></a>00591 + (*j).toString()
<a name="l00592"></a>00592 + <span class="stringliteral">"\n\nin datatype function application:\n\n "</span>
<a name="l00593"></a>00593 + e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00594"></a>00594 }
<a name="l00595"></a>00595 }
<a name="l00596"></a>00596 e.<a class="code" href="group__ExprPkg.html#ga07d47f902598e00097086deabf04d9c5" title="Set the cached type.">setType</a>(*j);
<a name="l00597"></a>00597 }
<a name="l00598"></a>00598 <span class="keywordflow">break</span>;
<a name="l00599"></a>00599 }
<a name="l00600"></a>00600 <span class="keywordflow">default</span>:
<a name="l00601"></a>00601 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"Unexpected kind in datatype::computeType: "</span>
<a name="l00602"></a>00602 +e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00603"></a>00603 }
<a name="l00604"></a>00604 }
<a name="l00605"></a>00605
<a name="l00606"></a>00606
<a name="l00607"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a8fa2a50fe50ccfda4b557783f566dbfc">00607</a> <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.">TheoryDatatype::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="l00608"></a>00608 }
<a name="l00609"></a>00609
<a name="l00610"></a>00610
<a name="l00611"></a>00611
<a name="l00612"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#ae50ed74ea28aae7d5919a3461302a83e">00612</a> <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.">TheoryDatatype::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="l00613"></a>00613 {
<a name="l00614"></a>00614 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> tcc(<a class="code" href="group__Theory__API.html#ga9278ad3a6eb8351865a71acd7bb7f968" title="Compute and cache the TCC of e.">Theory::computeTCC</a>(e));
<a name="l00615"></a>00615 <span class="keywordflow">switch</span> (e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()) {
<a name="l00616"></a>00616 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ae3aa1eb89fb69c62d502b57c020ed789">CONSTRUCTOR</a>:
<a name="l00617"></a>00617 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() == 0, <span class="stringliteral">"Expected leaf constructor"</span>);
<a name="l00618"></a>00618 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theory.html#ab8835beee96db67f3c26a604d96f2fe8" title="Return TRUE Expr.">trueExpr</a>();
<a name="l00619"></a>00619 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5c41450c4e719ca40d8e734f6a2008f0">APPLY</a>: {
<a name="l00620"></a>00620 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e.<a class="code" href="group__ExprPkg.html#ga1d6a6b4a9ce81b0dd8fd74870ff4284b">isApply</a>(), <span class="stringliteral">"Should be application"</span>);
<a name="l00621"></a>00621 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> op(e.<a class="code" href="group__ExprPkg.html#ga9f3328fe077191803a780cfd6566ff9b" title="Get expression of operator (for APPLY Exprs only)">getOpExpr</a>());
<a name="l00622"></a>00622 <span class="keywordflow">if</span> (op.getKind() != <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ac909f916e89d861b4a4e5eba782c5259">SELECTOR</a>) <span class="keywordflow">return</span> tcc;
<a name="l00623"></a>00623 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() == 1, <span class="stringliteral">"Expected single argument"</span>);
<a name="l00624"></a>00624 <span class="keyword">const</span> std::pair<Expr,unsigned>& p = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a5ae1a2fe60c6e2af77cf098340cabd53">getSelectorInfo</a>(op);
<a name="l00625"></a>00625 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> tester = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a51372d26e89b189c8a5f42d18dd2eedc">datatypeTestExpr</a>(p.first.getName(), e[0]);
<a name="l00626"></a>00626 <span class="keywordflow">return</span> tcc.<a class="code" href="group__ExprPkg.html#ga6c3651465ce69ed5f4e6fd461b9acf3c">andExpr</a>(tester);
<a name="l00627"></a>00627 }
<a name="l00628"></a>00628 <span class="keywordflow">default</span>:
<a name="l00629"></a>00629 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>,<span class="stringliteral">"Unexpected type: "</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00630"></a>00630 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theory.html#ab8835beee96db67f3c26a604d96f2fe8" title="Return TRUE Expr.">trueExpr</a>();
<a name="l00631"></a>00631 }
<a name="l00632"></a>00632 }
<a name="l00633"></a>00633 <span class="comment"></span>
<a name="l00634"></a>00634 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00635"></a>00635 <span class="comment"></span><span class="comment">// Pretty-printing //</span><span class="comment"></span>
<a name="l00636"></a>00636 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00637"></a>00637 <span class="comment"></span>
<a name="l00638"></a>00638
<a name="l00639"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a1d17495677079120272ec4073cd777db">00639</a> <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.">TheoryDatatype::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="l00640"></a>00640 <span class="keywordflow">switch</span> (os.<a class="code" href="classCVC3_1_1ExprStream.html#ac2b2872228aff3fd5d08bbd69c672543" title="Get the current output language.">lang</a>()) {
<a name="l00641"></a>00641 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0eaa315c228d5c3290ce37df81524ed8e9a" title="Nice SAL-like language for manually written specs.">PRESENTATION_LANG</a>:
<a name="l00642"></a>00642 <span class="keywordflow">switch</span> (e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()) {
<a name="l00643"></a>00643 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089a5cc02a3e0fe70ce33e5c3d450b38136c">DATATYPE_DECL</a>: {
<a name="l00644"></a>00644 os << <span class="stringliteral">"DATATYPE"</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00645"></a>00645 <span class="keywordtype">bool</span> first(<span class="keyword">true</span>);
<a name="l00646"></a>00646 <span class="keywordflow">for</span> (<a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> i = e.<a class="code" href="group__ExprPkg.html#gac890e13db184610276fc533fa4b4fe99" title="Begin iterator.">begin</a>(), iend = e.<a class="code" href="group__ExprPkg.html#gaf6048a5030c8fa2511bf5dfee868e653" title="End iterator.">end</a>(); i != iend; ++i) {
<a name="l00647"></a>00647 <span class="keywordflow">if</span> (first) first = <span class="keyword">false</span>;
<a name="l00648"></a>00648 <span class="keywordflow">else</span> os << <span class="stringliteral">","</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00649"></a>00649 os << <span class="stringliteral">" "</span> << <a class="code" href="group__ExprStream__Manip.html#ga2a0348c6d3f94f2f8febc6dd0a9c3218" title="Set the indentation to the current position.">push</a> << *i << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a> << <span class="stringliteral">"= "</span> << <a class="code" href="group__ExprStream__Manip.html#ga2a0348c6d3f94f2f8febc6dd0a9c3218" title="Set the indentation to the current position.">push</a>;
<a name="l00650"></a>00650 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>.<a class="code" href="classCVC3_1_1ExprMap.html#ae50ab1874dd63b575553e7db769abe28">find</a>(*i) != <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>.<a class="code" href="classCVC3_1_1ExprMap.html#a283ae6c44308cbdda0d82da5a16e52c8">end</a>(),
<a name="l00651"></a>00651 <span class="stringliteral">"Unknown datatype: "</span>+(*i).toString());
<a name="l00652"></a>00652 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<unsigned></a>& c = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>[*i];
<a name="l00653"></a>00653 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<unsigned>::iterator</a> c_it = c.<a class="code" href="classCVC3_1_1ExprMap.html#a3db85401f8535daf4054fde531cd46b1">begin</a>(), c_end = c.end();
<a name="l00654"></a>00654 <span class="keywordtype">bool</span> firstCons(<span class="keyword">true</span>);
<a name="l00655"></a>00655 <span class="keywordflow">for</span> (; c_it != c_end; ++c_it) {
<a name="l00656"></a>00656 <span class="keywordflow">if</span> (!firstCons) {
<a name="l00657"></a>00657 os << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a> << <span class="stringliteral">"| "</span>;
<a name="l00658"></a>00658 }
<a name="l00659"></a>00659 <span class="keywordflow">else</span> firstCons = <span class="keyword">false</span>;
<a name="l00660"></a>00660 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& cons = (*c_it).first;
<a name="l00661"></a>00661 os << cons;
<a name="l00662"></a>00662 vector<Expr>& sels = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a1e8e2818f2f0dcf45743b42b3d9778b3">d_constructorMap</a>[cons];
<a name="l00663"></a>00663 <span class="keywordtype">bool</span> firstSel(<span class="keyword">true</span>);
<a name="l00664"></a>00664 <span class="keywordflow">for</span> (<span class="keywordtype">unsigned</span> j = 0; j < sels.size(); ++j) {
<a name="l00665"></a>00665 <span class="keywordflow">if</span> (firstSel) {
<a name="l00666"></a>00666 firstSel = <span class="keyword">false</span>;
<a name="l00667"></a>00667 os << <span class="stringliteral">"("</span>;
<a name="l00668"></a>00668 } <span class="keywordflow">else</span> {
<a name="l00669"></a>00669 os << <span class="stringliteral">", "</span>;
<a name="l00670"></a>00670 }
<a name="l00671"></a>00671 os << sels[j] << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a> << <span class="stringliteral">": "</span>;
<a name="l00672"></a>00672 os << sels[j].getType().getExpr()[1];
<a name="l00673"></a>00673 }
<a name="l00674"></a>00674 <span class="keywordflow">if</span> (!firstSel) {
<a name="l00675"></a>00675 os << <span class="stringliteral">")"</span>;
<a name="l00676"></a>00676 }
<a name="l00677"></a>00677 }
<a name="l00678"></a>00678 os << <a class="code" href="group__ExprStream__Manip.html#gaddb050a787be87116afc51791293d3be" title="Restore the indentation.">pop</a>;
<a name="l00679"></a>00679 }
<a name="l00680"></a>00680 os << <a class="code" href="group__ExprStream__Manip.html#gaddb050a787be87116afc51791293d3be" title="Restore the indentation.">pop</a> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00681"></a>00681 os << <span class="stringliteral">"END;"</span>;
<a name="l00682"></a>00682 <span class="keywordflow">break</span>;
<a name="l00683"></a>00683 }
<a name="l00684"></a>00684 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ad94b8e65b0abc98bb6b5729da9e3b40a">DATATYPE</a>:
<a name="l00685"></a>00685 <span class="keywordflow">if</span> (e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() == 1 && e[0].<a class="code" href="group__ExprPkg.html#ga72034a21a6bcbd4d5d2085aa23c8f290">isString</a>()) {
<a name="l00686"></a>00686 os << e[0].<a class="code" href="group__ExprPkg.html#ga5e679ab39ad8166c3c027afee9004c26">getString</a>();
<a name="l00687"></a>00687 }
<a name="l00688"></a>00688 <span class="keywordflow">else</span> e.<a class="code" href="group__ExprPkg.html#ga092308b0a88e12a5c7ff2fc0a2eca818" title="Print the top node and then recurse through the children */.">printAST</a>(os);
<a name="l00689"></a>00689 <span class="keywordflow">break</span>;
<a name="l00690"></a>00690 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba5c41450c4e719ca40d8e734f6a2008f0">APPLY</a>:
<a name="l00691"></a>00691 os << e.<a class="code" href="group__ExprPkg.html#ga9f3328fe077191803a780cfd6566ff9b" title="Get expression of operator (for APPLY Exprs only)">getOpExpr</a>();
<a name="l00692"></a>00692 <span class="keywordflow">if</span>(e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() > 0) {
<a name="l00693"></a>00693 os << <span class="stringliteral">"("</span> << <a class="code" href="group__ExprStream__Manip.html#ga2a0348c6d3f94f2f8febc6dd0a9c3218" title="Set the indentation to the current position.">push</a>;
<a name="l00694"></a>00694 <span class="keywordtype">bool</span> first(<span class="keyword">true</span>);
<a name="l00695"></a>00695 <span class="keywordflow">for</span> (<a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> i=e.<a class="code" href="group__ExprPkg.html#gac890e13db184610276fc533fa4b4fe99" title="Begin iterator.">begin</a>(), iend=e.<a class="code" href="group__ExprPkg.html#gaf6048a5030c8fa2511bf5dfee868e653" title="End iterator.">end</a>(); i!=iend; ++i) {
<a name="l00696"></a>00696 <span class="keywordflow">if</span>(first) first = <span class="keyword">false</span>;
<a name="l00697"></a>00697 <span class="keywordflow">else</span> os << <span class="stringliteral">","</span> << <a class="code" href="group__ExprStream__Manip.html#ga02670eb229648e9e2d888f21f91b6810" title="Insert a single white space separator.">space</a>;
<a name="l00698"></a>00698 os << *i;
<a name="l00699"></a>00699 }
<a name="l00700"></a>00700 os << push << <span class="stringliteral">")"</span>;
<a name="l00701"></a>00701 }
<a name="l00702"></a>00702 <span class="keywordflow">break</span>;
<a name="l00703"></a>00703 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ae3aa1eb89fb69c62d502b57c020ed789">CONSTRUCTOR</a>:
<a name="l00704"></a>00704 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ac909f916e89d861b4a4e5eba782c5259">SELECTOR</a>:
<a name="l00705"></a>00705 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089a4df0e72bf250adc8dd78e81fea2f281c">TESTER</a>:
<a name="l00706"></a>00706 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e.<a class="code" href="group__ExprPkg.html#ga93059bf6ddd8020cef4e6796a3c9b5a4">isSymbol</a>(), <span class="stringliteral">"Expected symbol"</span>);
<a name="l00707"></a>00707 os << e.<a class="code" href="group__ExprPkg.html#gaa3023d9117f249f079b0a202a1dfc5c2">getName</a>();
<a name="l00708"></a>00708 <span class="keywordflow">break</span>;
<a name="l00709"></a>00709 <span class="keywordflow">default</span>:
<a name="l00710"></a>00710 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"TheoryDatatype::print: Unexpected kind: "</span>
<a name="l00711"></a>00711 +<a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()->getKindName(e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()));
<a name="l00712"></a>00712 }
<a name="l00713"></a>00713 <span class="keywordflow">break</span>;
<a name="l00714"></a>00714 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0ea548619427a4d459d859ccd041ced9bfa" title="SMT-LIB format.">SMTLIB_LANG</a>:
<a name="l00715"></a>00715 <a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"Not Implemented Yet"</span>);
<a name="l00716"></a>00716 <span class="keywordflow">break</span>;
<a name="l00717"></a>00717 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0ea00df691ed79361b36910e60b49824c35" title="Lisp-like format for automatically generated specs.">LISP_LANG</a>:
<a name="l00718"></a>00718 <a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"Not Implemented Yet"</span>);
<a name="l00719"></a>00719 <span class="keywordflow">break</span>;
<a name="l00720"></a>00720 <span class="keywordflow">default</span>:
<a name="l00721"></a>00721 e.<a class="code" href="group__ExprPkg.html#ga092308b0a88e12a5c7ff2fc0a2eca818" title="Print the top node and then recurse through the children */.">printAST</a>(os);
<a name="l00722"></a>00722 <span class="keywordflow">break</span>;
<a name="l00723"></a>00723 }
<a name="l00724"></a>00724 <span class="keywordflow">return</span> os;
<a name="l00725"></a>00725 }
<a name="l00726"></a>00726 <span class="comment"></span>
<a name="l00727"></a>00727 <span class="comment">//////////////////////////////////////////////////////////////////////////////</span>
<a name="l00728"></a>00728 <span class="comment"></span><span class="comment">//parseExprOp:</span>
<a name="l00729"></a>00729 <span class="comment">//translating special Exprs to regular EXPR??</span><span class="comment"></span>
<a name="l00730"></a>00730 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00731"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a464a093b6247645cf10c1bb8aa9a03a4">00731</a> <span class="comment"></span><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.">TheoryDatatype::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="l00732"></a>00732 {
<a name="l00733"></a>00733 <span class="comment">// If the expression is not a list, it must have been already</span>
<a name="l00734"></a>00734 <span class="comment">// parsed, so just return it as is.</span>
<a name="l00735"></a>00735 <span class="keywordflow">if</span>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a> != e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()) <span class="keywordflow">return</span> e;
<a name="l00736"></a>00736
<a name="l00737"></a>00737 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() > 0,
<a name="l00738"></a>00738 <span class="stringliteral">"TheoryDatatype::parseExprOp:\n e = "</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00739"></a>00739
<a name="l00740"></a>00740 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e[0].getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba001479a58fb44c39a29b20d565081a68" title="Identifier is (ID (STRING_EXPR "name"))">ID</a>,
<a name="l00741"></a>00741 <span class="stringliteral">"Expected ID kind for first elem in list expr"</span>);
<a name="l00742"></a>00742
<a name="l00743"></a>00743 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& c1 = e[0][0];
<a name="l00744"></a>00744 <span class="keywordtype">int</span> kind = <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga9e7929fab9329724812e74b066a3c90a" title="Return a kind associated with a name. Returns NULL_KIND if not found.">getKind</a>(c1.<a class="code" href="group__ExprPkg.html#ga5e679ab39ad8166c3c027afee9004c26">getString</a>());
<a name="l00745"></a>00745 <span class="keywordflow">switch</span>(kind) {
<a name="l00746"></a>00746 <span class="keywordflow">case</span> <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ad94b8e65b0abc98bb6b5729da9e3b40a">DATATYPE</a>: {
<a name="l00747"></a>00747 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() > 1,
<a name="l00748"></a>00748 <span class="stringliteral">"Empty DATATYPE expression\n"</span>
<a name="l00749"></a>00749 <span class="stringliteral">" (expected at least one datatype): "</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00750"></a>00750
<a name="l00751"></a>00751 vector<Expr> names;
<a name="l00752"></a>00752
<a name="l00753"></a>00753 vector<Expr> allConstructorNames;
<a name="l00754"></a>00754 vector<Expr> constructorNames;
<a name="l00755"></a>00755
<a name="l00756"></a>00756 vector<Expr> allSelectorNames;
<a name="l00757"></a>00757 vector<Expr> selectorNames;
<a name="l00758"></a>00758 vector<Expr> selectorNamesKids;
<a name="l00759"></a>00759
<a name="l00760"></a>00760 vector<Expr> allTypes;
<a name="l00761"></a>00761 vector<Expr> types;
<a name="l00762"></a>00762 vector<Expr> typesKids;
<a name="l00763"></a>00763
<a name="l00764"></a>00764 <span class="keywordtype">int</span> i,j,k;
<a name="l00765"></a>00765 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> dt, constructor, selectors, selector;
<a name="l00766"></a>00766
<a name="l00767"></a>00767 <span class="comment">// Get names of datatypes</span>
<a name="l00768"></a>00768 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> namesMap;
<a name="l00769"></a>00769 <span class="keywordflow">for</span> (i = 0; i < e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-1; ++i) {
<a name="l00770"></a>00770 dt = e[i+1];
<a name="l00771"></a>00771 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(dt.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a> && dt.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() == 2,
<a name="l00772"></a>00772 <span class="stringliteral">"Bad formed datatype expression"</span>
<a name="l00773"></a>00773 +dt.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00774"></a>00774 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(dt[0].getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba001479a58fb44c39a29b20d565081a68" title="Identifier is (ID (STRING_EXPR "name"))">ID</a>,
<a name="l00775"></a>00775 <span class="stringliteral">"Expected ID kind for datatype name"</span>
<a name="l00776"></a>00776 +dt.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00777"></a>00777 names.push_back(dt[0][0]);
<a name="l00778"></a>00778 <span class="keywordflow">if</span> (namesMap.<a class="code" href="classCVC3_1_1ExprMap.html#aa96dfa3a54a131cdb0964ef4b80e324f">count</a>(dt[0][0]) != 0) {
<a name="l00779"></a>00779 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1ParserException.html">ParserException</a>(<span class="stringliteral">"Datatype name used more than once"</span>+dt[0][0].getString());
<a name="l00780"></a>00780 }
<a name="l00781"></a>00781 namesMap.<a class="code" href="classCVC3_1_1ExprMap.html#a89122ac9deffe3cd839d067b6b92af1d">insert</a>(dt[0][0], <span class="keyword">true</span>);
<a name="l00782"></a>00782 }
<a name="l00783"></a>00783
<a name="l00784"></a>00784 <span class="comment">// Loop through datatypes</span>
<a name="l00785"></a>00785 <span class="keywordflow">for</span> (i = 0; i < e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-1; ++i) {
<a name="l00786"></a>00786 dt = e[i+1];
<a name="l00787"></a>00787 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(dt[1].getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a> && dt[1].arity() > 0,
<a name="l00788"></a>00788 <span class="stringliteral">"Expected non-empty list for datatype constructors"</span>
<a name="l00789"></a>00789 +dt.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00790"></a>00790 dt = dt[1];
<a name="l00791"></a>00791
<a name="l00792"></a>00792 <span class="comment">// Loop through constructors for this datatype</span>
<a name="l00793"></a>00793 <span class="keywordflow">for</span>(j = 0; j < dt.arity(); ++j) {
<a name="l00794"></a>00794 constructor = dt[j];
<a name="l00795"></a>00795 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(constructor.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a> &&
<a name="l00796"></a>00796 (constructor.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() == 1 || constructor.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() == 2),
<a name="l00797"></a>00797 <span class="stringliteral">"Unexpected constructor"</span>+constructor.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00798"></a>00798 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(constructor[0].getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba001479a58fb44c39a29b20d565081a68" title="Identifier is (ID (STRING_EXPR "name"))">ID</a>,
<a name="l00799"></a>00799 <span class="stringliteral">"Expected ID kind for constructor name"</span>
<a name="l00800"></a>00800 +constructor.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00801"></a>00801 constructorNames.push_back(constructor[0][0]);
<a name="l00802"></a>00802
<a name="l00803"></a>00803 <span class="keywordflow">if</span> (constructor.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() == 2) {
<a name="l00804"></a>00804 selectors = constructor[1];
<a name="l00805"></a>00805 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(selectors.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a> && selectors.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() > 0,
<a name="l00806"></a>00806 <span class="stringliteral">"Non-empty list expected as second argument of constructor:\n"</span>
<a name="l00807"></a>00807 +constructor.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00808"></a>00808
<a name="l00809"></a>00809 <span class="comment">// Loop through selectors for this constructor</span>
<a name="l00810"></a>00810 <span class="keywordflow">for</span> (k = 0; k < selectors.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>(); ++k) {
<a name="l00811"></a>00811 selector = selectors[k];
<a name="l00812"></a>00812 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(selector.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a> && selector.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() == 2,
<a name="l00813"></a>00813 <span class="stringliteral">"Expected list of arity 2 for selector"</span>
<a name="l00814"></a>00814 +selector.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00815"></a>00815 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(selector[0].getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba001479a58fb44c39a29b20d565081a68" title="Identifier is (ID (STRING_EXPR "name"))">ID</a>,
<a name="l00816"></a>00816 <span class="stringliteral">"Expected ID kind for selector name"</span>
<a name="l00817"></a>00817 +selector.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00818"></a>00818 selectorNamesKids.push_back(selector[0][0]);
<a name="l00819"></a>00819 <span class="keywordflow">if</span> (selector[1].getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba001479a58fb44c39a29b20d565081a68" title="Identifier is (ID (STRING_EXPR "name"))">ID</a> && namesMap.<a class="code" href="classCVC3_1_1ExprMap.html#aa96dfa3a54a131cdb0964ef4b80e324f">count</a>(selector[1][0]) > 0) {
<a name="l00820"></a>00820 typesKids.push_back(selector[1][0]);
<a name="l00821"></a>00821 }
<a name="l00822"></a>00822 <span class="keywordflow">else</span> {
<a name="l00823"></a>00823 typesKids.push_back(<a class="code" href="classCVC3_1_1Theory.html#abd5a64ee867dda0c216a04e9fc7fbd6c" title="Parse the generic expression.">parseExpr</a>(selector[1]));
<a name="l00824"></a>00824 }
<a name="l00825"></a>00825 }
<a name="l00826"></a>00826 selectorNames.push_back(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a>, selectorNamesKids));
<a name="l00827"></a>00827 selectorNamesKids.clear();
<a name="l00828"></a>00828 types.push_back(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a>, typesKids));
<a name="l00829"></a>00829 typesKids.clear();
<a name="l00830"></a>00830 }
<a name="l00831"></a>00831 <span class="keywordflow">else</span> {
<a name="l00832"></a>00832 selectorNames.push_back(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a>, selectorNamesKids, <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()));
<a name="l00833"></a>00833 types.push_back(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a>, typesKids, <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()));
<a name="l00834"></a>00834 }
<a name="l00835"></a>00835 }
<a name="l00836"></a>00836 allConstructorNames.push_back(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a>, constructorNames));
<a name="l00837"></a>00837 constructorNames.clear();
<a name="l00838"></a>00838 allSelectorNames.push_back(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a>, selectorNames));
<a name="l00839"></a>00839 selectorNames.clear();
<a name="l00840"></a>00840 allTypes.push_back(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a>, types));
<a name="l00841"></a>00841 types.clear();
<a name="l00842"></a>00842 }
<a name="l00843"></a>00843
<a name="l00844"></a>00844 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ad94b8e65b0abc98bb6b5729da9e3b40a">DATATYPE</a>,
<a name="l00845"></a>00845 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a>, names),
<a name="l00846"></a>00846 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a>, allConstructorNames),
<a name="l00847"></a>00847 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a>, allSelectorNames),
<a name="l00848"></a>00848 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a>, allTypes));
<a name="l00849"></a>00849 }
<a name="l00850"></a>00850
<a name="l00851"></a>00851 <span class="keywordflow">default</span>: {
<a name="l00852"></a>00852 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1ParserException.html">ParserException</a>(<span class="stringliteral">"Unexpected datatype expression: "</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00853"></a>00853 }
<a name="l00854"></a>00854 }
<a name="l00855"></a>00855 <span class="keywordflow">return</span> e;
<a name="l00856"></a>00856 }
<a name="l00857"></a>00857
<a name="l00858"></a>00858
<a name="l00859"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#ab31831ed547432e2a83f74c83a82e982">00859</a> <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">TheoryDatatype::dataType</a>(<span class="keyword">const</span> <span class="keywordtype">string</span>& name,
<a name="l00860"></a>00860 <span class="keyword">const</span> vector<string>& constructors,
<a name="l00861"></a>00861 <span class="keyword">const</span> vector<vector<string> >& selectors,
<a name="l00862"></a>00862 <span class="keyword">const</span> vector<vector<Expr> >& types)
<a name="l00863"></a>00863 {
<a name="l00864"></a>00864 vector<string> names;
<a name="l00865"></a>00865 vector<vector<string> > constructors2;
<a name="l00866"></a>00866 vector<vector<vector<string> > > selectors2;
<a name="l00867"></a>00867 vector<vector<vector<Expr> > > types2;
<a name="l00868"></a>00868 names.push_back(name);
<a name="l00869"></a>00869 constructors2.push_back(constructors);
<a name="l00870"></a>00870 selectors2.push_back(selectors);
<a name="l00871"></a>00871 types2.push_back(types);
<a name="l00872"></a>00872 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#ab31831ed547432e2a83f74c83a82e982">dataType</a>(names, constructors2, selectors2, types2);
<a name="l00873"></a>00873 }
<a name="l00874"></a>00874
<a name="l00875"></a>00875
<a name="l00876"></a>00876 <span class="comment">// Elements of types are either the expr from an existing type or a string</span>
<a name="l00877"></a>00877 <span class="comment">// naming one of the datatypes being defined</span>
<a name="l00878"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#ae7305309a6b11b8f9733d93b161c07e0">00878</a> <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">TheoryDatatype::dataType</a>(<span class="keyword">const</span> vector<string>& names,
<a name="l00879"></a>00879 <span class="keyword">const</span> vector<vector<string> >& allConstructors,
<a name="l00880"></a>00880 <span class="keyword">const</span> vector<vector<vector<string> > >& allSelectors,
<a name="l00881"></a>00881 <span class="keyword">const</span> vector<vector<vector<Expr> > >& allTypes)
<a name="l00882"></a>00882 {
<a name="l00883"></a>00883 vector<Expr> returnTypes;
<a name="l00884"></a>00884
<a name="l00885"></a>00885 <span class="comment">// bool wellFounded = false, infinite = false, </span>
<a name="l00886"></a>00886 <span class="keywordtype">bool</span> thisWellFounded;
<a name="l00887"></a>00887
<a name="l00888"></a>00888 <span class="keywordflow">if</span> (names.size() != allConstructors.size() ||
<a name="l00889"></a>00889 allConstructors.size() != allSelectors.size() ||
<a name="l00890"></a>00890 allSelectors.size() != allTypes.size()) {
<a name="l00891"></a>00891 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>
<a name="l00892"></a>00892 (<span class="stringliteral">"dataType: vector sizes don't match"</span>);
<a name="l00893"></a>00893 }
<a name="l00894"></a>00894
<a name="l00895"></a>00895 <span class="keywordtype">unsigned</span> i, j, k;
<a name="l00896"></a>00896 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e;
<a name="l00897"></a>00897
<a name="l00898"></a>00898 <span class="comment">// Create reachability predicate for constructor cycle detection</span>
<a name="l00899"></a>00899 vector<Type> funTypeArgs;
<a name="l00900"></a>00900 funTypeArgs.push_back(<a class="code" href="classCVC3_1_1Type.html#ae3477d8de1425fc5f278a8fbc76e56a0">Type::anyType</a>(<a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()));
<a name="l00901"></a>00901 funTypeArgs.push_back(<a class="code" href="classCVC3_1_1Type.html#ae3477d8de1425fc5f278a8fbc76e56a0">Type::anyType</a>(<a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()));
<a name="l00902"></a>00902 <a class="code" href="classCVC3_1_1Op.html">Op</a> op = <a class="code" href="classCVC3_1_1Theory.html#a97642364c244b753d33b551fc8c3bb9a" title="Create a new uninterpreted function.">newFunction</a>(<span class="stringliteral">"_reach_"</span>+names[0],
<a name="l00903"></a>00903 <a class="code" href="classCVC3_1_1Type.html#a3ebf8a1ba9d894c33df064ea37c5ead5">Type::funType</a>(funTypeArgs, <a class="code" href="classCVC3_1_1Theory.html#a705d998884ec8a53c22220373472d868" title="Return BOOLEAN type.">boolType</a>()),
<a name="l00904"></a>00904 <span class="keyword">true</span> <span class="comment">/* compute trans closure */</span>);
<a name="l00905"></a>00905 <a class="code" href="classCVC3_1_1Op.html">Op</a> reach = <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()-><a class="code" href="group__EM__Priv.html#gafddb4551e9dbb163823b1162248e58f0">newSymbolExpr</a>(op.<a class="code" href="classCVC3_1_1Op.html#a4a38071541d1e863583f12e9d81de3a2">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaa3023d9117f249f079b0a202a1dfc5c2">getName</a>(),
<a name="l00906"></a>00906 <a class="code" href="namespaceCVC3.html#afaaef5e303e3d0aec4e1874b5ef2923aa5d779af6a0a27075487337bf4ec8e92a">TRANS_CLOSURE</a>).mkOp();
<a name="l00907"></a>00907
<a name="l00908"></a>00908 <span class="keywordflow">for</span> (i = 0; i < names.size(); ++i) {
<a name="l00909"></a>00909 e = <a class="code" href="classCVC3_1_1Theory.html#a07b326cd94b2bb8bafa39faf07caaec5" title="Resolve an identifier, for use in parseExprOp()">resolveID</a>(names[i]);
<a name="l00910"></a>00910 <span class="keywordflow">if</span> (!e.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>()) {
<a name="l00911"></a>00911 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>
<a name="l00912"></a>00912 (<span class="stringliteral">"Attempt to define datatype "</span>+names[i]+<span class="stringliteral">":\n "</span>
<a name="l00913"></a>00913 <span class="stringliteral">"This variable is already defined."</span>);
<a name="l00914"></a>00914 }
<a name="l00915"></a>00915 e = <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ad94b8e65b0abc98bb6b5729da9e3b40a">DATATYPE</a>, <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()->newStringExpr(names[i]));
<a name="l00916"></a>00916 <a class="code" href="classCVC3_1_1Theory.html#a6b1c155465b0c24885213e7442dd0882" title="Install name as a new identifier associated with Expr e.">installID</a>(names[i], e);
<a name="l00917"></a>00917 returnTypes.push_back(e);
<a name="l00918"></a>00918 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a7aab890b7ccd92b61dafb89bcf9adc65">d_reach</a>[e] = reach;
<a name="l00919"></a>00919 }
<a name="l00920"></a>00920
<a name="l00921"></a>00921 vector<Expr> selectorVec;
<a name="l00922"></a>00922
<a name="l00923"></a>00923 <span class="keywordflow">for</span> (i = 0; i < names.size(); ++i) {
<a name="l00924"></a>00924
<a name="l00925"></a>00925 <span class="keyword">const</span> vector<string>& constructors = allConstructors[i];
<a name="l00926"></a>00926 <span class="keyword">const</span> vector<vector<string> >& selectors = allSelectors[i];
<a name="l00927"></a>00927 <span class="keyword">const</span> vector<vector<Expr> >& types = allTypes[i];
<a name="l00928"></a>00928
<a name="l00929"></a>00929 <span class="keywordflow">if</span> (constructors.size() == 0) {
<a name="l00930"></a>00930 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>
<a name="l00931"></a>00931 (<span class="stringliteral">"datatype: "</span>+names[i]+<span class="stringliteral">": must have at least one constructor"</span>);
<a name="l00932"></a>00932 }
<a name="l00933"></a>00933 <span class="keywordflow">if</span> (constructors.size() != selectors.size() ||
<a name="l00934"></a>00934 selectors.size() != types.size()) {
<a name="l00935"></a>00935 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>
<a name="l00936"></a>00936 (<span class="stringliteral">"dataType: vector sizes at index "</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(i)+<span class="stringliteral">" don't match"</span>);
<a name="l00937"></a>00937 }
<a name="l00938"></a>00938
<a name="l00939"></a>00939 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<unsigned></a>& constMap = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>[returnTypes[i]];
<a name="l00940"></a>00940
<a name="l00941"></a>00941 <span class="keywordflow">for</span> (j = 0; j < constructors.size(); ++j) {
<a name="l00942"></a>00942 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> c = <a class="code" href="classCVC3_1_1Theory.html#a07b326cd94b2bb8bafa39faf07caaec5" title="Resolve an identifier, for use in parseExprOp()">resolveID</a>(constructors[j]);
<a name="l00943"></a>00943 <span class="keywordflow">if</span> (!c.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>()) {
<a name="l00944"></a>00944 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>
<a name="l00945"></a>00945 (<span class="stringliteral">"Attempt to define datatype constructor "</span>+constructors[j]+<span class="stringliteral">":\n "</span>
<a name="l00946"></a>00946 <span class="stringliteral">"This variable is already defined."</span>);
<a name="l00947"></a>00947 }
<a name="l00948"></a>00948 c = <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()-><a class="code" href="group__EM__Priv.html#gafddb4551e9dbb163823b1162248e58f0">newSymbolExpr</a>(constructors[j], <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ae3aa1eb89fb69c62d502b57c020ed789">CONSTRUCTOR</a>);
<a name="l00949"></a>00949
<a name="l00950"></a>00950 <span class="keywordflow">if</span> (selectors[j].size() != types[j].size()) {
<a name="l00951"></a>00951 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>
<a name="l00952"></a>00952 (<span class="stringliteral">"dataType: constructor at index "</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(i)+<span class="stringliteral">", "</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(j)+
<a name="l00953"></a>00953 <span class="stringliteral">": number of selectors does not match number of types"</span>);
<a name="l00954"></a>00954 }
<a name="l00955"></a>00955 thisWellFounded = <span class="keyword">true</span>;
<a name="l00956"></a>00956 <span class="keyword">const</span> vector<string>& sels = selectors[j];
<a name="l00957"></a>00957 <span class="keyword">const</span> vector<Expr>& tps = types[j];
<a name="l00958"></a>00958
<a name="l00959"></a>00959 vector<Type> selTypes;
<a name="l00960"></a>00960 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> t;
<a name="l00961"></a>00961 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> s;
<a name="l00962"></a>00962 <span class="keywordflow">for</span> (k = 0; k < sels.size(); ++k) {
<a name="l00963"></a>00963 s = <a class="code" href="classCVC3_1_1Theory.html#a07b326cd94b2bb8bafa39faf07caaec5" title="Resolve an identifier, for use in parseExprOp()">resolveID</a>(sels[k]);
<a name="l00964"></a>00964 <span class="keywordflow">if</span> (!s.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>()) {
<a name="l00965"></a>00965 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>
<a name="l00966"></a>00966 (<span class="stringliteral">"Attempt to define datatype selector "</span>+sels[k]+<span class="stringliteral">":\n "</span>
<a name="l00967"></a>00967 <span class="stringliteral">"This variable is already defined."</span>);
<a name="l00968"></a>00968 }
<a name="l00969"></a>00969 s = <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()-><a class="code" href="group__EM__Priv.html#gafddb4551e9dbb163823b1162248e58f0">newSymbolExpr</a>(sels[k], <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ac909f916e89d861b4a4e5eba782c5259">SELECTOR</a>);
<a name="l00970"></a>00970 <span class="keywordflow">if</span> (tps[k].isString()) {
<a name="l00971"></a>00971 t = <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>(<a class="code" href="classCVC3_1_1Theory.html#a07b326cd94b2bb8bafa39faf07caaec5" title="Resolve an identifier, for use in parseExprOp()">resolveID</a>(tps[k].getString()));
<a name="l00972"></a>00972 <span class="keywordflow">if</span> (t.<a class="code" href="classCVC3_1_1Type.html#ab5fe00c99ee91f369e3339b26bab0bf7">isNull</a>()) {
<a name="l00973"></a>00973 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>
<a name="l00974"></a>00974 (<span class="stringliteral">"Unable to resolve type identifier: "</span>+tps[k].getString());
<a name="l00975"></a>00975 }
<a name="l00976"></a>00976 } <span class="keywordflow">else</span> t = <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>(tps[k]);
<a name="l00977"></a>00977 <span class="keywordflow">if</span> (t.<a class="code" href="classCVC3_1_1Type.html#a38bba404056eadf3c283a67ab2347e02">isBool</a>()) {
<a name="l00978"></a>00978 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>
<a name="l00979"></a>00979 (<span class="stringliteral">"Cannot have BOOLEAN inside of datatype"</span>);
<a name="l00980"></a>00980 }
<a name="l00981"></a>00981 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (t.<a class="code" href="classCVC3_1_1Type.html#a9c3be568546a63fb424e4cb49391dfa6">isFunction</a>()) {
<a name="l00982"></a>00982 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>
<a name="l00983"></a>00983 (<span class="stringliteral">"Cannot have function inside of datatype"</span>);
<a name="l00984"></a>00984 }
<a name="l00985"></a>00985
<a name="l00986"></a>00986 selTypes.push_back(<a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>(t));
<a name="l00987"></a>00987 s.<a class="code" href="group__ExprPkg.html#ga07d47f902598e00097086deabf04d9c5" title="Set the cached type.">setType</a>(<a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>(returnTypes[i]).funType(<a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>(t)));
<a name="l00988"></a>00988 <span class="keywordflow">if</span> (<a class="code" href="namespaceCVC3.html#a88890c6bdae30ff688fd2ea5bd799676">isDatatype</a>(<a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>(t)) && !t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaa7dc360962f097870ecc6a4cc14c4909">isWellFounded</a>()) {
<a name="l00989"></a>00989 thisWellFounded = <span class="keyword">false</span>;
<a name="l00990"></a>00990 }
<a name="l00991"></a>00991 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a63dc7258a77b6e3cb172c1a38994a06b">d_selectorMap</a>[s] = pair<Expr,unsigned>(c,k);
<a name="l00992"></a>00992 <a class="code" href="classCVC3_1_1Theory.html#a6b1c155465b0c24885213e7442dd0882" title="Install name as a new identifier associated with Expr e.">installID</a>(sels[k], s);
<a name="l00993"></a>00993 selectorVec.push_back(s);
<a name="l00994"></a>00994 }
<a name="l00995"></a>00995 <span class="keywordflow">if</span> (thisWellFounded) c.<a class="code" href="group__ExprPkg.html#ga3e4a13d6c9c5d1c14d44ca530ca8187d">setWellFounded</a>();
<a name="l00996"></a>00996 <span class="keywordflow">if</span> (selTypes.size() == 0) {
<a name="l00997"></a>00997 c.<a class="code" href="group__ExprPkg.html#ga07d47f902598e00097086deabf04d9c5" title="Set the cached type.">setType</a>(<a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>(returnTypes[i]));
<a name="l00998"></a>00998 c.<a class="code" href="group__ExprPkg.html#gaecb0afa375de675309b6d1ec72a5c648">setFinite</a>();
<a name="l00999"></a>00999 }
<a name="l01000"></a>01000 <span class="keywordflow">else</span> c.<a class="code" href="group__ExprPkg.html#ga07d47f902598e00097086deabf04d9c5" title="Set the cached type.">setType</a>(<a class="code" href="classCVC3_1_1Type.html#a3ebf8a1ba9d894c33df064ea37c5ead5">Type::funType</a>(selTypes, <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>(returnTypes[i])));
<a name="l01001"></a>01001 <a class="code" href="classCVC3_1_1Theory.html#a6b1c155465b0c24885213e7442dd0882" title="Install name as a new identifier associated with Expr e.">installID</a>(constructors[j], c);
<a name="l01002"></a>01002 constMap[c] = j;
<a name="l01003"></a>01003 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a1e8e2818f2f0dcf45743b42b3d9778b3">d_constructorMap</a>[c] = selectorVec;
<a name="l01004"></a>01004 selectorVec.<a class="code" href="classCVC3_1_1ExprMap.html#a173c2cf4753189d956073d74c36c7c58">clear</a>();
<a name="l01005"></a>01005
<a name="l01006"></a>01006 <span class="keywordtype">string</span> testerString = <span class="stringliteral">"is_"</span>+constructors[j];
<a name="l01007"></a>01007 e = <a class="code" href="classCVC3_1_1Theory.html#a07b326cd94b2bb8bafa39faf07caaec5" title="Resolve an identifier, for use in parseExprOp()">resolveID</a>(testerString);
<a name="l01008"></a>01008 <span class="keywordflow">if</span> (!e.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>()) {
<a name="l01009"></a>01009 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>
<a name="l01010"></a>01010 (<span class="stringliteral">"Attempt to define datatype tester "</span>+testerString+<span class="stringliteral">":\n "</span>
<a name="l01011"></a>01011 <span class="stringliteral">"This variable is already defined."</span>);
<a name="l01012"></a>01012 }
<a name="l01013"></a>01013 e = <a class="code" href="classCVC3_1_1Theory.html#abc2e30308c9e1f3cf752cfe8d939df1e" title="Access to ExprManager.">getEM</a>()-><a class="code" href="group__EM__Priv.html#gafddb4551e9dbb163823b1162248e58f0">newSymbolExpr</a>(testerString, <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089a4df0e72bf250adc8dd78e81fea2f281c">TESTER</a>);
<a name="l01014"></a>01014 e.<a class="code" href="group__ExprPkg.html#ga07d47f902598e00097086deabf04d9c5" title="Set the cached type.">setType</a>(<a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>(returnTypes[i]).funType(<a class="code" href="classCVC3_1_1Theory.html#a705d998884ec8a53c22220373472d868" title="Return BOOLEAN type.">boolType</a>()));
<a name="l01015"></a>01015 <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6c428d8d15b377753c2154f4109604c8">d_testerMap</a>[e] = c;
<a name="l01016"></a>01016 <a class="code" href="classCVC3_1_1Theory.html#a6b1c155465b0c24885213e7442dd0882" title="Install name as a new identifier associated with Expr e.">installID</a>(testerString, e);
<a name="l01017"></a>01017 }
<a name="l01018"></a>01018 }
<a name="l01019"></a>01019
<a name="l01020"></a>01020 <span class="comment">// Compute fixed point for wellfoundedness check</span>
<a name="l01021"></a>01021
<a name="l01022"></a>01022 <span class="keywordtype">bool</span> changed, thisFinite;
<a name="l01023"></a>01023 <span class="keywordtype">int</span> firstNotWellFounded;
<a name="l01024"></a>01024 <span class="keywordflow">do</span> {
<a name="l01025"></a>01025 changed = <span class="keyword">false</span>;
<a name="l01026"></a>01026 firstNotWellFounded = -1;
<a name="l01027"></a>01027 <span class="keywordflow">for</span> (i = 0; i < names.size(); ++i) {
<a name="l01028"></a>01028 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<unsigned></a>& c = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>[returnTypes[i]];
<a name="l01029"></a>01029 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<unsigned>::iterator</a> c_it = c.<a class="code" href="classCVC3_1_1ExprMap.html#a3db85401f8535daf4054fde531cd46b1">begin</a>(), c_end = c.<a class="code" href="classCVC3_1_1ExprMap.html#a283ae6c44308cbdda0d82da5a16e52c8">end</a>();
<a name="l01030"></a>01030 thisWellFounded = <span class="keyword">false</span>;
<a name="l01031"></a>01031 thisFinite = <span class="keyword">true</span>;
<a name="l01032"></a>01032 <span class="keywordflow">for</span> (; c_it != c_end; ++c_it) {
<a name="l01033"></a>01033 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& cons = (*c_it).first;
<a name="l01034"></a>01034 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> funType = <a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(cons).<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>();
<a name="l01035"></a>01035 <span class="keywordtype">int</span> j;
<a name="l01036"></a>01036 <span class="keywordflow">if</span> (!cons.<a class="code" href="group__ExprPkg.html#gacf628bd70fc2c4766afa268ed22ea947">isFinite</a>()) {
<a name="l01037"></a>01037 <span class="keywordflow">for</span> (j = 0; j < funType.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-1; ++j) {
<a name="l01038"></a>01038 <span class="keywordflow">if</span> (!<a class="code" href="namespaceCVC3.html#a88890c6bdae30ff688fd2ea5bd799676">isDatatype</a>(funType[j]) || !funType[j].<a class="code" href="group__ExprPkg.html#gacf628bd70fc2c4766afa268ed22ea947">isFinite</a>())
<a name="l01039"></a>01039 <span class="keywordflow">break</span>;
<a name="l01040"></a>01040 }
<a name="l01041"></a>01041 <span class="keywordflow">if</span> (j == funType.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-1) {
<a name="l01042"></a>01042 changed = <span class="keyword">true</span>;
<a name="l01043"></a>01043 cons.<a class="code" href="group__ExprPkg.html#gaecb0afa375de675309b6d1ec72a5c648">setFinite</a>();
<a name="l01044"></a>01044 }
<a name="l01045"></a>01045 <span class="keywordflow">else</span> thisFinite = <span class="keyword">false</span>;
<a name="l01046"></a>01046 }
<a name="l01047"></a>01047 <span class="keywordflow">if</span> (cons.<a class="code" href="group__ExprPkg.html#gaa7dc360962f097870ecc6a4cc14c4909">isWellFounded</a>()) {
<a name="l01048"></a>01048 thisWellFounded = <span class="keyword">true</span>;
<a name="l01049"></a>01049 <span class="keywordflow">continue</span>;
<a name="l01050"></a>01050 }
<a name="l01051"></a>01051 <span class="keywordflow">for</span> (j = 0; j < funType.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-1; ++j) {
<a name="l01052"></a>01052 <span class="keywordflow">if</span> (<a class="code" href="namespaceCVC3.html#a88890c6bdae30ff688fd2ea5bd799676">isDatatype</a>(funType[j]) && !funType[j].<a class="code" href="group__ExprPkg.html#gaa7dc360962f097870ecc6a4cc14c4909">isWellFounded</a>())
<a name="l01053"></a>01053 <span class="keywordflow">break</span>;
<a name="l01054"></a>01054 }
<a name="l01055"></a>01055 <span class="keywordflow">if</span> (j == funType.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-1) {
<a name="l01056"></a>01056 changed = <span class="keyword">true</span>;
<a name="l01057"></a>01057 cons.<a class="code" href="group__ExprPkg.html#ga3e4a13d6c9c5d1c14d44ca530ca8187d">setWellFounded</a>();
<a name="l01058"></a>01058 thisWellFounded = <span class="keyword">true</span>;
<a name="l01059"></a>01059 }
<a name="l01060"></a>01060 }
<a name="l01061"></a>01061 <span class="keywordflow">if</span> (!thisWellFounded) {
<a name="l01062"></a>01062 <span class="keywordflow">if</span> (firstNotWellFounded == -1) firstNotWellFounded = i;
<a name="l01063"></a>01063 }
<a name="l01064"></a>01064 <span class="keywordflow">else</span> {
<a name="l01065"></a>01065 <span class="keywordflow">if</span> (!returnTypes[i].isWellFounded()) {
<a name="l01066"></a>01066 changed = <span class="keyword">true</span>;
<a name="l01067"></a>01067 returnTypes[i].setWellFounded();
<a name="l01068"></a>01068 }
<a name="l01069"></a>01069 }
<a name="l01070"></a>01070 <span class="keywordflow">if</span> (thisFinite && !returnTypes[i].isFinite()) {
<a name="l01071"></a>01071 changed = <span class="keyword">true</span>;
<a name="l01072"></a>01072 returnTypes[i].setFinite();
<a name="l01073"></a>01073 }
<a name="l01074"></a>01074 }
<a name="l01075"></a>01075 } <span class="keywordflow">while</span> (changed);
<a name="l01076"></a>01076
<a name="l01077"></a>01077 <span class="keywordflow">if</span> (firstNotWellFounded >= 0) {
<a name="l01078"></a>01078 <span class="comment">// TODO: uninstall all ID's</span>
<a name="l01079"></a>01079 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1TypecheckException.html">TypecheckException</a>
<a name="l01080"></a>01080 (<span class="stringliteral">"Datatype "</span>+names[firstNotWellFounded]+<span class="stringliteral">" has no finite terms"</span>);
<a name="l01081"></a>01081 }
<a name="l01082"></a>01082
<a name="l01083"></a>01083 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089a5cc02a3e0fe70ce33e5c3d450b38136c">DATATYPE_DECL</a>, returnTypes);
<a name="l01084"></a>01084 }
<a name="l01085"></a>01085
<a name="l01086"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a12a7bb383d9780f84484de597892809b">01086</a> <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">TheoryDatatype::datatypeConsExpr</a>(<span class="keyword">const</span> <span class="keywordtype">string</span>& constructor,
<a name="l01087"></a>01087 <span class="keyword">const</span> vector<Expr>& args)
<a name="l01088"></a>01088 {
<a name="l01089"></a>01089 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e = <a class="code" href="classCVC3_1_1Theory.html#a07b326cd94b2bb8bafa39faf07caaec5" title="Resolve an identifier, for use in parseExprOp()">resolveID</a>(constructor);
<a name="l01090"></a>01090 <span class="keywordflow">if</span> (e.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>())
<a name="l01091"></a>01091 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1Exception.html">Exception</a>(<span class="stringliteral">"datatype: unknown constructor: "</span>+constructor);
<a name="l01092"></a>01092 <span class="keywordflow">if</span> (!(e.<a class="code" href="group__ExprPkg.html#ga93059bf6ddd8020cef4e6796a3c9b5a4">isSymbol</a>() && e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ae3aa1eb89fb69c62d502b57c020ed789">CONSTRUCTOR</a>))
<a name="l01093"></a>01093 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1Exception.html">Exception</a>(<span class="stringliteral">"datatype: "</span>+constructor+<span class="stringliteral">" resolves to: "</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>()+
<a name="l01094"></a>01094 <span class="stringliteral">"\nwhich is not a constructor"</span>);
<a name="l01095"></a>01095 <span class="keywordflow">if</span> (args.size() == 0) <span class="keywordflow">return</span> e;
<a name="l01096"></a>01096 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(e.<a class="code" href="group__ExprPkg.html#ga3aefe2fb15c2d8e3a51dd92dbcc5cdc5" title="Make the expr into an operator.">mkOp</a>(), args);
<a name="l01097"></a>01097 }
<a name="l01098"></a>01098
<a name="l01099"></a>01099
<a name="l01100"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#ac38281a765aa4e57af9a2c6ff4c3686c">01100</a> <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">TheoryDatatype::datatypeSelExpr</a>(<span class="keyword">const</span> <span class="keywordtype">string</span>& 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="l01101"></a>01101 {
<a name="l01102"></a>01102 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e = <a class="code" href="classCVC3_1_1Theory.html#a07b326cd94b2bb8bafa39faf07caaec5" title="Resolve an identifier, for use in parseExprOp()">resolveID</a>(selector);
<a name="l01103"></a>01103 <span class="keywordflow">if</span> (e.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>())
<a name="l01104"></a>01104 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1Exception.html">Exception</a>(<span class="stringliteral">"datatype: unknown selector: "</span>+selector);
<a name="l01105"></a>01105 <span class="keywordflow">if</span> (!(e.<a class="code" href="group__ExprPkg.html#ga93059bf6ddd8020cef4e6796a3c9b5a4">isSymbol</a>() && e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ac909f916e89d861b4a4e5eba782c5259">SELECTOR</a>))
<a name="l01106"></a>01106 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1Exception.html">Exception</a>(<span class="stringliteral">"datatype: "</span>+selector+<span class="stringliteral">" resolves to: "</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>()+
<a name="l01107"></a>01107 <span class="stringliteral">"\nwhich is not a selector"</span>);
<a name="l01108"></a>01108 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(e.<a class="code" href="group__ExprPkg.html#ga3aefe2fb15c2d8e3a51dd92dbcc5cdc5" title="Make the expr into an operator.">mkOp</a>(), arg);
<a name="l01109"></a>01109 }
<a name="l01110"></a>01110
<a name="l01111"></a>01111
<a name="l01112"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a51372d26e89b189c8a5f42d18dd2eedc">01112</a> <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">TheoryDatatype::datatypeTestExpr</a>(<span class="keyword">const</span> <span class="keywordtype">string</span>& 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="l01113"></a>01113 {
<a name="l01114"></a>01114 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e = <a class="code" href="classCVC3_1_1Theory.html#a07b326cd94b2bb8bafa39faf07caaec5" title="Resolve an identifier, for use in parseExprOp()">resolveID</a>(<span class="stringliteral">"is_"</span>+constructor);
<a name="l01115"></a>01115 <span class="keywordflow">if</span> (e.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>())
<a name="l01116"></a>01116 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1Exception.html">Exception</a>(<span class="stringliteral">"datatype: unknown tester: is_"</span>+constructor);
<a name="l01117"></a>01117 <span class="keywordflow">if</span> (!(e.<a class="code" href="group__ExprPkg.html#ga93059bf6ddd8020cef4e6796a3c9b5a4">isSymbol</a>() && e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089a4df0e72bf250adc8dd78e81fea2f281c">TESTER</a>))
<a name="l01118"></a>01118 <span class="keywordflow">throw</span> <a class="code" href="classCVC3_1_1Exception.html">Exception</a>(<span class="stringliteral">"datatype: is_"</span>+constructor+<span class="stringliteral">" resolves to: "</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>()+
<a name="l01119"></a>01119 <span class="stringliteral">"\nwhich is not a tester"</span>);
<a name="l01120"></a>01120 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(e.<a class="code" href="group__ExprPkg.html#ga3aefe2fb15c2d8e3a51dd92dbcc5cdc5" title="Make the expr into an operator.">mkOp</a>(), arg);
<a name="l01121"></a>01121 }
<a name="l01122"></a>01122
<a name="l01123"></a>01123
<a name="l01124"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a5ae1a2fe60c6e2af77cf098340cabd53">01124</a> <span class="keyword">const</span> pair<Expr,unsigned>& <a class="code" href="classCVC3_1_1TheoryDatatype.html#a5ae1a2fe60c6e2af77cf098340cabd53">TheoryDatatype::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="l01125"></a>01125 {
<a name="l01126"></a>01126 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ac909f916e89d861b4a4e5eba782c5259">SELECTOR</a>, <span class="stringliteral">"getSelectorInfo called on non-selector: "</span>
<a name="l01127"></a>01127 +e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l01128"></a>01128 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a63dc7258a77b6e3cb172c1a38994a06b">d_selectorMap</a>.<a class="code" href="classCVC3_1_1ExprMap.html#ae50ab1874dd63b575553e7db769abe28">find</a>(e) != <a class="code" href="classCVC3_1_1TheoryDatatype.html#a63dc7258a77b6e3cb172c1a38994a06b">d_selectorMap</a>.<a class="code" href="classCVC3_1_1ExprMap.html#a283ae6c44308cbdda0d82da5a16e52c8">end</a>(),
<a name="l01129"></a>01129 <span class="stringliteral">"Unknown selector: "</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l01130"></a>01130 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a63dc7258a77b6e3cb172c1a38994a06b">d_selectorMap</a>[e];
<a name="l01131"></a>01131 }
<a name="l01132"></a>01132
<a name="l01133"></a>01133
<a name="l01134"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#af39a46bc360e9f7c91bf0d85cc3908ca">01134</a> <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">TheoryDatatype::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="l01135"></a>01135 {
<a name="l01136"></a>01136 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089a4df0e72bf250adc8dd78e81fea2f281c">TESTER</a>,
<a name="l01137"></a>01137 <span class="stringliteral">"getConsForTester called on non-tester"</span>
<a name="l01138"></a>01138 +e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l01139"></a>01139 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a6c428d8d15b377753c2154f4109604c8">d_testerMap</a>.<a class="code" href="classCVC3_1_1ExprMap.html#ae50ab1874dd63b575553e7db769abe28">find</a>(e) != <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6c428d8d15b377753c2154f4109604c8">d_testerMap</a>.<a class="code" href="classCVC3_1_1ExprMap.html#a283ae6c44308cbdda0d82da5a16e52c8">end</a>(),
<a name="l01140"></a>01140 <span class="stringliteral">"Unknown tester: "</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l01141"></a>01141 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6c428d8d15b377753c2154f4109604c8">d_testerMap</a>[e];
<a name="l01142"></a>01142 }
<a name="l01143"></a>01143
<a name="l01144"></a>01144
<a name="l01145"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d93ab7a39a1eb3e82cb67f0425ffee">01145</a> <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d93ab7a39a1eb3e82cb67f0425ffee">TheoryDatatype::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="l01146"></a>01146 {
<a name="l01147"></a>01147 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="namespaceCVC3.html#af5adcbe1bc4a5aaacccfc9af11f98089ae3aa1eb89fb69c62d502b57c020ed789">CONSTRUCTOR</a>,
<a name="l01148"></a>01148 <span class="stringliteral">"getConsPos called on non-constructor"</span>);
<a name="l01149"></a>01149 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> t = <a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(e);
<a name="l01150"></a>01150 <span class="keywordflow">if</span> (t.isFunction()) t = t[t.arity()-1];
<a name="l01151"></a>01151 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="namespaceCVC3.html#a88890c6bdae30ff688fd2ea5bd799676">isDatatype</a>(t), <span class="stringliteral">"Expected datatype"</span>);
<a name="l01152"></a>01152 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>.<a class="code" href="classCVC3_1_1ExprMap.html#ae50ab1874dd63b575553e7db769abe28">find</a>(t.getExpr()) != <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>.<a class="code" href="classCVC3_1_1ExprMap.html#a283ae6c44308cbdda0d82da5a16e52c8">end</a>(),
<a name="l01153"></a>01153 <span class="stringliteral">"Could not find datatype: "</span>+t.toString());
<a name="l01154"></a>01154 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<unsigned></a>& constMap = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>[t.getExpr()];
<a name="l01155"></a>01155 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(constMap.find(e) != constMap.end(),
<a name="l01156"></a>01156 <span class="stringliteral">"Could not find constructor: "</span>+e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l01157"></a>01157 <span class="keywordflow">return</span> constMap[e];
<a name="l01158"></a>01158 }
<a name="l01159"></a>01159
<a name="l01160"></a>01160
<a name="l01161"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a60d3e5400ca66acaf39a1365bd378c7e">01161</a> <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">TheoryDatatype::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="l01162"></a>01162 {
<a name="l01163"></a>01163 <span class="comment">// if a cycle is detected, backtrack from this branch</span>
<a name="l01164"></a>01164 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoryDatatype.html#ae5ebfda4bb10cae8a4a3c620731bfb51">d_getConstantStack</a>.<a class="code" href="classCVC3_1_1ExprMap.html#aa96dfa3a54a131cdb0964ef4b80e324f">count</a>(t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>()) != 0) {
<a name="l01165"></a>01165 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>();
<a name="l01166"></a>01166 }
<a name="l01167"></a>01167 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#ae5ebfda4bb10cae8a4a3c620731bfb51">d_getConstantStack</a>.<a class="code" href="classCVC3_1_1ExprMap.html#a62589c597d245f3245df6d6a5fe6f4f1">size</a>() < 1000,
<a name="l01168"></a>01168 <span class="stringliteral">"TheoryDatatype::getconstant: too deep recursion depth"</span>);
<a name="l01169"></a>01169 <a class="code" href="classCVC3_1_1TheoryDatatype.html#ae5ebfda4bb10cae8a4a3c620731bfb51">d_getConstantStack</a>[t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>()] = <span class="keyword">true</span>;
<a name="l01170"></a>01170 <span class="keywordflow">if</span> (<a class="code" href="namespaceCVC3.html#a88890c6bdae30ff688fd2ea5bd799676">isDatatype</a>(t)) {
<a name="l01171"></a>01171 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>.<a class="code" href="classCVC3_1_1ExprMap.html#ae50ab1874dd63b575553e7db769abe28">find</a>(t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>()) != <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>.<a class="code" href="classCVC3_1_1ExprMap.html#a283ae6c44308cbdda0d82da5a16e52c8">end</a>(),
<a name="l01172"></a>01172 <span class="stringliteral">"Unknown datatype: "</span>+t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l01173"></a>01173 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<unsigned></a>& c = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>[t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>()];
<a name="l01174"></a>01174 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<unsigned>::iterator</a> i = c.<a class="code" href="classCVC3_1_1ExprMap.html#a3db85401f8535daf4054fde531cd46b1">begin</a>(), iend = c.end();
<a name="l01175"></a>01175 <span class="keywordflow">for</span> (; i != iend; ++i) {
<a name="l01176"></a>01176 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& cons = (*i).first;
<a name="l01177"></a>01177 <span class="keywordflow">if</span> (!<a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(cons).isFunction()) {
<a name="l01178"></a>01178 d_getConstantStack.erase(t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>());
<a name="l01179"></a>01179 <span class="keywordflow">return</span> cons;
<a name="l01180"></a>01180 }
<a name="l01181"></a>01181 }
<a name="l01182"></a>01182 <span class="keywordflow">for</span> (i = c.<a class="code" href="classCVC3_1_1ExprMap.html#a3db85401f8535daf4054fde531cd46b1">begin</a>(), iend = c.end(); i != iend; ++i) {
<a name="l01183"></a>01183 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& cons = (*i).first;
<a name="l01184"></a>01184 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> funType = <a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(cons).<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>();
<a name="l01185"></a>01185 vector<Expr> args;
<a name="l01186"></a>01186 <span class="keywordtype">int</span> j = 0;
<a name="l01187"></a>01187 <span class="keywordflow">for</span> (; j < funType.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-1; ++j) {
<a name="l01188"></a>01188 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> t_j = <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>(funType[j]);
<a name="l01189"></a>01189 <span class="keywordflow">if</span> (t_j == t || <a class="code" href="namespaceCVC3.html#a88890c6bdae30ff688fd2ea5bd799676">isDatatype</a>(t_j)) <span class="keywordflow">break</span>;
<a name="l01190"></a>01190 args.push_back(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a60d3e5400ca66acaf39a1365bd378c7e">getConstant</a>(t_j));
<a name="l01191"></a>01191 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!args.back().isNull(), <span class="stringliteral">"Expected non-null"</span>);
<a name="l01192"></a>01192 }
<a name="l01193"></a>01193 <span class="keywordflow">if</span> (j == funType.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-1) {
<a name="l01194"></a>01194 d_getConstantStack.erase(t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>());
<a name="l01195"></a>01195 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(cons.<a class="code" href="group__ExprPkg.html#ga3aefe2fb15c2d8e3a51dd92dbcc5cdc5" title="Make the expr into an operator.">mkOp</a>(), args);
<a name="l01196"></a>01196 }
<a name="l01197"></a>01197 }
<a name="l01198"></a>01198 <span class="keywordflow">for</span> (i = c.<a class="code" href="classCVC3_1_1ExprMap.html#a3db85401f8535daf4054fde531cd46b1">begin</a>(), iend = c.end(); i != iend; ++i) {
<a name="l01199"></a>01199 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& cons = (*i).first;
<a name="l01200"></a>01200 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> funType = <a class="code" href="classCVC3_1_1Theory.html#aa408fe61c3d28f4333b78a3027606bb8" title="Compute (or look up in cache) the base type of e and return the result.">getBaseType</a>(cons).<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>();
<a name="l01201"></a>01201 vector<Expr> args;
<a name="l01202"></a>01202 <span class="keywordtype">int</span> j = 0;
<a name="l01203"></a>01203 <span class="keywordflow">for</span> (; j < funType.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-1; ++j) {
<a name="l01204"></a>01204 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> t_j = <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>(funType[j]);
<a name="l01205"></a>01205 <span class="keywordflow">if</span> (t_j == t) <span class="keywordflow">break</span>;
<a name="l01206"></a>01206 args.push_back(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a60d3e5400ca66acaf39a1365bd378c7e">getConstant</a>(t_j));
<a name="l01207"></a>01207 <span class="keywordflow">if</span> (args.back().isNull()) <span class="keywordflow">break</span>;
<a name="l01208"></a>01208 }
<a name="l01209"></a>01209 <span class="keywordflow">if</span> (j == funType.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>()-1) {
<a name="l01210"></a>01210 d_getConstantStack.erase(t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>());
<a name="l01211"></a>01211 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(cons.<a class="code" href="group__ExprPkg.html#ga3aefe2fb15c2d8e3a51dd92dbcc5cdc5" title="Make the expr into an operator.">mkOp</a>(), args);
<a name="l01212"></a>01212 }
<a name="l01213"></a>01213 }
<a name="l01214"></a>01214 <a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"Couldn't find constant for"</span>
<a name="l01215"></a>01215 +t.<a class="code" href="classCVC3_1_1Type.html#a2f5ce4b1973ec02b2f2b2eba8ce3cc50">toString</a>());
<a name="l01216"></a>01216 }
<a name="l01217"></a>01217 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!t.<a class="code" href="classCVC3_1_1Type.html#a38bba404056eadf3c283a67ab2347e02">isBool</a>() && !t.<a class="code" href="classCVC3_1_1Type.html#a9c3be568546a63fb424e4cb49391dfa6">isFunction</a>(),
<a name="l01218"></a>01218 <span class="stringliteral">"Expected non-bool, non-function type"</span>);
<a name="l01219"></a>01219 <span class="comment">//TODO: this name could be an illegal identifier (i.e. could include spaces)</span>
<a name="l01220"></a>01220 <span class="keywordtype">string</span> name = <span class="stringliteral">"datatype_"</span>+t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>();
<a name="l01221"></a>01221 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e = <a class="code" href="classCVC3_1_1Theory.html#a07b326cd94b2bb8bafa39faf07caaec5" title="Resolve an identifier, for use in parseExprOp()">resolveID</a>(name);
<a name="l01222"></a>01222 d_getConstantStack.erase(t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>());
<a name="l01223"></a>01223 <span class="keywordflow">if</span> (e.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>()) <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Theory.html#a4f82b4903d68da2bd83afb104c2c62cc" title="Create a new variable given its name and type.">newVar</a>(name, t);
<a name="l01224"></a>01224 <span class="keywordflow">return</span> e;
<a name="l01225"></a>01225 }
<a name="l01226"></a>01226
<a name="l01227"></a>01227
<a name="l01228"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a53246e5e620d363d47497792573ea970">01228</a> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Op.html">Op</a>& <a class="code" href="classCVC3_1_1TheoryDatatype.html#a53246e5e620d363d47497792573ea970">TheoryDatatype::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="l01229"></a>01229 {
<a name="l01230"></a>01230 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="namespaceCVC3.html#a88890c6bdae30ff688fd2ea5bd799676">isDatatype</a>(t), <span class="stringliteral">"Expected datatype"</span>);
<a name="l01231"></a>01231 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#a7aab890b7ccd92b61dafb89bcf9adc65">d_reach</a>.<a class="code" href="classCVC3_1_1ExprMap.html#ae50ab1874dd63b575553e7db769abe28">find</a>(t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>()) != <a class="code" href="classCVC3_1_1TheoryDatatype.html#a7aab890b7ccd92b61dafb89bcf9adc65">d_reach</a>.<a class="code" href="classCVC3_1_1ExprMap.html#a283ae6c44308cbdda0d82da5a16e52c8">end</a>(),
<a name="l01232"></a>01232 <span class="stringliteral">"Couldn't find reachable predicate"</span>);
<a name="l01233"></a>01233 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a7aab890b7ccd92b61dafb89bcf9adc65">d_reach</a>[t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>()];
<a name="l01234"></a>01234 }
<a name="l01235"></a>01235
<a name="l01236"></a>01236
<a name="l01237"></a><a class="code" href="classCVC3_1_1TheoryDatatype.html#a513d221b48500cf4bc91393293d9b2f2">01237</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryDatatype.html#a513d221b48500cf4bc91393293d9b2f2">TheoryDatatype::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="l01238"></a>01238 {
<a name="l01239"></a>01239 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="namespaceCVC3.html#afdcf0b93fc0d1b03a5a14c4988443c7a">isSelector</a>(e), <span class="stringliteral">"canCollapse: Selector expression expected"</span>);
<a name="l01240"></a>01240 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() == 1, <span class="stringliteral">"expected arity 1"</span>);
<a name="l01241"></a>01241 <span class="keywordflow">if</span> (<a class="code" href="namespaceCVC3.html#a91840d293c43120244ce5b5165bdacc4">isConstructor</a>(e[0])) <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l01242"></a>01242 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a1cadecbd2d6fa614a2f2e9419aa43f33">find</a>(e[0]) == <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>.<a class="code" href="classCVC3_1_1CDMap.html#a2a26c7cc4db12cb17d273db5cfa5a890">end</a>()) <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l01243"></a>01243 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(e[0].hasFind() && <a class="code" href="classCVC3_1_1Theory.html#a08412b310cb743536f7edd9fccd60e46" title="Return the find of e, or e if it has no find.">findExpr</a>(e[0]) == e[0],
<a name="l01244"></a>01244 <span class="stringliteral">"canCollapse: Expected find(e[0])=e[0]"</span>);
<a name="l01245"></a>01245 <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a> u = <a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>[e[0]].get().get();
<a name="l01246"></a>01246 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> cons = <a class="code" href="classCVC3_1_1TheoryDatatype.html#a5ae1a2fe60c6e2af77cf098340cabd53">getSelectorInfo</a>(e.<a class="code" href="group__ExprPkg.html#ga9f3328fe077191803a780cfd6566ff9b" title="Get expression of operator (for APPLY Exprs only)">getOpExpr</a>()).first;
<a name="l01247"></a>01247 <a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a> uCons = (<a class="code" href="classCVC3_1_1Unsigned.html">Unsigned</a>)1 << <span class="keywordtype">unsigned</span>(<a class="code" href="classCVC3_1_1TheoryDatatype.html#af4d93ab7a39a1eb3e82cb67f0425ffee">getConsPos</a>(cons));
<a name="l01248"></a>01248 <span class="keywordflow">if</span> ((u & uCons) == 0) <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l01249"></a>01249 <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l01250"></a>01250 }
</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>
