<!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"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: CVC3::Expr Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<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="inherits.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_1Expr.html">Expr</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="summary">
<a href="#nested-classes">Classes</a> |
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pub-static-methods">Static Public Member Functions</a> |
<a href="#pri-types">Private Types</a> |
<a href="#pri-methods">Private Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> |
<a href="#pri-static-attribs">Static Private Attributes</a> |
<a href="#friends">Friends</a> |
<a href="classCVC3_1_1Expr-members.html">List of all members</a> </div>
<div class="headertitle">
<div class="title">CVC3::Expr Class Reference<div class="ingroups"><a class="el" href="group__ExprPkg.html">Expression Package</a></div></div> </div>
</div><!--header-->
<div class="contents">
<p>Data structure of expressions in <a class="el" href="namespaceCVC3.html">CVC3</a>.
<a href="classCVC3_1_1Expr.html#details">More...</a></p>
<p><code>#include <<a class="el" href="expr_8h_source.html">expr.h</a>></code></p>
<div class="dynheader">
Collaboration diagram for CVC3::Expr:</div>
<div class="dyncontent">
<div class="center"><img src="classCVC3_1_1Expr__coll__graph.gif" border="0" usemap="#CVC3_1_1Expr_coll__map" alt="Collaboration graph"/></div>
<map name="CVC3_1_1Expr_coll__map" id="CVC3_1_1Expr_coll__map">
</map>
</div>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="nested-classes"></a>
Classes</h2></td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">class  </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Expr_1_1iterator.html">iterator</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pub-methods"></a>
Public Member Functions</h2></td></tr>
<tr class="memitem:gaf3f35afa568a157d6f58ad24fd46b9d1"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaf3f35afa568a157d6f58ad24fd46b9d1">Expr</a> ()</td></tr>
<tr class="memdesc:gaf3f35afa568a157d6f58ad24fd46b9d1"><td class="mdescLeft"> </td><td class="mdescRight">Default constructor creates the Null <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="group__ExprPkg.html#gaf3f35afa568a157d6f58ad24fd46b9d1"></a><br/></td></tr>
<tr class="separator:gaf3f35afa568a157d6f58ad24fd46b9d1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga8e424c562e5d452d4ddc50f6e7b3e063"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga8e424c562e5d452d4ddc50f6e7b3e063">Expr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:ga8e424c562e5d452d4ddc50f6e7b3e063"><td class="mdescLeft"> </td><td class="mdescRight">Copy constructor and assignment (copy the pointer and take care of the refcount) <a href="group__ExprPkg.html#ga8e424c562e5d452d4ddc50f6e7b3e063"></a><br/></td></tr>
<tr class="separator:ga8e424c562e5d452d4ddc50f6e7b3e063"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga0cc4af99d81c96b3c529d3b866861550"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga0cc4af99d81c96b3c529d3b866861550">operator=</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:ga0cc4af99d81c96b3c529d3b866861550"><td class="mdescLeft"> </td><td class="mdescRight">Assignment operator: take care of the refcounting and GC. <a href="group__ExprPkg.html#ga0cc4af99d81c96b3c529d3b866861550"></a><br/></td></tr>
<tr class="separator:ga0cc4af99d81c96b3c529d3b866861550"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gafb0fbf8419f557068fc0f8293ecf1624"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gafb0fbf8419f557068fc0f8293ecf1624">Expr</a> (const <a class="el" href="classCVC3_1_1Op.html">Op</a> &op, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &child)</td></tr>
<tr class="separator:gafb0fbf8419f557068fc0f8293ecf1624"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga593d896e3c01b8596e57b822b948e6f2"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga593d896e3c01b8596e57b822b948e6f2">Expr</a> (const <a class="el" href="classCVC3_1_1Op.html">Op</a> &op, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &child0, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &child1)</td></tr>
<tr class="separator:ga593d896e3c01b8596e57b822b948e6f2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga67ac1e86cbda6dadb63c0739351fa19b"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga67ac1e86cbda6dadb63c0739351fa19b">Expr</a> (const <a class="el" href="classCVC3_1_1Op.html">Op</a> &op, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &child0, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &child1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &child2)</td></tr>
<tr class="separator:ga67ac1e86cbda6dadb63c0739351fa19b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga759ac04d93b19fcffd125924d668995e"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga759ac04d93b19fcffd125924d668995e">Expr</a> (const <a class="el" href="classCVC3_1_1Op.html">Op</a> &op, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &child0, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &child1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &child2, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &child3)</td></tr>
<tr class="separator:ga759ac04d93b19fcffd125924d668995e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaf6745550d2453e3e25af3bb9c4ea7a45"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaf6745550d2453e3e25af3bb9c4ea7a45">Expr</a> (const <a class="el" href="classCVC3_1_1Op.html">Op</a> &op, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &children, <a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> *em=NULL)</td></tr>
<tr class="separator:gaf6745550d2453e3e25af3bb9c4ea7a45"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga8be57c8709c3b35792306ea50cfc06d5"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga8be57c8709c3b35792306ea50cfc06d5">~Expr</a> ()</td></tr>
<tr class="memdesc:ga8be57c8709c3b35792306ea50cfc06d5"><td class="mdescLeft"> </td><td class="mdescRight">Destructor. <a href="group__ExprPkg.html#ga8be57c8709c3b35792306ea50cfc06d5"></a><br/></td></tr>
<tr class="separator:ga8be57c8709c3b35792306ea50cfc06d5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gacb48495ca445c895f95d0c3c1ae2070b"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gacb48495ca445c895f95d0c3c1ae2070b">eqExpr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &right) const </td></tr>
<tr class="separator:gacb48495ca445c895f95d0c3c1ae2070b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga59d07586d68ba39eadd98c86492acdac"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga59d07586d68ba39eadd98c86492acdac">notExpr</a> () const </td></tr>
<tr class="separator:ga59d07586d68ba39eadd98c86492acdac"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gab1ce461dc931af73bf04e88c8d37dcbc"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gab1ce461dc931af73bf04e88c8d37dcbc">negate</a> () const </td></tr>
<tr class="separator:gab1ce461dc931af73bf04e88c8d37dcbc"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga6c3651465ce69ed5f4e6fd461b9acf3c"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga6c3651465ce69ed5f4e6fd461b9acf3c">andExpr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &right) const </td></tr>
<tr class="separator:ga6c3651465ce69ed5f4e6fd461b9acf3c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaf310870d783fff343e77ba9c2277c626"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaf310870d783fff343e77ba9c2277c626">orExpr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &right) const </td></tr>
<tr class="separator:gaf310870d783fff343e77ba9c2277c626"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga5532cabad6f699c57da32a8db65a38da"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga5532cabad6f699c57da32a8db65a38da">iteExpr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &thenpart, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &elsepart) const </td></tr>
<tr class="separator:ga5532cabad6f699c57da32a8db65a38da"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaae017ca8e68af655ba285c985dd9fba5"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaae017ca8e68af655ba285c985dd9fba5">iffExpr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &right) const </td></tr>
<tr class="separator:gaae017ca8e68af655ba285c985dd9fba5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga8dd97bcdeb9d8870238f94a263fd083b"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga8dd97bcdeb9d8870238f94a263fd083b">impExpr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &right) const </td></tr>
<tr class="separator:ga8dd97bcdeb9d8870238f94a263fd083b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga37b3161a078f8992b71518992ab0b088"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga37b3161a078f8992b71518992ab0b088">xorExpr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &right) const </td></tr>
<tr class="separator:ga37b3161a078f8992b71518992ab0b088"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga1311a04a68f4cfae68a82826a3a0c5ad"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga1311a04a68f4cfae68a82826a3a0c5ad">skolemExpr</a> (int i) const </td></tr>
<tr class="memdesc:ga1311a04a68f4cfae68a82826a3a0c5ad"><td class="mdescLeft"> </td><td class="mdescRight">Create a Skolem constant for the i'th variable of an existential (*this) <a href="group__ExprPkg.html#ga1311a04a68f4cfae68a82826a3a0c5ad"></a><br/></td></tr>
<tr class="separator:ga1311a04a68f4cfae68a82826a3a0c5ad"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga3df149427d124797567614e07080519d"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga3df149427d124797567614e07080519d">rebuild</a> (<a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> *em) const </td></tr>
<tr class="memdesc:ga3df149427d124797567614e07080519d"><td class="mdescLeft"> </td><td class="mdescRight">Create a Boolean variable out of the expression. <a href="group__ExprPkg.html#ga3df149427d124797567614e07080519d"></a><br/></td></tr>
<tr class="separator:ga3df149427d124797567614e07080519d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga95e18015860195a80b317bf756055786"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga95e18015860195a80b317bf756055786">substExpr</a> (const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &oldTerms, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &newTerms) const </td></tr>
<tr class="separator:ga95e18015860195a80b317bf756055786"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga266ba75d3cf61c772b26a36ef5909a52"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga266ba75d3cf61c772b26a36ef5909a52">substExpr</a> (const <a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &oldToNew) const </td></tr>
<tr class="separator:ga266ba75d3cf61c772b26a36ef5909a52"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga7cbbc123771321651e176a346731d255"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga7cbbc123771321651e176a346731d255">substExprQuant</a> (const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &oldTerms, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &newTerms) const </td></tr>
<tr class="separator:ga7cbbc123771321651e176a346731d255"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga6d955aae7246b6e55c7de394fe7895d4"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga6d955aae7246b6e55c7de394fe7895d4">substExprQuant</a> (const <a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &oldToNew) const </td></tr>
<tr class="separator:ga6d955aae7246b6e55c7de394fe7895d4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gab13e5c897123bbde4b24e9571d27a88c"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gab13e5c897123bbde4b24e9571d27a88c">operator!</a> () const </td></tr>
<tr class="separator:gab13e5c897123bbde4b24e9571d27a88c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga0fff31138ef63bbc3a7defd92af9fca2"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga0fff31138ef63bbc3a7defd92af9fca2">operator&&</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &right) const </td></tr>
<tr class="separator:ga0fff31138ef63bbc3a7defd92af9fca2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga909307189b2a1c7e122d139ce6f093f0"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga909307189b2a1c7e122d139ce6f093f0">operator||</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &right) const </td></tr>
<tr class="separator:ga909307189b2a1c7e122d139ce6f093f0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gae11bd9d6d259d280c77cb1778520daa4"><td class="memItemLeft" align="right" valign="top">size_t </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gae11bd9d6d259d280c77cb1778520daa4">hash</a> () const </td></tr>
<tr class="separator:gae11bd9d6d259d280c77cb1778520daa4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga6173f64b22cba76472cd0c814bbf6dae"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga6173f64b22cba76472cd0c814bbf6dae">isFalse</a> () const </td></tr>
<tr class="separator:ga6173f64b22cba76472cd0c814bbf6dae"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gadf8596df73fa69ff8e6a22b9321f5c34"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gadf8596df73fa69ff8e6a22b9321f5c34">isTrue</a> () const </td></tr>
<tr class="separator:gadf8596df73fa69ff8e6a22b9321f5c34"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga5c2cee598096c66e80d87490d6505bc4"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga5c2cee598096c66e80d87490d6505bc4">isBoolConst</a> () const </td></tr>
<tr class="separator:ga5c2cee598096c66e80d87490d6505bc4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga55b6a203b4375e64598306596851d9ae"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga55b6a203b4375e64598306596851d9ae">isVar</a> () const </td></tr>
<tr class="separator:ga55b6a203b4375e64598306596851d9ae"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga01122f4c0d9a19d9b991600e480cc862"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga01122f4c0d9a19d9b991600e480cc862">isBoundVar</a> () const </td></tr>
<tr class="separator:ga01122f4c0d9a19d9b991600e480cc862"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga72034a21a6bcbd4d5d2085aa23c8f290"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga72034a21a6bcbd4d5d2085aa23c8f290">isString</a> () const </td></tr>
<tr class="separator:ga72034a21a6bcbd4d5d2085aa23c8f290"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga3127f52184d5bcb2d4056cb23f3a292b"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga3127f52184d5bcb2d4056cb23f3a292b">isClosure</a> () const </td></tr>
<tr class="separator:ga3127f52184d5bcb2d4056cb23f3a292b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga35249e04af38d4641c873e358188d47a"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga35249e04af38d4641c873e358188d47a">isQuantifier</a> () const </td></tr>
<tr class="separator:ga35249e04af38d4641c873e358188d47a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga165dba5b9e9502059c3cf01bddf4fe1e"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga165dba5b9e9502059c3cf01bddf4fe1e">isLambda</a> () const </td></tr>
<tr class="separator:ga165dba5b9e9502059c3cf01bddf4fe1e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga1d6a6b4a9ce81b0dd8fd74870ff4284b"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga1d6a6b4a9ce81b0dd8fd74870ff4284b">isApply</a> () const </td></tr>
<tr class="separator:ga1d6a6b4a9ce81b0dd8fd74870ff4284b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga93059bf6ddd8020cef4e6796a3c9b5a4"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga93059bf6ddd8020cef4e6796a3c9b5a4">isSymbol</a> () const </td></tr>
<tr class="separator:ga93059bf6ddd8020cef4e6796a3c9b5a4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga8ec720fa4004f3f7036b0fba87393d83"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga8ec720fa4004f3f7036b0fba87393d83">isTheorem</a> () const </td></tr>
<tr class="separator:ga8ec720fa4004f3f7036b0fba87393d83"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga3c3645e1962f6de72655c650639e7a2d"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga3c3645e1962f6de72655c650639e7a2d">isConstant</a> () const </td></tr>
<tr class="separator:ga3c3645e1962f6de72655c650639e7a2d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga61d63967e5419f6d32eb153e7e39a913"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga61d63967e5419f6d32eb153e7e39a913">isRawList</a> () const </td></tr>
<tr class="separator:ga61d63967e5419f6d32eb153e7e39a913"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaea43cdb4de7c9216d0adcc1807a6eccc"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaea43cdb4de7c9216d0adcc1807a6eccc">isType</a> () const </td></tr>
<tr class="memdesc:gaea43cdb4de7c9216d0adcc1807a6eccc"><td class="mdescLeft"> </td><td class="mdescRight"><a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> represents a type. <a href="group__ExprPkg.html#gaea43cdb4de7c9216d0adcc1807a6eccc"></a><br/></td></tr>
<tr class="separator:gaea43cdb4de7c9216d0adcc1807a6eccc"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gad21442cf6ecf46e8fcccbef451f4041b"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gad21442cf6ecf46e8fcccbef451f4041b">getExprValue</a> () const </td></tr>
<tr class="memdesc:gad21442cf6ecf46e8fcccbef451f4041b"><td class="mdescLeft"> </td><td class="mdescRight">Provide access to <a class="el" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a> for client subclasses of <a class="el" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a> <em>only</em> <a href="group__ExprPkg.html#gad21442cf6ecf46e8fcccbef451f4041b"></a><br/></td></tr>
<tr class="separator:gad21442cf6ecf46e8fcccbef451f4041b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gad527acb49daef3591b78c748746e7eef"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gad527acb49daef3591b78c748746e7eef">isTerm</a> () const </td></tr>
<tr class="memdesc:gad527acb49daef3591b78c748746e7eef"><td class="mdescLeft"> </td><td class="mdescRight">Test if e is a term (as opposed to a predicate/formula) <a href="group__ExprPkg.html#gad527acb49daef3591b78c748746e7eef"></a><br/></td></tr>
<tr class="separator:gad527acb49daef3591b78c748746e7eef"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga48a9219339b394280550069ac7b0474f"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga48a9219339b394280550069ac7b0474f">isAtomic</a> () const </td></tr>
<tr class="memdesc:ga48a9219339b394280550069ac7b0474f"><td class="mdescLeft"> </td><td class="mdescRight">Test if e is atomic. <a href="group__ExprPkg.html#ga48a9219339b394280550069ac7b0474f"></a><br/></td></tr>
<tr class="separator:ga48a9219339b394280550069ac7b0474f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga4b575e0a191cc42706ff5b5a169c3069"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga4b575e0a191cc42706ff5b5a169c3069">isAtomicFormula</a> () const </td></tr>
<tr class="memdesc:ga4b575e0a191cc42706ff5b5a169c3069"><td class="mdescLeft"> </td><td class="mdescRight">Test if e is an atomic formula. <a href="group__ExprPkg.html#ga4b575e0a191cc42706ff5b5a169c3069"></a><br/></td></tr>
<tr class="separator:ga4b575e0a191cc42706ff5b5a169c3069"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga5fe5158aefab64fd8adda48ecebb98f9"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga5fe5158aefab64fd8adda48ecebb98f9">isAbsAtomicFormula</a> () const </td></tr>
<tr class="memdesc:ga5fe5158aefab64fd8adda48ecebb98f9"><td class="mdescLeft"> </td><td class="mdescRight">An abstract atomic formua is an atomic formula or a quantified formula. <a href="group__ExprPkg.html#ga5fe5158aefab64fd8adda48ecebb98f9"></a><br/></td></tr>
<tr class="separator:ga5fe5158aefab64fd8adda48ecebb98f9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga26619060de89ad70f1f63a20b4d8d020"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga26619060de89ad70f1f63a20b4d8d020">isLiteral</a> () const </td></tr>
<tr class="memdesc:ga26619060de89ad70f1f63a20b4d8d020"><td class="mdescLeft"> </td><td class="mdescRight">Test if e is a literal. <a href="group__ExprPkg.html#ga26619060de89ad70f1f63a20b4d8d020"></a><br/></td></tr>
<tr class="separator:ga26619060de89ad70f1f63a20b4d8d020"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaac535dae48f02fcd093a5b1b1a062211"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaac535dae48f02fcd093a5b1b1a062211">isAbsLiteral</a> () const </td></tr>
<tr class="memdesc:gaac535dae48f02fcd093a5b1b1a062211"><td class="mdescLeft"> </td><td class="mdescRight">Test if e is an abstract literal. <a href="group__ExprPkg.html#gaac535dae48f02fcd093a5b1b1a062211"></a><br/></td></tr>
<tr class="separator:gaac535dae48f02fcd093a5b1b1a062211"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gac03948739e860fa791fd3bbb713c1076"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gac03948739e860fa791fd3bbb713c1076">isBoolConnective</a> () const </td></tr>
<tr class="memdesc:gac03948739e860fa791fd3bbb713c1076"><td class="mdescLeft"> </td><td class="mdescRight">A Bool connective is one of NOT,AND,OR,IMPLIES,IFF,XOR,ITE (with type Bool) <a href="group__ExprPkg.html#gac03948739e860fa791fd3bbb713c1076"></a><br/></td></tr>
<tr class="separator:gac03948739e860fa791fd3bbb713c1076"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gad8c63abfec9cc4a8319f3df1b47eee45"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gad8c63abfec9cc4a8319f3df1b47eee45">isPropAtom</a> () const </td></tr>
<tr class="memdesc:gad8c63abfec9cc4a8319f3df1b47eee45"><td class="mdescLeft"> </td><td class="mdescRight">True iff expr is not a Bool connective. <a href="group__ExprPkg.html#gad8c63abfec9cc4a8319f3df1b47eee45"></a><br/></td></tr>
<tr class="separator:gad8c63abfec9cc4a8319f3df1b47eee45"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaccf96ea73570e38c5c7e4ad39ed8b509"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaccf96ea73570e38c5c7e4ad39ed8b509">isPropLiteral</a> () const </td></tr>
<tr class="memdesc:gaccf96ea73570e38c5c7e4ad39ed8b509"><td class="mdescLeft"> </td><td class="mdescRight">PropAtom or negation of PropAtom. <a href="group__ExprPkg.html#gaccf96ea73570e38c5c7e4ad39ed8b509"></a><br/></td></tr>
<tr class="separator:gaccf96ea73570e38c5c7e4ad39ed8b509"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaf53e6a6f9dc01481d2cf94673c5505ce"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaf53e6a6f9dc01481d2cf94673c5505ce">containsTermITE</a> () const </td></tr>
<tr class="memdesc:gaf53e6a6f9dc01481d2cf94673c5505ce"><td class="mdescLeft"> </td><td class="mdescRight">Return whether <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> contains a non-bool type ITE as a sub-term. <a href="group__ExprPkg.html#gaf53e6a6f9dc01481d2cf94673c5505ce"></a><br/></td></tr>
<tr class="separator:gaf53e6a6f9dc01481d2cf94673c5505ce"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gac4af2026c180da0f18d66ac616f61f3a"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gac4af2026c180da0f18d66ac616f61f3a">isEq</a> () const </td></tr>
<tr class="separator:gac4af2026c180da0f18d66ac616f61f3a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga1a898858ccadce833df5a294c7740f11"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a> () const </td></tr>
<tr class="separator:ga1a898858ccadce833df5a294c7740f11"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga383260cf4f8919728e2712e6e11f21fa"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga383260cf4f8919728e2712e6e11f21fa">isAnd</a> () const </td></tr>
<tr class="separator:ga383260cf4f8919728e2712e6e11f21fa"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga36f1eff876808586db368dc1b6da5f56"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga36f1eff876808586db368dc1b6da5f56">isOr</a> () const </td></tr>
<tr class="separator:ga36f1eff876808586db368dc1b6da5f56"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaef13fa4752a1fb28e129a1efd0e26f01"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaef13fa4752a1fb28e129a1efd0e26f01">isITE</a> () const </td></tr>
<tr class="separator:gaef13fa4752a1fb28e129a1efd0e26f01"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gabe385fb97505cccb75702378511c5375"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gabe385fb97505cccb75702378511c5375">isIff</a> () const </td></tr>
<tr class="separator:gabe385fb97505cccb75702378511c5375"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga9067c706c6454ea1761ace7d7837af46"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga9067c706c6454ea1761ace7d7837af46">isImpl</a> () const </td></tr>
<tr class="separator:ga9067c706c6454ea1761ace7d7837af46"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gace27719ae0da2a171560b9fda9e10c8b"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gace27719ae0da2a171560b9fda9e10c8b">isXor</a> () const </td></tr>
<tr class="separator:gace27719ae0da2a171560b9fda9e10c8b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaad6095e1d8b1551a006602d9421fb988"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a> () const </td></tr>
<tr class="separator:gaad6095e1d8b1551a006602d9421fb988"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga1c922163af59ed6bc101728d65e04d16"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga1c922163af59ed6bc101728d65e04d16">isExists</a> () const </td></tr>
<tr class="separator:ga1c922163af59ed6bc101728d65e04d16"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gac5ced6adc7a60945ea6707ef494aa28f"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gac5ced6adc7a60945ea6707ef494aa28f">isRational</a> () const </td></tr>
<tr class="separator:gac5ced6adc7a60945ea6707ef494aa28f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gab181584fa647ee5ef5f10e9050225562"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gab181584fa647ee5ef5f10e9050225562">isSkolem</a> () const </td></tr>
<tr class="separator:gab181584fa647ee5ef5f10e9050225562"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaa3023d9117f249f079b0a202a1dfc5c2"><td class="memItemLeft" align="right" valign="top">const std::string & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaa3023d9117f249f079b0a202a1dfc5c2">getName</a> () const </td></tr>
<tr class="separator:gaa3023d9117f249f079b0a202a1dfc5c2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga2b086a0194b24a3f31afd402cea7de94"><td class="memItemLeft" align="right" valign="top">const std::string & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga2b086a0194b24a3f31afd402cea7de94">getUid</a> () const </td></tr>
<tr class="memdesc:ga2b086a0194b24a3f31afd402cea7de94"><td class="mdescLeft"> </td><td class="mdescRight">For BOUND_VAR, get the UID. <a href="group__ExprPkg.html#ga2b086a0194b24a3f31afd402cea7de94"></a><br/></td></tr>
<tr class="separator:ga2b086a0194b24a3f31afd402cea7de94"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga5e679ab39ad8166c3c027afee9004c26"><td class="memItemLeft" align="right" valign="top">const std::string & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga5e679ab39ad8166c3c027afee9004c26">getString</a> () const </td></tr>
<tr class="separator:ga5e679ab39ad8166c3c027afee9004c26"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaad22e223d0e273780557aca9d87620cd"><td class="memItemLeft" align="right" valign="top">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd">getVars</a> () const </td></tr>
<tr class="memdesc:gaad22e223d0e273780557aca9d87620cd"><td class="mdescLeft"> </td><td class="mdescRight">Get bound variables from a closure <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd"></a><br/></td></tr>
<tr class="separator:gaad22e223d0e273780557aca9d87620cd"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaf12c1f078a1106ba7d7896c45b2eb4cb"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaf12c1f078a1106ba7d7896c45b2eb4cb">getExistential</a> () const </td></tr>
<tr class="memdesc:gaf12c1f078a1106ba7d7896c45b2eb4cb"><td class="mdescLeft"> </td><td class="mdescRight">Get the existential axiom expression for skolem constant. <a href="group__ExprPkg.html#gaf12c1f078a1106ba7d7896c45b2eb4cb"></a><br/></td></tr>
<tr class="separator:gaf12c1f078a1106ba7d7896c45b2eb4cb"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga58d51b54987242f54071bdcc0d7d183f"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga58d51b54987242f54071bdcc0d7d183f">getBoundIndex</a> () const </td></tr>
<tr class="memdesc:ga58d51b54987242f54071bdcc0d7d183f"><td class="mdescLeft"> </td><td class="mdescRight">Get the index of the bound var that skolem constant comes from. <a href="group__ExprPkg.html#ga58d51b54987242f54071bdcc0d7d183f"></a><br/></td></tr>
<tr class="separator:ga58d51b54987242f54071bdcc0d7d183f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga9060193194020fee3dac69ed1876a940"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940">getBody</a> () const </td></tr>
<tr class="memdesc:ga9060193194020fee3dac69ed1876a940"><td class="mdescLeft"> </td><td class="mdescRight">Get the body of the closure <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940"></a><br/></td></tr>
<tr class="separator:ga9060193194020fee3dac69ed1876a940"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gad15dc19335e0f59dddbb75d1d27579e7"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gad15dc19335e0f59dddbb75d1d27579e7">setTriggers</a> (const std::vector< std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > > &triggers) const </td></tr>
<tr class="memdesc:gad15dc19335e0f59dddbb75d1d27579e7"><td class="mdescLeft"> </td><td class="mdescRight">Set the triggers for a closure <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="group__ExprPkg.html#gad15dc19335e0f59dddbb75d1d27579e7"></a><br/></td></tr>
<tr class="separator:gad15dc19335e0f59dddbb75d1d27579e7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga05ec7fb847036e29c782c3595f758a70"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga05ec7fb847036e29c782c3595f758a70">setTriggers</a> (const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &triggers) const </td></tr>
<tr class="separator:ga05ec7fb847036e29c782c3595f758a70"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga4e0dcc7b987305b845414ce0a7089381"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga4e0dcc7b987305b845414ce0a7089381">setTrigger</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &trigger) const </td></tr>
<tr class="separator:ga4e0dcc7b987305b845414ce0a7089381"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga91a460603cf210681cfdec52a98fa076"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga91a460603cf210681cfdec52a98fa076">setMultiTrigger</a> (const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &multiTrigger) const </td></tr>
<tr class="separator:ga91a460603cf210681cfdec52a98fa076"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gae4cffec57be4b7d81e8486328c2396fc"><td class="memItemLeft" align="right" valign="top">const std::vector< std::vector<br class="typebreak"/>
< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > > & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gae4cffec57be4b7d81e8486328c2396fc">getTriggers</a> () const </td></tr>
<tr class="memdesc:gae4cffec57be4b7d81e8486328c2396fc"><td class="mdescLeft"> </td><td class="mdescRight">Get the manual triggers of the closure <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="group__ExprPkg.html#gae4cffec57be4b7d81e8486328c2396fc"></a><br/></td></tr>
<tr class="separator:gae4cffec57be4b7d81e8486328c2396fc"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gab0eee70e4a7f97c09954dc61b71b65e5"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Rational.html">Rational</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gab0eee70e4a7f97c09954dc61b71b65e5">getRational</a> () const </td></tr>
<tr class="memdesc:gab0eee70e4a7f97c09954dc61b71b65e5"><td class="mdescLeft"> </td><td class="mdescRight">Get the <a class="el" href="classCVC3_1_1Rational.html">Rational</a> value out of RATIONAL_EXPR. <a href="group__ExprPkg.html#gab0eee70e4a7f97c09954dc61b71b65e5"></a><br/></td></tr>
<tr class="separator:gab0eee70e4a7f97c09954dc61b71b65e5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga29db2c821567c944bc14f8156eb092b6"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga29db2c821567c944bc14f8156eb092b6">getTheorem</a> () const </td></tr>
<tr class="memdesc:ga29db2c821567c944bc14f8156eb092b6"><td class="mdescLeft"> </td><td class="mdescRight">Get theorem from THEOREM_EXPR. <a href="group__ExprPkg.html#ga29db2c821567c944bc14f8156eb092b6"></a><br/></td></tr>
<tr class="separator:ga29db2c821567c944bc14f8156eb092b6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gab57ce3dfa78947a906241d090c7cf34d"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a> () const </td></tr>
<tr class="separator:gab57ce3dfa78947a906241d090c7cf34d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga1e18ae89889e781591eb2874a4196b73"><td class="memItemLeft" align="right" valign="top">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga1e18ae89889e781591eb2874a4196b73">getKids</a> () const </td></tr>
<tr class="separator:ga1e18ae89889e781591eb2874a4196b73"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga7814e4f55f65c7ca860c637413df5f4d"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a> () const </td></tr>
<tr class="separator:ga7814e4f55f65c7ca860c637413df5f4d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gadaddb9b0566ecddd4611a10e820dc544"><td class="memItemLeft" align="right" valign="top"><a class="el" href="namespaceCVC3.html#a4233916514848331ee104548acbab912">ExprIndex</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gadaddb9b0566ecddd4611a10e820dc544">getIndex</a> () const </td></tr>
<tr class="separator:gadaddb9b0566ecddd4611a10e820dc544"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaa930fda58c8146f27f3dacaab017015c"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaa930fda58c8146f27f3dacaab017015c">hasLastIndex</a> () const </td></tr>
<tr class="separator:gaa930fda58c8146f27f3dacaab017015c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga3aefe2fb15c2d8e3a51dd92dbcc5cdc5"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Op.html">Op</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga3aefe2fb15c2d8e3a51dd92dbcc5cdc5">mkOp</a> () const </td></tr>
<tr class="memdesc:ga3aefe2fb15c2d8e3a51dd92dbcc5cdc5"><td class="mdescLeft"> </td><td class="mdescRight">Make the expr into an operator. <a href="group__ExprPkg.html#ga3aefe2fb15c2d8e3a51dd92dbcc5cdc5"></a><br/></td></tr>
<tr class="separator:ga3aefe2fb15c2d8e3a51dd92dbcc5cdc5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gace479f04faca399219496195152f7806"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Op.html">Op</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gace479f04faca399219496195152f7806">getOp</a> () const </td></tr>
<tr class="memdesc:gace479f04faca399219496195152f7806"><td class="mdescLeft"> </td><td class="mdescRight">Get operator from expression. <a href="group__ExprPkg.html#gace479f04faca399219496195152f7806"></a><br/></td></tr>
<tr class="separator:gace479f04faca399219496195152f7806"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga9f3328fe077191803a780cfd6566ff9b"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga9f3328fe077191803a780cfd6566ff9b">getOpExpr</a> () const </td></tr>
<tr class="memdesc:ga9f3328fe077191803a780cfd6566ff9b"><td class="mdescLeft"> </td><td class="mdescRight">Get expression of operator (for APPLY Exprs only) <a href="group__ExprPkg.html#ga9f3328fe077191803a780cfd6566ff9b"></a><br/></td></tr>
<tr class="separator:ga9f3328fe077191803a780cfd6566ff9b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gad036a3a3597d590ca6ee694505c6e1cd"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gad036a3a3597d590ca6ee694505c6e1cd">getOpKind</a> () const </td></tr>
<tr class="memdesc:gad036a3a3597d590ca6ee694505c6e1cd"><td class="mdescLeft"> </td><td class="mdescRight">Get kind of operator (for APPLY Exprs only) <a href="group__ExprPkg.html#gad036a3a3597d590ca6ee694505c6e1cd"></a><br/></td></tr>
<tr class="separator:gad036a3a3597d590ca6ee694505c6e1cd"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga28b901d05e52a5c646f83a95cc74f94b"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a> () const </td></tr>
<tr class="separator:ga28b901d05e52a5c646f83a95cc74f94b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga5b242a4834df256dc2055e310fb0e727"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga5b242a4834df256dc2055e310fb0e727">operator[]</a> (int i) const </td></tr>
<tr class="separator:ga5b242a4834df256dc2055e310fb0e727"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga39070a3fb12c398dc5bb7526d6aeb7f3"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga39070a3fb12c398dc5bb7526d6aeb7f3">unnegate</a> () const </td></tr>
<tr class="memdesc:ga39070a3fb12c398dc5bb7526d6aeb7f3"><td class="mdescLeft"> </td><td class="mdescRight">Remove leading NOT if any. <a href="group__ExprPkg.html#ga39070a3fb12c398dc5bb7526d6aeb7f3"></a><br/></td></tr>
<tr class="separator:ga39070a3fb12c398dc5bb7526d6aeb7f3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gac890e13db184610276fc533fa4b4fe99"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr_1_1iterator.html">iterator</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gac890e13db184610276fc533fa4b4fe99">begin</a> () const </td></tr>
<tr class="memdesc:gac890e13db184610276fc533fa4b4fe99"><td class="mdescLeft"> </td><td class="mdescRight">Begin iterator. <a href="group__ExprPkg.html#gac890e13db184610276fc533fa4b4fe99"></a><br/></td></tr>
<tr class="separator:gac890e13db184610276fc533fa4b4fe99"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaf6048a5030c8fa2511bf5dfee868e653"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr_1_1iterator.html">iterator</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaf6048a5030c8fa2511bf5dfee868e653">end</a> () const </td></tr>
<tr class="memdesc:gaf6048a5030c8fa2511bf5dfee868e653"><td class="mdescLeft"> </td><td class="mdescRight">End iterator. <a href="group__ExprPkg.html#gaf6048a5030c8fa2511bf5dfee868e653"></a><br/></td></tr>
<tr class="separator:gaf6048a5030c8fa2511bf5dfee868e653"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga0265d1ca42fa59c95aaff3ca675b6504"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a> () const </td></tr>
<tr class="separator:ga0265d1ca42fa59c95aaff3ca675b6504"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaa3359d5f6638eba5479c4c4036a551a8"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaa3359d5f6638eba5479c4c4036a551a8">isInitialized</a> () const </td></tr>
<tr class="separator:gaa3359d5f6638eba5479c4c4036a551a8"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaca3ae54b26443a7d5a74cc7d6f5e81e3"><td class="memItemLeft" align="right" valign="top">size_t </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaca3ae54b26443a7d5a74cc7d6f5e81e3">getMMIndex</a> () const </td></tr>
<tr class="memdesc:gaca3ae54b26443a7d5a74cc7d6f5e81e3"><td class="mdescLeft"> </td><td class="mdescRight">Get the memory manager index (it uniquely identifies the subclass) <a href="group__ExprPkg.html#gaca3ae54b26443a7d5a74cc7d6f5e81e3"></a><br/></td></tr>
<tr class="separator:gaca3ae54b26443a7d5a74cc7d6f5e81e3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga4dc94c33ae308ff8d9d004f49df8f42b"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga4dc94c33ae308ff8d9d004f49df8f42b">hasFind</a> () const </td></tr>
<tr class="separator:ga4dc94c33ae308ff8d9d004f49df8f42b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga9be55edbdc2c0878fec750921a9fcc89"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga9be55edbdc2c0878fec750921a9fcc89">getFind</a> () const </td></tr>
<tr class="separator:ga9be55edbdc2c0878fec750921a9fcc89"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga45ea7926a65c7c5559c81f1f20bde281"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga45ea7926a65c7c5559c81f1f20bde281">getFindLevel</a> () const </td></tr>
<tr class="separator:ga45ea7926a65c7c5559c81f1f20bde281"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaac6e2bdafe4cb6b91d4bec8fa656bcb2"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaac6e2bdafe4cb6b91d4bec8fa656bcb2">getEqNext</a> () const </td></tr>
<tr class="separator:gaac6e2bdafe4cb6b91d4bec8fa656bcb2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gace67f5f11fd81d9ecebba441b8c02e07"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1NotifyList.html">NotifyList</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gace67f5f11fd81d9ecebba441b8c02e07">getNotify</a> () const </td></tr>
<tr class="separator:gace67f5f11fd81d9ecebba441b8c02e07"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga42929221eb172250697b72c28af6de07"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Type.html">Type</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga42929221eb172250697b72c28af6de07">getType</a> () const </td></tr>
<tr class="memdesc:ga42929221eb172250697b72c28af6de07"><td class="mdescLeft"> </td><td class="mdescRight">Get the type. Recursively compute if necessary. <a href="group__ExprPkg.html#ga42929221eb172250697b72c28af6de07"></a><br/></td></tr>
<tr class="separator:ga42929221eb172250697b72c28af6de07"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga801d77a373d26549c735dbd8a7fda1a5"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Type.html">Type</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga801d77a373d26549c735dbd8a7fda1a5">lookupType</a> () const </td></tr>
<tr class="memdesc:ga801d77a373d26549c735dbd8a7fda1a5"><td class="mdescLeft"> </td><td class="mdescRight">Look up the current type. Do not recursively compute (i.e. may be NULL) <a href="group__ExprPkg.html#ga801d77a373d26549c735dbd8a7fda1a5"></a><br/></td></tr>
<tr class="separator:ga801d77a373d26549c735dbd8a7fda1a5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga9030cf2556acc13a160355c55e0a1b4e"><td class="memItemLeft" align="right" valign="top"><a class="el" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54">Cardinality</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga9030cf2556acc13a160355c55e0a1b4e">typeCard</a> () const </td></tr>
<tr class="memdesc:ga9030cf2556acc13a160355c55e0a1b4e"><td class="mdescLeft"> </td><td class="mdescRight">Return cardinality of type. <a href="group__ExprPkg.html#ga9030cf2556acc13a160355c55e0a1b4e"></a><br/></td></tr>
<tr class="separator:ga9030cf2556acc13a160355c55e0a1b4e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga9abac5907964bb1ca7d6ad7d1280791c"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga9abac5907964bb1ca7d6ad7d1280791c">typeEnumerateFinite</a> (<a class="el" href="classCVC3_1_1Unsigned.html">Unsigned</a> n) const </td></tr>
<tr class="memdesc:ga9abac5907964bb1ca7d6ad7d1280791c"><td class="mdescLeft"> </td><td class="mdescRight">Return nth (starting with 0) element in a finite type. <a href="group__ExprPkg.html#ga9abac5907964bb1ca7d6ad7d1280791c"></a><br/></td></tr>
<tr class="separator:ga9abac5907964bb1ca7d6ad7d1280791c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaefc32b444057849c6364e63b7d4c3cf3"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Unsigned.html">Unsigned</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaefc32b444057849c6364e63b7d4c3cf3">typeSizeFinite</a> () const </td></tr>
<tr class="memdesc:gaefc32b444057849c6364e63b7d4c3cf3"><td class="mdescLeft"> </td><td class="mdescRight">Return size of a finite type; returns 0 if size cannot be determined. <a href="group__ExprPkg.html#gaefc32b444057849c6364e63b7d4c3cf3"></a><br/></td></tr>
<tr class="separator:gaefc32b444057849c6364e63b7d4c3cf3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga99348741c5062f8c8e62962b787a73fd"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga99348741c5062f8c8e62962b787a73fd">validSimpCache</a> () const </td></tr>
<tr class="memdesc:ga99348741c5062f8c8e62962b787a73fd"><td class="mdescLeft"> </td><td class="mdescRight">Return true if there is a valid cached value for calling simplify on this <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="group__ExprPkg.html#ga99348741c5062f8c8e62962b787a73fd"></a><br/></td></tr>
<tr class="separator:ga99348741c5062f8c8e62962b787a73fd"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga5dbb07a3a7f3a7154ad3bcdb58bbdec6"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga5dbb07a3a7f3a7154ad3bcdb58bbdec6">getSimpCache</a> () const </td></tr>
<tr class="separator:ga5dbb07a3a7f3a7154ad3bcdb58bbdec6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaed5d5a14a8089122a0e05a55e38fc37f"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaed5d5a14a8089122a0e05a55e38fc37f">isValidType</a> () const </td></tr>
<tr class="separator:gaed5d5a14a8089122a0e05a55e38fc37f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga501126e42edf75538f510b7b87df96f1"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga501126e42edf75538f510b7b87df96f1">validIsAtomicFlag</a> () const </td></tr>
<tr class="separator:ga501126e42edf75538f510b7b87df96f1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga0016a263d60de73f5924072848515699"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga0016a263d60de73f5924072848515699">validTerminalsConstFlag</a> () const </td></tr>
<tr class="separator:ga0016a263d60de73f5924072848515699"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaaa895b97bdc2413b72419cc781178995"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaaa895b97bdc2413b72419cc781178995">getIsAtomicFlag</a> () const </td></tr>
<tr class="separator:gaaa895b97bdc2413b72419cc781178995"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gab990a9104757ac6854b92c3b98727b9c"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gab990a9104757ac6854b92c3b98727b9c">getTerminalsConstFlag</a> () const </td></tr>
<tr class="separator:gab990a9104757ac6854b92c3b98727b9c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gad27a864cc3351877b2b132f3dfe4ac1c"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gad27a864cc3351877b2b132f3dfe4ac1c">isRewriteNormal</a> () const </td></tr>
<tr class="separator:gad27a864cc3351877b2b132f3dfe4ac1c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gacf628bd70fc2c4766afa268ed22ea947"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gacf628bd70fc2c4766afa268ed22ea947">isFinite</a> () const </td></tr>
<tr class="separator:gacf628bd70fc2c4766afa268ed22ea947"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaa7dc360962f097870ecc6a4cc14c4909"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaa7dc360962f097870ecc6a4cc14c4909">isWellFounded</a> () const </td></tr>
<tr class="separator:gaa7dc360962f097870ecc6a4cc14c4909"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gac3aeac6fba7a1d6cacfe4bd653c5a084"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gac3aeac6fba7a1d6cacfe4bd653c5a084">computeTransClosure</a> () const </td></tr>
<tr class="separator:gac3aeac6fba7a1d6cacfe4bd653c5a084"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gacafcbc459ee158f84e3666eaf32ca3f9"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gacafcbc459ee158f84e3666eaf32ca3f9">containsBoundVar</a> () const </td></tr>
<tr class="separator:gacafcbc459ee158f84e3666eaf32ca3f9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga0f1f1ce3472f18a4b6575805e0347bce"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga0f1f1ce3472f18a4b6575805e0347bce">usesCC</a> () const </td></tr>
<tr class="separator:ga0f1f1ce3472f18a4b6575805e0347bce"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaabb885ae903ae169ed75137653dc2538"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaabb885ae903ae169ed75137653dc2538">notArrayNormalized</a> () const </td></tr>
<tr class="separator:gaabb885ae903ae169ed75137653dc2538"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga5d92d645899807eb4351502f2e74369e"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga5d92d645899807eb4351502f2e74369e">isImpliedLiteral</a> () const </td></tr>
<tr class="separator:ga5d92d645899807eb4351502f2e74369e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gadeefef680b6323acc5d79a553644be8e"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gadeefef680b6323acc5d79a553644be8e">isUserAssumption</a> () const </td></tr>
<tr class="separator:gadeefef680b6323acc5d79a553644be8e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga110d4a1734b738dbb999b7798e07c3d1"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga110d4a1734b738dbb999b7798e07c3d1">inUserAssumption</a> () const </td></tr>
<tr class="separator:ga110d4a1734b738dbb999b7798e07c3d1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaf42121131fd56040faef7a64d9e67729"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaf42121131fd56040faef7a64d9e67729">isIntAssumption</a> () const </td></tr>
<tr class="separator:gaf42121131fd56040faef7a64d9e67729"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga3cf472ba2fa033f3e1401e4b67a3f8a0"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga3cf472ba2fa033f3e1401e4b67a3f8a0">isJustified</a> () const </td></tr>
<tr class="separator:ga3cf472ba2fa033f3e1401e4b67a3f8a0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gabe0b99a2c155f75ceedd4f06263ddebb"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gabe0b99a2c155f75ceedd4f06263ddebb">isTranslated</a> () const </td></tr>
<tr class="separator:gabe0b99a2c155f75ceedd4f06263ddebb"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga8296386eb481a436937b6f0b140f8af0"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga8296386eb481a436937b6f0b140f8af0">isUserRegisteredAtom</a> () const </td></tr>
<tr class="separator:ga8296386eb481a436937b6f0b140f8af0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga8b55ff94d7f47d1166350cf308f2dd09"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga8b55ff94d7f47d1166350cf308f2dd09">isRegisteredAtom</a> () const </td></tr>
<tr class="separator:ga8b55ff94d7f47d1166350cf308f2dd09"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga3292a2d664355dd3246479f21e6f26cb"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga3292a2d664355dd3246479f21e6f26cb">isSelected</a> () const </td></tr>
<tr class="separator:ga3292a2d664355dd3246479f21e6f26cb"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga2dab8e7d46762ef10be1f34bd14e751b"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga2dab8e7d46762ef10be1f34bd14e751b">isStoredPredicate</a> () const </td></tr>
<tr class="separator:ga2dab8e7d46762ef10be1f34bd14e751b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gab9779994b0bb78e555c4f9e2163571ed"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gab9779994b0bb78e555c4f9e2163571ed">getFlag</a> () const </td></tr>
<tr class="memdesc:gab9779994b0bb78e555c4f9e2163571ed"><td class="mdescLeft"> </td><td class="mdescRight">Check if the generic flag is set. <a href="group__ExprPkg.html#gab9779994b0bb78e555c4f9e2163571ed"></a><br/></td></tr>
<tr class="separator:gab9779994b0bb78e555c4f9e2163571ed"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga4695a56a4bdc943174eda1f41cbcead4"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga4695a56a4bdc943174eda1f41cbcead4">setFlag</a> () const </td></tr>
<tr class="memdesc:ga4695a56a4bdc943174eda1f41cbcead4"><td class="mdescLeft"> </td><td class="mdescRight">Set the generic flag. <a href="group__ExprPkg.html#ga4695a56a4bdc943174eda1f41cbcead4"></a><br/></td></tr>
<tr class="separator:ga4695a56a4bdc943174eda1f41cbcead4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga463076527f4fb2b87362ee268abc013f"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga463076527f4fb2b87362ee268abc013f">clearFlags</a> () const </td></tr>
<tr class="memdesc:ga463076527f4fb2b87362ee268abc013f"><td class="mdescLeft"> </td><td class="mdescRight">Clear the generic flag in all Exprs. <a href="group__ExprPkg.html#ga463076527f4fb2b87362ee268abc013f"></a><br/></td></tr>
<tr class="separator:ga463076527f4fb2b87362ee268abc013f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaf3028bb1619f8cc69b66ec712e1adb54"><td class="memItemLeft" align="right" valign="top">std::string </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54">toString</a> () const </td></tr>
<tr class="memdesc:gaf3028bb1619f8cc69b66ec712e1adb54"><td class="mdescLeft"> </td><td class="mdescRight">Print the expression to a string. <a href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54"></a><br/></td></tr>
<tr class="separator:gaf3028bb1619f8cc69b66ec712e1adb54"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga306e932ab9a486c9350d55e216ae0de5"><td class="memItemLeft" align="right" valign="top">std::string </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga306e932ab9a486c9350d55e216ae0de5">toString</a> (<a class="el" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e">InputLanguage</a> lang) const </td></tr>
<tr class="memdesc:ga306e932ab9a486c9350d55e216ae0de5"><td class="mdescLeft"> </td><td class="mdescRight">Print the expression to a string using the given output language. <a href="group__ExprPkg.html#ga306e932ab9a486c9350d55e216ae0de5"></a><br/></td></tr>
<tr class="separator:ga306e932ab9a486c9350d55e216ae0de5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga76180628bc1561af88e41be586973fac"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga76180628bc1561af88e41be586973fac">print</a> (<a class="el" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e">InputLanguage</a> lang, bool dagify=true) const </td></tr>
<tr class="memdesc:ga76180628bc1561af88e41be586973fac"><td class="mdescLeft"> </td><td class="mdescRight">Print the expression in the specified format. <a href="group__ExprPkg.html#ga76180628bc1561af88e41be586973fac"></a><br/></td></tr>
<tr class="separator:ga76180628bc1561af88e41be586973fac"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gae30ed55f3ca40745ad3735ddc7c55645"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gae30ed55f3ca40745ad3735ddc7c55645">print</a> () const </td></tr>
<tr class="memdesc:gae30ed55f3ca40745ad3735ddc7c55645"><td class="mdescLeft"> </td><td class="mdescRight">Print the expression as AST (lisp-like format) <a href="group__ExprPkg.html#gae30ed55f3ca40745ad3735ddc7c55645"></a><br/></td></tr>
<tr class="separator:gae30ed55f3ca40745ad3735ddc7c55645"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga974964d4dba5b50f35ee03e2418e7fe9"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga974964d4dba5b50f35ee03e2418e7fe9">printnodag</a> () const </td></tr>
<tr class="memdesc:ga974964d4dba5b50f35ee03e2418e7fe9"><td class="mdescLeft"> </td><td class="mdescRight">Print the expression as AST without dagifying. <a href="group__ExprPkg.html#ga974964d4dba5b50f35ee03e2418e7fe9"></a><br/></td></tr>
<tr class="separator:ga974964d4dba5b50f35ee03e2418e7fe9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga3aa47bf8af3f2c88b8bc27e0cd07554e"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga3aa47bf8af3f2c88b8bc27e0cd07554e">pprint</a> () const </td></tr>
<tr class="memdesc:ga3aa47bf8af3f2c88b8bc27e0cd07554e"><td class="mdescLeft"> </td><td class="mdescRight">Pretty-print the expression. <a href="group__ExprPkg.html#ga3aa47bf8af3f2c88b8bc27e0cd07554e"></a><br/></td></tr>
<tr class="separator:ga3aa47bf8af3f2c88b8bc27e0cd07554e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga010ae48d41f33790c6b9bb10829105e3"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga010ae48d41f33790c6b9bb10829105e3">pprintnodag</a> () const </td></tr>
<tr class="memdesc:ga010ae48d41f33790c6b9bb10829105e3"><td class="mdescLeft"> </td><td class="mdescRight">Pretty-print without dagifying. <a href="group__ExprPkg.html#ga010ae48d41f33790c6b9bb10829105e3"></a><br/></td></tr>
<tr class="separator:ga010ae48d41f33790c6b9bb10829105e3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaa26519c37fd631580f14664d83dcb4fa"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaa26519c37fd631580f14664d83dcb4fa">print</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &os) const </td></tr>
<tr class="memdesc:gaa26519c37fd631580f14664d83dcb4fa"><td class="mdescLeft"> </td><td class="mdescRight">Print a leaf node. <a href="group__ExprPkg.html#gaa26519c37fd631580f14664d83dcb4fa"></a><br/></td></tr>
<tr class="separator:gaa26519c37fd631580f14664d83dcb4fa"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga092308b0a88e12a5c7ff2fc0a2eca818"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga092308b0a88e12a5c7ff2fc0a2eca818">printAST</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &os) const </td></tr>
<tr class="memdesc:ga092308b0a88e12a5c7ff2fc0a2eca818"><td class="mdescLeft"> </td><td class="mdescRight">Print the top node and then recurse through the children */. <a href="group__ExprPkg.html#ga092308b0a88e12a5c7ff2fc0a2eca818"></a><br/></td></tr>
<tr class="separator:ga092308b0a88e12a5c7ff2fc0a2eca818"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga9050d11fa8e8ece11ab586a560081196"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga9050d11fa8e8ece11ab586a560081196">indent</a> (int n, bool permanent=false)</td></tr>
<tr class="memdesc:ga9050d11fa8e8ece11ab586a560081196"><td class="mdescLeft"> </td><td class="mdescRight">Set initial indentation to n. <a href="group__ExprPkg.html#ga9050d11fa8e8ece11ab586a560081196"></a><br/></td></tr>
<tr class="separator:ga9050d11fa8e8ece11ab586a560081196"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga5318abf2b6333d23b3cfa8877a93151d"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga5318abf2b6333d23b3cfa8877a93151d">setFind</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e) const </td></tr>
<tr class="memdesc:ga5318abf2b6333d23b3cfa8877a93151d"><td class="mdescLeft"> </td><td class="mdescRight">Set the find attribute to e. <a href="group__ExprPkg.html#ga5318abf2b6333d23b3cfa8877a93151d"></a><br/></td></tr>
<tr class="separator:ga5318abf2b6333d23b3cfa8877a93151d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gae283f0adb5cb21761081fc267ba8eba2"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gae283f0adb5cb21761081fc267ba8eba2">setEqNext</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e) const </td></tr>
<tr class="memdesc:gae283f0adb5cb21761081fc267ba8eba2"><td class="mdescLeft"> </td><td class="mdescRight">Set the eqNext attribute to e. <a href="group__ExprPkg.html#gae283f0adb5cb21761081fc267ba8eba2"></a><br/></td></tr>
<tr class="separator:gae283f0adb5cb21761081fc267ba8eba2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga159d60cb0f32e09df89a395b2680664a"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga159d60cb0f32e09df89a395b2680664a">addToNotify</a> (<a class="el" href="classCVC3_1_1Theory.html">Theory</a> *i, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e) const </td></tr>
<tr class="memdesc:ga159d60cb0f32e09df89a395b2680664a"><td class="mdescLeft"> </td><td class="mdescRight">Add (e,i) to the notify list of this expression. <a href="group__ExprPkg.html#ga159d60cb0f32e09df89a395b2680664a"></a><br/></td></tr>
<tr class="separator:ga159d60cb0f32e09df89a395b2680664a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga07d47f902598e00097086deabf04d9c5"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga07d47f902598e00097086deabf04d9c5">setType</a> (const <a class="el" href="classCVC3_1_1Type.html">Type</a> &t) const </td></tr>
<tr class="memdesc:ga07d47f902598e00097086deabf04d9c5"><td class="mdescLeft"> </td><td class="mdescRight">Set the cached type. <a href="group__ExprPkg.html#ga07d47f902598e00097086deabf04d9c5"></a><br/></td></tr>
<tr class="separator:ga07d47f902598e00097086deabf04d9c5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga933505a9529110425c3e7d3cd2e90c2c"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga933505a9529110425c3e7d3cd2e90c2c">setSimpCache</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e) const </td></tr>
<tr class="separator:ga933505a9529110425c3e7d3cd2e90c2c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gab854295d8dd4be1c54f62030301e94bd"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gab854295d8dd4be1c54f62030301e94bd">setValidType</a> () const </td></tr>
<tr class="separator:gab854295d8dd4be1c54f62030301e94bd"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga5c1a2072d2478708bc788814385e00c4"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga5c1a2072d2478708bc788814385e00c4">setIsAtomicFlag</a> (bool value) const </td></tr>
<tr class="separator:ga5c1a2072d2478708bc788814385e00c4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga4158db17700c28f6fbd6be955c4ad075"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga4158db17700c28f6fbd6be955c4ad075">setTerminalsConstFlag</a> (bool value) const </td></tr>
<tr class="separator:ga4158db17700c28f6fbd6be955c4ad075"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga06284723527dbaa4784949f63f586877"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga06284723527dbaa4784949f63f586877">setRewriteNormal</a> () const </td></tr>
<tr class="separator:ga06284723527dbaa4784949f63f586877"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga643f89574537ab6acf9bb1bc2f703c77"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga643f89574537ab6acf9bb1bc2f703c77">clearRewriteNormal</a> () const </td></tr>
<tr class="separator:ga643f89574537ab6acf9bb1bc2f703c77"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaecb0afa375de675309b6d1ec72a5c648"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaecb0afa375de675309b6d1ec72a5c648">setFinite</a> () const </td></tr>
<tr class="separator:gaecb0afa375de675309b6d1ec72a5c648"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga3e4a13d6c9c5d1c14d44ca530ca8187d"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga3e4a13d6c9c5d1c14d44ca530ca8187d">setWellFounded</a> () const </td></tr>
<tr class="separator:ga3e4a13d6c9c5d1c14d44ca530ca8187d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga5513f05f1d104aa5dc4fd8724b46e221"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga5513f05f1d104aa5dc4fd8724b46e221">setComputeTransClosure</a> () const </td></tr>
<tr class="separator:ga5513f05f1d104aa5dc4fd8724b46e221"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga46031ec4323f6c373c7ffb59b4db30e9"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga46031ec4323f6c373c7ffb59b4db30e9">setContainsBoundVar</a> () const </td></tr>
<tr class="separator:ga46031ec4323f6c373c7ffb59b4db30e9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga243c5d26015ee1fd946f8ccce5f83568"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga243c5d26015ee1fd946f8ccce5f83568">setUsesCC</a> () const </td></tr>
<tr class="separator:ga243c5d26015ee1fd946f8ccce5f83568"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaa09f6f3f2938359d472a0c099ff0c634"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaa09f6f3f2938359d472a0c099ff0c634">setNotArrayNormalized</a> () const </td></tr>
<tr class="separator:gaa09f6f3f2938359d472a0c099ff0c634"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaece7bfa79c995a45964a7dc5f2408e55"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaece7bfa79c995a45964a7dc5f2408e55">setImpliedLiteral</a> () const </td></tr>
<tr class="separator:gaece7bfa79c995a45964a7dc5f2408e55"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga63eb3b8c124654cf056b2814794c4236"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga63eb3b8c124654cf056b2814794c4236">setUserAssumption</a> (int scope=-1) const </td></tr>
<tr class="separator:ga63eb3b8c124654cf056b2814794c4236"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gacfaaa30a1743a0955e0568b3bcd7cc08"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gacfaaa30a1743a0955e0568b3bcd7cc08">setInUserAssumption</a> (int scope=-1) const </td></tr>
<tr class="separator:gacfaaa30a1743a0955e0568b3bcd7cc08"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga8b1ac81529d2ebee895a385a35460d39"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga8b1ac81529d2ebee895a385a35460d39">setIntAssumption</a> () const </td></tr>
<tr class="separator:ga8b1ac81529d2ebee895a385a35460d39"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga98a725d64a530023a36be8045d87863a"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga98a725d64a530023a36be8045d87863a">setJustified</a> () const </td></tr>
<tr class="separator:ga98a725d64a530023a36be8045d87863a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaf941ebb5b9a8e6ee0ca004d59425fb42"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaf941ebb5b9a8e6ee0ca004d59425fb42">setTranslated</a> (int scope=-1) const </td></tr>
<tr class="memdesc:gaf941ebb5b9a8e6ee0ca004d59425fb42"><td class="mdescLeft"> </td><td class="mdescRight">Set the translated flag for this <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="group__ExprPkg.html#gaf941ebb5b9a8e6ee0ca004d59425fb42"></a><br/></td></tr>
<tr class="separator:gaf941ebb5b9a8e6ee0ca004d59425fb42"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga6f8db899f4680e53c4cf11c20dc10735"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga6f8db899f4680e53c4cf11c20dc10735">setUserRegisteredAtom</a> () const </td></tr>
<tr class="memdesc:ga6f8db899f4680e53c4cf11c20dc10735"><td class="mdescLeft"> </td><td class="mdescRight">Set the UserRegisteredAtom flag for this <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="group__ExprPkg.html#ga6f8db899f4680e53c4cf11c20dc10735"></a><br/></td></tr>
<tr class="separator:ga6f8db899f4680e53c4cf11c20dc10735"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga6adb700b834218ed8aaf4296458d9bf9"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga6adb700b834218ed8aaf4296458d9bf9">setRegisteredAtom</a> () const </td></tr>
<tr class="memdesc:ga6adb700b834218ed8aaf4296458d9bf9"><td class="mdescLeft"> </td><td class="mdescRight">Set the RegisteredAtom flag for this <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="group__ExprPkg.html#ga6adb700b834218ed8aaf4296458d9bf9"></a><br/></td></tr>
<tr class="separator:ga6adb700b834218ed8aaf4296458d9bf9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga50ebe7a6fa50064b2d01e0eaa25f931a"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga50ebe7a6fa50064b2d01e0eaa25f931a">setSelected</a> () const </td></tr>
<tr class="memdesc:ga50ebe7a6fa50064b2d01e0eaa25f931a"><td class="mdescLeft"> </td><td class="mdescRight">Set the Selected flag for this <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="group__ExprPkg.html#ga50ebe7a6fa50064b2d01e0eaa25f931a"></a><br/></td></tr>
<tr class="separator:ga50ebe7a6fa50064b2d01e0eaa25f931a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga911ab512eb2b3d2f8e59280261b847d6"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga911ab512eb2b3d2f8e59280261b847d6">setStoredPredicate</a> () const </td></tr>
<tr class="memdesc:ga911ab512eb2b3d2f8e59280261b847d6"><td class="mdescLeft"> </td><td class="mdescRight">Set the Stored Predicate flag for this <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>. <a href="group__ExprPkg.html#ga911ab512eb2b3d2f8e59280261b847d6"></a><br/></td></tr>
<tr class="separator:ga911ab512eb2b3d2f8e59280261b847d6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga4b89f3d46b36f66acb191a4fb359d69f"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga4b89f3d46b36f66acb191a4fb359d69f">subExprOf</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e) const </td></tr>
<tr class="memdesc:ga4b89f3d46b36f66acb191a4fb359d69f"><td class="mdescLeft"> </td><td class="mdescRight">Check if the current <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> (*this) is a subexpression of e. <a href="group__ExprPkg.html#ga4b89f3d46b36f66acb191a4fb359d69f"></a><br/></td></tr>
<tr class="separator:ga4b89f3d46b36f66acb191a4fb359d69f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gad2f1fb7c447bcc3a7d352fd24a8f265a"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Unsigned.html">Unsigned</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gad2f1fb7c447bcc3a7d352fd24a8f265a">getSize</a> () const </td></tr>
<tr class="separator:gad2f1fb7c447bcc3a7d352fd24a8f265a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga3cc4e5ec0d7310f1bce3630455147bb3"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga3cc4e5ec0d7310f1bce3630455147bb3">hasSig</a> () const </td></tr>
<tr class="separator:ga3cc4e5ec0d7310f1bce3630455147bb3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gae71c95cf1ca998d57b02a136b379172b"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gae71c95cf1ca998d57b02a136b379172b">hasRep</a> () const </td></tr>
<tr class="separator:gae71c95cf1ca998d57b02a136b379172b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gae281b04465cc1bf24b5797c8b5e9cbb4"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gae281b04465cc1bf24b5797c8b5e9cbb4">getSig</a> () const </td></tr>
<tr class="separator:gae281b04465cc1bf24b5797c8b5e9cbb4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaa4b5652980861e593ab8a741b5521779"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaa4b5652980861e593ab8a741b5521779">getRep</a> () const </td></tr>
<tr class="separator:gaa4b5652980861e593ab8a741b5521779"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaaaba7ddaccd58bd37e3259fe9b949645"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gaaaba7ddaccd58bd37e3259fe9b949645">setSig</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e) const </td></tr>
<tr class="separator:gaaaba7ddaccd58bd37e3259fe9b949645"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga7b85677789c5a03e1a5dc2c93f0b6288"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga7b85677789c5a03e1a5dc2c93f0b6288">setRep</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e) const </td></tr>
<tr class="separator:ga7b85677789c5a03e1a5dc2c93f0b6288"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pub-static-methods"></a>
Static Public Member Functions</h2></td></tr>
<tr class="memitem:gadf3d59da15e4f78daf0c41ef7779a749"><td class="memItemLeft" align="right" valign="top">static size_t </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gadf3d59da15e4f78daf0c41ef7779a749">hash</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:gadf3d59da15e4f78daf0c41ef7779a749"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-types"></a>
Private Types</h2></td></tr>
<tr class="memitem:ga5285f004f382cfb7a002f8dea3b3316c"><td class="memItemLeft" align="right" valign="top">enum  </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga5285f004f382cfb7a002f8dea3b3316c">StaticFlagsEnum</a> { <br/>
  <a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316ca064c35d31f9b779c3c327a38c22f7d5a">VALID_TYPE</a> = 0x1,
