<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: CVC3::Expr Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="hierarchy.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a> </li>
<li class="navelem"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </li>
</ul>
</div>
</div>
<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> </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>
<div class="contents">
<!-- doxytag: class="CVC3::Expr" -->
<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>
<p><a href="classCVC3_1_1Expr-members.html">List of all members.</a></p>
<h2><a name="nested-classes"></a>
Classes</h2>
<ul>
<li>class <a class="el" href="classCVC3_1_1Expr_1_1iterator.html">iterator</a>
</ul>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="group__ExprPkg.html#gaf3f35afa568a157d6f58ad24fd46b9d1">Expr</a> ()
<dl class="el"><dd 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/></dl><li><a class="el" href="group__ExprPkg.html#ga8e424c562e5d452d4ddc50f6e7b3e063">Expr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Copy constructor and assignment (copy the pointer and take care of the refcount) <a href="group__ExprPkg.html#ga8e424c562e5d452d4ddc50f6e7b3e063"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="group__ExprPkg.html#ga0cc4af99d81c96b3c529d3b866861550">operator=</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Assignment operator: take care of the refcounting and GC. <a href="group__ExprPkg.html#ga0cc4af99d81c96b3c529d3b866861550"></a><br/></dl><li><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)
<li><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)
<li><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)
<li><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)
<li><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)
<li><a class="el" href="group__ExprPkg.html#ga8be57c8709c3b35792306ea50cfc06d5">~Expr</a> ()
<dl class="el"><dd class="mdescRight">Destructor. <a href="group__ExprPkg.html#ga8be57c8709c3b35792306ea50cfc06d5"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__ExprPkg.html#gacb48495ca445c895f95d0c3c1ae2070b">eqExpr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &right) const
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__ExprPkg.html#ga59d07586d68ba39eadd98c86492acdac">notExpr</a> () const
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__ExprPkg.html#gab1ce461dc931af73bf04e88c8d37dcbc">negate</a> () const
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__ExprPkg.html#ga6c3651465ce69ed5f4e6fd461b9acf3c">andExpr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &right) const
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__ExprPkg.html#gaf310870d783fff343e77ba9c2277c626">orExpr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &right) const
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <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
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__ExprPkg.html#gaae017ca8e68af655ba285c985dd9fba5">iffExpr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &right) const
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__ExprPkg.html#ga8dd97bcdeb9d8870238f94a263fd083b">impExpr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &right) const
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__ExprPkg.html#ga37b3161a078f8992b71518992ab0b088">xorExpr</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &right) const
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__ExprPkg.html#ga1311a04a68f4cfae68a82826a3a0c5ad">skolemExpr</a> (int i) const
<dl class="el"><dd class="mdescRight">Create a Skolem constant for the i'th variable of an existential (*this) <a href="group__ExprPkg.html#ga1311a04a68f4cfae68a82826a3a0c5ad"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__ExprPkg.html#ga3df149427d124797567614e07080519d">rebuild</a> (<a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> *em) const
<dl class="el"><dd class="mdescRight">Create a Boolean variable out of the expression. <a href="group__ExprPkg.html#ga3df149427d124797567614e07080519d"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <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
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <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
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <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
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <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
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__ExprPkg.html#gab13e5c897123bbde4b24e9571d27a88c">operator!</a> () const
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__ExprPkg.html#ga0fff31138ef63bbc3a7defd92af9fca2">operator&&</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &right) const
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__ExprPkg.html#ga909307189b2a1c7e122d139ce6f093f0">operator||</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &right) const
<li>size_t <a class="el" href="group__ExprPkg.html#gae11bd9d6d259d280c77cb1778520daa4">hash</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga6173f64b22cba76472cd0c814bbf6dae">isFalse</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gadf8596df73fa69ff8e6a22b9321f5c34">isTrue</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga5c2cee598096c66e80d87490d6505bc4">isBoolConst</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga55b6a203b4375e64598306596851d9ae">isVar</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga01122f4c0d9a19d9b991600e480cc862">isBoundVar</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga72034a21a6bcbd4d5d2085aa23c8f290">isString</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga3127f52184d5bcb2d4056cb23f3a292b">isClosure</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga35249e04af38d4641c873e358188d47a">isQuantifier</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga165dba5b9e9502059c3cf01bddf4fe1e">isLambda</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga1d6a6b4a9ce81b0dd8fd74870ff4284b">isApply</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga93059bf6ddd8020cef4e6796a3c9b5a4">isSymbol</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga8ec720fa4004f3f7036b0fba87393d83">isTheorem</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga3c3645e1962f6de72655c650639e7a2d">isConstant</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga61d63967e5419f6d32eb153e7e39a913">isRawList</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gaea43cdb4de7c9216d0adcc1807a6eccc">isType</a> () const
<dl class="el"><dd 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/></dl><li>const <a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> * <a class="el" href="group__ExprPkg.html#gad21442cf6ecf46e8fcccbef451f4041b">getExprValue</a> () const
<dl class="el"><dd 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> *only*. <a href="group__ExprPkg.html#gad21442cf6ecf46e8fcccbef451f4041b"></a><br/></dl><li>bool <a class="el" href="group__ExprPkg.html#gad527acb49daef3591b78c748746e7eef">isTerm</a> () const
<dl class="el"><dd class="mdescRight">Test if e is a term (as opposed to a predicate/formula) <a href="group__ExprPkg.html#gad527acb49daef3591b78c748746e7eef"></a><br/></dl><li>bool <a class="el" href="group__ExprPkg.html#ga48a9219339b394280550069ac7b0474f">isAtomic</a> () const
<dl class="el"><dd class="mdescRight">Test if e is atomic. <a href="group__ExprPkg.html#ga48a9219339b394280550069ac7b0474f"></a><br/></dl><li>bool <a class="el" href="group__ExprPkg.html#ga4b575e0a191cc42706ff5b5a169c3069">isAtomicFormula</a> () const
<dl class="el"><dd class="mdescRight">Test if e is an atomic formula. <a href="group__ExprPkg.html#ga4b575e0a191cc42706ff5b5a169c3069"></a><br/></dl><li>bool <a class="el" href="group__ExprPkg.html#ga5fe5158aefab64fd8adda48ecebb98f9">isAbsAtomicFormula</a> () const
<dl class="el"><dd class="mdescRight">An abstract atomic formua is an atomic formula or a quantified formula. <a href="group__ExprPkg.html#ga5fe5158aefab64fd8adda48ecebb98f9"></a><br/></dl><li>bool <a class="el" href="group__ExprPkg.html#ga26619060de89ad70f1f63a20b4d8d020">isLiteral</a> () const
<dl class="el"><dd class="mdescRight">Test if e is a literal. <a href="group__ExprPkg.html#ga26619060de89ad70f1f63a20b4d8d020"></a><br/></dl><li>bool <a class="el" href="group__ExprPkg.html#gaac535dae48f02fcd093a5b1b1a062211">isAbsLiteral</a> () const
<dl class="el"><dd class="mdescRight">Test if e is an abstract literal. <a href="group__ExprPkg.html#gaac535dae48f02fcd093a5b1b1a062211"></a><br/></dl><li>bool <a class="el" href="group__ExprPkg.html#gac03948739e860fa791fd3bbb713c1076">isBoolConnective</a> () const
<dl class="el"><dd 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/></dl><li>bool <a class="el" href="group__ExprPkg.html#gad8c63abfec9cc4a8319f3df1b47eee45">isPropAtom</a> () const
<dl class="el"><dd class="mdescRight">True iff expr is not a Bool connective. <a href="group__ExprPkg.html#gad8c63abfec9cc4a8319f3df1b47eee45"></a><br/></dl><li>bool <a class="el" href="group__ExprPkg.html#gaccf96ea73570e38c5c7e4ad39ed8b509">isPropLiteral</a> () const
<dl class="el"><dd class="mdescRight">PropAtom or negation of PropAtom. <a href="group__ExprPkg.html#gaccf96ea73570e38c5c7e4ad39ed8b509"></a><br/></dl><li>bool <a class="el" href="group__ExprPkg.html#gaf53e6a6f9dc01481d2cf94673c5505ce">containsTermITE</a> () const
<dl class="el"><dd 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/></dl><li>bool <a class="el" href="group__ExprPkg.html#gac4af2026c180da0f18d66ac616f61f3a">isEq</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga383260cf4f8919728e2712e6e11f21fa">isAnd</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga36f1eff876808586db368dc1b6da5f56">isOr</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gaef13fa4752a1fb28e129a1efd0e26f01">isITE</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gabe385fb97505cccb75702378511c5375">isIff</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga9067c706c6454ea1761ace7d7837af46">isImpl</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gace27719ae0da2a171560b9fda9e10c8b">isXor</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga1c922163af59ed6bc101728d65e04d16">isExists</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gac5ced6adc7a60945ea6707ef494aa28f">isRational</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gab181584fa647ee5ef5f10e9050225562">isSkolem</a> () const
<li>const std::string & <a class="el" href="group__ExprPkg.html#gaa3023d9117f249f079b0a202a1dfc5c2">getName</a> () const
<li>const std::string & <a class="el" href="group__ExprPkg.html#ga2b086a0194b24a3f31afd402cea7de94">getUid</a> () const
<dl class="el"><dd class="mdescRight">For BOUND_VAR, get the UID. <a href="group__ExprPkg.html#ga2b086a0194b24a3f31afd402cea7de94"></a><br/></dl><li>const std::string & <a class="el" href="group__ExprPkg.html#ga5e679ab39ad8166c3c027afee9004c26">getString</a> () const
<li>const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & <a class="el" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd">getVars</a> () const
<dl class="el"><dd 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/></dl><li>const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="group__ExprPkg.html#gaf12c1f078a1106ba7d7896c45b2eb4cb">getExistential</a> () const
<dl class="el"><dd class="mdescRight">Get the existential axiom expression for skolem constant. <a href="group__ExprPkg.html#gaf12c1f078a1106ba7d7896c45b2eb4cb"></a><br/></dl><li>int <a class="el" href="group__ExprPkg.html#ga58d51b54987242f54071bdcc0d7d183f">getBoundIndex</a> () const
<dl class="el"><dd class="mdescRight">Get the index of the bound var that skolem constant comes from. <a href="group__ExprPkg.html#ga58d51b54987242f54071bdcc0d7d183f"></a><br/></dl><li>const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940">getBody</a> () const
<dl class="el"><dd 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/></dl><li>void <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
<dl class="el"><dd 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/></dl><li>void <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
<li>void <a class="el" href="group__ExprPkg.html#ga4e0dcc7b987305b845414ce0a7089381">setTrigger</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &trigger) const
<li>void <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
<li>const std::vector< std::vector<br class="typebreak"/>
< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > > & <a class="el" href="group__ExprPkg.html#gae4cffec57be4b7d81e8486328c2396fc">getTriggers</a> () const
<dl class="el"><dd 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/></dl><li>const <a class="el" href="classCVC3_1_1Rational.html">Rational</a> & <a class="el" href="group__ExprPkg.html#gab0eee70e4a7f97c09954dc61b71b65e5">getRational</a> () const
<dl class="el"><dd 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/></dl><li>const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & <a class="el" href="group__ExprPkg.html#ga29db2c821567c944bc14f8156eb092b6">getTheorem</a> () const
<dl class="el"><dd class="mdescRight">Get theorem from THEOREM_EXPR. <a href="group__ExprPkg.html#ga29db2c821567c944bc14f8156eb092b6"></a><br/></dl><li><a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> * <a class="el" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a> () const
<li>const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & <a class="el" href="group__ExprPkg.html#ga1e18ae89889e781591eb2874a4196b73">getKids</a> () const
<li>int <a class="el" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a> () const
<li><a class="el" href="namespaceCVC3.html#a4233916514848331ee104548acbab912">ExprIndex</a> <a class="el" href="group__ExprPkg.html#gadaddb9b0566ecddd4611a10e820dc544">getIndex</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gaa930fda58c8146f27f3dacaab017015c">hasLastIndex</a> () const
<li><a class="el" href="classCVC3_1_1Op.html">Op</a> <a class="el" href="group__ExprPkg.html#ga3aefe2fb15c2d8e3a51dd92dbcc5cdc5">mkOp</a> () const
<dl class="el"><dd class="mdescRight">Make the expr into an operator. <a href="group__ExprPkg.html#ga3aefe2fb15c2d8e3a51dd92dbcc5cdc5"></a><br/></dl><li><a class="el" href="classCVC3_1_1Op.html">Op</a> <a class="el" href="group__ExprPkg.html#gace479f04faca399219496195152f7806">getOp</a> () const
<dl class="el"><dd class="mdescRight">Get operator from expression. <a href="group__ExprPkg.html#gace479f04faca399219496195152f7806"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__ExprPkg.html#ga9f3328fe077191803a780cfd6566ff9b">getOpExpr</a> () const
<dl class="el"><dd class="mdescRight">Get expression of operator (for APPLY Exprs only) <a href="group__ExprPkg.html#ga9f3328fe077191803a780cfd6566ff9b"></a><br/></dl><li>int <a class="el" href="group__ExprPkg.html#gad036a3a3597d590ca6ee694505c6e1cd">getOpKind</a> () const
<dl class="el"><dd class="mdescRight">Get kind of operator (for APPLY Exprs only) <a href="group__ExprPkg.html#gad036a3a3597d590ca6ee694505c6e1cd"></a><br/></dl><li>int <a class="el" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a> () const
<li>const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="group__ExprPkg.html#ga5b242a4834df256dc2055e310fb0e727">operator[]</a> (int i) const
<li>const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="group__ExprPkg.html#ga39070a3fb12c398dc5bb7526d6aeb7f3">unnegate</a> () const
<dl class="el"><dd class="mdescRight">Remove leading NOT if any. <a href="group__ExprPkg.html#ga39070a3fb12c398dc5bb7526d6aeb7f3"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr_1_1iterator.html">iterator</a> <a class="el" href="group__ExprPkg.html#gac890e13db184610276fc533fa4b4fe99">begin</a> () const
<dl class="el"><dd class="mdescRight">Begin iterator. <a href="group__ExprPkg.html#gac890e13db184610276fc533fa4b4fe99"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr_1_1iterator.html">iterator</a> <a class="el" href="group__ExprPkg.html#gaf6048a5030c8fa2511bf5dfee868e653">end</a> () const
<dl class="el"><dd class="mdescRight">End iterator. <a href="group__ExprPkg.html#gaf6048a5030c8fa2511bf5dfee868e653"></a><br/></dl><li>bool <a class="el" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gaa3359d5f6638eba5479c4c4036a551a8">isInitialized</a> () const
<li>size_t <a class="el" href="group__ExprPkg.html#gaca3ae54b26443a7d5a74cc7d6f5e81e3">getMMIndex</a> () const
<dl class="el"><dd class="mdescRight">Get the memory manager index (it uniquely identifies the subclass) <a href="group__ExprPkg.html#gaca3ae54b26443a7d5a74cc7d6f5e81e3"></a><br/></dl><li>bool <a class="el" href="group__ExprPkg.html#ga4dc94c33ae308ff8d9d004f49df8f42b">hasFind</a> () const
<li>const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & <a class="el" href="group__ExprPkg.html#ga9be55edbdc2c0878fec750921a9fcc89">getFind</a> () const
<li>int <a class="el" href="group__ExprPkg.html#ga45ea7926a65c7c5559c81f1f20bde281">getFindLevel</a> () const
<li>const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & <a class="el" href="group__ExprPkg.html#gaac6e2bdafe4cb6b91d4bec8fa656bcb2">getEqNext</a> () const
<li><a class="el" href="classCVC3_1_1NotifyList.html">NotifyList</a> * <a class="el" href="group__ExprPkg.html#gace67f5f11fd81d9ecebba441b8c02e07">getNotify</a> () const
<li><a class="el" href="classCVC3_1_1Type.html">Type</a> <a class="el" href="group__ExprPkg.html#ga42929221eb172250697b72c28af6de07">getType</a> () const
<dl class="el"><dd class="mdescRight">Get the type. Recursively compute if necessary. <a href="group__ExprPkg.html#ga42929221eb172250697b72c28af6de07"></a><br/></dl><li><a class="el" href="classCVC3_1_1Type.html">Type</a> <a class="el" href="group__ExprPkg.html#ga801d77a373d26549c735dbd8a7fda1a5">lookupType</a> () const
<dl class="el"><dd class="mdescRight">Look up the current type. Do not recursively compute (i.e. may be NULL) <a href="group__ExprPkg.html#ga801d77a373d26549c735dbd8a7fda1a5"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54">Cardinality</a> <a class="el" href="group__ExprPkg.html#ga9030cf2556acc13a160355c55e0a1b4e">typeCard</a> () const
<dl class="el"><dd class="mdescRight">Return cardinality of type. <a href="group__ExprPkg.html#ga9030cf2556acc13a160355c55e0a1b4e"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__ExprPkg.html#ga9abac5907964bb1ca7d6ad7d1280791c">typeEnumerateFinite</a> (<a class="el" href="classCVC3_1_1Unsigned.html">Unsigned</a> n) const
<dl class="el"><dd class="mdescRight">Return nth (starting with 0) element in a finite type. <a href="group__ExprPkg.html#ga9abac5907964bb1ca7d6ad7d1280791c"></a><br/></dl><li><a class="el" href="classCVC3_1_1Unsigned.html">Unsigned</a> <a class="el" href="group__ExprPkg.html#gaefc32b444057849c6364e63b7d4c3cf3">typeSizeFinite</a> () const
<dl class="el"><dd class="mdescRight">Return size of a finite type; returns 0 if size cannot be determined. <a href="group__ExprPkg.html#gaefc32b444057849c6364e63b7d4c3cf3"></a><br/></dl><li>bool <a class="el" href="group__ExprPkg.html#ga99348741c5062f8c8e62962b787a73fd">validSimpCache</a> () const
<dl class="el"><dd 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/></dl><li>const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & <a class="el" href="group__ExprPkg.html#ga5dbb07a3a7f3a7154ad3bcdb58bbdec6">getSimpCache</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gaed5d5a14a8089122a0e05a55e38fc37f">isValidType</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga501126e42edf75538f510b7b87df96f1">validIsAtomicFlag</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga0016a263d60de73f5924072848515699">validTerminalsConstFlag</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gaaa895b97bdc2413b72419cc781178995">getIsAtomicFlag</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gab990a9104757ac6854b92c3b98727b9c">getTerminalsConstFlag</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gad27a864cc3351877b2b132f3dfe4ac1c">isRewriteNormal</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gacf628bd70fc2c4766afa268ed22ea947">isFinite</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gaa7dc360962f097870ecc6a4cc14c4909">isWellFounded</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gac3aeac6fba7a1d6cacfe4bd653c5a084">computeTransClosure</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gacafcbc459ee158f84e3666eaf32ca3f9">containsBoundVar</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga0f1f1ce3472f18a4b6575805e0347bce">usesCC</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gaabb885ae903ae169ed75137653dc2538">notArrayNormalized</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga5d92d645899807eb4351502f2e74369e">isImpliedLiteral</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gadeefef680b6323acc5d79a553644be8e">isUserAssumption</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga110d4a1734b738dbb999b7798e07c3d1">inUserAssumption</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gaf42121131fd56040faef7a64d9e67729">isIntAssumption</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga3cf472ba2fa033f3e1401e4b67a3f8a0">isJustified</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gabe0b99a2c155f75ceedd4f06263ddebb">isTranslated</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga8296386eb481a436937b6f0b140f8af0">isUserRegisteredAtom</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga8b55ff94d7f47d1166350cf308f2dd09">isRegisteredAtom</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga3292a2d664355dd3246479f21e6f26cb">isSelected</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga2dab8e7d46762ef10be1f34bd14e751b">isStoredPredicate</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gab9779994b0bb78e555c4f9e2163571ed">getFlag</a> () const
<dl class="el"><dd class="mdescRight">Check if the generic flag is set. <a href="group__ExprPkg.html#gab9779994b0bb78e555c4f9e2163571ed"></a><br/></dl><li>void <a class="el" href="group__ExprPkg.html#ga4695a56a4bdc943174eda1f41cbcead4">setFlag</a> () const
<dl class="el"><dd class="mdescRight">Set the generic flag. <a href="group__ExprPkg.html#ga4695a56a4bdc943174eda1f41cbcead4"></a><br/></dl><li>void <a class="el" href="group__ExprPkg.html#ga463076527f4fb2b87362ee268abc013f">clearFlags</a> () const
<dl class="el"><dd class="mdescRight">Clear the generic flag in all Exprs. <a href="group__ExprPkg.html#ga463076527f4fb2b87362ee268abc013f"></a><br/></dl><li>std::string <a class="el" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54">toString</a> () const
<dl class="el"><dd class="mdescRight">Print the expression to a string. <a href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54"></a><br/></dl><li>std::string <a class="el" href="group__ExprPkg.html#ga306e932ab9a486c9350d55e216ae0de5">toString</a> (<a class="el" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e">InputLanguage</a> lang) const
<dl class="el"><dd class="mdescRight">Print the expression to a string using the given output language. <a href="group__ExprPkg.html#ga306e932ab9a486c9350d55e216ae0de5"></a><br/></dl><li>void <a class="el" href="group__ExprPkg.html#ga76180628bc1561af88e41be586973fac">print</a> (<a class="el" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e">InputLanguage</a> lang, bool dagify=true) const
<dl class="el"><dd class="mdescRight">Print the expression in the specified format. <a href="group__ExprPkg.html#ga76180628bc1561af88e41be586973fac"></a><br/></dl><li>void <a class="el" href="group__ExprPkg.html#gae30ed55f3ca40745ad3735ddc7c55645">print</a> () const
<dl class="el"><dd class="mdescRight">Print the expression as AST (lisp-like format) <a href="group__ExprPkg.html#gae30ed55f3ca40745ad3735ddc7c55645"></a><br/></dl><li>void <a class="el" href="group__ExprPkg.html#ga974964d4dba5b50f35ee03e2418e7fe9">printnodag</a> () const
<dl class="el"><dd class="mdescRight">Print the expression as AST without dagifying. <a href="group__ExprPkg.html#ga974964d4dba5b50f35ee03e2418e7fe9"></a><br/></dl><li>void <a class="el" href="group__ExprPkg.html#ga3aa47bf8af3f2c88b8bc27e0cd07554e">pprint</a> () const
<dl class="el"><dd class="mdescRight">Pretty-print the expression. <a href="group__ExprPkg.html#ga3aa47bf8af3f2c88b8bc27e0cd07554e"></a><br/></dl><li>void <a class="el" href="group__ExprPkg.html#ga010ae48d41f33790c6b9bb10829105e3">pprintnodag</a> () const
<dl class="el"><dd class="mdescRight">Pretty-print without dagifying. <a href="group__ExprPkg.html#ga010ae48d41f33790c6b9bb10829105e3"></a><br/></dl><li><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & <a class="el" href="group__ExprPkg.html#gaa26519c37fd631580f14664d83dcb4fa">print</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &os) const
<dl class="el"><dd class="mdescRight">Print a leaf node. <a href="group__ExprPkg.html#gaa26519c37fd631580f14664d83dcb4fa"></a><br/></dl><li><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & <a class="el" href="group__ExprPkg.html#ga092308b0a88e12a5c7ff2fc0a2eca818">printAST</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &os) const
<dl class="el"><dd class="mdescRight">Print the top node and then recurse through the children */. <a href="group__ExprPkg.html#ga092308b0a88e12a5c7ff2fc0a2eca818"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="group__ExprPkg.html#ga9050d11fa8e8ece11ab586a560081196">indent</a> (int n, bool permanent=false)
<dl class="el"><dd class="mdescRight">Set initial indentation to n. <a href="group__ExprPkg.html#ga9050d11fa8e8ece11ab586a560081196"></a><br/></dl><li>void <a class="el" href="group__ExprPkg.html#ga5318abf2b6333d23b3cfa8877a93151d">setFind</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e) const
<dl class="el"><dd class="mdescRight">Set the find attribute to e. <a href="group__ExprPkg.html#ga5318abf2b6333d23b3cfa8877a93151d"></a><br/></dl><li>void <a class="el" href="group__ExprPkg.html#gae283f0adb5cb21761081fc267ba8eba2">setEqNext</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e) const
<dl class="el"><dd class="mdescRight">Set the eqNext attribute to e. <a href="group__ExprPkg.html#gae283f0adb5cb21761081fc267ba8eba2"></a><br/></dl><li>void <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
<dl class="el"><dd class="mdescRight">Add (e,i) to the notify list of this expression. <a href="group__ExprPkg.html#ga159d60cb0f32e09df89a395b2680664a"></a><br/></dl><li>void <a class="el" href="group__ExprPkg.html#ga07d47f902598e00097086deabf04d9c5">setType</a> (const <a class="el" href="classCVC3_1_1Type.html">Type</a> &t) const
<dl class="el"><dd class="mdescRight">Set the cached type. <a href="group__ExprPkg.html#ga07d47f902598e00097086deabf04d9c5"></a><br/></dl><li>void <a class="el" href="group__ExprPkg.html#ga933505a9529110425c3e7d3cd2e90c2c">setSimpCache</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e) const
<li>void <a class="el" href="group__ExprPkg.html#gab854295d8dd4be1c54f62030301e94bd">setValidType</a> () const
<li>void <a class="el" href="group__ExprPkg.html#ga5c1a2072d2478708bc788814385e00c4">setIsAtomicFlag</a> (bool value) const
<li>void <a class="el" href="group__ExprPkg.html#ga4158db17700c28f6fbd6be955c4ad075">setTerminalsConstFlag</a> (bool value) const
<li>void <a class="el" href="group__ExprPkg.html#ga06284723527dbaa4784949f63f586877">setRewriteNormal</a> () const
<li>void <a class="el" href="group__ExprPkg.html#ga643f89574537ab6acf9bb1bc2f703c77">clearRewriteNormal</a> () const
<li>void <a class="el" href="group__ExprPkg.html#gaecb0afa375de675309b6d1ec72a5c648">setFinite</a> () const
<li>void <a class="el" href="group__ExprPkg.html#ga3e4a13d6c9c5d1c14d44ca530ca8187d">setWellFounded</a> () const
<li>void <a class="el" href="group__ExprPkg.html#ga5513f05f1d104aa5dc4fd8724b46e221">setComputeTransClosure</a> () const
<li>void <a class="el" href="group__ExprPkg.html#ga46031ec4323f6c373c7ffb59b4db30e9">setContainsBoundVar</a> () const
<li>void <a class="el" href="group__ExprPkg.html#ga243c5d26015ee1fd946f8ccce5f83568">setUsesCC</a> () const
<li>void <a class="el" href="group__ExprPkg.html#gaa09f6f3f2938359d472a0c099ff0c634">setNotArrayNormalized</a> () const
<li>void <a class="el" href="group__ExprPkg.html#gaece7bfa79c995a45964a7dc5f2408e55">setImpliedLiteral</a> () const
<li>void <a class="el" href="group__ExprPkg.html#ga63eb3b8c124654cf056b2814794c4236">setUserAssumption</a> (int scope=-1) const
<li>void <a class="el" href="group__ExprPkg.html#gacfaaa30a1743a0955e0568b3bcd7cc08">setInUserAssumption</a> (int scope=-1) const
<li>void <a class="el" href="group__ExprPkg.html#ga8b1ac81529d2ebee895a385a35460d39">setIntAssumption</a> () const
<li>void <a class="el" href="group__ExprPkg.html#ga98a725d64a530023a36be8045d87863a">setJustified</a> () const
<li>void <a class="el" href="group__ExprPkg.html#gaf941ebb5b9a8e6ee0ca004d59425fb42">setTranslated</a> (int scope=-1) const
<dl class="el"><dd 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/></dl><li>void <a class="el" href="group__ExprPkg.html#ga6f8db899f4680e53c4cf11c20dc10735">setUserRegisteredAtom</a> () const
<dl class="el"><dd 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/></dl><li>void <a class="el" href="group__ExprPkg.html#ga6adb700b834218ed8aaf4296458d9bf9">setRegisteredAtom</a> () const
<dl class="el"><dd 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/></dl><li>void <a class="el" href="group__ExprPkg.html#ga50ebe7a6fa50064b2d01e0eaa25f931a">setSelected</a> () const
<dl class="el"><dd 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/></dl><li>void <a class="el" href="group__ExprPkg.html#ga911ab512eb2b3d2f8e59280261b847d6">setStoredPredicate</a> () const
<dl class="el"><dd 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/></dl><li>bool <a class="el" href="group__ExprPkg.html#ga4b89f3d46b36f66acb191a4fb359d69f">subExprOf</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e) const
<dl class="el"><dd 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/></dl><li><a class="el" href="classCVC3_1_1Unsigned.html">Unsigned</a> <a class="el" href="group__ExprPkg.html#gad2f1fb7c447bcc3a7d352fd24a8f265a">getSize</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#ga3cc4e5ec0d7310f1bce3630455147bb3">hasSig</a> () const
<li>bool <a class="el" href="group__ExprPkg.html#gae71c95cf1ca998d57b02a136b379172b">hasRep</a> () const
<li>const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & <a class="el" href="group__ExprPkg.html#gae281b04465cc1bf24b5797c8b5e9cbb4">getSig</a> () const
<li>const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & <a class="el" href="group__ExprPkg.html#gaa4b5652980861e593ab8a741b5521779">getRep</a> () const
<li>void <a class="el" href="group__ExprPkg.html#gaaaba7ddaccd58bd37e3259fe9b949645">setSig</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e) const
<li>void <a class="el" href="group__ExprPkg.html#ga7b85677789c5a03e1a5dc2c93f0b6288">setRep</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e) const
</ul>
<h2><a name="pub-static-methods"></a>
Static Public Member Functions</h2>
<ul>
<li>static size_t <a class="el" href="group__ExprPkg.html#gadf3d59da15e4f78daf0c41ef7779a749">hash</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
</ul>
<h2><a name="pri-types"></a>
Private Types</h2>
<ul>
<li>enum <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/>
}
<dl class="el"><dd class="mdescRight">bit-masks for static flags <a href="group__ExprPkg.html#ga5285f004f382cfb7a002f8dea3b3316c">More...</a><br/></dl><li>enum <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/>
}
<dl class="el"><dd class="mdescRight">bit-masks for dynamic flags <a href="group__ExprPkg.html#ga74e5360ad3392aa4779d981670887936">More...</a><br/></dl></ul>
<h2><a name="pri-methods"></a>
Private Member Functions</h2>
<ul>
<li><a class="el" href="group__ExprPkg.html#gadebfef27e4d0ea75d7d37c3fdbcfb727">Expr</a> (<a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> *expr)
<dl class="el"><dd class="mdescRight">Private constructor, simply wraps around the pointer. <a href="group__ExprPkg.html#gadebfef27e4d0ea75d7d37c3fdbcfb727"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <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
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <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
<li>std::vector< std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > > <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
</ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li><a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> * <a class="el" href="group__ExprPkg.html#ga3a08bea4e8715a268083e1671e340a2e">d_expr</a>
</ul>
<h2><a name="pri-static-attribs"></a>
Static Private Attributes</h2>
<ul>
<li>static <a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__ExprPkg.html#ga7ad4f1f01878e19f3a6318a846dbfe6f">s_null</a>
<dl class="el"><dd class="mdescRight">Convenient null expr. <a href="group__ExprPkg.html#ga7ad4f1f01878e19f3a6318a846dbfe6f"></a><br/></dl></ul>
<h2><a name="friends"></a>
Friends</h2>
<ul>
<li>class <a class="el" href="classCVC3_1_1Expr.html#a966b1c64eb8abb1688f28451453d3479">ExprHasher</a>
<li>class <a class="el" href="classCVC3_1_1Expr.html#a53c627979d9a14928590601b9fd195c2">ExprManager</a>
<li>class <a class="el" href="classCVC3_1_1Expr.html#a2c31e8a3c11caeb061d69db14ebb0e95">Op</a>
<li>class <a class="el" href="classCVC3_1_1Expr.html#a6b4e0ce748563841be8fe35c34ee7975">ExprValue</a>
<li>class <a class="el" href="classCVC3_1_1Expr.html#af86989fa451681663344e67f9ae1be0d">ExprNode</a>
<li>class <a class="el" href="classCVC3_1_1Expr.html#a53271ded90a8b528132eeb7247936492">ExprClosure</a>
<li>class <a class="el" href="classCVC3_1_1Expr.html#a61a2a0fa995725e9988683c6dabd503c">::CInterface</a>
<li>class <a class="el" href="classCVC3_1_1Expr.html#a51f48d7e14c97707595cfe5f8f6df209">Theorem</a>
<li>CVC_DLL std::ostream & <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)
<li>int <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)
<li>bool <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)
<li>bool <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)
<li>bool <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)
<li>bool <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)
<li>bool <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)
<li>bool <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)
</ul>
<hr/><a name="details" id="details"></a><h2>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><hr/><h2>Friends And Related Function Documentation</h2>
<a class="anchor" id="a966b1c64eb8abb1688f28451453d3479"></a><!-- doxytag: member="CVC3::Expr::ExprHasher" ref="a966b1c64eb8abb1688f28451453d3479" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class ExprHasher<code> [friend]</code></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><!-- doxytag: member="CVC3::Expr::ExprManager" ref="a53c627979d9a14928590601b9fd195c2" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a><code> [friend]</code></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><!-- doxytag: member="CVC3::Expr::Op" ref="a2c31e8a3c11caeb061d69db14ebb0e95" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1Op.html">Op</a><code> [friend]</code></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><!-- doxytag: member="CVC3::Expr::ExprValue" ref="a6b4e0ce748563841be8fe35c34ee7975" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a><code> [friend]</code></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><!-- doxytag: member="CVC3::Expr::ExprNode" ref="af86989fa451681663344e67f9ae1be0d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1ExprNode.html">ExprNode</a><code> [friend]</code></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><!-- doxytag: member="CVC3::Expr::ExprClosure" ref="a53271ded90a8b528132eeb7247936492" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1ExprClosure.html">ExprClosure</a><code> [friend]</code></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><!-- doxytag: member="CVC3::Expr::::CInterface" ref="a61a2a0fa995725e9988683c6dabd503c" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class ::CInterface<code> [friend]</code></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><!-- doxytag: member="CVC3::Expr::Theorem" ref="a51f48d7e14c97707595cfe5f8f6df209" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a><code> [friend]</code></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>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
