Sophie

Sophie

distrib > PLD > th > x86_64 > by-pkgid > 9f869ff92bf81fc4b13902b2b85811f8 > files > 339

cvc3-doc-2.4.1-1.noarch.rpm

<!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: Member List</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&#160;Page</span></a></li>
      <li><a href="pages.html"><span>Related&#160;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&#160;List</span></a></li>
      <li><a href="classes.html"><span>Class&#160;Index</span></a></li>
      <li><a href="inherits.html"><span>Class&#160;Hierarchy</span></a></li>
      <li><a href="functions.html"><span>Class&#160;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="headertitle">
<div class="title">CVC3::Expr Member List</div>  </div>
</div><!--header-->
<div class="contents">

<p>This is the complete list of members for <a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a>, including all inherited members.</p>
<table class="directory">
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Expr.html#a61a2a0fa995725e9988683c6dabd503c">::CInterface</a> class</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga159d60cb0f32e09df89a395b2680664a">addToNotify</a>(Theory *i, const Expr &amp;e) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga6c3651465ce69ed5f4e6fd461b9acf3c">andExpr</a>(const Expr &amp;right) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gac890e13db184610276fc533fa4b4fe99">begin</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga463076527f4fb2b87362ee268abc013f">clearFlags</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga643f89574537ab6acf9bb1bc2f703c77">clearRewriteNormal</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gadeeaa34664eae73d96a147b6fad0c0e1">compare</a>(const Expr &amp;e1, const Expr &amp;e2)</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316caabe5302ce9b2cf701cb301b81e28315d">COMPUTE_TRANS_CLOSURE</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gac3aeac6fba7a1d6cacfe4bd653c5a084">computeTransClosure</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316ca37150acb5faf924bcfdffd46fb91fb3f">CONTAINS_BOUND_VAR</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gacafcbc459ee158f84e3666eaf32ca3f9">containsBoundVar</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaf53e6a6f9dc01481d2cf94673c5505ce">containsTermITE</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga3a08bea4e8715a268083e1671e340a2e">d_expr</a></td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga74e5360ad3392aa4779d981670887936">DynamicFlagsEnum</a> enum name</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gaf6048a5030c8fa2511bf5dfee868e653">end</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gacb48495ca445c895f95d0c3c1ae2070b">eqExpr</a>(const Expr &amp;right) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gadebfef27e4d0ea75d7d37c3fdbcfb727">Expr</a>(ExprValue *expr)</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">private</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaf3f35afa568a157d6f58ad24fd46b9d1">Expr</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga8e424c562e5d452d4ddc50f6e7b3e063">Expr</a>(const Expr &amp;e)</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gafb0fbf8419f557068fc0f8293ecf1624">Expr</a>(const Op &amp;op, const Expr &amp;child)</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga593d896e3c01b8596e57b822b948e6f2">Expr</a>(const Op &amp;op, const Expr &amp;child0, const Expr &amp;child1)</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga67ac1e86cbda6dadb63c0739351fa19b">Expr</a>(const Op &amp;op, const Expr &amp;child0, const Expr &amp;child1, const Expr &amp;child2)</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga759ac04d93b19fcffd125924d668995e">Expr</a>(const Op &amp;op, const Expr &amp;child0, const Expr &amp;child1, const Expr &amp;child2, const Expr &amp;child3)</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaf6745550d2453e3e25af3bb9c4ea7a45">Expr</a>(const Op &amp;op, const std::vector&lt; Expr &gt; &amp;children, ExprManager *em=NULL)</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1Expr.html#a53271ded90a8b528132eeb7247936492">ExprClosure</a> class</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Expr.html#a966b1c64eb8abb1688f28451453d3479">ExprHasher</a> class</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1Expr.html#a53c627979d9a14928590601b9fd195c2">ExprManager</a> class</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Expr.html#af86989fa451681663344e67f9ae1be0d">ExprNode</a> class</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1Expr.html#a6b4e0ce748563841be8fe35c34ee7975">ExprValue</a> class</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940">getBody</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga58d51b54987242f54071bdcc0d7d183f">getBoundIndex</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gaac6e2bdafe4cb6b91d4bec8fa656bcb2">getEqNext</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaf12c1f078a1106ba7d7896c45b2eb4cb">getExistential</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gad21442cf6ecf46e8fcccbef451f4041b">getExprValue</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga9be55edbdc2c0878fec750921a9fcc89">getFind</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga45ea7926a65c7c5559c81f1f20bde281">getFindLevel</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gab9779994b0bb78e555c4f9e2163571ed">getFlag</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gadaddb9b0566ecddd4611a10e820dc544">getIndex</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaaa895b97bdc2413b72419cc781178995">getIsAtomicFlag</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga1e18ae89889e781591eb2874a4196b73">getKids</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gaca3ae54b26443a7d5a74cc7d6f5e81e3">getMMIndex</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaa3023d9117f249f079b0a202a1dfc5c2">getName</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gace67f5f11fd81d9ecebba441b8c02e07">getNotify</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gace479f04faca399219496195152f7806">getOp</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga9f3328fe077191803a780cfd6566ff9b">getOpExpr</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gad036a3a3597d590ca6ee694505c6e1cd">getOpKind</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gab0eee70e4a7f97c09954dc61b71b65e5">getRational</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaa4b5652980861e593ab8a741b5521779">getRep</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gae281b04465cc1bf24b5797c8b5e9cbb4">getSig</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga5dbb07a3a7f3a7154ad3bcdb58bbdec6">getSimpCache</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gad2f1fb7c447bcc3a7d352fd24a8f265a">getSize</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga5e679ab39ad8166c3c027afee9004c26">getString</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gab990a9104757ac6854b92c3b98727b9c">getTerminalsConstFlag</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga29db2c821567c944bc14f8156eb092b6">getTheorem</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gae4cffec57be4b7d81e8486328c2396fc">getTriggers</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga42929221eb172250697b72c28af6de07">getType</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga2b086a0194b24a3f31afd402cea7de94">getUid</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd">getVars</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga4dc94c33ae308ff8d9d004f49df8f42b">hasFind</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gadf3d59da15e4f78daf0c41ef7779a749">hash</a>(const Expr &amp;e)</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">static</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gae11bd9d6d259d280c77cb1778520daa4">hash</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaa930fda58c8146f27f3dacaab017015c">hasLastIndex</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gae71c95cf1ca998d57b02a136b379172b">hasRep</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga3cc4e5ec0d7310f1bce3630455147bb3">hasSig</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gaae017ca8e68af655ba285c985dd9fba5">iffExpr</a>(const Expr &amp;right) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga8dd97bcdeb9d8870238f94a263fd083b">impExpr</a>(const Expr &amp;right) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936a34b44b8fd97e8950a24f9d1d939fd3ac">IMPLIED_LITERAL</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936aec9453c0bef6971761ee89e60baa4a80">IN_USER_ASSUMPTION</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga9050d11fa8e8ece11ab586a560081196">indent</a>(int n, bool permanent=false)</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga110d4a1734b738dbb999b7798e07c3d1">inUserAssumption</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316caf25f8b67eed5f06cdff26bfe7e5f004b">IS_ATOMIC</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316ca8282a0d9539e4019a384810c6ddf80ff">IS_FINITE</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936a4e904444fd219938f8743b8e951eba6d">IS_INT_ASSUMPTION</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936a5fdae20b9b42f2eae992d1fe377c32b8">IS_JUSTIFIED</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936a96ef34cf7e9afffe1442ddd8bc3d946f">IS_REGISTERED_ATOM</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936a1b8256ca353bb0d0e7baf1c1442209d6">IS_SELECTED</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936ad3d25a426b786f2336d6112309b2b80f">IS_STORED_PREDICATE</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936a72910ce6e23c9b05b457f5d324141e86">IS_TRANSLATED</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936ae7079560c1a0d6742b7dd084401327ac">IS_USER_ASSUMPTION</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936aa8205caf0608f22ab9f3aab9704f4876">IS_USER_REGISTERED_ATOM</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga5fe5158aefab64fd8adda48ecebb98f9">isAbsAtomicFormula</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaac535dae48f02fcd093a5b1b1a062211">isAbsLiteral</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga383260cf4f8919728e2712e6e11f21fa">isAnd</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga1d6a6b4a9ce81b0dd8fd74870ff4284b">isApply</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga48a9219339b394280550069ac7b0474f">isAtomic</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga4b575e0a191cc42706ff5b5a169c3069">isAtomicFormula</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gac03948739e860fa791fd3bbb713c1076">isBoolConnective</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga5c2cee598096c66e80d87490d6505bc4">isBoolConst</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga01122f4c0d9a19d9b991600e480cc862">isBoundVar</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga3127f52184d5bcb2d4056cb23f3a292b">isClosure</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga3c3645e1962f6de72655c650639e7a2d">isConstant</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gac4af2026c180da0f18d66ac616f61f3a">isEq</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga1c922163af59ed6bc101728d65e04d16">isExists</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga6173f64b22cba76472cd0c814bbf6dae">isFalse</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gacf628bd70fc2c4766afa268ed22ea947">isFinite</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gabe385fb97505cccb75702378511c5375">isIff</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga9067c706c6454ea1761ace7d7837af46">isImpl</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga5d92d645899807eb4351502f2e74369e">isImpliedLiteral</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaa3359d5f6638eba5479c4c4036a551a8">isInitialized</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gaf42121131fd56040faef7a64d9e67729">isIntAssumption</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaef13fa4752a1fb28e129a1efd0e26f01">isITE</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga3cf472ba2fa033f3e1401e4b67a3f8a0">isJustified</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga165dba5b9e9502059c3cf01bddf4fe1e">isLambda</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga26619060de89ad70f1f63a20b4d8d020">isLiteral</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga36f1eff876808586db368dc1b6da5f56">isOr</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gad8c63abfec9cc4a8319f3df1b47eee45">isPropAtom</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaccf96ea73570e38c5c7e4ad39ed8b509">isPropLiteral</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga35249e04af38d4641c873e358188d47a">isQuantifier</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gac5ced6adc7a60945ea6707ef494aa28f">isRational</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga61d63967e5419f6d32eb153e7e39a913">isRawList</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga8b55ff94d7f47d1166350cf308f2dd09">isRegisteredAtom</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gad27a864cc3351877b2b132f3dfe4ac1c">isRewriteNormal</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga3292a2d664355dd3246479f21e6f26cb">isSelected</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gab181584fa647ee5ef5f10e9050225562">isSkolem</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga2dab8e7d46762ef10be1f34bd14e751b">isStoredPredicate</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga72034a21a6bcbd4d5d2085aa23c8f290">isString</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga93059bf6ddd8020cef4e6796a3c9b5a4">isSymbol</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gad527acb49daef3591b78c748746e7eef">isTerm</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga8ec720fa4004f3f7036b0fba87393d83">isTheorem</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gabe0b99a2c155f75ceedd4f06263ddebb">isTranslated</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gadf8596df73fa69ff8e6a22b9321f5c34">isTrue</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gaea43cdb4de7c9216d0adcc1807a6eccc">isType</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gadeefef680b6323acc5d79a553644be8e">isUserAssumption</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga8296386eb481a436937b6f0b140f8af0">isUserRegisteredAtom</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaed5d5a14a8089122a0e05a55e38fc37f">isValidType</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga55b6a203b4375e64598306596851d9ae">isVar</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaa7dc360962f097870ecc6a4cc14c4909">isWellFounded</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gace27719ae0da2a171560b9fda9e10c8b">isXor</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga5532cabad6f699c57da32a8db65a38da">iteExpr</a>(const Expr &amp;thenpart, const Expr &amp;elsepart) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga801d77a373d26549c735dbd8a7fda1a5">lookupType</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga3aefe2fb15c2d8e3a51dd92dbcc5cdc5">mkOp</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gab1ce461dc931af73bf04e88c8d37dcbc">negate</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gga74e5360ad3392aa4779d981670887936a0328c59b775199c11653b376c0f3c8cb">NOT_ARRAY_NORMALIZED</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gaabb885ae903ae169ed75137653dc2538">notArrayNormalized</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga59d07586d68ba39eadd98c86492acdac">notExpr</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1Expr.html#a2c31e8a3c11caeb061d69db14ebb0e95">Op</a> class</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gab13e5c897123bbde4b24e9571d27a88c">operator!</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga7da18dfc7cf83f48c3b68eaf7bdaeca0">operator!=</a>(const Expr &amp;e1, const Expr &amp;e2)</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga0fff31138ef63bbc3a7defd92af9fca2">operator&amp;&amp;</a>(const Expr &amp;right) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga1d72417bdb285b126416d7d169e463dd">operator&lt;</a>(const Expr &amp;e1, const Expr &amp;e2)</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga691d71052166260b4f5b5a2ee3cda464">operator&lt;&lt;</a>(std::ostream &amp;os, const Expr &amp;e)</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga205ae18c57fd12d497996c7edad4c073">operator&lt;=</a>(const Expr &amp;e1, const Expr &amp;e2)</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga0cc4af99d81c96b3c529d3b866861550">operator=</a>(const Expr &amp;e)</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gab39e411af6eecf3b4a34ebcd5c37c1d9">operator==</a>(const Expr &amp;e1, const Expr &amp;e2)</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga38fa42aec5b81d57acd5a605c73ead83">operator&gt;</a>(const Expr &amp;e1, const Expr &amp;e2)</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga5a1d868d3eb493b773101b5601984156">operator&gt;=</a>(const Expr &amp;e1, const Expr &amp;e2)</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga5b242a4834df256dc2055e310fb0e727">operator[]</a>(int i) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga909307189b2a1c7e122d139ce6f093f0">operator||</a>(const Expr &amp;right) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaf310870d783fff343e77ba9c2277c626">orExpr</a>(const Expr &amp;right) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga3aa47bf8af3f2c88b8bc27e0cd07554e">pprint</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga010ae48d41f33790c6b9bb10829105e3">pprintnodag</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga76180628bc1561af88e41be586973fac">print</a>(InputLanguage lang, bool dagify=true) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gae30ed55f3ca40745ad3735ddc7c55645">print</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gaa26519c37fd631580f14664d83dcb4fa">print</a>(ExprStream &amp;os) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga092308b0a88e12a5c7ff2fc0a2eca818">printAST</a>(ExprStream &amp;os) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga974964d4dba5b50f35ee03e2418e7fe9">printnodag</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga3df149427d124797567614e07080519d">rebuild</a>(ExprManager *em) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga644bfdf1ae59727d6626c764208483e8">recursiveQuantSubst</a>(const ExprHashMap&lt; Expr &gt; &amp;subst, ExprHashMap&lt; Expr &gt; &amp;visited) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga7ee0a2ffca952496e3f1d8c9c9d66aab">recursiveSubst</a>(const ExprHashMap&lt; Expr &gt; &amp;subst, ExprHashMap&lt; Expr &gt; &amp;visited) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316ca6279757281c85b060623657eae639d11">REWRITE_NORMAL</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga7ad4f1f01878e19f3a6318a846dbfe6f">s_null</a></td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span><span class="mlabel">static</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga5513f05f1d104aa5dc4fd8724b46e221">setComputeTransClosure</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga46031ec4323f6c373c7ffb59b4db30e9">setContainsBoundVar</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gae283f0adb5cb21761081fc267ba8eba2">setEqNext</a>(const Theorem &amp;e) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga5318abf2b6333d23b3cfa8877a93151d">setFind</a>(const Theorem &amp;e) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gaecb0afa375de675309b6d1ec72a5c648">setFinite</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga4695a56a4bdc943174eda1f41cbcead4">setFlag</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gaece7bfa79c995a45964a7dc5f2408e55">setImpliedLiteral</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga8b1ac81529d2ebee895a385a35460d39">setIntAssumption</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gacfaaa30a1743a0955e0568b3bcd7cc08">setInUserAssumption</a>(int scope=-1) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga5c1a2072d2478708bc788814385e00c4">setIsAtomicFlag</a>(bool value) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga98a725d64a530023a36be8045d87863a">setJustified</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga91a460603cf210681cfdec52a98fa076">setMultiTrigger</a>(const std::vector&lt; Expr &gt; &amp;multiTrigger) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gaa09f6f3f2938359d472a0c099ff0c634">setNotArrayNormalized</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga6adb700b834218ed8aaf4296458d9bf9">setRegisteredAtom</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga7b85677789c5a03e1a5dc2c93f0b6288">setRep</a>(const Theorem &amp;e) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga06284723527dbaa4784949f63f586877">setRewriteNormal</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga50ebe7a6fa50064b2d01e0eaa25f931a">setSelected</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaaaba7ddaccd58bd37e3259fe9b949645">setSig</a>(const Theorem &amp;e) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga933505a9529110425c3e7d3cd2e90c2c">setSimpCache</a>(const Theorem &amp;e) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga911ab512eb2b3d2f8e59280261b847d6">setStoredPredicate</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga4158db17700c28f6fbd6be955c4ad075">setTerminalsConstFlag</a>(bool value) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaf941ebb5b9a8e6ee0ca004d59425fb42">setTranslated</a>(int scope=-1) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga4e0dcc7b987305b845414ce0a7089381">setTrigger</a>(const Expr &amp;trigger) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gad15dc19335e0f59dddbb75d1d27579e7">setTriggers</a>(const std::vector&lt; std::vector&lt; Expr &gt; &gt; &amp;triggers) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga05ec7fb847036e29c782c3595f758a70">setTriggers</a>(const std::vector&lt; Expr &gt; &amp;triggers) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga07d47f902598e00097086deabf04d9c5">setType</a>(const Type &amp;t) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga63eb3b8c124654cf056b2814794c4236">setUserAssumption</a>(int scope=-1) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga6f8db899f4680e53c4cf11c20dc10735">setUserRegisteredAtom</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga243c5d26015ee1fd946f8ccce5f83568">setUsesCC</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gab854295d8dd4be1c54f62030301e94bd">setValidType</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga3e4a13d6c9c5d1c14d44ca530ca8187d">setWellFounded</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga1311a04a68f4cfae68a82826a3a0c5ad">skolemExpr</a>(int i) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga5285f004f382cfb7a002f8dea3b3316c">StaticFlagsEnum</a> enum name</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga4b89f3d46b36f66acb191a4fb359d69f">subExprOf</a>(const Expr &amp;e) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga95e18015860195a80b317bf756055786">substExpr</a>(const std::vector&lt; Expr &gt; &amp;oldTerms, const std::vector&lt; Expr &gt; &amp;newTerms) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga266ba75d3cf61c772b26a36ef5909a52">substExpr</a>(const ExprHashMap&lt; Expr &gt; &amp;oldToNew) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga7cbbc123771321651e176a346731d255">substExprQuant</a>(const std::vector&lt; Expr &gt; &amp;oldTerms, const std::vector&lt; Expr &gt; &amp;newTerms) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga6d955aae7246b6e55c7de394fe7895d4">substExprQuant</a>(const ExprHashMap&lt; Expr &gt; &amp;oldToNew) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga2605b52bcaa9bf4c04115a63ea773c9c">substTriggers</a>(const ExprHashMap&lt; Expr &gt; &amp;subst, ExprHashMap&lt; Expr &gt; &amp;visited) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316ca8f04196095a0b34d324a5c004d08317d">TERMINALS_CONST</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1Expr.html#a51f48d7e14c97707595cfe5f8f6df209">Theorem</a> class</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54">toString</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga306e932ab9a486c9350d55e216ae0de5">toString</a>(InputLanguage lang) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga9030cf2556acc13a160355c55e0a1b4e">typeCard</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga9abac5907964bb1ca7d6ad7d1280791c">typeEnumerateFinite</a>(Unsigned n) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gaefc32b444057849c6364e63b7d4c3cf3">typeSizeFinite</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga39070a3fb12c398dc5bb7526d6aeb7f3">unnegate</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316cad414c75c14f9cc186e6e7df225396627">USES_CC</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga0f1f1ce3472f18a4b6575805e0347bce">usesCC</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316ca4bc8d45f29e985faa033b685c209c934">VALID_IS_ATOMIC</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316ca501e68dd8eb63c2ed0d6f52f1eb844f8">VALID_TERMINALS_CONST</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316ca064c35d31f9b779c3c327a38c22f7d5a">VALID_TYPE</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga501126e42edf75538f510b7b87df96f1">validIsAtomicFlag</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga99348741c5062f8c8e62962b787a73fd">validSimpCache</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga0016a263d60de73f5924072848515699">validTerminalsConstFlag</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316ca9f0f9b43c297449dc513bba12a343c0d">WELL_FOUNDED</a> enum value</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
  <tr><td class="entry"><a class="el" href="group__ExprPkg.html#ga37b3161a078f8992b71518992ab0b088">xorExpr</a>(const Expr &amp;right) const </td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="group__ExprPkg.html#ga8be57c8709c3b35792306ea50cfc06d5">~Expr</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
</table></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:17 for CVC3 by &#160;<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>