<a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316ca4bc8d45f29e985faa033b685c209c934">VALID_IS_ATOMIC</a> = 0x2,
<a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316caf25f8b67eed5f06cdff26bfe7e5f004b">IS_ATOMIC</a> = 0x4,
<a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316ca6279757281c85b060623657eae639d11">REWRITE_NORMAL</a> = 0x8,
<br/>
  <a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316ca8282a0d9539e4019a384810c6ddf80ff">IS_FINITE</a> = 0x400,
<a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316ca9f0f9b43c297449dc513bba12a343c0d">WELL_FOUNDED</a> = 0x800,
<a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316caabe5302ce9b2cf701cb301b81e28315d">COMPUTE_TRANS_CLOSURE</a> = 0x1000,
<a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316ca37150acb5faf924bcfdffd46fb91fb3f">CONTAINS_BOUND_VAR</a> = 0x00020000,
<br/>
  <a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316cad414c75c14f9cc186e6e7df225396627">USES_CC</a> = 0x00080000,
<a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316ca501e68dd8eb63c2ed0d6f52f1eb844f8">VALID_TERMINALS_CONST</a> = 0x00100000,
<a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316ca8f04196095a0b34d324a5c004d08317d">TERMINALS_CONST</a> = 0x00200000
<br/>
}</td></tr>
<tr class="memdesc:ga5285f004f382cfb7a002f8dea3b3316c"><td class="mdescLeft"> </td><td class="mdescRight">bit-masks for static flags <a href="group__ExprPkg.html#ga5285f004f382cfb7a002f8dea3b3316c">More...</a><br/></td></tr>
<tr class="separator:ga5285f004f382cfb7a002f8dea3b3316c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga74e5360ad3392aa4779d981670887936"><td class="memItemLeft" align="right" valign="top">enum  </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga74e5360ad3392aa4779d981670887936">DynamicFlagsEnum</a> { <br/>
  <a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936a34b44b8fd97e8950a24f9d1d939fd3ac">IMPLIED_LITERAL</a> = 0x10,
