<!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::Type 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_1Type.html">Type</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pub-static-methods">Static Public Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> </div>
<div class="headertitle">
<div class="title">CVC3::Type Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::Type" -->
<p>MS C++ specific settings.
<a href="classCVC3_1_1Type.html#details">More...</a></p>
<p><code>#include <<a class="el" href="type_8h_source.html">type.h</a>></code></p>
<p><a href="classCVC3_1_1Type-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_1Type.html#a0c0779105402ab3486650cfac3c97fd1">Type</a> ()
<li><a class="el" href="classCVC3_1_1Type.html#a6dbeaa3c209ebef10debb276963d29b9">Type</a> (<a class="el" href="classCVC3_1_1Expr.html">Expr</a> expr)
<li><a class="el" href="classCVC3_1_1Type.html#a199a98692c61cd04ce289db78a4815f5">Type</a> (const <a class="el" href="classCVC3_1_1Type.html">Type</a> &type)
<dl class="el"><dd class="mdescRight">Special constructor that doesn't check if expr is a type. <a href="#a199a98692c61cd04ce289db78a4815f5"></a><br/></dl><li><a class="el" href="classCVC3_1_1Type.html#a3f51087d6da0a2120ed542390fc52996">Type</a> (<a class="el" href="classCVC3_1_1Expr.html">Expr</a> expr, bool dummy)
<li>const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a> () const
<li>int <a class="el" href="classCVC3_1_1Type.html#abd7ab3fcb112e27aa05da8981b56e02c">arity</a> () const
<li><a class="el" href="classCVC3_1_1Type.html">Type</a> <a class="el" href="classCVC3_1_1Type.html#a2842ab1445c09508fcf85ada98d474e5">operator[]</a> (int i) const
<li>bool <a class="el" href="classCVC3_1_1Type.html#ab5fe00c99ee91f369e3339b26bab0bf7">isNull</a> () const
<li>bool <a class="el" href="classCVC3_1_1Type.html#a38bba404056eadf3c283a67ab2347e02">isBool</a> () const
<li>bool <a class="el" href="classCVC3_1_1Type.html#a6b7881db7856a8403553f4f2f3833c74">isSubtype</a> () const
<li>bool <a class="el" href="classCVC3_1_1Type.html#a9c3be568546a63fb424e4cb49391dfa6">isFunction</a> () const
<li><a class="el" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54">Cardinality</a> <a class="el" href="classCVC3_1_1Type.html#a79df1e87774d07af2e0f1e63ef9a5898">card</a> () const
<dl class="el"><dd class="mdescRight">Return cardinality of type. <a href="#a79df1e87774d07af2e0f1e63ef9a5898"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1Type.html#aaf312d59704ec785b26661aeba90b7bc">enumerateFinite</a> (<a class="el" href="classCVC3_1_1Unsigned.html">Unsigned</a> n) const
<dl class="el"><dd class="mdescRight">Return nth (starting with 0) element in a finite type. <a href="#aaf312d59704ec785b26661aeba90b7bc"></a><br/></dl><li><a class="el" href="classCVC3_1_1Unsigned.html">Unsigned</a> <a class="el" href="classCVC3_1_1Type.html#a139b7b4132051557791bcbaea66bd377">sizeFinite</a> () const
<dl class="el"><dd class="mdescRight">Return size of a finite type; returns 0 if size cannot be determined. <a href="#a139b7b4132051557791bcbaea66bd377"></a><br/></dl><li><a class="el" href="classCVC3_1_1Type.html">Type</a> <a class="el" href="classCVC3_1_1Type.html#a2c8b5f5720002766f6fab19157c3f6c0">funType</a> (const <a class="el" href="classCVC3_1_1Type.html">Type</a> &typeRan) const
<li>std::string <a class="el" href="classCVC3_1_1Type.html#a2f5ce4b1973ec02b2f2b2eba8ce3cc50">toString</a> () const
</ul>
<h2><a name="pub-static-methods"></a>
Static Public Member Functions</h2>
<ul>
<li>static <a class="el" href="classCVC3_1_1Type.html">Type</a> <a class="el" href="classCVC3_1_1Type.html#a20b55d497b79ffc60b68ffe512dc2b56">typeBool</a> (<a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> *em)
<li>static <a class="el" href="classCVC3_1_1Type.html">Type</a> <a class="el" href="classCVC3_1_1Type.html#ae3477d8de1425fc5f278a8fbc76e56a0">anyType</a> (<a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> *em)
<li>static <a class="el" href="classCVC3_1_1Type.html">Type</a> <a class="el" href="classCVC3_1_1Type.html#a3ebf8a1ba9d894c33df064ea37c5ead5">funType</a> (const std::vector< <a class="el" href="classCVC3_1_1Type.html">Type</a> > &typeDom, const <a class="el" href="classCVC3_1_1Type.html">Type</a> &typeRan)
</ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1Type.html#aa2fd6d88b18d9e9135cb2b9d59bdf20a">d_expr</a>
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock"><p>MS C++ specific settings. </p>
<p>Definition at line <a class="el" href="type_8h_source.html#l00042">42</a> of file <a class="el" href="type_8h_source.html">type.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a0c0779105402ab3486650cfac3c97fd1"></a><!-- doxytag: member="CVC3::Type::Type" ref="a0c0779105402ab3486650cfac3c97fd1" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Type::Type </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="type_8h_source.html#l00046">46</a> of file <a class="el" href="type_8h_source.html">type.h</a>.</p>
<p>Referenced by <a class="el" href="expr_8cpp_source.html#l00641">funType()</a>.</p>
</div>
</div>
<a class="anchor" id="a6dbeaa3c209ebef10debb276963d29b9"></a><!-- doxytag: member="CVC3::Type::Type" ref="a6dbeaa3c209ebef10debb276963d29b9" args="(Expr expr)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Type::Type </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td>
<td class="paramname"><em>expr</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr_8cpp_source.html#l00634">634</a> of file <a class="el" href="expr_8cpp_source.html">expr.cpp</a>.</p>
<p>References <a class="el" href="expr__manager_8cpp_source.html#l00472">CVC3::ExprManager::checkType()</a>, <a class="el" href="expr_8h_source.html#l01156">CVC3::Expr::getEM()</a>, and <a class="el" href="expr_8h_source.html#l01223">CVC3::Expr::isNull()</a>.</p>
</div>
</div>
<a class="anchor" id="a199a98692c61cd04ce289db78a4815f5"></a><!-- doxytag: member="CVC3::Type::Type" ref="a199a98692c61cd04ce289db78a4815f5" args="(const Type &type)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Type::Type </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Type.html">Type</a> & </td>
<td class="paramname"><em>type</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Special constructor that doesn't check if expr is a type. </p>
<p>Definition at line <a class="el" href="type_8h_source.html#l00050">50</a> of file <a class="el" href="type_8h_source.html">type.h</a>.</p>
</div>
</div>
<a class="anchor" id="a3f51087d6da0a2120ed542390fc52996"></a><!-- doxytag: member="CVC3::Type::Type" ref="a3f51087d6da0a2120ed542390fc52996" args="(Expr expr, bool dummy)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Type::Type </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td>
<td class="paramname"><em>expr</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>dummy</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="type_8h_source.html#l00051">51</a> of file <a class="el" href="type_8h_source.html">type.h</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="a0bc1eebf8dbd9d2880e1f18d7804e5c2"></a><!-- doxytag: member="CVC3::Type::getExpr" ref="a0bc1eebf8dbd9d2880e1f18d7804e5c2" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a>& CVC3::Type::getExpr </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="type_8h_source.html#l00052">52</a> of file <a class="el" href="type_8h_source.html">type.h</a>.</p>
<p>Referenced by <a class="el" href="theory__array_8h_source.html#l00116">CVC3::arrayType()</a>, <a class="el" href="theory__records_8cpp_source.html#l00129">CVC3::TheoryRecords::assertFact()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00201">CVC3::TheoryDatatype::assertFact()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06324">CVC3::BitvectorTheoremProducer::bitblastBVMult()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06407">CVC3::BitvectorTheoremProducer::bitblastBVPlus()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00225">CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00142">CVC3::BitvectorTheoremProducer::bitBlastEqnRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01575">CVC3::BitvectorTheoremProducer::bitExtractBitwise()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01829">CVC3::BitvectorTheoremProducer::bitExtractBVASHR()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01775">CVC3::BitvectorTheoremProducer::bitExtractBVLSHR()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01141">CVC3::BitvectorTheoremProducer::bitExtractBVMult()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01721">CVC3::BitvectorTheoremProducer::bitExtractBVSHL()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01074">CVC3::BitvectorTheoremProducer::bitExtractConstBVMult()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01206">CVC3::BitvectorTheoremProducer::bitExtractExtraction()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01619">CVC3::BitvectorTheoremProducer::bitExtractFixedLeftShift()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01668">CVC3::BitvectorTheoremProducer::bitExtractFixedRightShift()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01539">CVC3::BitvectorTheoremProducer::bitExtractNot()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03329">CVC3::BitvectorTheoremProducer::bvmultConst()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06462">CVC3::BitvectorTheoremProducer::bvSDivRewrite()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02068">CVC3::BitvectorTheoremProducer::bvshlSplit()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00045">CVC3::TheoryBitvector::BVSize()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06574">CVC3::BitvectorTheoremProducer::bvSModRewrite()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06518">CVC3::BitvectorTheoremProducer::bvSRemRewrite()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06272">CVC3::BitvectorTheoremProducer::bvUDivTheorem()</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">CVC3::TheoryDatatype::checkSat()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00471">CVC3::TheoryUF::computeBaseType()</a>, <a class="el" href="theory__records_8cpp_source.html#l00484">CVC3::TheoryRecords::computeBaseType()</a>, <a class="el" href="theory__core_8cpp_source.html#l01620">CVC3::TheoryCore::computeBaseType()</a>, <a class="el" href="theory__array_8cpp_source.html#l00887">CVC3::TheoryArray::computeBaseType()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03808">CVC3::TheoryArithOld::computeBaseType()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l02018">CVC3::TheoryArithNew::computeBaseType()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02830">CVC3::TheoryArith3::computeBaseType()</a>, <a class="el" href="theory__records_8cpp_source.html#l00281">CVC3::TheoryRecords::computeModel()</a>, <a class="el" href="theory__records_8cpp_source.html#l00261">CVC3::TheoryRecords::computeModelTerm()</a>, <a class="el" href="theory__array_8cpp_source.html#l00899">CVC3::TheoryArray::computeModelTerm()</a>, <a class="el" href="theory__records_8cpp_source.html#l00228">CVC3::TheoryRecords::computeTCC()</a>, <a class="el" href="theory__records_8cpp_source.html#l00388">CVC3::TheoryRecords::computeType()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00562">CVC3::TheoryDatatype::computeType()</a>, <a class="el" href="theory__core_8cpp_source.html#l01471">CVC3::TheoryCore::computeType()</a>, <a class="el" href="theory__core_8cpp_source.html#l00074">CVC3::TypeComputerCore::computeType()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l02969">CVC3::TheoryBitvector::computeType()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00465">CVC3::ExprManager::computeType()</a>, <a class="el" href="theory__records_8cpp_source.html#l00312">CVC3::TheoryRecords::computeTypePred()</a>, <a class="el" href="theory__core_8cpp_source.html#l01704">CVC3::TheoryCore::computeTypePred()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l03411">CVC3::TheoryBitvector::computeTypePred()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03603">CVC3::TheoryArithOld::computeTypePred()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01860">CVC3::TheoryArithNew::computeTypePred()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02625">CVC3::TheoryArith3::computeTypePred()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03785">CVC3::BitvectorTheoremProducer::createNewPlusCollection()</a>, <a class="el" href="vcl_8cpp_source.html#l01169">CVC3::VCL::createOp()</a>, <a class="el" href="vcl_8cpp_source.html#l00885">CVC3::VCL::createType()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00878">CVC3::TheoryDatatype::dataType()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01911">CVC3::BitvectorTheoremProducer::eqToBits()</a>, <a class="el" href="records__theorem__producer_8cpp_source.html#l00205">CVC3::RecordsTheoremProducer::expandEq()</a>, <a class="el" href="records__theorem__producer_8cpp_source.html#l00158">CVC3::RecordsTheoremProducer::expandNeq()</a>, <a class="el" href="translator_8cpp_source.html#l01145">CVC3::Translator::finish()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00457">CVC3::TheoryDatatype::finiteTypeInfo()</a>, <a class="el" href="expr_8cpp_source.html#l00641">funType()</a>, <a class="el" href="theory_8cpp_source.html#l00389">CVC3::Theory::getBaseType()</a>, <a class="el" href="theory__bitvector_8h_source.html#l00380">CVC3::TheoryBitvector::getBitvectorTypeParam()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01161">CVC3::TheoryDatatype::getConstant()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01228">CVC3::TheoryDatatype::getReachablePredicate()</a>, <a class="el" href="theory_8cpp_source.html#l00406">CVC3::Theory::getTypePred()</a>, <a class="el" href="vcl_8cpp_source.html#l01071">CVC3::VCL::importType()</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">CVC3::TheoryDatatype::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">CVC3::TheoryDatatype::instantiate()</a>, <a class="el" href="theory__array_8h_source.html#l00109">CVC3::isArray()</a>, <a class="el" href="theory__datatype_8h_source.html#l00133">CVC3::isDatatype()</a>, <a class="el" href="theory__arith_8h_source.html#l00174">CVC3::isInt()</a>, <a class="el" href="theory__arith_8h_source.html#l00173">CVC3::isReal()</a>, <a class="el" href="theory__records_8h_source.html#l00099">CVC3::TheoryRecords::isRecordType()</a>, <a class="el" href="theory__records_8h_source.html#l00156">CVC3::TheoryRecords::isTupleType()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04650">CVC3::TheoryBitvector::newBitvectorTypePred()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04940">CVC3::TheoryBitvector::newBoolExtractExpr()</a>, <a class="el" href="expr__manager_8h_source.html#l00488">CVC3::ExprManager::newBoundVarExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04656">CVC3::TheoryBitvector::newBVAndExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04809">CVC3::TheoryBitvector::newBVCompExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l05237">CVC3::TheoryBitvector::newBVExtractExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04882">CVC3::TheoryBitvector::newBVIndexExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04856">CVC3::TheoryBitvector::newBVLEExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04845">CVC3::TheoryBitvector::newBVLTExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l05038">CVC3::TheoryBitvector::newBVMultExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04728">CVC3::TheoryBitvector::newBVNandExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04920">CVC3::TheoryBitvector::newBVNegExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04743">CVC3::TheoryBitvector::newBVNorExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04692">CVC3::TheoryBitvector::newBVOrExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l05275">CVC3::TheoryBitvector::newBVPlusExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l05111">CVC3::TheoryBitvector::newBVSDivExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04909">CVC3::TheoryBitvector::newBVSLEExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04898">CVC3::TheoryBitvector::newBVSLTExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l05133">CVC3::TheoryBitvector::newBVSModExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l05122">CVC3::TheoryBitvector::newBVSRemExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l05260">CVC3::TheoryBitvector::newBVSubExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l05089">CVC3::TheoryBitvector::newBVUDivExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04930">CVC3::TheoryBitvector::newBVUminusExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l05100">CVC3::TheoryBitvector::newBVURemExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04794">CVC3::TheoryBitvector::newBVXnorExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04758">CVC3::TheoryBitvector::newBVXorExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04997">CVC3::TheoryBitvector::newConcatExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04968">CVC3::TheoryBitvector::newFixedConstWidthLeftShiftExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04954">CVC3::TheoryBitvector::newFixedLeftShiftExpr()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04982">CVC3::TheoryBitvector::newFixedRightShiftExpr()</a>, <a class="el" href="theory_8cpp_source.html#l00647">CVC3::Theory::newFunction()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00258">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04867">CVC3::TheoryBitvector::newSXExpr()</a>, <a class="el" href="theory_8cpp_source.html#l00872">CVC3::Theory::newTypeExpr()</a>, <a class="el" href="theory_8cpp_source.html#l00569">CVC3::Theory::newVar()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00082">CVC3::QuantTheoremProducer::normalizeQuant()</a>, <a class="el" href="type_8h_source.html#l00086">CVC3::operator!=()</a>, <a class="el" href="theory__quant_8h_source.html#l00194">CVC3::TheoryQuant::TypeComp::operator()()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00226">CVC3::operator<<()</a>, <a class="el" href="type_8h_source.html#l00083">CVC3::operator==()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00059">CVC3::TheoryBitvector::pad()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03424">CVC3::BitvectorTheoremProducer::pad()</a>, <a class="el" href="theory__records_8cpp_source.html#l00880">CVC3::TheoryRecords::parseExprOp()</a>, <a class="el" href="theory__core_8cpp_source.html#l01724">CVC3::TheoryCore::parseExprOp()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l04087">CVC3::TheoryBitvector::parseExprOp()</a>, <a class="el" href="translator_8cpp_source.html#l00563">CVC3::Translator::preprocess2Rec()</a>, <a class="el" href="theory__core_8cpp_source.html#l02055">CVC3::TheoryCore::print()</a>, <a class="el" href="translator_8cpp_source.html#l01063">CVC3::Translator::processType()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00251">CVC3::ExprManager::rebuildRec()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06109">CVC3::BitvectorTheoremProducer::repeatRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00863">CVC3::CommonTheoremProducer::rewriteIteFalse()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00885">CVC3::CommonTheoremProducer::rewriteIteSame()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00841">CVC3::CommonTheoremProducer::rewriteIteTrue()</a>, <a class="el" href="theory__core_8cpp_source.html#l04029">CVC3::TheoryCore::rewriteLiteral()</a>, <a class="el" href="datatype__theorem__producer_8cpp_source.html#l00063">CVC3::DatatypeTheoremProducer::rewriteSelCons()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00221">CVC3::CommonTheoremProducer::rewriteUsingSymmetry()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06142">CVC3::BitvectorTheoremProducer::rotlRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06173">CVC3::BitvectorTheoremProducer::rotrRule()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00246">CVC3::TheoryDatatypeLazy::setup()</a>, <a class="el" href="theory__core_8cpp_source.html#l04260">CVC3::TheoryCore::setupTerm()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00339">CVC3::BitvectorTheoremProducer::signExtendRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00187">CVC3::CommonTheoremProducer::symmetryRule()</a>, <a class="el" href="theory_8cpp_source.html#l00260">CVC3::Theory::theoryOf()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00245">CVC3::CommonTheoremProducer::transitivityRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04277">CVC3::BitvectorTheoremProducer::typePredBit()</a>, <a class="el" href="vcl_8cpp_source.html#l00900">CVC3::VCL::varExpr()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06081">CVC3::BitvectorTheoremProducer::zeroExtendRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01470">CVC3::BitvectorTheoremProducer::zeroPaddingRule()</a>, and <a class="el" href="translator_8cpp_source.html#l01943">CVC3::Translator::zeroVar()</a>.</p>
</div>
</div>
<a class="anchor" id="abd7ab3fcb112e27aa05da8981b56e02c"></a><!-- doxytag: member="CVC3::Type::arity" ref="abd7ab3fcb112e27aa05da8981b56e02c" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CVC3::Type::arity </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="type_8h_source.html#l00055">55</a> of file <a class="el" href="type_8h_source.html">type.h</a>.</p>
<p>Referenced by <a class="el" href="theory__simulate_8cpp_source.html#l00164">CVC3::TheorySimulate::computeTCC()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00417">CVC3::TheoryUF::computeType()</a>, <a class="el" href="theory__simulate_8cpp_source.html#l00065">CVC3::TheorySimulate::computeType()</a>, <a class="el" href="theory__core_8cpp_source.html#l01471">CVC3::TheoryCore::computeType()</a>, <a class="el" href="vcl_8cpp_source.html#l01181">CVC3::VCL::createOp()</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">CVC3::TheoryDatatype::instantiate()</a>, <a class="el" href="theory__datatype_8h_source.html#l00136">CVC3::isConstructor()</a>, <a class="el" href="theory_8cpp_source.html#l00647">CVC3::Theory::newFunction()</a>, <a class="el" href="theory_8cpp_source.html#l00569">CVC3::Theory::newVar()</a>, and <a class="el" href="datatype__theorem__producer_8cpp_source.html#l00147">CVC3::DatatypeTheoremProducer::noCycle()</a>.</p>
</div>
</div>
<a class="anchor" id="a2842ab1445c09508fcf85ada98d474e5"></a><!-- doxytag: member="CVC3::Type::operator[]" ref="a2842ab1445c09508fcf85ada98d474e5" args="(int i) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Type.html">Type</a> CVC3::Type::operator[] </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="type_8h_source.html#l00056">56</a> of file <a class="el" href="type_8h_source.html">type.h</a>.</p>
</div>
</div>
<a class="anchor" id="ab5fe00c99ee91f369e3339b26bab0bf7"></a><!-- doxytag: member="CVC3::Type::isNull" ref="ab5fe00c99ee91f369e3339b26bab0bf7" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Type::isNull </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="type_8h_source.html#l00059">59</a> of file <a class="el" href="type_8h_source.html">type.h</a>.</p>
<p>Referenced by <a class="el" href="theory_8cpp_source.html#l00738">CVC3::Theory::addBoundVar()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00383">CVC3::CoreTheoremProducer::AndToIte()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00562">CVC3::TheoryDatatype::computeType()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00878">CVC3::TheoryDatatype::dataType()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="expr__manager_8h_source.html#l00488">CVC3::ExprManager::newBoundVarExpr()</a>, <a class="el" href="theory_8cpp_source.html#l00647">CVC3::Theory::newFunction()</a>, <a class="el" href="theory_8cpp_source.html#l00569">CVC3::Theory::newVar()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00345">CVC3::CoreTheoremProducer::OrToIte()</a>, <a class="el" href="translator_8cpp_source.html#l00563">CVC3::Translator::preprocess2Rec()</a>, <a class="el" href="theory__core_8cpp_source.html#l02055">CVC3::TheoryCore::print()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00251">CVC3::ExprManager::rebuildRec()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00161">CVC3::CoreTheoremProducer::rewriteIteElse()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00863">CVC3::CommonTheoremProducer::rewriteIteFalse()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00885">CVC3::CommonTheoremProducer::rewriteIteSame()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00136">CVC3::CoreTheoremProducer::rewriteIteThen()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00841">CVC3::CommonTheoremProducer::rewriteIteTrue()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00221">CVC3::CommonTheoremProducer::rewriteUsingSymmetry()</a>, and <a class="el" href="common__theorem__producer_8cpp_source.html#l00245">CVC3::CommonTheoremProducer::transitivityRule()</a>.</p>
</div>
</div>
<a class="anchor" id="a38bba404056eadf3c283a67ab2347e02"></a><!-- doxytag: member="CVC3::Type::isBool" ref="a38bba404056eadf3c283a67ab2347e02" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Type::isBool </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="type_8h_source.html#l00060">60</a> of file <a class="el" href="type_8h_source.html">type.h</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00048">BOOLEAN</a>.</p>
<p>Referenced by <a class="el" href="vcl_8cpp_source.html#l01848">CVC3::VCL::assertFormula()</a>, <a class="el" href="theory__core_8cpp_source.html#l03713">CVC3::TheoryCore::assignValue()</a>, <a class="el" href="search__sat_8cpp_source.html#l00638">CVC3::SearchSat::check()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00337">CVC3::TheoryUF::checkType()</a>, <a class="el" href="theory__records_8cpp_source.html#l00344">CVC3::TheoryRecords::checkType()</a>, <a class="el" href="theory__array_8cpp_source.html#l00731">CVC3::TheoryArray::checkType()</a>, <a class="el" href="search__simple_8cpp_source.html#l00165">CVC3::SearchSimple::checkValidInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01350">CVC3::CompleteInstPreProcessor::collectHeads()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08683">CVC3::TheoryQuant::computeType()</a>, <a class="el" href="theory__core_8cpp_source.html#l01471">CVC3::TheoryCore::computeType()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00878">CVC3::TheoryDatatype::dataType()</a>, <a class="el" href="records__theorem__producer_8cpp_source.html#l00205">CVC3::RecordsTheoremProducer::expandEq()</a>, <a class="el" href="records__theorem__producer_8cpp_source.html#l00158">CVC3::RecordsTheoremProducer::expandNeq()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01322">CVC3::CommonTheoremProducer::findITE()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01166">findPolarity()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01626">findPolarityAtomic()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00762">CVC3::BitvectorTheoremProducer::generalIneqn()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01161">CVC3::TheoryDatatype::getConstant()</a>, <a class="el" href="theorem__value_8h_source.html#l00500">CVC3::RWTheoremValue::getExpr()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00641">CVC3::CommonTheoremProducer::iffContrapositive()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01206">CVC3::SearchEngineTheoremProducer::iffToClauses()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00423">CVC3::CoreTheoremProducer::IffToIte()</a>, <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00208">CVC3::CNF_TheoremProducer::ifLiftRule()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00588">CVC3::CoreTheoremProducer::ifLiftUnaryRule()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00439">CVC3::CoreTheoremProducer::ImpToIte()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00264">CVC3::ArrayTheoremProducer::interchangeIndices()</a>, <a class="el" href="expr_8h_source.html#l01021">CVC3::Expr::isTerm()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01186">CVC3::SearchEngineTheoremProducer::iteToClauses()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04271">CVC3::TheoryQuant::matchListNew()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04075">CVC3::TheoryQuant::matchListOld()</a>, <a class="el" href="theory_8cpp_source.html#l00647">CVC3::Theory::newFunction()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00282">CVC3::ExprTransform::newPP()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00334">CVC3::ExprTransform::newPPrec()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04377">CVC3::TheoryQuant::newTopMatchNoSig()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04671">CVC3::TheoryQuant::newTopMatchSig()</a>, <a class="el" href="theory_8cpp_source.html#l00569">CVC3::Theory::newVar()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00328">CVC3::CoreTheoremProducer::NotToIte()</a>, <a class="el" href="theory__core_8cpp_source.html#l02055">CVC3::TheoryCore::print()</a>, <a class="el" href="theory__core_8cpp_source.html#l00291">CVC3::TheoryCore::processUpdates()</a>, <a class="el" href="vcl_8cpp_source.html#l01929">CVC3::VCL::query()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01499">CVC3::CompleteInstPreProcessor::recInstMacros()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01763">CVC3::CompleteInstPreProcessor::recRewriteNot()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01693">CVC3::CompleteInstPreProcessor::recSkolemize()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08565">CVC3::TheoryQuant::recursiveMap()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00074">SAT::CNF_Manager::replaceITErec()</a>, <a class="el" href="search__simple_8cpp_source.html#l00207">CVC3::SearchSimple::restartInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01750">CVC3::SearchEngineFast::restartInternal()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00211">CVC3::TheoryUF::rewrite()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00186">CVC3::CoreTheoremProducer::rewriteIteBool()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00161">CVC3::CoreTheoremProducer::rewriteIteElse()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00863">CVC3::CommonTheoremProducer::rewriteIteFalse()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00885">CVC3::CommonTheoremProducer::rewriteIteSame()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00136">CVC3::CoreTheoremProducer::rewriteIteThen()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00841">CVC3::CommonTheoremProducer::rewriteIteTrue()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00149">CVC3::ArrayTheoremProducer::rewriteReadWrite()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00173">CVC3::ArrayTheoremProducer::rewriteReadWrite2()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00070">CVC3::ArrayTheoremProducer::rewriteSameStore()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00122">CVC3::ArrayTheoremProducer::rewriteWriteWrite()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02917">CVC3::TheoryQuant::setupTriggers()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01462">CVC3::CompleteInstPreProcessor::simplifyEq()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00476">CVC3::ExprTransform::simplifyWithCare()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00296">CVC3::ExprTransform::specialSimplify()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00187">CVC3::CommonTheoremProducer::symmetryRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00245">CVC3::CommonTheoremProducer::transitivityRule()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00257">CVC3::TheoryUF::update()</a>, <a class="el" href="theory_8cpp_source.html#l00473">CVC3::Theory::updateCC()</a>, and <a class="el" href="common__theorem__producer_8cpp_source.html#l01202">CVC3::CommonTheoremProducer::varIntroRule()</a>.</p>
</div>
</div>
<a class="anchor" id="a6b7881db7856a8403553f4f2f3833c74"></a><!-- doxytag: member="CVC3::Type::isSubtype" ref="a6b7881db7856a8403553f4f2f3833c74" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Type::isSubtype </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="type_8h_source.html#l00061">61</a> of file <a class="el" href="type_8h_source.html">type.h</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00193">SUBTYPE</a>.</p>
</div>
</div>
<a class="anchor" id="a9c3be568546a63fb424e4cb49391dfa6"></a><!-- doxytag: member="CVC3::Type::isFunction" ref="a9c3be568546a63fb424e4cb49391dfa6" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Type::isFunction </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="type_8h_source.html#l00062">62</a> of file <a class="el" href="type_8h_source.html">type.h</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00051">ARROW</a>.</p>
<p>Referenced by <a class="el" href="theory__uf_8cpp_source.html#l00337">CVC3::TheoryUF::checkType()</a>, <a class="el" href="theory__records_8cpp_source.html#l00344">CVC3::TheoryRecords::checkType()</a>, <a class="el" href="theory__core_8cpp_source.html#l01408">CVC3::TheoryCore::checkType()</a>, <a class="el" href="theory__array_8cpp_source.html#l00731">CVC3::TheoryArray::checkType()</a>, <a class="el" href="theory__core_8cpp_source.html#l01620">CVC3::TheoryCore::computeBaseType()</a>, <a class="el" href="theory__simulate_8cpp_source.html#l00164">CVC3::TheorySimulate::computeTCC()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00417">CVC3::TheoryUF::computeType()</a>, <a class="el" href="theory__simulate_8cpp_source.html#l00065">CVC3::TheorySimulate::computeType()</a>, <a class="el" href="theory__core_8cpp_source.html#l01471">CVC3::TheoryCore::computeType()</a>, <a class="el" href="vcl_8cpp_source.html#l01169">CVC3::VCL::createOp()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00878">CVC3::TheoryDatatype::dataType()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01161">CVC3::TheoryDatatype::getConstant()</a>, <a class="el" href="theory_8cpp_source.html#l00647">CVC3::Theory::newFunction()</a>, and <a class="el" href="theory_8cpp_source.html#l00569">CVC3::Theory::newVar()</a>.</p>
</div>
</div>
<a class="anchor" id="a79df1e87774d07af2e0f1e63ef9a5898"></a><!-- doxytag: member="CVC3::Type::card" ref="a79df1e87774d07af2e0f1e63ef9a5898" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54">Cardinality</a> CVC3::Type::card </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Return cardinality of type. </p>
<p>Definition at line <a class="el" href="type_8h_source.html#l00064">64</a> of file <a class="el" href="type_8h_source.html">type.h</a>.</p>
<p>Referenced by <a class="el" href="theory__array_8cpp_source.html#l00757">CVC3::TheoryArray::finiteTypeInfo()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00236">CVC3::TheoryUF::setup()</a>, and <a class="el" href="theory__array_8cpp_source.html#l00490">CVC3::TheoryArray::setup()</a>.</p>
</div>
</div>
<a class="anchor" id="aaf312d59704ec785b26661aeba90b7bc"></a><!-- doxytag: member="CVC3::Type::enumerateFinite" ref="aaf312d59704ec785b26661aeba90b7bc" args="(Unsigned n) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> CVC3::Type::enumerateFinite </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Unsigned.html">Unsigned</a> </td>
<td class="paramname"><em>n</em></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Return nth (starting with 0) element in a finite type. </p>
<p>Returns NULL <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> if unable to compute nth element </p>
<p>Definition at line <a class="el" href="type_8h_source.html#l00068">68</a> of file <a class="el" href="type_8h_source.html">type.h</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01277">CVC3::Expr::typeEnumerateFinite()</a>.</p>
<p>Referenced by <a class="el" href="theory__array_8cpp_source.html#l00757">CVC3::TheoryArray::finiteTypeInfo()</a>.</p>
</div>
</div>
<a class="anchor" id="a139b7b4132051557791bcbaea66bd377"></a><!-- doxytag: member="CVC3::Type::sizeFinite" ref="a139b7b4132051557791bcbaea66bd377" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Unsigned.html">Unsigned</a> CVC3::Type::sizeFinite </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Return size of a finite type; returns 0 if size cannot be determined. </p>
<p>Definition at line <a class="el" href="type_8h_source.html#l00070">70</a> of file <a class="el" href="type_8h_source.html">type.h</a>.</p>
<p>Referenced by <a class="el" href="theory__array_8cpp_source.html#l00757">CVC3::TheoryArray::finiteTypeInfo()</a>.</p>
</div>
</div>
<a class="anchor" id="a20b55d497b79ffc60b68ffe512dc2b56"></a><!-- doxytag: member="CVC3::Type::typeBool" ref="a20b55d497b79ffc60b68ffe512dc2b56" args="(ExprManager *em)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">static <a class="el" href="classCVC3_1_1Type.html">Type</a> CVC3::Type::typeBool </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> * </td>
<td class="paramname"><em>em</em></td><td>)</td>
<td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="type_8h_source.html#l00073">73</a> of file <a class="el" href="type_8h_source.html">type.h</a>.</p>
<p>References <a class="el" href="expr__manager_8h_source.html#l00276">CVC3::ExprManager::boolExpr()</a>.</p>
<p>Referenced by <a class="el" href="theory_8h_source.html#l00576">CVC3::Theory::boolType()</a>, and <a class="el" href="expr__manager_8cpp_source.html#l00070">CVC3::ExprManager::ExprManager()</a>.</p>
</div>
</div>
<a class="anchor" id="ae3477d8de1425fc5f278a8fbc76e56a0"></a><!-- doxytag: member="CVC3::Type::anyType" ref="ae3477d8de1425fc5f278a8fbc76e56a0" args="(ExprManager *em)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">static <a class="el" href="classCVC3_1_1Type.html">Type</a> CVC3::Type::anyType </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> * </td>
<td class="paramname"><em>em</em></td><td>)</td>
<td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="type_8h_source.html#l00074">74</a> of file <a class="el" href="type_8h_source.html">type.h</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00050">ANY_TYPE</a>, and <a class="el" href="expr__manager_8h_source.html#l00454">CVC3::ExprManager::newLeafExpr()</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l01471">CVC3::TheoryCore::computeType()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l02969">CVC3::TheoryBitvector::computeType()</a>, <a class="el" href="theory__array_8cpp_source.html#l00810">CVC3::TheoryArray::computeType()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00878">CVC3::TheoryDatatype::dataType()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l00140">CVC3::TheoryQuant::TheoryQuant()</a>.</p>
</div>
</div>
<a class="anchor" id="a3ebf8a1ba9d894c33df064ea37c5ead5"></a><!-- doxytag: member="CVC3::Type::funType" ref="a3ebf8a1ba9d894c33df064ea37c5ead5" args="(const std::vector< Type > &typeDom, const Type &typeRan)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Type.html">Type</a> CVC3::Type::funType </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Type.html">Type</a> > & </td>
<td class="paramname"><em>typeDom</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>typeRan</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr_8cpp_source.html#l00641">641</a> of file <a class="el" href="expr_8cpp_source.html">expr.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00051">ARROW</a>, <a class="el" href="type_8h_source.html#l00052">getExpr()</a>, and <a class="el" href="type_8h_source.html#l00046">Type()</a>.</p>
<p>Referenced by <a class="el" href="theory__uf_8cpp_source.html#l00417">CVC3::TheoryUF::computeType()</a>, <a class="el" href="theory__simulate_8cpp_source.html#l00065">CVC3::TheorySimulate::computeType()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00878">CVC3::TheoryDatatype::dataType()</a>, and <a class="el" href="vcl_8cpp_source.html#l00864">CVC3::VCL::funType()</a>.</p>
</div>
</div>
<a class="anchor" id="a2c8b5f5720002766f6fab19157c3f6c0"></a><!-- doxytag: member="CVC3::Type::funType" ref="a2c8b5f5720002766f6fab19157c3f6c0" args="(const Type &typeRan) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Type.html">Type</a> CVC3::Type::funType </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Type.html">Type</a> & </td>
<td class="paramname"><em>typeRan</em></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="type_8h_source.html#l00076">76</a> of file <a class="el" href="type_8h_source.html">type.h</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00051">ARROW</a>, and <a class="el" href="type_8h_source.html#l00043">d_expr</a>.</p>
</div>
</div>
<a class="anchor" id="a2f5ce4b1973ec02b2f2b2eba8ce3cc50"></a><!-- doxytag: member="CVC3::Type::toString" ref="a2f5ce4b1973ec02b2f2b2eba8ce3cc50" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string CVC3::Type::toString </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="type_8h_source.html#l00080">80</a> of file <a class="el" href="type_8h_source.html">type.h</a>.</p>
<p>Referenced by <a class="el" href="theory_8cpp_source.html#l00738">CVC3::Theory::addBoundVar()</a>, <a class="el" href="vcl_8cpp_source.html#l01848">CVC3::VCL::assertFormula()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01575">CVC3::BitvectorTheoremProducer::bitExtractBitwise()</a>, <a class="el" href="search__sat_8cpp_source.html#l00638">CVC3::SearchSat::check()</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">CVC3::TheoryDatatype::checkSat()</a>, <a class="el" href="search__simple_8cpp_source.html#l00165">CVC3::SearchSimple::checkValidInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00471">CVC3::TheoryUF::computeBaseType()</a>, <a class="el" href="theory__records_8cpp_source.html#l00484">CVC3::TheoryRecords::computeBaseType()</a>, <a class="el" href="theory__core_8cpp_source.html#l01620">CVC3::TheoryCore::computeBaseType()</a>, <a class="el" href="theory__array_8cpp_source.html#l00887">CVC3::TheoryArray::computeBaseType()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03808">CVC3::TheoryArithOld::computeBaseType()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l02018">CVC3::TheoryArithNew::computeBaseType()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02830">CVC3::TheoryArith3::computeBaseType()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00417">CVC3::TheoryUF::computeType()</a>, <a class="el" href="theory__simulate_8cpp_source.html#l00065">CVC3::TheorySimulate::computeType()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08683">CVC3::TheoryQuant::computeType()</a>, <a class="el" href="theory__core_8cpp_source.html#l01471">CVC3::TheoryCore::computeType()</a>, <a class="el" href="theory__array_8cpp_source.html#l00810">CVC3::TheoryArray::computeType()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03725">CVC3::TheoryArithOld::computeType()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01936">CVC3::TheoryArithNew::computeType()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02747">CVC3::TheoryArith3::computeType()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l03411">CVC3::TheoryBitvector::computeTypePred()</a>, <a class="el" href="vcl_8cpp_source.html#l01181">CVC3::VCL::createOp()</a>, <a class="el" href="theory_8cpp_source.html#l00389">CVC3::Theory::getBaseType()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l01161">CVC3::TheoryDatatype::getConstant()</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">CVC3::TheoryDatatype::instantiate()</a>, <a class="el" href="theory_8cpp_source.html#l00647">CVC3::Theory::newFunction()</a>, <a class="el" href="theory_8cpp_source.html#l00569">CVC3::Theory::newVar()</a>, <a class="el" href="vcl_8cpp_source.html#l01929">CVC3::VCL::query()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08565">CVC3::TheoryQuant::recursiveMap()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02726">CVC3::TheoryArithOld::refineCounterExample()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01298">CVC3::TheoryArithNew::refineCounterExample()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02147">CVC3::TheoryArith3::refineCounterExample()</a>, <a class="el" href="search__simple_8cpp_source.html#l00207">CVC3::SearchSimple::restartInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01750">CVC3::SearchEngineFast::restartInternal()</a>, <a class="el" href="theory__core_8cpp_source.html#l00968">CVC3::TheoryCore::rewrite()</a>, and <a class="el" href="vcl_8cpp_source.html#l00910">CVC3::VCL::varExpr()</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="aa2fd6d88b18d9e9135cb2b9d59bdf20a"></a><!-- doxytag: member="CVC3::Type::d_expr" ref="aa2fd6d88b18d9e9135cb2b9d59bdf20a" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1Type.html#aa2fd6d88b18d9e9135cb2b9d59bdf20a">CVC3::Type::d_expr</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="type_8h_source.html#l00043">43</a> of file <a class="el" href="type_8h_source.html">type.h</a>.</p>
<p>Referenced by <a class="el" href="type_8h_source.html#l00076">funType()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="type_8h_source.html">type.h</a></li>
<li><a class="el" href="expr_8cpp_source.html">expr.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>
