<!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: CVC3::TheoryDatatype Class Reference</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 class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="hierarchy.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a> </li>
<li class="navelem"><a class="el" href="classCVC3_1_1TheoryDatatype.html">TheoryDatatype</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pro-methods">Protected Member Functions</a> |
<a href="#pro-attribs">Protected Attributes</a> </div>
<div class="headertitle">
<div class="title">CVC3::TheoryDatatype Class Reference<div class="ingroups"><a class="el" href="group__Theories.html">Theories</a></div></div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::TheoryDatatype" --><!-- doxytag: inherits="CVC3::Theory" -->
<p>This theory handles datatypes.
<a href="classCVC3_1_1TheoryDatatype.html#details">More...</a></p>
<p><code>#include <<a class="el" href="theory__datatype_8h_source.html">theory_datatype.h</a>></code></p>
<div class="dynheader">
Inheritance diagram for CVC3::TheoryDatatype:</div>
<div class="dyncontent">
<div class="center">
<img src="classCVC3_1_1TheoryDatatype.png" usemap="#CVC3::TheoryDatatype_map" alt=""/>
<map id="CVC3::TheoryDatatype_map" name="CVC3::TheoryDatatype_map">
<area href="classCVC3_1_1Theory.html" title="Base class for theories." alt="CVC3::Theory" shape="rect" coords="0,0,169,24"/>
<area href="classCVC3_1_1TheoryDatatypeLazy.html" title="This theory handles datatypes." alt="CVC3::TheoryDatatypeLazy" shape="rect" coords="0,112,169,136"/>
</map>
</div></div>
<p><a href="classCVC3_1_1TheoryDatatype-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="classCVC3_1_1TheoryDatatype.html#a9a9fd251c5310efadde13129eff997e1">TheoryDatatype</a> (<a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> *theoryCore)
<li>virtual <a class="el" href="classCVC3_1_1TheoryDatatype.html#a409850e0e05071bb71ac2494665729e3">~TheoryDatatype</a> ()
<li><a class="el" href="classCVC3_1_1DatatypeProofRules.html">DatatypeProofRules</a> * <a class="el" href="classCVC3_1_1TheoryDatatype.html#a2c187b27067bc4d794cac14046216598">createProofRules</a> ()
<li>void <a class="el" href="classCVC3_1_1TheoryDatatype.html#a998e0cd18f7d41f9e7df014d7f86edbc">addSharedTerm</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Notify theory of a new shared term. <a href="#a998e0cd18f7d41f9e7df014d7f86edbc"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1TheoryDatatype.html#a640ba909d9c6470c40600a82cdb65417">assertFact</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e)
<dl class="el"><dd class="mdescRight">Assert a new fact to the decision procedure. <a href="#a640ba909d9c6470c40600a82cdb65417"></a><br/></dl><li>virtual void <a class="el" href="classCVC3_1_1TheoryDatatype.html#a50136aaaf32b6b42751290cb2ccfedf6">checkSat</a> (bool fullEffort)
<dl class="el"><dd class="mdescRight">Check for satisfiability in the theory. <a href="#a50136aaaf32b6b42751290cb2ccfedf6"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1TheoryDatatype.html#a5fea4f3ab06825c2df409082095f7d96">rewrite</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Theory-specific rewrite rules. <a href="#a5fea4f3ab06825c2df409082095f7d96"></a><br/></dl><li>virtual void <a class="el" href="classCVC3_1_1TheoryDatatype.html#a8825c26c5b357ec4a6fde28aaceeea44">setup</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Set up the term e for call-backs when e or its children change. <a href="#a8825c26c5b357ec4a6fde28aaceeea44"></a><br/></dl><li>virtual void <a class="el" href="classCVC3_1_1TheoryDatatype.html#a4d1da766acf310b425f564027c70b8b9">update</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &d)
<dl class="el"><dd class="mdescRight">Notify a theory of a new equality. <a href="#a4d1da766acf310b425f564027c70b8b9"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1TheoryDatatype.html#ab5f431756db284b50c011774862f9f16">solve</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e)
<dl class="el"><dd class="mdescRight">An optional solver. <a href="#ab5f431756db284b50c011774862f9f16"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1TheoryDatatype.html#acf535107486ee65ec245d080c48c277f">checkType</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Check that e is a valid <a class="el" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> expr. <a href="#acf535107486ee65ec245d080c48c277f"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54">Cardinality</a> <a class="el" href="classCVC3_1_1TheoryDatatype.html#ad370efc075c3da6b8b081020cd56a55e">finiteTypeInfo</a> (<a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1Unsigned.html">Unsigned</a> &n, bool enumerate, bool computeSize)
<dl class="el"><dd class="mdescRight">Compute information related to finiteness of types. <a href="#ad370efc075c3da6b8b081020cd56a55e"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1TheoryDatatype.html#af1237546f5860ded939958b0c31c6669">computeType</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Compute and store the type of e. <a href="#af1237546f5860ded939958b0c31c6669"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1TheoryDatatype.html#a8fa2a50fe50ccfda4b557783f566dbfc">computeModelTerm</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &v)
<dl class="el"><dd class="mdescRight">Add variables from 'e' to 'v' for constructing a concrete model. <a href="#a8fa2a50fe50ccfda4b557783f566dbfc"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryDatatype.html#ae50ed74ea28aae7d5919a3461302a83e">computeTCC</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Compute and cache the TCC of e. <a href="#ae50ed74ea28aae7d5919a3461302a83e"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryDatatype.html#a464a093b6247645cf10c1bb8aa9a03a4">parseExprOp</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Theory-specific parsing implemented by the DP. <a href="#a464a093b6247645cf10c1bb8aa9a03a4"></a><br/></dl><li><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & <a class="el" href="classCVC3_1_1TheoryDatatype.html#a1d17495677079120272ec4073cd777db">print</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &os, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Theory-specific pretty-printing. <a href="#a1d17495677079120272ec4073cd777db"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryDatatype.html#ab31831ed547432e2a83f74c83a82e982">dataType</a> (const std::string &name, const std::vector< std::string > &constructors, const std::vector< std::vector< std::string > > &selectors, const std::vector< std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > > &types)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryDatatype.html#ae7305309a6b11b8f9733d93b161c07e0">dataType</a> (const std::vector< std::string > &names, const std::vector< std::vector< std::string > > &constructors, const std::vector< std::vector< std::vector< std::string > > > &selectors, const std::vector< std::vector< std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > > > &types)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryDatatype.html#a12a7bb383d9780f84484de597892809b">datatypeConsExpr</a> (const std::string &constructor, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &args)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryDatatype.html#ac38281a765aa4e57af9a2c6ff4c3686c">datatypeSelExpr</a> (const std::string &selector, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &arg)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryDatatype.html#a51372d26e89b189c8a5f42d18dd2eedc">datatypeTestExpr</a> (const std::string &constructor, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &arg)
<li>const std::pair< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, unsigned > & <a class="el" href="classCVC3_1_1TheoryDatatype.html#a5ae1a2fe60c6e2af77cf098340cabd53">getSelectorInfo</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryDatatype.html#af39a46bc360e9f7c91bf0d85cc3908ca">getConsForTester</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li>unsigned <a class="el" href="classCVC3_1_1TheoryDatatype.html#af4d93ab7a39a1eb3e82cb67f0425ffee">getConsPos</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryDatatype.html#a60d3e5400ca66acaf39a1365bd378c7e">getConstant</a> (const <a class="el" href="classCVC3_1_1Type.html">Type</a> &t)
<li>const <a class="el" href="classCVC3_1_1Op.html">Op</a> & <a class="el" href="classCVC3_1_1TheoryDatatype.html#a53246e5e620d363d47497792573ea970">getReachablePredicate</a> (const <a class="el" href="classCVC3_1_1Type.html">Type</a> &t)
<li>bool <a class="el" href="classCVC3_1_1TheoryDatatype.html#a513d221b48500cf4bc91393293d9b2f2">canCollapse</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
</ul>
<h2><a name="pro-methods"></a>
Protected Member Functions</h2>
<ul>
<li>virtual void <a class="el" href="classCVC3_1_1TheoryDatatype.html#a61b966ebd57ae1b2819f8d6ac73555f6">instantiate</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const <a class="el" href="classCVC3_1_1Unsigned.html">Unsigned</a> &u)
<li>virtual void <a class="el" href="classCVC3_1_1TheoryDatatype.html#a3915e378cdf3889e9776b7f0e8c7ee15">initializeLabels</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const <a class="el" href="classCVC3_1_1Type.html">Type</a> &t)
<li>virtual void <a class="el" href="classCVC3_1_1TheoryDatatype.html#a942fa3974b5c4bc2f44e202a6adc80c8">mergeLabels</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e2)
<li>virtual void <a class="el" href="classCVC3_1_1TheoryDatatype.html#a602556d54fd1ad24a04437416613c7a4">mergeLabels</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, unsigned position, bool positive)
</ul>
<h2><a name="pro-attribs"></a>
Protected Attributes</h2>
<ul>
<li><a class="el" href="classCVC3_1_1DatatypeProofRules.html">DatatypeProofRules</a> * <a class="el" href="classCVC3_1_1TheoryDatatype.html#abcd88b0572b5751bddccd9210939f5d0">d_rules</a>
<li><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< unsigned > > <a class="el" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">d_datatypes</a>
<li><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > > <a class="el" href="classCVC3_1_1TheoryDatatype.html#a1e8e2818f2f0dcf45743b42b3d9778b3">d_constructorMap</a>
<li><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< std::pair< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <br class="typebreak"/>
unsigned > > <a class="el" href="classCVC3_1_1TheoryDatatype.html#a63dc7258a77b6e3cb172c1a38994a06b">d_selectorMap</a>
<li><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > <a class="el" href="classCVC3_1_1TheoryDatatype.html#a6c428d8d15b377753c2154f4109604c8">d_testerMap</a>
<li><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< <a class="el" href="classCVC3_1_1Op.html">Op</a> > <a class="el" href="classCVC3_1_1TheoryDatatype.html#a7aab890b7ccd92b61dafb89bcf9adc65">d_reach</a>
<li><a class="el" href="classCVC3_1_1CDMap.html">CDMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="classCVC3_1_1SmartCDO.html">SmartCDO</a>< <a class="el" href="classCVC3_1_1Unsigned.html">Unsigned</a> > > <a class="el" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">d_labels</a>
<li><a class="el" href="classCVC3_1_1CDList.html">CDList</a>< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > <a class="el" href="classCVC3_1_1TheoryDatatype.html#a64a98802daa8a6a7c4f683b60740961f">d_facts</a>
<li><a class="el" href="classCVC3_1_1CDList.html">CDList</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > <a class="el" href="classCVC3_1_1TheoryDatatype.html#a3b16dee83eb2df2c860c14752913a12e">d_splitters</a>
<li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< unsigned > <a class="el" href="classCVC3_1_1TheoryDatatype.html#a1952cec9cef126b4c3d9611738f7169e">d_splittersIndex</a>
<li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< bool > <a class="el" href="classCVC3_1_1TheoryDatatype.html#a73d20b00d4a702698ea0a9baea9c5bc2">d_splitterAsserted</a>
<li>const bool & <a class="el" href="classCVC3_1_1TheoryDatatype.html#a44dee8f4a9da185dcbac872295d342a4">d_smartSplits</a>
<li><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > <a class="el" href="classCVC3_1_1TheoryDatatype.html#ae5ebfda4bb10cae8a4a3c620731bfb51">d_getConstantStack</a>
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock"><p>This theory handles datatypes. </p>
<p>Author: Clark Barrett</p>
<p>Created: Wed Dec 1 22:27:12 2004 </p>
<p>Definition at line <a class="el" href="theory__datatype_8h_source.html#l00052">52</a> of file <a class="el" href="theory__datatype_8h_source.html">theory_datatype.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a9a9fd251c5310efadde13129eff997e1"></a><!-- doxytag: member="CVC3::TheoryDatatype::TheoryDatatype" ref="a9a9fd251c5310efadde13129eff997e1" args="(TheoryCore *theoryCore)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">TheoryDatatype::TheoryDatatype </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> * </td>
<td class="paramname"><em>theoryCore</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00041">41</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="theory__datatype_8h_source.html#l00036">CVC3::CONSTRUCTOR</a>, <a class="el" href="datatype__theorem__producer_8cpp_source.html#l00042">createProofRules()</a>, <a class="el" href="theory__datatype_8h_source.html#l00054">d_rules</a>, <a class="el" href="theory__datatype_8h_source.html#l00035">CVC3::DATATYPE</a>, <a class="el" href="theory__datatype_8h_source.html#l00034">CVC3::DATATYPE_DECL</a>, <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00367">CVC3::ExprManager::newKind()</a>, <a class="el" href="theory_8cpp_source.html#l00203">CVC3::Theory::registerTheory()</a>, <a class="el" href="theory__datatype_8h_source.html#l00037">CVC3::SELECTOR</a>, and <a class="el" href="theory__datatype_8h_source.html#l00038">CVC3::TESTER</a>.</p>
</div>
</div>
<a class="anchor" id="a409850e0e05071bb71ac2494665729e3"></a><!-- doxytag: member="CVC3::TheoryDatatype::~TheoryDatatype" ref="a409850e0e05071bb71ac2494665729e3" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">TheoryDatatype::~TheoryDatatype </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00070">70</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="theory__datatype_8h_source.html#l00054">d_rules</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="a61b966ebd57ae1b2819f8d6ac73555f6"></a><!-- doxytag: member="CVC3::TheoryDatatype::instantiate" ref="a61b966ebd57ae1b2819f8d6ac73555f6" args="(const Expr &e, const Unsigned &u)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryDatatype::instantiate </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Unsigned.html">Unsigned</a> & </td>
<td class="paramname"><em>u</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [protected, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classCVC3_1_1TheoryDatatypeLazy.html#a7e7f8d89852266d4a66d27c5a61237bc">CVC3::TheoryDatatypeLazy</a>.</p>
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00075">75</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="type_8h_source.html#l00055">CVC3::Type::arity()</a>, <a class="el" href="expr__map_8h_source.html#l00190">CVC3::ExprMap< Data >::begin()</a>, <a class="el" href="theory__datatype_8h_source.html#l00057">d_datatypes</a>, <a class="el" href="theory__datatype_8h_source.html#l00068">d_facts</a>, <a class="el" href="theory__datatype_8h_source.html#l00054">d_rules</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="classCVC3_1_1DatatypeProofRules.html#a1f1fede903939b996f001baf43ec1f17">CVC3::DatatypeProofRules::dummyTheorem()</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="theory_8cpp_source.html#l00128">CVC3::Theory::enqueueFact()</a>, <a class="el" href="expr_8h_source.html#l00929">CVC3::Expr::eqExpr()</a>, <a class="el" href="kinds_8h_source.html#l00085">EXISTS</a>, <a class="el" href="expr__map_8h_source.html#l00194">CVC3::ExprMap< Data >::find()</a>, <a class="el" href="theory_8h_source.html#l00503">CVC3::Theory::findExpr()</a>, <a class="el" href="theory_8cpp_source.html#l00383">CVC3::Theory::getBaseType()</a>, <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="expr_8h_source.html#l01232">CVC3::Expr::hasFind()</a>, <a class="el" href="theory__datatype_8h_source.html#l00136">CVC3::isConstructor()</a>, <a class="el" href="expr_8h_source.html#l01326">CVC3::Expr::isFinite()</a>, <a class="el" href="expr_8h_source.html#l01382">CVC3::Expr::isSelected()</a>, <a class="el" href="expr_8h_source.html#l01178">CVC3::Expr::mkOp()</a>, <a class="el" href="expr__manager_8h_source.html#l00506">CVC3::ExprManager::newClosureExpr()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="type_8h_source.html#l00080">CVC3::Type::toString()</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l00112">initializeLabels()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l00144">mergeLabels()</a>.</p>
</div>
</div>
<a class="anchor" id="a3915e378cdf3889e9776b7f0e8c7ee15"></a><!-- doxytag: member="CVC3::TheoryDatatype::initializeLabels" ref="a3915e378cdf3889e9776b7f0e8c7ee15" args="(const Expr &e, const Type &t)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryDatatype::initializeLabels </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Type.html">Type</a> & </td>
<td class="paramname"><em>t</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [protected, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classCVC3_1_1TheoryDatatypeLazy.html#a273b34945dbc3a4f1e4e3d020a20fc88">CVC3::TheoryDatatypeLazy</a>.</p>
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00112">112</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="theory__datatype_8h_source.html#l00057">d_datatypes</a>, <a class="el" href="theory__datatype_8h_source.html#l00066">d_labels</a>, <a class="el" href="theory__datatype_8h_source.html#l00072">d_smartSplits</a>, <a class="el" href="theory__datatype_8h_source.html#l00069">d_splitters</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cdmap_8h_source.html#l00258">CVC3::CDMap< Key, Data, HashFcn >::end()</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="cdmap_8h_source.html#l00303">CVC3::CDMap< Key, Data, HashFcn >::find()</a>, <a class="el" href="expr__map_8h_source.html#l00194">CVC3::ExprMap< Data >::find()</a>, <a class="el" href="theory_8h_source.html#l00503">CVC3::Theory::findExpr()</a>, <a class="el" href="theory__datatype_8h_source.html#l00146">CVC3::getConstructor()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="cdmap_8h_source.html#l00190">CVC3::CDMap< Key, Data, HashFcn >::insert()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00075">instantiate()</a>, <a class="el" href="theory__datatype_8h_source.html#l00136">CVC3::isConstructor()</a>, <a class="el" href="expr_8h_source.html#l01326">CVC3::Expr::isFinite()</a>, <a class="el" href="cdlist_8h_source.html#l00066">CVC3::CDList< T >::push_back()</a>, <a class="el" href="theory_8h_source.html#l00093">CVC3::Theory::theoryCore()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l00191">addSharedTerm()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00201">assertFact()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00339">setup()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l00359">update()</a>.</p>
</div>
</div>
<a class="anchor" id="a942fa3974b5c4bc2f44e202a6adc80c8"></a><!-- doxytag: member="CVC3::TheoryDatatype::mergeLabels" ref="a942fa3974b5c4bc2f44e202a6adc80c8" args="(const Theorem &thm, const Expr &e1, const Expr &e2)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryDatatype::mergeLabels </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [protected, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classCVC3_1_1TheoryDatatypeLazy.html#a59df564de13b5482c49581880e816c8f">CVC3::TheoryDatatypeLazy</a>.</p>
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00144">144</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="theory__datatype_8h_source.html#l00068">d_facts</a>, <a class="el" href="theory__datatype_8h_source.html#l00066">d_labels</a>, <a class="el" href="theory__datatype_8h_source.html#l00054">d_rules</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="classCVC3_1_1DatatypeProofRules.html#a1f1fede903939b996f001baf43ec1f17">CVC3::DatatypeProofRules::dummyTheorem()</a>, <a class="el" href="cdmap_8h_source.html#l00258">CVC3::CDMap< Key, Data, HashFcn >::end()</a>, <a class="el" href="theory_8h_source.html#l00579">CVC3::Theory::falseExpr()</a>, <a class="el" href="cdmap_8h_source.html#l00303">CVC3::CDMap< Key, Data, HashFcn >::find()</a>, <a class="el" href="theory_8h_source.html#l00503">CVC3::Theory::findExpr()</a>, <a class="el" href="theory_8cpp_source.html#l00383">CVC3::Theory::getBaseType()</a>, <a class="el" href="expr_8h_source.html#l01232">CVC3::Expr::hasFind()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00075">instantiate()</a>, <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>, <a class="el" href="cdlist_8h_source.html#l00066">CVC3::CDList< T >::push_back()</a>, and <a class="el" href="theory_8cpp_source.html#l00103">CVC3::Theory::setInconsistent()</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l00201">assertFact()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00339">setup()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l00359">update()</a>.</p>
</div>
</div>
<a class="anchor" id="a602556d54fd1ad24a04437416613c7a4"></a><!-- doxytag: member="CVC3::TheoryDatatype::mergeLabels" ref="a602556d54fd1ad24a04437416613c7a4" args="(const Theorem &thm, const Expr &e, unsigned position, bool positive)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryDatatype::mergeLabels </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">unsigned </td>
<td class="paramname"><em>position</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>positive</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [protected, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reimplemented in <a class="el" href="classCVC3_1_1TheoryDatatypeLazy.html#a7e537c63d898af8fea10fb11c526ef2a">CVC3::TheoryDatatypeLazy</a>.</p>
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00167">167</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="theory__datatype_8h_source.html#l00068">d_facts</a>, <a class="el" href="theory__datatype_8h_source.html#l00066">d_labels</a>, <a class="el" href="theory__datatype_8h_source.html#l00054">d_rules</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="classCVC3_1_1DatatypeProofRules.html#a1f1fede903939b996f001baf43ec1f17">CVC3::DatatypeProofRules::dummyTheorem()</a>, <a class="el" href="cdmap_8h_source.html#l00258">CVC3::CDMap< Key, Data, HashFcn >::end()</a>, <a class="el" href="theory_8h_source.html#l00579">CVC3::Theory::falseExpr()</a>, <a class="el" href="cdmap_8h_source.html#l00303">CVC3::CDMap< Key, Data, HashFcn >::find()</a>, <a class="el" href="theory_8h_source.html#l00503">CVC3::Theory::findExpr()</a>, <a class="el" href="expr_8h_source.html#l01232">CVC3::Expr::hasFind()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00075">instantiate()</a>, <a class="el" href="cdlist_8h_source.html#l00066">CVC3::CDList< T >::push_back()</a>, and <a class="el" href="theory_8cpp_source.html#l00103">CVC3::Theory::setInconsistent()</a>.</p>
</div>
</div>
<a class="anchor" id="a2c187b27067bc4d794cac14046216598"></a><!-- doxytag: member="CVC3::TheoryDatatype::createProofRules" ref="a2c187b27067bc4d794cac14046216598" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1DatatypeProofRules.html">DatatypeProofRules</a> * TheoryDatatype::createProofRules </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="datatype__theorem__producer_8cpp_source.html#l00042">42</a> of file <a class="el" href="datatype__theorem__producer_8cpp_source.html">datatype_theorem_producer.cpp</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l00041">TheoryDatatype()</a>.</p>
</div>
</div>
<a class="anchor" id="a998e0cd18f7d41f9e7df014d7f86edbc"></a><!-- doxytag: member="CVC3::TheoryDatatype::addSharedTerm" ref="a998e0cd18f7d41f9e7df014d7f86edbc" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryDatatype::addSharedTerm </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Notify theory of a new shared term. </p>
<p>When a term e associated with theory i occurs as a child of an expression associated with theory j, the framework calls i->addSharedTerm(e) and j->addSharedTerm(e) </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#ga664e787b0eb7e5e6fdb03efeb409d38a">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00191">191</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="expr_8cpp_source.html#l00517">CVC3::Expr::addToNotify()</a>, <a class="el" href="theory__datatype_8h_source.html#l00066">d_labels</a>, <a class="el" href="theory__datatype_8h_source.html#l00035">CVC3::DATATYPE</a>, <a class="el" href="cdmap_8h_source.html#l00258">CVC3::CDMap< Key, Data, HashFcn >::end()</a>, <a class="el" href="cdmap_8h_source.html#l00303">CVC3::CDMap< Key, Data, HashFcn >::find()</a>, <a class="el" href="theory_8cpp_source.html#l00383">CVC3::Theory::getBaseType()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l00112">initializeLabels()</a>.</p>
</div>
</div>
<a class="anchor" id="a640ba909d9c6470c40600a82cdb65417"></a><!-- doxytag: member="CVC3::TheoryDatatype::assertFact" ref="a640ba909d9c6470c40600a82cdb65417" args="(const Theorem &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryDatatype::assertFact </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Assert a new fact to the decision procedure. </p>
<p>Each fact that makes it into the core framework is assigned to exactly one theory: the theory associated with that fact. assertFact is called to inform the theory that a new fact has been assigned to the theory. </p>
<p>Implements <a class="el" href="group__Theory__API.html#ga58de37714dd855f4d50de15108b8dbc7">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00201">201</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="expr_8cpp_source.html#l00517">CVC3::Expr::addToNotify()</a>, <a class="el" href="expr_8h_source.html#l00941">CVC3::Expr::andExpr()</a>, <a class="el" href="expr__map_8h_source.html#l00190">CVC3::ExprMap< Data >::begin()</a>, <a class="el" href="theory__datatype_8h_source.html#l00059">d_constructorMap</a>, <a class="el" href="theory__datatype_8h_source.html#l00057">d_datatypes</a>, <a class="el" href="theory__datatype_8h_source.html#l00068">d_facts</a>, <a class="el" href="theory__datatype_8h_source.html#l00066">d_labels</a>, <a class="el" href="theory__datatype_8h_source.html#l00054">d_rules</a>, <a class="el" href="theory__datatype_8h_source.html#l00035">CVC3::DATATYPE</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01112">datatypeTestExpr()</a>, <a class="el" href="classCVC3_1_1DatatypeProofRules.html#a1f1fede903939b996f001baf43ec1f17">CVC3::DatatypeProofRules::dummyTheorem()</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="cdmap_8h_source.html#l00258">CVC3::CDMap< Key, Data, HashFcn >::end()</a>, <a class="el" href="theory_8cpp_source.html#l00128">CVC3::Theory::enqueueFact()</a>, <a class="el" href="expr_8h_source.html#l00929">CVC3::Expr::eqExpr()</a>, <a class="el" href="cdmap_8h_source.html#l00303">CVC3::CDMap< Key, Data, HashFcn >::find()</a>, <a class="el" href="theory_8cpp_source.html#l00383">CVC3::Theory::getBaseType()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01134">getConsForTester()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01145">getConsPos()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="expr_8h_source.html#l01191">CVC3::Expr::getOpExpr()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="expr_8h_source.html#l00969">CVC3::Expr::impExpr()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00112">initializeLabels()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="expr_8h_source.html#l01223">CVC3::Expr::isNull()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00144">mergeLabels()</a>, and <a class="el" href="theory__datatype_8h_source.html#l00038">CVC3::TESTER</a>.</p>
</div>
</div>
<a class="anchor" id="a50136aaaf32b6b42751290cb2ccfedf6"></a><!-- doxytag: member="CVC3::TheoryDatatype::checkSat" ref="a50136aaaf32b6b42751290cb2ccfedf6" args="(bool fullEffort)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryDatatype::checkSat </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>fullEffort</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Check for satisfiability in the theory. </p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">fullEffort</td><td>when it is false, checkSat can do as much or as little work as it likes, though simple inferences and checks for consistency should be done to increase efficiency. If fullEffort is true, checkSat must check whether the set of facts given by assertFact together with the arrangement of shared terms (provided by addSharedTerm) induced by the global find database equivalence relation are satisfiable. If satisfiable, checkSat does nothing.</td></tr>
</table>
</dd>
</dl>
<p>If satisfiability can be acheived by merging some of the shared terms, a new fact must be enqueued using enqueueFact (this fact need not be a literal). If there is no way to make things satisfiable, setInconsistent must be called. </p>
<p>Implements <a class="el" href="group__Theory__API.html#gae0bb3d506dad8d69da546777cae27228">CVC3::Theory</a>.</p>
<p>Reimplemented in <a class="el" href="classCVC3_1_1TheoryDatatypeLazy.html#ad89c1890b5ed73dea2be216f5c299f6b">CVC3::TheoryDatatypeLazy</a>.</p>
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00260">260</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="theory_8cpp_source.html#l00148">CVC3::Theory::addSplitter()</a>, <a class="el" href="expr__map_8h_source.html#l00190">CVC3::ExprMap< Data >::begin()</a>, <a class="el" href="theory__datatype_8h_source.html#l00057">d_datatypes</a>, <a class="el" href="theory__datatype_8h_source.html#l00068">d_facts</a>, <a class="el" href="theory__datatype_8h_source.html#l00066">d_labels</a>, <a class="el" href="theory__datatype_8h_source.html#l00054">d_rules</a>, <a class="el" href="theory__datatype_8h_source.html#l00072">d_smartSplits</a>, <a class="el" href="theory__datatype_8h_source.html#l00071">d_splitterAsserted</a>, <a class="el" href="theory__datatype_8h_source.html#l00069">d_splitters</a>, <a class="el" href="theory__datatype_8h_source.html#l00070">d_splittersIndex</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01112">datatypeTestExpr()</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="classCVC3_1_1DatatypeProofRules.html#a1f1fede903939b996f001baf43ec1f17">CVC3::DatatypeProofRules::dummyTheorem()</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="cdmap_8h_source.html#l00258">CVC3::CDMap< Key, Data, HashFcn >::end()</a>, <a class="el" href="theory_8cpp_source.html#l00128">CVC3::Theory::enqueueFact()</a>, <a class="el" href="expr__map_8h_source.html#l00194">CVC3::ExprMap< Data >::find()</a>, <a class="el" href="cdmap_8h_source.html#l00303">CVC3::CDMap< Key, Data, HashFcn >::find()</a>, <a class="el" href="theory_8h_source.html#l00503">CVC3::Theory::findExpr()</a>, <a class="el" href="theory_8cpp_source.html#l00383">CVC3::Theory::getBaseType()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01145">getConsPos()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="expr_8h_source.html#l01191">CVC3::Expr::getOpExpr()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01124">getSelectorInfo()</a>, <a class="el" href="theory__datatype_8h_source.html#l00140">CVC3::isSelector()</a>, <a class="el" href="kinds_8h_source.html#l00068">OR</a>, <a class="el" href="cdlist_8h_source.html#l00064">CVC3::CDList< T >::size()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="type_8h_source.html#l00080">CVC3::Type::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="a5fea4f3ab06825c2df409082095f7d96"></a><!-- doxytag: member="CVC3::TheoryDatatype::rewrite" ref="a5fea4f3ab06825c2df409082095f7d96" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> TheoryDatatype::rewrite </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Theory-specific rewrite rules. </p>
<p>By default, rewrite just returns a reflexive theorem stating that the input expression is equivalent to itself. However, rewrite is allowed to return any theorem which describes how the input expression is equivalent to some new expression. rewrite should be used to perform simplifications, normalization, and any other preprocessing on theory-specific expressions that needs to be done. </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#gaa6475baeb444915fa3b2f5c58dc5148a">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00320">320</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="theory__datatype_8cpp_source.html#l01237">canCollapse()</a>, <a class="el" href="theory__datatype_8h_source.html#l00068">d_facts</a>, <a class="el" href="theory__datatype_8h_source.html#l00054">d_rules</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="theory__datatype_8h_source.html#l00136">CVC3::isConstructor()</a>, <a class="el" href="theory__datatype_8h_source.html#l00140">CVC3::isSelector()</a>, <a class="el" href="theory__datatype_8h_source.html#l00143">CVC3::isTester()</a>, <a class="el" href="theory_8h_source.html#l00673">CVC3::Theory::reflexivityRule()</a>, <a class="el" href="classCVC3_1_1DatatypeProofRules.html#a8ecc9e0e858ab2da52632df61ee8a44e">CVC3::DatatypeProofRules::rewriteSelCons()</a>, <a class="el" href="classCVC3_1_1DatatypeProofRules.html#ad6df2a8a8c661ed1a1be34ce66910a36">CVC3::DatatypeProofRules::rewriteTestCons()</a>, <a class="el" href="theory_8cpp_source.html#l00119">CVC3::Theory::simplify()</a>, and <a class="el" href="theory_8h_source.html#l00681">CVC3::Theory::transitivityRule()</a>.</p>
</div>
</div>
<a class="anchor" id="a8825c26c5b357ec4a6fde28aaceeea44"></a><!-- doxytag: member="CVC3::TheoryDatatype::setup" ref="a8825c26c5b357ec4a6fde28aaceeea44" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryDatatype::setup </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Set up the term e for call-backs when e or its children change. </p>
<p>setup is called once for each expression associated with the theory. It is typically used to setup theory-specific data for an expression and to add call-back information for use with update. </p>
<dl class="see"><dt><b>See also:</b></dt><dd><a class="el" href="classCVC3_1_1TheoryDatatype.html#a4d1da766acf310b425f564027c70b8b9" title="Notify a theory of a new equality.">update</a> </dd></dl>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#ga6896845c1e25b3452238059d779fc4c8">CVC3::Theory</a>.</p>
<p>Reimplemented in <a class="el" href="classCVC3_1_1TheoryDatatypeLazy.html#ab9b700715fb9450717a3afded5a378ec">CVC3::TheoryDatatypeLazy</a>.</p>
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00339">339</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="expr_8cpp_source.html#l00517">CVC3::Expr::addToNotify()</a>, <a class="el" href="kinds_8h_source.html#l00090">APPLY</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theory__datatype_8h_source.html#l00066">d_labels</a>, <a class="el" href="theory__datatype_8h_source.html#l00054">d_rules</a>, <a class="el" href="theory__datatype_8h_source.html#l00072">d_smartSplits</a>, <a class="el" href="theory__datatype_8h_source.html#l00069">d_splitters</a>, <a class="el" href="theory__datatype_8h_source.html#l00035">CVC3::DATATYPE</a>, <a class="el" href="cdmap_8h_source.html#l00258">CVC3::CDMap< Key, Data, HashFcn >::end()</a>, <a class="el" href="theory_8cpp_source.html#l00128">CVC3::Theory::enqueueFact()</a>, <a class="el" href="cdmap_8h_source.html#l00303">CVC3::CDMap< Key, Data, HashFcn >::find()</a>, <a class="el" href="theory_8cpp_source.html#l00383">CVC3::Theory::getBaseType()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00112">initializeLabels()</a>, <a class="el" href="theory__datatype_8h_source.html#l00136">CVC3::isConstructor()</a>, <a class="el" href="theory__datatype_8h_source.html#l00140">CVC3::isSelector()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00144">mergeLabels()</a>, <a class="el" href="classCVC3_1_1DatatypeProofRules.html#acbe824de0e366b711db6d23e23b72509">CVC3::DatatypeProofRules::noCycle()</a>, <a class="el" href="cdlist_8h_source.html#l00066">CVC3::CDList< T >::push_back()</a>, <a class="el" href="expr_8h_source.html#l01533">CVC3::Expr::setSelected()</a>, and <a class="el" href="theory_8cpp_source.html#l00459">CVC3::Theory::setupCC()</a>.</p>
</div>
</div>
<a class="anchor" id="a4d1da766acf310b425f564027c70b8b9"></a><!-- doxytag: member="CVC3::TheoryDatatype::update" ref="a4d1da766acf310b425f564027c70b8b9" args="(const Theorem &e, const Expr &d)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryDatatype::update </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>d</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Notify a theory of a new equality. </p>
<p>update is a call-back used by the notify mechanism of the core theory. It works as follows. When an equation t1 = t2 makes it into the core framework, the two find equivalence classes for t1 and t2 are merged. The result is that t2 is the new equivalence class representative and t1 is no longer an equivalence class representative. When this happens, the notify list of t1 is traversed. Notify list entries consist of a theory and an expression d. For each entry (i,d), i->update(e, d) is called, where e is the theorem corresponding to the equality t1=t2.</p>
<p>To add the entry (i,d) to a term t1's notify list, a call must be made to t1.addNotify(i,d). This is typically done in setup.</p>
<dl class="see"><dt><b>See also:</b></dt><dd><a class="el" href="classCVC3_1_1TheoryDatatype.html#a8825c26c5b357ec4a6fde28aaceeea44" title="Set up the term e for call-backs when e or its children change.">setup</a> </dd></dl>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#gac41af6a90290fe83b2ee6c53cbfc4a62">CVC3::Theory</a>.</p>
<p>Reimplemented in <a class="el" href="classCVC3_1_1TheoryDatatypeLazy.html#a1f5719671fd527eb010fbb2a2f14e79d">CVC3::TheoryDatatypeLazy</a>.</p>
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00359">359</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="expr_8cpp_source.html#l00517">CVC3::Expr::addToNotify()</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01237">canCollapse()</a>, <a class="el" href="theory__datatype_8h_source.html#l00068">d_facts</a>, <a class="el" href="theory__datatype_8h_source.html#l00066">d_labels</a>, <a class="el" href="theory__datatype_8h_source.html#l00054">d_rules</a>, <a class="el" href="theory__datatype_8h_source.html#l00035">CVC3::DATATYPE</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="classCVC3_1_1DatatypeProofRules.html#a0ae4bc02188f1115e9ba2a44185b1d16">CVC3::DatatypeProofRules::decompose()</a>, <a class="el" href="cdmap_8h_source.html#l00258">CVC3::CDMap< Key, Data, HashFcn >::end()</a>, <a class="el" href="theory_8cpp_source.html#l00128">CVC3::Theory::enqueueFact()</a>, <a class="el" href="cdmap_8h_source.html#l00303">CVC3::CDMap< Key, Data, HashFcn >::find()</a>, <a class="el" href="theory_8cpp_source.html#l00383">CVC3::Theory::getBaseType()</a>, <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="expr_8h_source.html#l01191">CVC3::Expr::getOpExpr()</a>, <a class="el" href="expr_8h_source.html#l01569">CVC3::Expr::getRep()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="expr_8h_source.html#l01560">CVC3::Expr::getSig()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00112">initializeLabels()</a>, <a class="el" href="expr__manager_8h_source.html#l00341">CVC3::ExprManager::invalidateSimpCache()</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, <a class="el" href="theory__datatype_8h_source.html#l00136">CVC3::isConstructor()</a>, <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>, <a class="el" href="expr_8h_source.html#l01223">CVC3::Expr::isNull()</a>, <a class="el" href="expr_8h_source.html#l01382">CVC3::Expr::isSelected()</a>, <a class="el" href="theory__datatype_8h_source.html#l00140">CVC3::isSelector()</a>, <a class="el" href="theory__datatype_8h_source.html#l00143">CVC3::isTester()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00144">mergeLabels()</a>, <a class="el" href="cdlist_8h_source.html#l00066">CVC3::CDList< T >::push_back()</a>, <a class="el" href="classCVC3_1_1DatatypeProofRules.html#a8ecc9e0e858ab2da52632df61ee8a44e">CVC3::DatatypeProofRules::rewriteSelCons()</a>, <a class="el" href="classCVC3_1_1DatatypeProofRules.html#ad6df2a8a8c661ed1a1be34ce66910a36">CVC3::DatatypeProofRules::rewriteTestCons()</a>, <a class="el" href="expr_8h_source.html#l01589">CVC3::Expr::setRep()</a>, <a class="el" href="expr_8h_source.html#l01533">CVC3::Expr::setSelected()</a>, <a class="el" href="expr_8h_source.html#l01578">CVC3::Expr::setSig()</a>, <a class="el" href="theory_8h_source.html#l00677">CVC3::Theory::symmetryRule()</a>, <a class="el" href="theory_8h_source.html#l00681">CVC3::Theory::transitivityRule()</a>, and <a class="el" href="theory_8cpp_source.html#l00417">CVC3::Theory::updateHelper()</a>.</p>
</div>
</div>
<a class="anchor" id="ab5f431756db284b50c011774862f9f16"></a><!-- doxytag: member="CVC3::TheoryDatatype::solve" ref="ab5f431756db284b50c011774862f9f16" args="(const Theorem &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> TheoryDatatype::solve </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>An optional solver. </p>
<p>The solve method can be used to implement a Shostak-style solver. Since solvers do not in general combine, the following technique is used. One theory is designated as the primary solver (in our case, it is the theory of arithmetic). For each equation that enters the core framework, the primary solver is called to ensure that the equation is in solved form with respect to the primary theory.</p>
<p>After the primary solver, the solver for the theory associated with the equation is called. This solver can do whatever it likes, as long as the result is still in solved form with respect to the primary solver. This is a slight generalization of what is described in my (Clark)'s PhD thesis. </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#ga3908ecb66d7ba9830e7cf5d1a8ab91c3">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00425">425</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="theory__datatype_8h_source.html#l00136">CVC3::isConstructor()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, <a class="el" href="expr_8h_source.html#l01021">CVC3::Expr::isTerm()</a>, and <a class="el" href="theory_8h_source.html#l00677">CVC3::Theory::symmetryRule()</a>.</p>
</div>
</div>
<a class="anchor" id="acf535107486ee65ec245d080c48c277f"></a><!-- doxytag: member="CVC3::TheoryDatatype::checkType" ref="acf535107486ee65ec245d080c48c277f" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryDatatype::checkType </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Check that e is a valid <a class="el" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> expr. </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#gac22e5fff02a4681c3972e3637bd15748">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00436">436</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theory__datatype_8h_source.html#l00036">CVC3::CONSTRUCTOR</a>, <a class="el" href="theory__datatype_8h_source.html#l00035">CVC3::DATATYPE</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01006">CVC3::Expr::isString()</a>, <a class="el" href="theory_8cpp_source.html#l00887">CVC3::Theory::resolveID()</a>, <a class="el" href="theory__datatype_8h_source.html#l00037">CVC3::SELECTOR</a>, <a class="el" href="theory__datatype_8h_source.html#l00038">CVC3::TESTER</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="ad370efc075c3da6b8b081020cd56a55e"></a><!-- doxytag: member="CVC3::TheoryDatatype::finiteTypeInfo" ref="ad370efc075c3da6b8b081020cd56a55e" args="(Expr &e, Unsigned &n, bool enumerate, bool computeSize)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54">Cardinality</a> TheoryDatatype::finiteTypeInfo </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Unsigned.html">Unsigned</a> & </td>
<td class="paramname"><em>n</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>enumerate</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>computeSize</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Compute information related to finiteness of types. </p>
<p>Used by the TypeComputer defined in <a class="el" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">TheoryCore</a> (theories should not call this funtion directly -- they should use the methods in <a class="el" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> instead). Each theory should implement this if it contains any types that could be non-infinite.</p>
<p>1. Returns Cardinality of the type (finite, infinite, or unknown) 2. If cardinality = finite and enumerate is true, sets e to the nth element of the type if it can sets e to NULL if n is out of bounds or if unable to compute nth element 3. If cardinality = finite and computeSize is true, sets n to the size of the type if it can sets n to 0 otherwise </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#ga166b2a0c7ec3b09e079c2f84bb6087bc">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00457">457</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr__map_8h_source.html#l00190">CVC3::ExprMap< Data >::begin()</a>, <a class="el" href="expr_8h_source.html#l00081">CVC3::CARD_FINITE</a>, <a class="el" href="expr_8h_source.html#l00082">CVC3::CARD_INFINITE</a>, <a class="el" href="expr_8h_source.html#l00083">CVC3::CARD_UNKNOWN</a>, <a class="el" href="expr__map_8h_source.html#l00173">CVC3::ExprMap< Data >::count()</a>, <a class="el" href="theory__datatype_8h_source.html#l00057">d_datatypes</a>, <a class="el" href="theory__datatype_8h_source.html#l00073">d_getConstantStack</a>, <a class="el" href="theory__datatype_8h_source.html#l00035">CVC3::DATATYPE</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr__map_8h_source.html#l00178">CVC3::ExprMap< Data >::erase()</a>, <a class="el" href="theory_8h_source.html#l00252">CVC3::Theory::finiteTypeInfo()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="expr_8h_source.html#l01178">CVC3::Expr::mkOp()</a>, <a class="el" href="theory_8cpp_source.html#l00252">CVC3::Theory::theoryOf()</a>, <a class="el" href="expr_8h_source.html#l01277">CVC3::Expr::typeEnumerateFinite()</a>, and <a class="el" href="expr_8h_source.html#l01285">CVC3::Expr::typeSizeFinite()</a>.</p>
</div>
</div>
<a class="anchor" id="af1237546f5860ded939958b0c31c6669"></a><!-- doxytag: member="CVC3::TheoryDatatype::computeType" ref="af1237546f5860ded939958b0c31c6669" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryDatatype::computeType </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Compute and store the type of e. </p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">e</td><td>is the expression whose type is computed.</td></tr>
</table>
</dd>
</dl>
<p>This function computes the type of the top-level operator of e, and recurses into children using getType(), if necessary. </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#gabaed6b47e6fdea3ae1e53ff75f1882db">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00562">562</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="kinds_8h_source.html#l00051">ARROW</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="theory__datatype_8h_source.html#l00036">CVC3::CONSTRUCTOR</a>, <a class="el" href="theory__datatype_8h_source.html#l00035">CVC3::DATATYPE</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="theory_8cpp_source.html#l00383">CVC3::Theory::getBaseType()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="expr__op_8h_source.html#l00084">CVC3::Op::getExpr()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01183">CVC3::Expr::getOp()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, <a class="el" href="type_8h_source.html#l00059">CVC3::Type::isNull()</a>, <a class="el" href="theory__datatype_8h_source.html#l00037">CVC3::SELECTOR</a>, <a class="el" href="expr_8h_source.html#l01427">CVC3::Expr::setType()</a>, <a class="el" href="theory__datatype_8h_source.html#l00038">CVC3::TESTER</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="a8fa2a50fe50ccfda4b557783f566dbfc"></a><!-- doxytag: member="CVC3::TheoryDatatype::computeModelTerm" ref="a8fa2a50fe50ccfda4b557783f566dbfc" args="(const Expr &e, std::vector< Expr > &v)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryDatatype::computeModelTerm </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>v</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Add variables from 'e' to 'v' for constructing a concrete model. </p>
<p>If e is already of primitive type, do NOT add it to v. </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#ga37309ea20a161f2529cbb0ab79f9ed3f">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00607">607</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="ae50ed74ea28aae7d5919a3461302a83e"></a><!-- doxytag: member="CVC3::TheoryDatatype::computeTCC" ref="ae50ed74ea28aae7d5919a3461302a83e" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> TheoryDatatype::computeTCC </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Compute and cache the TCC of e. </p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">e</td><td>is an expression (term or formula). This function computes the TCC of e which is true iff the expression is defined.</td></tr>
</table>
</dd>
</dl>
<p>This function computes the TCC or predicate of the top-level operator of e, and recurses into children using <a class="el" href="classCVC3_1_1Theory.html#af38bdeb162a9ab9bd81ce40f598f608f" title="Compute the TCC of e, or the subtyping predicate, if e is a type.">getTCC()</a>, if necessary.</p>
<p>The default implementation is to compute TCCs recursively for all children, and return their conjunction. </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#ga9278ad3a6eb8351865a71acd7bb7f968">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00612">612</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00941">CVC3::Expr::andExpr()</a>, <a class="el" href="kinds_8h_source.html#l00090">APPLY</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theory_8cpp_source.html#l00081">CVC3::Theory::computeTCC()</a>, <a class="el" href="theory__datatype_8h_source.html#l00036">CVC3::CONSTRUCTOR</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01112">datatypeTestExpr()</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01191">CVC3::Expr::getOpExpr()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01124">getSelectorInfo()</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, <a class="el" href="theory__datatype_8h_source.html#l00037">CVC3::SELECTOR</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theory_8h_source.html#l00582">CVC3::Theory::trueExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="a464a093b6247645cf10c1bb8aa9a03a4"></a><!-- doxytag: member="CVC3::TheoryDatatype::parseExprOp" ref="a464a093b6247645cf10c1bb8aa9a03a4" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> TheoryDatatype::parseExprOp </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Theory-specific parsing implemented by the DP. </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#ga378bef078620e67fc80f36fa79320d91">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00731">731</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr__map_8h_source.html#l00173">CVC3::ExprMap< Data >::count()</a>, <a class="el" href="theory__datatype_8h_source.html#l00035">CVC3::DATATYPE</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00412">CVC3::ExprManager::getKind()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01055">CVC3::Expr::getString()</a>, <a class="el" href="kinds_8h_source.html#l00046">ID</a>, <a class="el" href="expr__map_8h_source.html#l00177">CVC3::ExprMap< Data >::insert()</a>, <a class="el" href="theory_8cpp_source.html#l00519">CVC3::Theory::parseExpr()</a>, <a class="el" href="kinds_8h_source.html#l00044">RAW_LIST</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="a1d17495677079120272ec4073cd777db"></a><!-- doxytag: member="CVC3::TheoryDatatype::print" ref="a1d17495677079120272ec4073cd777db" args="(ExprStream &os, const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & TheoryDatatype::print </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Theory-specific pretty-printing. </p>
<p>By default, print the top node in AST, and resume pretty-printing the children. The same call e.print(os) can be used in DP-specific printers to use AST printing for the given node. In fact, it is strongly recommended to add e.print(os) as the default for all the cases/kinds that are not handled by the particular pretty-printer. </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#ga49009744d64bbc47785f3fc5fa6884ca">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00639">639</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00090">APPLY</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr__map_8h_source.html#l00190">CVC3::ExprMap< Data >::begin()</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="theory__datatype_8h_source.html#l00036">CVC3::CONSTRUCTOR</a>, <a class="el" href="theory__datatype_8h_source.html#l00059">d_constructorMap</a>, <a class="el" href="theory__datatype_8h_source.html#l00057">d_datatypes</a>, <a class="el" href="theory__datatype_8h_source.html#l00035">CVC3::DATATYPE</a>, <a class="el" href="theory__datatype_8h_source.html#l00034">CVC3::DATATYPE_DECL</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, <a class="el" href="expr__map_8h_source.html#l00194">CVC3::ExprMap< Data >::find()</a>, <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01050">CVC3::Expr::getName()</a>, <a class="el" href="expr_8h_source.html#l01191">CVC3::Expr::getOpExpr()</a>, <a class="el" href="expr_8h_source.html#l01055">CVC3::Expr::getString()</a>, <a class="el" href="expr_8h_source.html#l01006">CVC3::Expr::isString()</a>, <a class="el" href="expr_8h_source.html#l01018">CVC3::Expr::isSymbol()</a>, <a class="el" href="expr__stream_8h_source.html#l00165">CVC3::ExprStream::lang()</a>, <a class="el" href="lang_8h_source.html#l00036">CVC3::LISP_LANG</a>, <a class="el" href="expr__stream_8cpp_source.html#l00301">CVC3::pop()</a>, <a class="el" href="lang_8h_source.html#l00032">CVC3::PRESENTATION_LANG</a>, <a class="el" href="expr_8cpp_source.html#l00400">CVC3::Expr::printAST()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00298">CVC3::push()</a>, <a class="el" href="theory__datatype_8h_source.html#l00037">CVC3::SELECTOR</a>, <a class="el" href="lang_8h_source.html#l00034">CVC3::SMTLIB_LANG</a>, <a class="el" href="expr__stream_8cpp_source.html#l00326">CVC3::space()</a>, and <a class="el" href="theory__datatype_8h_source.html#l00038">CVC3::TESTER</a>.</p>
</div>
</div>
<a class="anchor" id="ab31831ed547432e2a83f74c83a82e982"></a><!-- doxytag: member="CVC3::TheoryDatatype::dataType" ref="ab31831ed547432e2a83f74c83a82e982" args="(const std::string &name, const std::vector< std::string > &constructors, const std::vector< std::vector< std::string > > &selectors, const std::vector< std::vector< Expr > > &types)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> TheoryDatatype::dataType </td>
<td>(</td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>name</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< std::string > & </td>
<td class="paramname"><em>constructors</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< std::vector< std::string > > & </td>
<td class="paramname"><em>selectors</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > > & </td>
<td class="paramname"><em>types</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00859">859</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="ae7305309a6b11b8f9733d93b161c07e0"></a><!-- doxytag: member="CVC3::TheoryDatatype::dataType" ref="ae7305309a6b11b8f9733d93b161c07e0" args="(const std::vector< std::string > &names, const std::vector< std::vector< std::string > > &constructors, const std::vector< std::vector< std::vector< std::string > > > &selectors, const std::vector< std::vector< std::vector< Expr > > > &types)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> TheoryDatatype::dataType </td>
<td>(</td>
<td class="paramtype">const std::vector< std::string > & </td>
<td class="paramname"><em>names</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< std::vector< std::string > > & </td>
<td class="paramname"><em>constructors</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< std::vector< std::vector< std::string > > > & </td>
<td class="paramname"><em>selectors</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< std::vector< std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > > > & </td>
<td class="paramname"><em>types</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l00878">878</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="type_8h_source.html#l00074">CVC3::Type::anyType()</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr__map_8h_source.html#l00190">CVC3::ExprMap< Data >::begin()</a>, <a class="el" href="theory_8h_source.html#l00576">CVC3::Theory::boolType()</a>, <a class="el" href="expr__map_8h_source.html#l00175">CVC3::ExprMap< Data >::clear()</a>, <a class="el" href="theory__datatype_8h_source.html#l00036">CVC3::CONSTRUCTOR</a>, <a class="el" href="theory__datatype_8h_source.html#l00059">d_constructorMap</a>, <a class="el" href="theory__datatype_8h_source.html#l00057">d_datatypes</a>, <a class="el" href="theory__datatype_8h_source.html#l00064">d_reach</a>, <a class="el" href="theory__datatype_8h_source.html#l00061">d_selectorMap</a>, <a class="el" href="theory__datatype_8h_source.html#l00063">d_testerMap</a>, <a class="el" href="theory__datatype_8h_source.html#l00035">CVC3::DATATYPE</a>, <a class="el" href="theory__datatype_8h_source.html#l00034">CVC3::DATATYPE_DECL</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr_8cpp_source.html#l00641">CVC3::Type::funType()</a>, <a class="el" href="theory_8cpp_source.html#l00383">CVC3::Theory::getBaseType()</a>, <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="expr__op_8h_source.html#l00084">CVC3::Op::getExpr()</a>, <a class="el" href="expr_8h_source.html#l01050">CVC3::Expr::getName()</a>, <a class="el" href="theory_8cpp_source.html#l00910">CVC3::Theory::installID()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="theory__datatype_8h_source.html#l00133">CVC3::isDatatype()</a>, <a class="el" href="expr_8h_source.html#l01326">CVC3::Expr::isFinite()</a>, <a class="el" href="type_8h_source.html#l00062">CVC3::Type::isFunction()</a>, <a class="el" href="type_8h_source.html#l00059">CVC3::Type::isNull()</a>, <a class="el" href="expr_8h_source.html#l01223">CVC3::Expr::isNull()</a>, <a class="el" href="expr_8h_source.html#l01330">CVC3::Expr::isWellFounded()</a>, <a class="el" href="theory_8cpp_source.html#l00647">CVC3::Theory::newFunction()</a>, <a class="el" href="expr__manager_8h_source.html#l00481">CVC3::ExprManager::newSymbolExpr()</a>, <a class="el" href="theory_8cpp_source.html#l00887">CVC3::Theory::resolveID()</a>, <a class="el" href="theory__datatype_8h_source.html#l00037">CVC3::SELECTOR</a>, <a class="el" href="expr_8h_source.html#l01463">CVC3::Expr::setFinite()</a>, <a class="el" href="expr_8h_source.html#l01427">CVC3::Expr::setType()</a>, <a class="el" href="expr_8h_source.html#l01468">CVC3::Expr::setWellFounded()</a>, <a class="el" href="theory__datatype_8h_source.html#l00038">CVC3::TESTER</a>, and <a class="el" href="theory__uf_8h_source.html#l00033">CVC3::TRANS_CLOSURE</a>.</p>
</div>
</div>
<a class="anchor" id="a12a7bb383d9780f84484de597892809b"></a><!-- doxytag: member="CVC3::TheoryDatatype::datatypeConsExpr" ref="a12a7bb383d9780f84484de597892809b" args="(const std::string &constructor, const std::vector< Expr > &args)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> TheoryDatatype::datatypeConsExpr </td>
<td>(</td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>constructor</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>args</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l01086">1086</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="theory__datatype_8h_source.html#l00036">CVC3::CONSTRUCTOR</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01223">CVC3::Expr::isNull()</a>, <a class="el" href="expr_8h_source.html#l01018">CVC3::Expr::isSymbol()</a>, <a class="el" href="expr_8h_source.html#l01178">CVC3::Expr::mkOp()</a>, <a class="el" href="theory_8cpp_source.html#l00887">CVC3::Theory::resolveID()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="ac38281a765aa4e57af9a2c6ff4c3686c"></a><!-- doxytag: member="CVC3::TheoryDatatype::datatypeSelExpr" ref="ac38281a765aa4e57af9a2c6ff4c3686c" args="(const std::string &selector, const Expr &arg)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> TheoryDatatype::datatypeSelExpr </td>
<td>(</td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>selector</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>arg</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l01100">1100</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01223">CVC3::Expr::isNull()</a>, <a class="el" href="expr_8h_source.html#l01018">CVC3::Expr::isSymbol()</a>, <a class="el" href="expr_8h_source.html#l01178">CVC3::Expr::mkOp()</a>, <a class="el" href="theory_8cpp_source.html#l00887">CVC3::Theory::resolveID()</a>, <a class="el" href="theory__datatype_8h_source.html#l00037">CVC3::SELECTOR</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="a51372d26e89b189c8a5f42d18dd2eedc"></a><!-- doxytag: member="CVC3::TheoryDatatype::datatypeTestExpr" ref="a51372d26e89b189c8a5f42d18dd2eedc" args="(const std::string &constructor, const Expr &arg)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> TheoryDatatype::datatypeTestExpr </td>
<td>(</td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>constructor</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>arg</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l01112">1112</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01223">CVC3::Expr::isNull()</a>, <a class="el" href="expr_8h_source.html#l01018">CVC3::Expr::isSymbol()</a>, <a class="el" href="expr_8h_source.html#l01178">CVC3::Expr::mkOp()</a>, <a class="el" href="theory_8cpp_source.html#l00887">CVC3::Theory::resolveID()</a>, <a class="el" href="theory__datatype_8h_source.html#l00038">CVC3::TESTER</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l00201">assertFact()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00178">CVC3::TheoryDatatypeLazy::checkSat()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00260">checkSat()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l00612">computeTCC()</a>.</p>
</div>
</div>
<a class="anchor" id="a5ae1a2fe60c6e2af77cf098340cabd53"></a><!-- doxytag: member="CVC3::TheoryDatatype::getSelectorInfo" ref="a5ae1a2fe60c6e2af77cf098340cabd53" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const pair< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, unsigned > & TheoryDatatype::getSelectorInfo </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l01124">1124</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="theory__datatype_8h_source.html#l00061">d_selectorMap</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr__map_8h_source.html#l00194">CVC3::ExprMap< Data >::find()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="theory__datatype_8h_source.html#l00037">CVC3::SELECTOR</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l01237">canCollapse()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00260">checkSat()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l00612">computeTCC()</a>.</p>
</div>
</div>
<a class="anchor" id="af39a46bc360e9f7c91bf0d85cc3908ca"></a><!-- doxytag: member="CVC3::TheoryDatatype::getConsForTester" ref="af39a46bc360e9f7c91bf0d85cc3908ca" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> TheoryDatatype::getConsForTester </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l01134">1134</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="theory__datatype_8h_source.html#l00063">d_testerMap</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr__map_8h_source.html#l00194">CVC3::ExprMap< Data >::find()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="theory__datatype_8h_source.html#l00038">CVC3::TESTER</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l00201">assertFact()</a>.</p>
</div>
</div>
<a class="anchor" id="af4d93ab7a39a1eb3e82cb67f0425ffee"></a><!-- doxytag: member="CVC3::TheoryDatatype::getConsPos" ref="af4d93ab7a39a1eb3e82cb67f0425ffee" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned TheoryDatatype::getConsPos </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l01145">1145</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="theory__datatype_8h_source.html#l00036">CVC3::CONSTRUCTOR</a>, <a class="el" href="theory__datatype_8h_source.html#l00057">d_datatypes</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr__map_8h_source.html#l00194">CVC3::ExprMap< Data >::find()</a>, <a class="el" href="theory_8cpp_source.html#l00383">CVC3::Theory::getBaseType()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="theory__datatype_8h_source.html#l00133">CVC3::isDatatype()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l00201">assertFact()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01237">canCollapse()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l00260">checkSat()</a>.</p>
</div>
</div>
<a class="anchor" id="a60d3e5400ca66acaf39a1365bd378c7e"></a><!-- doxytag: member="CVC3::TheoryDatatype::getConstant" ref="a60d3e5400ca66acaf39a1365bd378c7e" args="(const Type &t)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> TheoryDatatype::getConstant </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Type.html">Type</a> & </td>
<td class="paramname"><em>t</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l01161">1161</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr__map_8h_source.html#l00190">CVC3::ExprMap< Data >::begin()</a>, <a class="el" href="expr__map_8h_source.html#l00173">CVC3::ExprMap< Data >::count()</a>, <a class="el" href="theory__datatype_8h_source.html#l00057">d_datatypes</a>, <a class="el" href="theory__datatype_8h_source.html#l00073">d_getConstantStack</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, <a class="el" href="expr__map_8h_source.html#l00194">CVC3::ExprMap< Data >::find()</a>, <a class="el" href="theory_8cpp_source.html#l00383">CVC3::Theory::getBaseType()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="theory__datatype_8h_source.html#l00133">CVC3::isDatatype()</a>, <a class="el" href="type_8h_source.html#l00062">CVC3::Type::isFunction()</a>, <a class="el" href="expr_8h_source.html#l01223">CVC3::Expr::isNull()</a>, <a class="el" href="expr_8h_source.html#l01178">CVC3::Expr::mkOp()</a>, <a class="el" href="theory_8cpp_source.html#l00569">CVC3::Theory::newVar()</a>, <a class="el" href="theory_8cpp_source.html#l00887">CVC3::Theory::resolveID()</a>, <a class="el" href="expr__map_8h_source.html#l00171">CVC3::ExprMap< Data >::size()</a>, <a class="el" href="type_8h_source.html#l00080">CVC3::Type::toString()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="a53246e5e620d363d47497792573ea970"></a><!-- doxytag: member="CVC3::TheoryDatatype::getReachablePredicate" ref="a53246e5e620d363d47497792573ea970" args="(const Type &t)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Op.html">Op</a> & TheoryDatatype::getReachablePredicate </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Type.html">Type</a> & </td>
<td class="paramname"><em>t</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l01228">1228</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="theory__datatype_8h_source.html#l00064">d_reach</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr__map_8h_source.html#l00194">CVC3::ExprMap< Data >::find()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, and <a class="el" href="theory__datatype_8h_source.html#l00133">CVC3::isDatatype()</a>.</p>
</div>
</div>
<a class="anchor" id="a513d221b48500cf4bc91393293d9b2f2"></a><!-- doxytag: member="CVC3::TheoryDatatype::canCollapse" ref="a513d221b48500cf4bc91393293d9b2f2" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool TheoryDatatype::canCollapse </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8cpp_source.html#l01237">1237</a> of file <a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theory__datatype_8h_source.html#l00066">d_labels</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cdmap_8h_source.html#l00258">CVC3::CDMap< Key, Data, HashFcn >::end()</a>, <a class="el" href="cdmap_8h_source.html#l00303">CVC3::CDMap< Key, Data, HashFcn >::find()</a>, <a class="el" href="theory_8h_source.html#l00503">CVC3::Theory::findExpr()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01145">getConsPos()</a>, <a class="el" href="expr_8h_source.html#l01191">CVC3::Expr::getOpExpr()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01124">getSelectorInfo()</a>, <a class="el" href="theory__datatype_8h_source.html#l00136">CVC3::isConstructor()</a>, and <a class="el" href="theory__datatype_8h_source.html#l00140">CVC3::isSelector()</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l00320">rewrite()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00267">CVC3::TheoryDatatypeLazy::update()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l00359">update()</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="abcd88b0572b5751bddccd9210939f5d0"></a><!-- doxytag: member="CVC3::TheoryDatatype::d_rules" ref="abcd88b0572b5751bddccd9210939f5d0" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1DatatypeProofRules.html">DatatypeProofRules</a>* <a class="el" href="classCVC3_1_1TheoryDatatype.html#abcd88b0572b5751bddccd9210939f5d0">CVC3::TheoryDatatype::d_rules</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8h_source.html#l00054">54</a> of file <a class="el" href="theory__datatype_8h_source.html">theory_datatype.h</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l00201">assertFact()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00260">checkSat()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00050">CVC3::TheoryDatatypeLazy::instantiate()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00075">instantiate()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00123">CVC3::TheoryDatatypeLazy::mergeLabels()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00144">mergeLabels()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00320">rewrite()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00246">CVC3::TheoryDatatypeLazy::setup()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00339">setup()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00041">TheoryDatatype()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00267">CVC3::TheoryDatatypeLazy::update()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00359">update()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l00070">~TheoryDatatype()</a>.</p>
</div>
</div>
<a class="anchor" id="a6ec421864b0680b8a2cf581304e6b31a"></a><!-- doxytag: member="CVC3::TheoryDatatype::d_datatypes" ref="a6ec421864b0680b8a2cf581304e6b31a" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a><<a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a><unsigned> > <a class="el" href="classCVC3_1_1TheoryDatatype.html#a6ec421864b0680b8a2cf581304e6b31a">CVC3::TheoryDatatype::d_datatypes</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8h_source.html#l00057">57</a> of file <a class="el" href="theory__datatype_8h_source.html">theory_datatype.h</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l00201">assertFact()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00178">CVC3::TheoryDatatypeLazy::checkSat()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00260">checkSat()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00878">dataType()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00457">finiteTypeInfo()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01145">getConsPos()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01161">getConstant()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00090">CVC3::TheoryDatatypeLazy::initializeLabels()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00112">initializeLabels()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00050">CVC3::TheoryDatatypeLazy::instantiate()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00075">instantiate()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l00639">print()</a>.</p>
</div>
</div>
<a class="anchor" id="a1e8e2818f2f0dcf45743b42b3d9778b3"></a><!-- doxytag: member="CVC3::TheoryDatatype::d_constructorMap" ref="a1e8e2818f2f0dcf45743b42b3d9778b3" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a><std::vector<<a class="el" href="classCVC3_1_1Expr.html">Expr</a>> > <a class="el" href="classCVC3_1_1TheoryDatatype.html#a1e8e2818f2f0dcf45743b42b3d9778b3">CVC3::TheoryDatatype::d_constructorMap</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8h_source.html#l00059">59</a> of file <a class="el" href="theory__datatype_8h_source.html">theory_datatype.h</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l00201">assertFact()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00878">dataType()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l00639">print()</a>.</p>
</div>
</div>
<a class="anchor" id="a63dc7258a77b6e3cb172c1a38994a06b"></a><!-- doxytag: member="CVC3::TheoryDatatype::d_selectorMap" ref="a63dc7258a77b6e3cb172c1a38994a06b" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a><std::pair<<a class="el" href="classCVC3_1_1Expr.html">Expr</a>,unsigned> > <a class="el" href="classCVC3_1_1TheoryDatatype.html#a63dc7258a77b6e3cb172c1a38994a06b">CVC3::TheoryDatatype::d_selectorMap</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8h_source.html#l00061">61</a> of file <a class="el" href="theory__datatype_8h_source.html">theory_datatype.h</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l00878">dataType()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l01124">getSelectorInfo()</a>.</p>
</div>
</div>
<a class="anchor" id="a6c428d8d15b377753c2154f4109604c8"></a><!-- doxytag: member="CVC3::TheoryDatatype::d_testerMap" ref="a6c428d8d15b377753c2154f4109604c8" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a><<a class="el" href="classCVC3_1_1Expr.html">Expr</a>> <a class="el" href="classCVC3_1_1TheoryDatatype.html#a6c428d8d15b377753c2154f4109604c8">CVC3::TheoryDatatype::d_testerMap</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8h_source.html#l00063">63</a> of file <a class="el" href="theory__datatype_8h_source.html">theory_datatype.h</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l00878">dataType()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l01134">getConsForTester()</a>.</p>
</div>
</div>
<a class="anchor" id="a7aab890b7ccd92b61dafb89bcf9adc65"></a><!-- doxytag: member="CVC3::TheoryDatatype::d_reach" ref="a7aab890b7ccd92b61dafb89bcf9adc65" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a><<a class="el" href="classCVC3_1_1Op.html">Op</a>> <a class="el" href="classCVC3_1_1TheoryDatatype.html#a7aab890b7ccd92b61dafb89bcf9adc65">CVC3::TheoryDatatype::d_reach</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8h_source.html#l00064">64</a> of file <a class="el" href="theory__datatype_8h_source.html">theory_datatype.h</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l00878">dataType()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l01228">getReachablePredicate()</a>.</p>
</div>
</div>
<a class="anchor" id="af4d5b05a1dad378a941cb8c40d0142ff"></a><!-- doxytag: member="CVC3::TheoryDatatype::d_labels" ref="af4d5b05a1dad378a941cb8c40d0142ff" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDMap.html">CDMap</a><<a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="classCVC3_1_1SmartCDO.html">SmartCDO</a><<a class="el" href="classCVC3_1_1Unsigned.html">Unsigned</a>> > <a class="el" href="classCVC3_1_1TheoryDatatype.html#af4d5b05a1dad378a941cb8c40d0142ff">CVC3::TheoryDatatype::d_labels</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8h_source.html#l00066">66</a> of file <a class="el" href="theory__datatype_8h_source.html">theory_datatype.h</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l00191">addSharedTerm()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00201">assertFact()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01237">canCollapse()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00178">CVC3::TheoryDatatypeLazy::checkSat()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00260">checkSat()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00090">CVC3::TheoryDatatypeLazy::initializeLabels()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00112">initializeLabels()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00123">CVC3::TheoryDatatypeLazy::mergeLabels()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00144">mergeLabels()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00246">CVC3::TheoryDatatypeLazy::setup()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00339">setup()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l00359">update()</a>.</p>
</div>
</div>
<a class="anchor" id="a64a98802daa8a6a7c4f683b60740961f"></a><!-- doxytag: member="CVC3::TheoryDatatype::d_facts" ref="a64a98802daa8a6a7c4f683b60740961f" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDList.html">CDList</a><<a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>> <a class="el" href="classCVC3_1_1TheoryDatatype.html#a64a98802daa8a6a7c4f683b60740961f">CVC3::TheoryDatatype::d_facts</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8h_source.html#l00068">68</a> of file <a class="el" href="theory__datatype_8h_source.html">theory_datatype.h</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l00201">assertFact()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00178">CVC3::TheoryDatatypeLazy::checkSat()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00260">checkSat()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00050">CVC3::TheoryDatatypeLazy::instantiate()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00075">instantiate()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00123">CVC3::TheoryDatatypeLazy::mergeLabels()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00144">mergeLabels()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00320">rewrite()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00267">CVC3::TheoryDatatypeLazy::update()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l00359">update()</a>.</p>
</div>
</div>
<a class="anchor" id="a3b16dee83eb2df2c860c14752913a12e"></a><!-- doxytag: member="CVC3::TheoryDatatype::d_splitters" ref="a3b16dee83eb2df2c860c14752913a12e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDList.html">CDList</a><<a class="el" href="classCVC3_1_1Expr.html">Expr</a>> <a class="el" href="classCVC3_1_1TheoryDatatype.html#a3b16dee83eb2df2c860c14752913a12e">CVC3::TheoryDatatype::d_splitters</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8h_source.html#l00069">69</a> of file <a class="el" href="theory__datatype_8h_source.html">theory_datatype.h</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00178">CVC3::TheoryDatatypeLazy::checkSat()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00260">checkSat()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00090">CVC3::TheoryDatatypeLazy::initializeLabels()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00112">initializeLabels()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l00339">setup()</a>.</p>
</div>
</div>
<a class="anchor" id="a1952cec9cef126b4c3d9611738f7169e"></a><!-- doxytag: member="CVC3::TheoryDatatype::d_splittersIndex" ref="a1952cec9cef126b4c3d9611738f7169e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDO.html">CDO</a><unsigned> <a class="el" href="classCVC3_1_1TheoryDatatype.html#a1952cec9cef126b4c3d9611738f7169e">CVC3::TheoryDatatype::d_splittersIndex</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8h_source.html#l00070">70</a> of file <a class="el" href="theory__datatype_8h_source.html">theory_datatype.h</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00178">CVC3::TheoryDatatypeLazy::checkSat()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l00260">checkSat()</a>.</p>
</div>
</div>
<a class="anchor" id="a73d20b00d4a702698ea0a9baea9c5bc2"></a><!-- doxytag: member="CVC3::TheoryDatatype::d_splitterAsserted" ref="a73d20b00d4a702698ea0a9baea9c5bc2" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CDO.html">CDO</a><bool> <a class="el" href="classCVC3_1_1TheoryDatatype.html#a73d20b00d4a702698ea0a9baea9c5bc2">CVC3::TheoryDatatype::d_splitterAsserted</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8h_source.html#l00071">71</a> of file <a class="el" href="theory__datatype_8h_source.html">theory_datatype.h</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00178">CVC3::TheoryDatatypeLazy::checkSat()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l00260">checkSat()</a>.</p>
</div>
</div>
<a class="anchor" id="a44dee8f4a9da185dcbac872295d342a4"></a><!-- doxytag: member="CVC3::TheoryDatatype::d_smartSplits" ref="a44dee8f4a9da185dcbac872295d342a4" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const bool& <a class="el" href="classCVC3_1_1TheoryDatatype.html#a44dee8f4a9da185dcbac872295d342a4">CVC3::TheoryDatatype::d_smartSplits</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8h_source.html#l00072">72</a> of file <a class="el" href="theory__datatype_8h_source.html">theory_datatype.h</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l00260">checkSat()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00112">initializeLabels()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l00339">setup()</a>.</p>
</div>
</div>
<a class="anchor" id="ae5ebfda4bb10cae8a4a3c620731bfb51"></a><!-- doxytag: member="CVC3::TheoryDatatype::d_getConstantStack" ref="ae5ebfda4bb10cae8a4a3c620731bfb51" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a><bool> <a class="el" href="classCVC3_1_1TheoryDatatype.html#ae5ebfda4bb10cae8a4a3c620731bfb51">CVC3::TheoryDatatype::d_getConstantStack</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__datatype_8h_source.html#l00073">73</a> of file <a class="el" href="theory__datatype_8h_source.html">theory_datatype.h</a>.</p>
<p>Referenced by <a class="el" href="theory__datatype_8cpp_source.html#l00457">finiteTypeInfo()</a>, and <a class="el" href="theory__datatype_8cpp_source.html#l01161">getConstant()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="theory__datatype_8h_source.html">theory_datatype.h</a></li>
<li><a class="el" href="datatype__theorem__producer_8cpp_source.html">datatype_theorem_producer.cpp</a></li>
<li><a class="el" href="theory__datatype_8cpp_source.html">theory_datatype.cpp</a></li>
</ul>
</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>