<a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936ae7079560c1a0d6742b7dd084401327ac">IS_USER_ASSUMPTION</a> = 0x20,
<a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936a4e904444fd219938f8743b8e951eba6d">IS_INT_ASSUMPTION</a> = 0x40,
<a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936a5fdae20b9b42f2eae992d1fe377c32b8">IS_JUSTIFIED</a> = 0x80,
<br/>
  <a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936a72910ce6e23c9b05b457f5d324141e86">IS_TRANSLATED</a> = 0x100,
<a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936aa8205caf0608f22ab9f3aab9704f4876">IS_USER_REGISTERED_ATOM</a> = 0x200,
<a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936a1b8256ca353bb0d0e7baf1c1442209d6">IS_SELECTED</a> = 0x2000,
<a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936ad3d25a426b786f2336d6112309b2b80f">IS_STORED_PREDICATE</a> = 0x4000,
<br/>
  <a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936a96ef34cf7e9afffe1442ddd8bc3d946f">IS_REGISTERED_ATOM</a> = 0x8000,
<a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936aec9453c0bef6971761ee89e60baa4a80">IN_USER_ASSUMPTION</a> = 0x00010000,
<a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936a0328c59b775199c11653b376c0f3c8cb">NOT_ARRAY_NORMALIZED</a> = 0x00040000
<br/>
}</td></tr>
<tr class="memdesc:ga74e5360ad3392aa4779d981670887936"><td class="mdescLeft"> </td><td class="mdescRight">bit-masks for dynamic flags <a href="group__ExprPkg.html#ga74e5360ad3392aa4779d981670887936">More...</a><br/></td></tr>
<tr class="separator:ga74e5360ad3392aa4779d981670887936"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-methods"></a>
Private Member Functions</h2></td></tr>
<tr class="memitem:gadebfef27e4d0ea75d7d37c3fdbcfb727"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gadebfef27e4d0ea75d7d37c3fdbcfb727">Expr</a> (<a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> *expr)</td></tr>
<tr class="memdesc:gadebfef27e4d0ea75d7d37c3fdbcfb727"><td class="mdescLeft"> </td><td class="mdescRight">Private constructor, simply wraps around the pointer. <a href="group__ExprPkg.html#gadebfef27e4d0ea75d7d37c3fdbcfb727"></a><br/></td></tr>
<tr class="separator:gadebfef27e4d0ea75d7d37c3fdbcfb727"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga7ee0a2ffca952496e3f1d8c9c9d66aab"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga7ee0a2ffca952496e3f1d8c9c9d66aab">recursiveSubst</a> (const <a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &subst, <a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &visited) const </td></tr>
<tr class="separator:ga7ee0a2ffca952496e3f1d8c9c9d66aab"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga644bfdf1ae59727d6626c764208483e8"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga644bfdf1ae59727d6626c764208483e8">recursiveQuantSubst</a> (const <a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &subst, <a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &visited) const </td></tr>
<tr class="separator:ga644bfdf1ae59727d6626c764208483e8"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga2605b52bcaa9bf4c04115a63ea773c9c"><td class="memItemLeft" align="right" valign="top">std::vector< std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > > </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga2605b52bcaa9bf4c04115a63ea773c9c">substTriggers</a> (const <a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &subst, <a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &visited) const </td></tr>
<tr class="separator:ga2605b52bcaa9bf4c04115a63ea773c9c"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-attribs"></a>
Private Attributes</h2></td></tr>
<tr class="memitem:ga3a08bea4e8715a268083e1671e340a2e"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga3a08bea4e8715a268083e1671e340a2e">d_expr</a></td></tr>
<tr class="separator:ga3a08bea4e8715a268083e1671e340a2e"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-static-attribs"></a>
Static Private Attributes</h2></td></tr>
<tr class="memitem:ga7ad4f1f01878e19f3a6318a846dbfe6f"><td class="memItemLeft" align="right" valign="top">static <a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga7ad4f1f01878e19f3a6318a846dbfe6f">s_null</a></td></tr>
<tr class="memdesc:ga7ad4f1f01878e19f3a6318a846dbfe6f"><td class="mdescLeft"> </td><td class="mdescRight">Convenient null expr. <a href="group__ExprPkg.html#ga7ad4f1f01878e19f3a6318a846dbfe6f"></a><br/></td></tr>
<tr class="separator:ga7ad4f1f01878e19f3a6318a846dbfe6f"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="friends"></a>
Friends</h2></td></tr>
<tr class="memitem:a966b1c64eb8abb1688f28451453d3479"><td class="memItemLeft" align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Expr.html#a966b1c64eb8abb1688f28451453d3479">ExprHasher</a></td></tr>
<tr class="separator:a966b1c64eb8abb1688f28451453d3479"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a53c627979d9a14928590601b9fd195c2"><td class="memItemLeft" align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Expr.html#a53c627979d9a14928590601b9fd195c2">ExprManager</a></td></tr>
<tr class="separator:a53c627979d9a14928590601b9fd195c2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2c31e8a3c11caeb061d69db14ebb0e95"><td class="memItemLeft" align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Expr.html#a2c31e8a3c11caeb061d69db14ebb0e95">Op</a></td></tr>
<tr class="separator:a2c31e8a3c11caeb061d69db14ebb0e95"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6b4e0ce748563841be8fe35c34ee7975"><td class="memItemLeft" align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Expr.html#a6b4e0ce748563841be8fe35c34ee7975">ExprValue</a></td></tr>
<tr class="separator:a6b4e0ce748563841be8fe35c34ee7975"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:af86989fa451681663344e67f9ae1be0d"><td class="memItemLeft" align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Expr.html#af86989fa451681663344e67f9ae1be0d">ExprNode</a></td></tr>
<tr class="separator:af86989fa451681663344e67f9ae1be0d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a53271ded90a8b528132eeb7247936492"><td class="memItemLeft" align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Expr.html#a53271ded90a8b528132eeb7247936492">ExprClosure</a></td></tr>
<tr class="separator:a53271ded90a8b528132eeb7247936492"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a61a2a0fa995725e9988683c6dabd503c"><td class="memItemLeft" align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Expr.html#a61a2a0fa995725e9988683c6dabd503c">::CInterface</a></td></tr>
<tr class="separator:a61a2a0fa995725e9988683c6dabd503c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a51f48d7e14c97707595cfe5f8f6df209"><td class="memItemLeft" align="right" valign="top">class </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Expr.html#a51f48d7e14c97707595cfe5f8f6df209">Theorem</a></td></tr>
<tr class="separator:a51f48d7e14c97707595cfe5f8f6df209"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga691d71052166260b4f5b5a2ee3cda464"><td class="memItemLeft" align="right" valign="top"><a class="el" href="type_8h.html#a0035aac6379df39aa69feba98b2751ba">CVC_DLL</a> std::ostream & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga691d71052166260b4f5b5a2ee3cda464">operator<<</a> (std::ostream &os, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:ga691d71052166260b4f5b5a2ee3cda464"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gadeeaa34664eae73d96a147b6fad0c0e1"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gadeeaa34664eae73d96a147b6fad0c0e1">compare</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e2)</td></tr>
<tr class="separator:gadeeaa34664eae73d96a147b6fad0c0e1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gab39e411af6eecf3b4a34ebcd5c37c1d9"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#gab39e411af6eecf3b4a34ebcd5c37c1d9">operator==</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e2)</td></tr>
<tr class="separator:gab39e411af6eecf3b4a34ebcd5c37c1d9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga7da18dfc7cf83f48c3b68eaf7bdaeca0"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga7da18dfc7cf83f48c3b68eaf7bdaeca0">operator!=</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e2)</td></tr>
<tr class="separator:ga7da18dfc7cf83f48c3b68eaf7bdaeca0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga1d72417bdb285b126416d7d169e463dd"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga1d72417bdb285b126416d7d169e463dd">operator<</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e2)</td></tr>
<tr class="separator:ga1d72417bdb285b126416d7d169e463dd"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga205ae18c57fd12d497996c7edad4c073"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga205ae18c57fd12d497996c7edad4c073">operator<=</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e2)</td></tr>
<tr class="separator:ga205ae18c57fd12d497996c7edad4c073"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga38fa42aec5b81d57acd5a605c73ead83"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga38fa42aec5b81d57acd5a605c73ead83">operator></a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e2)</td></tr>
<tr class="separator:ga38fa42aec5b81d57acd5a605c73ead83"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga5a1d868d3eb493b773101b5601984156"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__ExprPkg.html#ga5a1d868d3eb493b773101b5601984156">operator>=</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e2)</td></tr>
<tr class="separator:ga5a1d868d3eb493b773101b5601984156"><td class="memSeparator" colspan="2"> </td></tr>
</table>
<a name="details" id="details"></a><h2 class="groupheader">Detailed Description</h2>
<div class="textblock"><p>Data structure of expressions in <a class="el" href="namespaceCVC3.html">CVC3</a>. </p>
<p>Class: <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <br/>
Author: Clark Barrett <br/>
Created: Mon Nov 25 15:29:37 2002</p>
<p>This class is the main data structure for expressions that all other components should use. It is actually a <em>smart pointer</em> to the actual data holding class <a class="el" href="classCVC3_1_1ExprValue.html" title="The base class for holding the actual data in expressions.">ExprValue</a> and its subclasses.</p>
<p>Expressions are represented as DAGs with maximal sharing of subexpressions. Therefore, testing for equality is a constant time operation (simply compare the pointers).</p>
<p>Unused expressions are automatically garbage-collected. The use is determined by a reference counting mechanism. In particular, this means that if there is a circular dependency among expressions (e.g. an attribute points back to the expression itself), these expressions will not be garbage-collected, even if no one else is using them.</p>
<p>The most frequently used operations are <a class="el" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind()</a> (determining the kind of the top level node of the expression), <a class="el" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity()</a> (how many children an <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> has), <a class="el" href="group__ExprPkg.html#ga5b242a4834df256dc2055e310fb0e727">operator[]()</a> for accessing a child, and various testers and methods for constructing new expressions.</p>
<p>In addition, a total ordering <a class="el" href="group__ExprPkg.html#ga1d72417bdb285b126416d7d169e463dd">operator<()</a> is provided. It is guaranteed to remain the same for the lifetime of the expressions (it may change, however, if the expression is garbage-collected and reborn). </p>
<p>Definition at line <a class="el" href="expr_8h_source.html#l00133">133</a> of file <a class="el" href="expr_8h_source.html">expr.h</a>.</p>
</div><h2 class="groupheader">Friends And Related Function Documentation</h2>
<a class="anchor" id="a966b1c64eb8abb1688f28451453d3479"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">friend class ExprHasher</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr_8h_source.html#l00134">134</a> of file <a class="el" href="expr_8h_source.html">expr.h</a>.</p>
</div>
</div>
<a class="anchor" id="a53c627979d9a14928590601b9fd195c2"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr_8h_source.html#l00135">135</a> of file <a class="el" href="expr_8h_source.html">expr.h</a>.</p>
</div>
</div>
<a class="anchor" id="a2c31e8a3c11caeb061d69db14ebb0e95"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1Op.html">Op</a></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr_8h_source.html#l00136">136</a> of file <a class="el" href="expr_8h_source.html">expr.h</a>.</p>
<p>Referenced by <a class="el" href="expr_8h_source.html#l01183">getOp()</a>, and <a class="el" href="expr_8h_source.html#l01178">mkOp()</a>.</p>
</div>
</div>
<a class="anchor" id="a6b4e0ce748563841be8fe35c34ee7975"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr_8h_source.html#l00137">137</a> of file <a class="el" href="expr_8h_source.html">expr.h</a>.</p>
</div>
</div>
<a class="anchor" id="af86989fa451681663344e67f9ae1be0d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1ExprNode.html">ExprNode</a></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr_8h_source.html#l00138">138</a> of file <a class="el" href="expr_8h_source.html">expr.h</a>.</p>
</div>
</div>
<a class="anchor" id="a53271ded90a8b528132eeb7247936492"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1ExprClosure.html">ExprClosure</a></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr_8h_source.html#l00139">139</a> of file <a class="el" href="expr_8h_source.html">expr.h</a>.</p>
</div>
</div>
<a class="anchor" id="a61a2a0fa995725e9988683c6dabd503c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">friend class ::CInterface</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr_8h_source.html#l00140">140</a> of file <a class="el" href="expr_8h_source.html">expr.h</a>.</p>
</div>
</div>
<a class="anchor" id="a51f48d7e14c97707595cfe5f8f6df209"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="expr_8h_source.html#l00141">141</a> of file <a class="el" href="expr_8h_source.html">expr.h</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="expr_8h_source.html">expr.h</a></li>
<li><a class="el" href="expr_8cpp_source.html">expr.cpp</a></li>
</ul>
</div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:17 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
