<!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::Theorem 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_1Theorem.html">Theorem</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pub-static-methods">Static Public Member Functions</a> |
<a href="#pri-methods">Private Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> |
<a href="#friends">Friends</a> </div>
<div class="headertitle">
<div class="title">CVC3::Theorem Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::Theorem" -->
<p><code>#include <<a class="el" href="theorem_8h_source.html">theorem.h</a>></code></p>
<p><a href="classCVC3_1_1Theorem-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li>void <a class="el" href="classCVC3_1_1Theorem.html#ad9da69b34ab2bab4192e5977e5c10498">printDebug</a> () const
<li><a class="el" href="classCVC3_1_1Theorem.html#a4b7574a16eed728fac6e37d2404fdbf8">Theorem</a> ()
<li><a class="el" href="classCVC3_1_1Theorem.html#a43974f559b8faa8db89d81993e911881">Theorem</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &th)
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & <a class="el" href="classCVC3_1_1Theorem.html#adacab84dc4dc38aeb12ddabcb3c4a51d">operator=</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &th)
<li><a class="el" href="classCVC3_1_1Theorem.html#ad72ac2b7be75f1b2848e9d6199c01c83">~Theorem</a> ()
<li>bool <a class="el" href="classCVC3_1_1Theorem.html#ad4573ca6be017cab3c83d28c2dbcebd8">withProof</a> () const
<li>bool <a class="el" href="classCVC3_1_1Theorem.html#a90349125fe644e8a075e1a47a49872c7">withAssumptions</a> () const
<li>bool <a class="el" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a> () const
<li>bool <a class="el" href="classCVC3_1_1Theorem.html#a362c1d70e03803d804bbe300e5f6dc87">isRewrite</a> () const
<li>bool <a class="el" href="classCVC3_1_1Theorem.html#a05282db6832afb4f198d8c6b2b67aeb1">isAssump</a> () const
<li>bool <a class="el" href="classCVC3_1_1Theorem.html#a16f074e60b9e076187efb478889d2c47">isRefl</a> () const
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a> () const
<li>const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="classCVC3_1_1Theorem.html#a206c04f39fbbcacef2337148675553f4">getLHS</a> () const
<li>const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a> () const
<li>void <a class="el" href="classCVC3_1_1Theorem.html#aad446d2963572258f7b8f0c74fb9e299">GetSatAssumptions</a> (std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &assumptions) const
<li>void <a class="el" href="classCVC3_1_1Theorem.html#a524b4dafa4fb8f14742baa856612d92b">getLeafAssumptions</a> (std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &assumptions, bool negate=false) const
<li>void <a class="el" href="classCVC3_1_1Theorem.html#a69c948a7ecc79597eac8eb816e8d76a1">getAssumptionsAndCong</a> (std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &assumptions, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &congruences, bool negate=false) const
<li>const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & <a class="el" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a> () const
<li><a class="el" href="classCVC3_1_1Proof.html">Proof</a> <a class="el" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a> () const
<li>int <a class="el" href="classCVC3_1_1Theorem.html#a112466d9793abcf97015233ffdc4ec5e">getScope</a> () const
<li>unsigned <a class="el" href="classCVC3_1_1Theorem.html#a26b6f0af9e9b2f2a8c22a7dcb9fbb0b1">getQuantLevel</a> () const
<dl class="el"><dd class="mdescRight">Return quantification level for this theorem. <a href="#a26b6f0af9e9b2f2a8c22a7dcb9fbb0b1"></a><br/></dl><li>unsigned <a class="el" href="classCVC3_1_1Theorem.html#abd3642f4230db7cd61aab78fdcc329e3">getQuantLevelDebug</a> () const
<li>void <a class="el" href="classCVC3_1_1Theorem.html#ab3309c937f827595d1d92fa48cb5a471">setQuantLevel</a> (unsigned level)
<dl class="el"><dd class="mdescRight">Set the quantification level for this theorem. <a href="#ab3309c937f827595d1d92fa48cb5a471"></a><br/></dl><li>size_t <a class="el" href="classCVC3_1_1Theorem.html#abe268eaf2b89ffdc4ccb291c0a2eaeb9">hash</a> () const
<li>std::string <a class="el" href="classCVC3_1_1Theorem.html#ac4b1c9570ffb9cc901627ef2abb9ff77">toString</a> () const
<li>void <a class="el" href="classCVC3_1_1Theorem.html#aeb41e125749338e05d680beca6df9ee4">printx</a> () const
<li>void <a class="el" href="classCVC3_1_1Theorem.html#a44f518efb0307d256450628cbc6085d2">printxnodag</a> () const
<li>void <a class="el" href="classCVC3_1_1Theorem.html#ab188a2869b745cb0d5f0e1f0d9081dfa">pprintx</a> () const
<li>void <a class="el" href="classCVC3_1_1Theorem.html#a2ccfcbaed17e735e3e008900d5a06e78">pprintxnodag</a> () const
<li>void <a class="el" href="classCVC3_1_1Theorem.html#af412e1fca4a31f24a63c948f85c18358">print</a> () const
<li>std::ostream & <a class="el" href="classCVC3_1_1Theorem.html#a6ead218343fdbf3e92c26d8c76b9d399">print</a> (std::ostream &os, const std::string &name) const
<dl class="el"><dd class="mdescRight">Printing a theorem to a stream, calling it "name". <a href="#a6ead218343fdbf3e92c26d8c76b9d399"></a><br/></dl></ul>
<tr><td colspan="2"><div class="groupHeader">Methods for Theorem Attributes</div></td></tr>
<tr><td colspan="2"><div class="groupText"><p>Several attributes used in conflict analysis and assumptions graph traversals. </p>
</div></td></tr>
<ul>
<li>bool <a class="el" href="classCVC3_1_1Theorem.html#a1695c9afc9a5c1f8cd000d40b9e2a9cd">isFlagged</a> () const
<dl class="el"><dd class="mdescRight">Check if the flag attribute is set. <a href="#a1695c9afc9a5c1f8cd000d40b9e2a9cd"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1Theorem.html#a621ab2150eedc0e3b38d34275ac206cd">clearAllFlags</a> () const
<dl class="el"><dd class="mdescRight">Clear the flag attribute in all the theorems. <a href="#a621ab2150eedc0e3b38d34275ac206cd"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1Theorem.html#af83d6b4d71bfb558296a1c296a69c3d7">setFlag</a> () const
<dl class="el"><dd class="mdescRight">Set the flag attribute. <a href="#af83d6b4d71bfb558296a1c296a69c3d7"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1Theorem.html#a979f97355a4ecd2d8d8b96b679df5240">setSubst</a> () const
<dl class="el"><dd class="mdescRight">Set flag stating that theorem is an instance of substitution. <a href="#a979f97355a4ecd2d8d8b96b679df5240"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1Theorem.html#ad413df893f7cc81cd2e0a59178b981db">isSubst</a> () const
<dl class="el"><dd class="mdescRight">Is theorem an instance of substitution. <a href="#ad413df893f7cc81cd2e0a59178b981db"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1Theorem.html#a30644e9241516daa6483f5d9c0be4caf">setExpandFlag</a> (bool val) const
<dl class="el"><dd class="mdescRight">Set the "expand" attribute. <a href="#a30644e9241516daa6483f5d9c0be4caf"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1Theorem.html#a2eefa550b2e04a012adc03ba456af38b">getExpandFlag</a> () const
<dl class="el"><dd class="mdescRight">Check the "expand" attribute. <a href="#a2eefa550b2e04a012adc03ba456af38b"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1Theorem.html#a575a8519a298b25db8b728f4c273972c">setLitFlag</a> (bool val) const
<dl class="el"><dd class="mdescRight">Set the "literal" attribute. <a href="#a575a8519a298b25db8b728f4c273972c"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1Theorem.html#a8442e9bc88086d84648ccea5b373cdb0">getLitFlag</a> () const
<dl class="el"><dd class="mdescRight">Check the "literal" attribute. <a href="#a8442e9bc88086d84648ccea5b373cdb0"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1Theorem.html#aed1590a02166f6099e5538dbf681a60c">isAbsLiteral</a> () const
<dl class="el"><dd class="mdescRight">Check if the theorem is a literal. <a href="#aed1590a02166f6099e5538dbf681a60c"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c">refutes</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e) const
<dl class="el"><dd class="mdescRight">Check if the flag attribute is set. <a href="#a657f0037f907743988443bffdf2e505c"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d">proves</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e) const
<dl class="el"><dd class="mdescRight">Check if the flag attribute is set. <a href="#afd8511ead1dfc424a75089f4b4afb95d"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1Theorem.html#a1d50e47a6c0a1dc6ac9328c5b8e63d1c">matches</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e) const
<dl class="el"><dd class="mdescRight">Check if the flag attribute is set. <a href="#a1d50e47a6c0a1dc6ac9328c5b8e63d1c"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1Theorem.html#a293ebbc3162763fbbeaa9fbd8ea1c657">setCachedValue</a> (int value) const
<dl class="el"><dd class="mdescRight">Check if the flag attribute is set. <a href="#a293ebbc3162763fbbeaa9fbd8ea1c657"></a><br/></dl><li>int <a class="el" href="classCVC3_1_1Theorem.html#a0062fd610006e5bc0b4093ae72943342">getCachedValue</a> () const
<dl class="el"><dd class="mdescRight">Check if the flag attribute is set. <a href="#a0062fd610006e5bc0b4093ae72943342"></a><br/></dl></ul>
<h2><a name="pub-static-methods"></a>
Static Public Member Functions</h2>
<ul>
<li>static bool <a class="el" href="classCVC3_1_1Theorem.html#aaf9a1a9a97d765b069eac3d3460545be">TheoremEq</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t1, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t2)
</ul>
<h2><a name="pri-methods"></a>
Private Member Functions</h2>
<ul>
<li><a class="el" href="classCVC3_1_1Theorem.html#a2fefec275dfdf6d8932c6f74b03bec4d">Theorem</a> (<a class="el" href="classCVC3_1_1TheoremValue.html">TheoremValue</a> *thm)
<dl class="el"><dd class="mdescRight">Constructor only used by <a class="el" href="classCVC3_1_1TheoremValue.html">TheoremValue</a> for assumptions. <a href="#a2fefec275dfdf6d8932c6f74b03bec4d"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html#ae7e657235650f951a2e61affb3a55ef2">Theorem</a> (<a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> *tm, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &thm, const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> &assump, const <a class="el" href="classCVC3_1_1Proof.html">Proof</a> &pf, bool isAssump=false, int scope=-1)
<dl class="el"><dd class="mdescRight">Constructor for a new theorem. <a href="#ae7e657235650f951a2e61affb3a55ef2"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html#a1e1b1005316fefef5d78a7c4d3ae6060">Theorem</a> (<a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> *tm, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &lhs, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &rhs, const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> &assump, const <a class="el" href="classCVC3_1_1Proof.html">Proof</a> &pf, bool isAssump=false, int scope=-1)
<dl class="el"><dd class="mdescRight">Constructor for rewrite theorems. <a href="#a1e1b1005316fefef5d78a7c4d3ae6060"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html#ab27afa1904c73f44a38dae8945749a6a">Theorem</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Constructor for a reflexivity theorem: |-t=t or |-phi<=>phi. <a href="#ab27afa1904c73f44a38dae8945749a6a"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1Theorem.html#a472f420688e07c506969a4ed6b9a110e">recursivePrint</a> (int &i) const
<li>void <a class="el" href="classCVC3_1_1Theorem.html#ab3e8c740e4da0bd7ae74754ef25af049">getAssumptionsRec</a> (std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &assumptions) const
<li>void <a class="el" href="classCVC3_1_1Theorem.html#a0c8eec45e649b4608ba1c88ca5f2e617">getAssumptionsAndCongRec</a> (std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &assumptions, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &congruences) const
<li>void <a class="el" href="classCVC3_1_1Theorem.html#adf7fd8a76fe1052914bc88ed3a303660">GetSatAssumptionsRec</a> (std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &assumptions) const
<li><a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> * <a class="el" href="classCVC3_1_1Theorem.html#a67e2a295b1598057cfbb51120a0c1ad6">exprValue</a> () const
<li><a class="el" href="classCVC3_1_1TheoremValue.html">TheoremValue</a> * <a class="el" href="classCVC3_1_1Theorem.html#a12de358e2b6cb67415f508ceca6913d1">thm</a> () const
</ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li>union {
<ul>
<li>   intptr_t    <a class="el" href="classCVC3_1_1Theorem.html#a696e2281069af317ec3fb6510845ca6c">d_thm</a>
<li>   <a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a> *    <a class="el" href="classCVC3_1_1Theorem.html#a798f8085ec077b69aae198a155077774">d_expr</a>
</ul>
<li>};
</ul>
<h2><a name="friends"></a>
Friends</h2>
<ul>
<li>class <a class="el" href="classCVC3_1_1Theorem.html#adb16a6e6bad96912c4150299576eaf9a">TheoremProducer</a>
<li>class <a class="el" href="classCVC3_1_1Theorem.html#acc3b40272a636c6365e02a387cfc4c82">Theorem3</a>
<li>class <a class="el" href="classCVC3_1_1Theorem.html#a2fc7fcb35dcb6d97f101ffb632ac1dcd">RegTheoremValue</a>
<li>class <a class="el" href="classCVC3_1_1Theorem.html#add1e5fec863ffafbd22cac7aa0d1b689">RWTheoremValue</a>
<li>int <a class="el" href="classCVC3_1_1Theorem.html#a4b6ae0abb7c60306b856e52d64c774c0">compare</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t1, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t2)
<dl class="el"><dd class="mdescRight">Compare Theorems by their expressions. Return -1, 0, or 1. <a href="#a4b6ae0abb7c60306b856e52d64c774c0"></a><br/></dl><li>int <a class="el" href="classCVC3_1_1Theorem.html#ab15840d10f28308594233c883b5662bb">compare</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t1, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e2)
<dl class="el"><dd class="mdescRight">Compare a <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> with an <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> (as if <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> is a <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>) <a href="#ab15840d10f28308594233c883b5662bb"></a><br/></dl><li>int <a class="el" href="classCVC3_1_1Theorem.html#ad1783549762b1401c0ec14c39099196d">compareByPtr</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t1, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t2)
<dl class="el"><dd class="mdescRight">Compare Theorems by <a class="el" href="classCVC3_1_1TheoremValue.html">TheoremValue</a> pointers. Return -1, 0, or 1. <a href="#ad1783549762b1401c0ec14c39099196d"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1Theorem.html#a6f08e5df7b32fccb7bba2e689518569e">operator==</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t1, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t2)
<dl class="el"><dd class="mdescRight">Equality is w.r.t. <a class="el" href="classCVC3_1_1Theorem.html#a4b6ae0abb7c60306b856e52d64c774c0" title="Compare Theorems by their expressions. Return -1, 0, or 1.">compare()</a> <a href="#a6f08e5df7b32fccb7bba2e689518569e"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1Theorem.html#acf65eea626a36c24c83abcee026ec205">operator!=</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t1, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t2)
<dl class="el"><dd class="mdescRight">Disequality is w.r.t. <a class="el" href="classCVC3_1_1Theorem.html#a4b6ae0abb7c60306b856e52d64c774c0" title="Compare Theorems by their expressions. Return -1, 0, or 1.">compare()</a> <a href="#acf65eea626a36c24c83abcee026ec205"></a><br/></dl><li>std::ostream & <a class="el" href="classCVC3_1_1Theorem.html#afde7ac3dde23e989a6df667b6836ecfa">operator<<</a> (std::ostream &os, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t)
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00076">76</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a2fefec275dfdf6d8932c6f74b03bec4d"></a><!-- doxytag: member="CVC3::Theorem::Theorem" ref="a2fefec275dfdf6d8932c6f74b03bec4d" args="(TheoremValue *thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Theorem::Theorem </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoremValue.html">TheoremValue</a> * </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Constructor only used by <a class="el" href="classCVC3_1_1TheoremValue.html">TheoremValue</a> for assumptions. </p>
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00109">109</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
</div>
</div>
<a class="anchor" id="ae7e657235650f951a2e61affb3a55ef2"></a><!-- doxytag: member="CVC3::Theorem::Theorem" ref="ae7e657235650f951a2e61affb3a55ef2" args="(TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump=false, int scope=-1)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Theorem::Theorem </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> * </td>
<td class="paramname"><em>tm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>thm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & </td>
<td class="paramname"><em>assump</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Proof.html">Proof</a> & </td>
<td class="paramname"><em>pf</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>isAssump</em> = <code>false</code>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>scope</em> = <code>-1</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Constructor for a new theorem. </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00131">131</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00197">CVC3::Expr::d_expr</a>, <a class="el" href="theorem__value_8h_source.html#l00074">CVC3::TheoremValue::d_refcount</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem__manager_8h_source.html#l00078">CVC3::TheoremManager::getMM()</a>, <a class="el" href="theorem__manager_8h_source.html#l00079">CVC3::TheoremManager::getRWMM()</a>, <a class="el" href="expr__value_8h_source.html#l00142">CVC3::ExprValue::incRefcount()</a>, <a class="el" href="expr_8h_source.html#l00419">CVC3::Expr::isEq()</a>, <a class="el" href="expr_8h_source.html#l00424">CVC3::Expr::isIff()</a>, and <a class="el" href="proof_8h_source.html#l00047">CVC3::Proof::isNull()</a>.</p>
</div>
</div>
<a class="anchor" id="a1e1b1005316fefef5d78a7c4d3ae6060"></a><!-- doxytag: member="CVC3::Theorem::Theorem" ref="a1e1b1005316fefef5d78a7c4d3ae6060" args="(TheoremManager *tm, const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf, bool isAssump=false, int scope=-1)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Theorem::Theorem </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> * </td>
<td class="paramname"><em>tm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>lhs</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>rhs</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & </td>
<td class="paramname"><em>assump</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Proof.html">Proof</a> & </td>
<td class="paramname"><em>pf</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>isAssump</em> = <code>false</code>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>scope</em> = <code>-1</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Constructor for rewrite theorems. </p>
<p>These use a special efficient subclass of <a class="el" href="classCVC3_1_1TheoremValue.html">TheoremValue</a> for theorems which represent rewrites: A |- t = t' or A |- phi<=>phi' </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00152">152</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00197">CVC3::Expr::d_expr</a>, <a class="el" href="theorem__value_8h_source.html#l00074">CVC3::TheoremValue::d_refcount</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem__manager_8h_source.html#l00079">CVC3::TheoremManager::getRWMM()</a>, <a class="el" href="expr__value_8h_source.html#l00142">CVC3::ExprValue::incRefcount()</a>, and <a class="el" href="proof_8h_source.html#l00047">CVC3::Proof::isNull()</a>.</p>
</div>
</div>
<a class="anchor" id="ab27afa1904c73f44a38dae8945749a6a"></a><!-- doxytag: member="CVC3::Theorem::Theorem" ref="ab27afa1904c73f44a38dae8945749a6a" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Theorem::Theorem </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Constructor for a reflexivity theorem: |-t=t or |-phi<=>phi. </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00182">182</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="theorem_8h_source.html#l00092">d_expr</a>, and <a class="el" href="expr__value_8h_source.html#l00142">CVC3::ExprValue::incRefcount()</a>.</p>
</div>
</div>
<a class="anchor" id="a4b7574a16eed728fac6e37d2404fdbf8"></a><!-- doxytag: member="CVC3::Theorem::Theorem" ref="a4b7574a16eed728fac6e37d2404fdbf8" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Theorem::Theorem </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00151">151</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
</div>
</div>
<a class="anchor" id="a43974f559b8faa8db89d81993e911881"></a><!-- doxytag: member="CVC3::Theorem::Theorem" ref="a43974f559b8faa8db89d81993e911881" args="(const Theorem &th)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Theorem::Theorem </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>th</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00170">170</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00074">CVC3::TheoremValue::d_refcount</a>, <a class="el" href="theorem_8h_source.html#l00091">d_thm</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8h_source.html#l00132">exprValue()</a>, <a class="el" href="expr__value_8h_source.html#l00142">CVC3::ExprValue::incRefcount()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
</div>
</div>
<a class="anchor" id="ad72ac2b7be75f1b2848e9d6199c01c83"></a><!-- doxytag: member="CVC3::Theorem::~Theorem" ref="ad72ac2b7be75f1b2848e9d6199c01c83" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Theorem::~Theorem </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00188">188</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00074">CVC3::TheoremValue::d_refcount</a>, <a class="el" href="theorem_8h_source.html#l00091">d_thm</a>, <a class="el" href="expr__value_8h_source.html#l00145">CVC3::ExprValue::decRefcount()</a>, <a class="el" href="classCVC3_1_1MemoryManager.html#ad29fac88d3a07566d9a8f9dc8d8e059c">CVC3::MemoryManager::deleteData()</a>, <a class="el" href="theorem_8h_source.html#l00132">exprValue()</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, <a class="el" href="classCVC3_1_1TheoremValue.html#af8bf999e469afe124c04bfbbb6aba1e2">CVC3::TheoremValue::getMM()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="a472f420688e07c506969a4ed6b9a110e"></a><!-- doxytag: member="CVC3::Theorem::recursivePrint" ref="a472f420688e07c506969a4ed6b9a110e" args="(int &i) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::recursivePrint </td>
<td>(</td>
<td class="paramtype">int & </td>
<td class="paramname"><em>i</em></td><td>)</td>
<td> const<code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00516">516</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00151">CVC3::Assumptions::begin()</a>, <a class="el" href="assumptions_8h_source.html#l00152">CVC3::Assumptions::end()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="theorem_8cpp_source.html#l00385">getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00441">getCachedValue()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00486">getScope()</a>, <a class="el" href="theorem_8cpp_source.html#l00395">isAssump()</a>, <a class="el" href="theorem_8cpp_source.html#l00452">isSubst()</a>, and <a class="el" href="theorem_8cpp_source.html#l00435">setCachedValue()</a>.</p>
</div>
</div>
<a class="anchor" id="ab3e8c740e4da0bd7ae74754ef25af049"></a><!-- doxytag: member="CVC3::Theorem::getAssumptionsRec" ref="ab3e8c740e4da0bd7ae74754ef25af049" args="(std::set< Expr > &assumptions) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::getAssumptionsRec </td>
<td>(</td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>assumptions</em></td><td>)</td>
<td> const<code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00259">259</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00151">CVC3::Assumptions::begin()</a>, <a class="el" href="assumptions_8h_source.html#l00152">CVC3::Assumptions::end()</a>, <a class="el" href="theorem_8cpp_source.html#l00385">getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00395">isAssump()</a>, <a class="el" href="theorem_8cpp_source.html#l00416">isFlagged()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, and <a class="el" href="theorem_8cpp_source.html#l00429">setFlag()</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00274">getLeafAssumptions()</a>.</p>
</div>
</div>
<a class="anchor" id="a0c8eec45e649b4608ba1c88ca5f2e617"></a><!-- doxytag: member="CVC3::Theorem::getAssumptionsAndCongRec" ref="a0c8eec45e649b4608ba1c88ca5f2e617" args="(std::set< Expr > &assumptions, std::vector< Expr > &congruences) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::getAssumptionsAndCongRec </td>
<td>(</td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>assumptions</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>congruences</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td> const<code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00320">320</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00151">CVC3::Assumptions::begin()</a>, <a class="el" href="assumptions_8h_source.html#l00152">CVC3::Assumptions::end()</a>, <a class="el" href="theorem_8cpp_source.html#l00320">getAssumptionsAndCongRec()</a>, <a class="el" href="theorem_8cpp_source.html#l00385">getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">getLHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">getRHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00395">isAssump()</a>, <a class="el" href="expr_8cpp_source.html#l00550">CVC3::Expr::isAtomic()</a>, <a class="el" href="expr_8cpp_source.html#l00571">CVC3::Expr::isAtomicFormula()</a>, <a class="el" href="theorem_8cpp_source.html#l00416">isFlagged()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">isRewrite()</a>, <a class="el" href="theorem_8cpp_source.html#l00452">isSubst()</a>, <a class="el" href="expr_8h_source.html#l01021">CVC3::Expr::isTerm()</a>, <a class="el" href="kinds_8h_source.html#l00068">OR</a>, <a class="el" href="theorem_8cpp_source.html#l00429">setFlag()</a>, <a class="el" href="assumptions_8h_source.html#l00094">CVC3::Assumptions::size()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00370">getAssumptionsAndCong()</a>, and <a class="el" href="theorem_8cpp_source.html#l00320">getAssumptionsAndCongRec()</a>.</p>
</div>
</div>
<a class="anchor" id="adf7fd8a76fe1052914bc88ed3a303660"></a><!-- doxytag: member="CVC3::Theorem::GetSatAssumptionsRec" ref="adf7fd8a76fe1052914bc88ed3a303660" args="(std::vector< Theorem > &assumptions) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::GetSatAssumptionsRec </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>assumptions</em></td><td>)</td>
<td> const<code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00288">288</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00151">CVC3::Assumptions::begin()</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="assumptions_8h_source.html#l00152">CVC3::Assumptions::end()</a>, <a class="el" href="theorem_8cpp_source.html#l00385">getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">getExpr()</a>, <a class="el" href="expr_8h_source.html#l00406">CVC3::Expr::isAbsLiteral()</a>, <a class="el" href="theorem_8cpp_source.html#l00395">isAssump()</a>, <a class="el" href="theorem_8cpp_source.html#l00416">isFlagged()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, <a class="el" href="expr_8h_source.html#l01378">CVC3::Expr::isRegisteredAtom()</a>, and <a class="el" href="theorem_8cpp_source.html#l00429">setFlag()</a>.</p>
</div>
</div>
<a class="anchor" id="a67e2a295b1598057cfbb51120a0c1ad6"></a><!-- doxytag: member="CVC3::Theorem::exprValue" ref="a67e2a295b1598057cfbb51120a0c1ad6" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a>* CVC3::Theorem::exprValue </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00132">132</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00422">clearAllFlags()</a>, <a class="el" href="theorem_8cpp_source.html#l00441">getCachedValue()</a>, <a class="el" href="theorem_8cpp_source.html#l00464">getExpandFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00476">getLitFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">getProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00416">isFlagged()</a>, <a class="el" href="theorem_8cpp_source.html#l00091">operator=()</a>, <a class="el" href="theorem_8cpp_source.html#l00435">setCachedValue()</a>, <a class="el" href="theorem_8cpp_source.html#l00458">setExpandFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00429">setFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00470">setLitFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00170">Theorem()</a>, <a class="el" href="theorem_8cpp_source.html#l00219">withAssumptions()</a>, <a class="el" href="theorem_8cpp_source.html#l00214">withProof()</a>, and <a class="el" href="theorem_8cpp_source.html#l00188">~Theorem()</a>.</p>
</div>
</div>
<a class="anchor" id="a12de358e2b6cb67415f508ceca6913d1"></a><!-- doxytag: member="CVC3::Theorem::thm" ref="a12de358e2b6cb67415f508ceca6913d1" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoremValue.html">TheoremValue</a>* CVC3::Theorem::thm </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00133">133</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00422">clearAllFlags()</a>, <a class="el" href="theorem_8cpp_source.html#l00320">getAssumptionsAndCongRec()</a>, <a class="el" href="theorem_8cpp_source.html#l00385">getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00441">getCachedValue()</a>, <a class="el" href="theorem_8cpp_source.html#l00464">getExpandFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">getLHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00476">getLitFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">getProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00491">getQuantLevel()</a>, <a class="el" href="theorem_8cpp_source.html#l00497">getQuantLevelDebug()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">getRHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00486">getScope()</a>, <a class="el" href="theorem_8cpp_source.html#l00395">isAssump()</a>, <a class="el" href="theorem_8cpp_source.html#l00416">isFlagged()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">isRewrite()</a>, <a class="el" href="theorem_8cpp_source.html#l00452">isSubst()</a>, <a class="el" href="theorem_8cpp_source.html#l00580">print()</a>, <a class="el" href="theorem_8cpp_source.html#l00435">setCachedValue()</a>, <a class="el" href="theorem_8cpp_source.html#l00458">setExpandFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00429">setFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00470">setLitFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00504">setQuantLevel()</a>, <a class="el" href="theorem_8cpp_source.html#l00447">setSubst()</a>, <a class="el" href="theorem_8cpp_source.html#l00170">Theorem()</a>, <a class="el" href="theorem_8cpp_source.html#l00219">withAssumptions()</a>, <a class="el" href="theorem_8cpp_source.html#l00214">withProof()</a>, and <a class="el" href="theorem_8cpp_source.html#l00188">~Theorem()</a>.</p>
</div>
</div>
<a class="anchor" id="ad9da69b34ab2bab4192e5977e5c10498"></a><!-- doxytag: member="CVC3::Theorem::printDebug" ref="ad9da69b34ab2bab4192e5977e5c10498" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::printDebug </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00140">140</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>, <a class="el" href="theorem_8h_source.html#l00341">CVC3::Theorem3::printDebug()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="adacab84dc4dc38aeb12ddabcb3c4a51d"></a><!-- doxytag: member="CVC3::Theorem::operator=" ref="adacab84dc4dc38aeb12ddabcb3c4a51d" args="(const Theorem &th)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & CVC3::Theorem::operator= </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>th</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00091">91</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00074">CVC3::TheoremValue::d_refcount</a>, <a class="el" href="theorem_8h_source.html#l00091">d_thm</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="classCVC3_1_1MemoryManager.html#ad29fac88d3a07566d9a8f9dc8d8e059c">CVC3::MemoryManager::deleteData()</a>, <a class="el" href="theorem_8h_source.html#l00132">exprValue()</a>, <a class="el" href="classCVC3_1_1TheoremValue.html#af8bf999e469afe124c04bfbbb6aba1e2">CVC3::TheoremValue::getMM()</a>, and <a class="el" href="expr__value_8h_source.html#l00142">CVC3::ExprValue::incRefcount()</a>.</p>
</div>
</div>
<a class="anchor" id="ad4573ca6be017cab3c83d28c2dbcebd8"></a><!-- doxytag: member="CVC3::Theorem::withProof" ref="ad4573ca6be017cab3c83d28c2dbcebd8" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem::withProof </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00214">214</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="expr__value_8h_source.html#l00132">CVC3::ExprValue::d_em</a>, <a class="el" href="theorem__value_8h_source.html#l00065">CVC3::TheoremValue::d_tm</a>, <a class="el" href="theorem_8h_source.html#l00132">exprValue()</a>, <a class="el" href="expr__manager_8h_source.html#l00331">CVC3::ExprManager::getTM()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, <a class="el" href="theorem_8h_source.html#l00133">thm()</a>, and <a class="el" href="theorem__manager_8h_source.html#l00091">CVC3::TheoremManager::withProof()</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00402">getProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00580">print()</a>, and <a class="el" href="theorem_8h_source.html#l00377">CVC3::Theorem3::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a90349125fe644e8a075e1a47a49872c7"></a><!-- doxytag: member="CVC3::Theorem::withAssumptions" ref="a90349125fe644e8a075e1a47a49872c7" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem::withAssumptions </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00219">219</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="expr__value_8h_source.html#l00132">CVC3::ExprValue::d_em</a>, <a class="el" href="theorem__value_8h_source.html#l00065">CVC3::TheoremValue::d_tm</a>, <a class="el" href="theorem_8h_source.html#l00132">exprValue()</a>, <a class="el" href="expr__manager_8h_source.html#l00331">CVC3::ExprManager::getTM()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, <a class="el" href="theorem_8h_source.html#l00133">thm()</a>, and <a class="el" href="theorem__manager_8h_source.html#l00094">CVC3::TheoremManager::withAssumptions()</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00580">print()</a>, and <a class="el" href="theorem_8h_source.html#l00378">CVC3::Theorem3::withAssumptions()</a>.</p>
</div>
</div>
<a class="anchor" id="afc6fdb0507eb3669e28d9be5ed0bd333"></a><!-- doxytag: member="CVC3::Theorem::isNull" ref="afc6fdb0507eb3669e28d9be5ed0bd333" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem::isNull </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00164">164</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l04788">CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00359">CVC3::TheoryBitvector::bitBlastTerm()</a>, <a class="el" href="theory__core_8cpp_source.html#l03862">CVC3::TheoryCore::buildModel()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02913">CVC3::TheoryArithOld::checkIntegerEquality()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00156">CVC3::TheoryUF::checkSat()</a>, <a class="el" href="theory__array_8cpp_source.html#l00154">CVC3::TheoryArray::checkSat()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02606">CVC3::TheoryArithOld::checkSat()</a>, <a class="el" href="theorem_8cpp_source.html#l00422">clearAllFlags()</a>, <a class="el" href="theorem_8cpp_source.html#l00045">CVC3::compare()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l05535">CVC3::TheoryArithOld::computeTermBounds()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00139">SAT::CNF_Manager::concreteThm()</a>, <a class="el" href="minisat__derivation_8cpp_source.html#l00260">MiniSat::Derivation::createProof()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00432">CVC3::TheoryArith3::doSolve()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08653">CVC3::TheoryQuant::findInstAssumptions()</a>, <a class="el" href="assumptions_8cpp_source.html#l00034">CVC3::Assumptions::findTheorem()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00258">generateSatProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00370">getAssumptionsAndCong()</a>, <a class="el" href="vcl_8cpp_source.html#l00354">CVC3::VCL::getAssumptionsRec()</a>, <a class="el" href="theorem_8cpp_source.html#l00385">getAssumptionsRef()</a>, <a class="el" href="vcl_8cpp_source.html#l02085">CVC3::VCL::getAssumptionsUsed()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00297">CVC3::SearchImplBase::getAssumptionsUsed()</a>, <a class="el" href="theorem_8cpp_source.html#l00441">getCachedValue()</a>, <a class="el" href="search__sat_8cpp_source.html#l01169">CVC3::SearchSat::getCounterExample()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00247">CVC3::SearchImplBase::getCounterExample()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l04888">CVC3::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems()</a>, <a class="el" href="theorem_8cpp_source.html#l00464">getExpandFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">getExpr()</a>, <a class="el" href="search__sat_8cpp_source.html#l00284">CVC3::SearchSat::getImplication()</a>, <a class="el" href="vcl_8cpp_source.html#l01904">CVC3::VCL::getImpliedLiteral()</a>, <a class="el" href="theorem_8cpp_source.html#l00274">getLeafAssumptions()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">getLHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00476">getLitFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">getProof()</a>, <a class="el" href="search__sat_8cpp_source.html#l01178">CVC3::SearchSat::getProof()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00282">CVC3::SearchImplBase::getProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00491">getQuantLevel()</a>, <a class="el" href="theorem_8cpp_source.html#l00497">getQuantLevelDebug()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">getRHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00486">getScope()</a>, <a class="el" href="expr_8h_source.html#l01232">CVC3::Expr::hasFind()</a>, <a class="el" href="expr_8h_source.html#l01554">CVC3::Expr::hasRep()</a>, <a class="el" href="expr_8h_source.html#l01548">CVC3::Expr::hasSig()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00775">CVC3::CommonTheoremProducer::implIntro()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00085">CVC3::CommonTheoremProducer::implIntro3()</a>, <a class="el" href="theorem_8cpp_source.html#l00395">isAssump()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l05799">CVC3::TheoryArithOld::isConstrained()</a>, <a class="el" href="theorem_8cpp_source.html#l00416">isFlagged()</a>, <a class="el" href="theory__arith__old_8h_source.html#l00258">CVC3::TheoryArithOld::isInteger()</a>, <a class="el" href="theory__arith__new_8h_source.html#l00189">CVC3::TheoryArithNew::isInteger()</a>, <a class="el" href="theory__arith3_8h_source.html#l00233">CVC3::TheoryArith3::isInteger()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00081">CVC3::TheoryArithOld::isIntegerDerive()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00076">CVC3::TheoryArithNew::isIntegerDerive()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00076">CVC3::TheoryArith3::isIntegerDerive()</a>, <a class="el" href="sat__proof_8h_source.html#l00058">SAT::SatProofNode::isLeaf()</a>, <a class="el" href="theorem_8h_source.html#l00351">CVC3::Theorem3::isNull()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">isRewrite()</a>, <a class="el" href="theorem_8cpp_source.html#l00452">isSubst()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04271">CVC3::TheoryQuant::matchListNew()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04075">CVC3::TheoryQuant::matchListOld()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00123">CVC3::TheoryDatatypeLazy::mergeLabels()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00144">CVC3::TheoryDatatype::mergeLabels()</a>, <a class="el" href="theory__quant_8cpp_source.html#l03950">CVC3::TheoryQuant::multMatchChild()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00141">CVC3::SearchImplBase::newUserAssumption()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l01822">CVC3::TheoryArithOld::normalizeProjectIneqs()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l01449">CVC3::TheoryArith3::normalizeProjectIneqs()</a>, <a class="el" href="variable_8cpp_source.html#l00337">CVC3::operator<<()</a>, <a class="el" href="theorem_8cpp_source.html#l00580">print()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00330">printSatProof()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00317">CVC3::SearchImplBase::processResult()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00739">CVC3::TheoryArithOld::processSimpleIntEq()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00507">CVC3::TheoryArithNew::processSimpleIntEq()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00759">CVC3::TheoryArith3::processSimpleIntEq()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l01710">CVC3::TheoryArithOld::projectInequalities()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l01346">CVC3::TheoryArith3::projectInequalities()</a>, <a class="el" href="circuit_8cpp_source.html#l00047">CVC3::Circuit::propagate()</a>, <a class="el" href="theory__array_8cpp_source.html#l00345">CVC3::TheoryArray::pullIndex()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02953">CVC3::TheoryArithOld::rafineInequalityToInteger()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01541">CVC3::TheoryArithNew::rafineIntegerConstraints()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00804">CVC3::SearchImplBase::replaceITE()</a>, <a class="el" href="theory__array_8cpp_source.html#l00368">CVC3::TheoryArray::rewrite()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02387">CVC3::TheoryArith3::rewrite()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l01638">CVC3::TheoryBitvector::rewriteBoolean()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00887">CVC3::TheoryBitvector::rewriteBV()</a>, <a class="el" href="theory_8cpp_source.html#l00512">CVC3::Theory::rewriteCC()</a>, <a class="el" href="sat__proof_8h_source.html#l00045">SAT::SatProofNode::SatProofNode()</a>, <a class="el" href="theorem_8cpp_source.html#l00435">setCachedValue()</a>, <a class="el" href="theorem_8cpp_source.html#l00458">setExpandFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00429">setFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00470">setLitFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00504">setQuantLevel()</a>, <a class="el" href="theorem_8cpp_source.html#l00447">setSubst()</a>, <a class="el" href="theory__records_8cpp_source.html#l00508">CVC3::TheoryRecords::setup()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00812">CVC3::TheoryBitvector::simplifyOp()</a>, <a class="el" href="theorem_8h_source.html#l00281">TheoremEq()</a>, <a class="el" href="search__fast_8cpp_source.html#l01096">TheoremEq()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00245">CVC3::CommonTheoremProducer::transitivityRule()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00147">SAT::CNF_Manager::translateExprRec()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00257">CVC3::TheoryUF::update()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00267">CVC3::TheoryDatatypeLazy::update()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00359">CVC3::TheoryDatatype::update()</a>, <a class="el" href="theory__array_8cpp_source.html#l00550">CVC3::TheoryArray::update()</a>, and <a class="el" href="theory_8cpp_source.html#l00473">CVC3::Theory::updateCC()</a>.</p>
</div>
</div>
<a class="anchor" id="a362c1d70e03803d804bbe300e5f6dc87"></a><!-- doxytag: member="CVC3::Theorem::isRewrite" ref="a362c1d70e03803d804bbe300e5f6dc87" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem::isRewrite </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00224">224</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, <a class="el" href="theorem__value_8h_source.html#l00295">CVC3::TheoremValue::isRewrite()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00723">CVC3::SearchImplBase::addToCNFCache()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>, <a class="el" href="theory__core_8cpp_source.html#l04093">CVC3::TheoryCore::assertEqualities()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00201">CVC3::TheoryDatatype::assertFact()</a>, <a class="el" href="theory__core_8cpp_source.html#l00321">CVC3::TheoryCore::assertFactCore()</a>, <a class="el" href="theory__core_8cpp_source.html#l03734">CVC3::TheoryCore::assignValue()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03621">CVC3::TheoryArithOld::checkAssertEqInvariant()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02643">CVC3::TheoryArith3::checkAssertEqInvariant()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02913">CVC3::TheoryArithOld::checkIntegerEquality()</a>, <a class="el" href="theorem_8cpp_source.html#l00045">CVC3::compare()</a>, <a class="el" href="datatype__theorem__producer_8cpp_source.html#l00118">CVC3::DatatypeTheoremProducer::decompose()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00447">CVC3::TheoryArithOld::doSolve()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00331">CVC3::TheoryArithNew::doSolve()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00432">CVC3::TheoryArith3::doSolve()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, <a class="el" href="theory__core_8cpp_source.html#l04213">CVC3::TheoryCore::enqueueFact()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02708">CVC3::ArithTheoremProducerOld::eqElimIntRule()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02506">CVC3::ArithTheoremProducer3::eqElimIntRule()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02531">CVC3::ArithTheoremProducer::eqElimIntRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01911">CVC3::BitvectorTheoremProducer::eqToBits()</a>, <a class="el" href="records__theorem__producer_8cpp_source.html#l00205">CVC3::RecordsTheoremProducer::expandEq()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00750">CVC3::SearchImplBase::findInCNFCache()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00762">CVC3::BitvectorTheoremProducer::generalIneqn()</a>, <a class="el" href="theorem_8cpp_source.html#l00320">getAssumptionsAndCongRec()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00641">CVC3::CommonTheoremProducer::iffContrapositive()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00626">CVC3::CommonTheoremProducer::iffFalseElim()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00667">CVC3::CommonTheoremProducer::iffMP()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01206">CVC3::SearchEngineTheoremProducer::iffToClauses()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00612">CVC3::CommonTheoremProducer::iffTrueElim()</a>, <a class="el" href="theorem_8h_source.html#l00354">CVC3::Theorem3::isRewrite()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03070">CVC3::TheoryArithOld::normalize()</a>, <a class="el" href="theory__arith__new_8h_source.html#l00550">CVC3::TheoryArithNew::BoundInfo::operator<()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00869">CVC3::TheoryArithOld::processIntEq()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00642">CVC3::TheoryArithNew::processIntEq()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00889">CVC3::TheoryArith3::processIntEq()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00739">CVC3::TheoryArithOld::processSimpleIntEq()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00507">CVC3::TheoryArithNew::processSimpleIntEq()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00759">CVC3::TheoryArith3::processSimpleIntEq()</a>, <a class="el" href="theory__core_8cpp_source.html#l00291">CVC3::TheoryCore::processUpdates()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00225">CVC3::ExprTransform::pushNegationRec()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02953">CVC3::TheoryArithOld::rafineInequalityToInteger()</a>, <a class="el" href="theory_8cpp_source.html#l00935">CVC3::Theory::renameExpr()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00804">CVC3::SearchImplBase::replaceITE()</a>, <a class="el" href="theory__core_8cpp_source.html#l00257">CVC3::TheoryCore::rewriteCore()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00161">CVC3::CoreTheoremProducer::rewriteIteElse()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00136">CVC3::CoreTheoremProducer::rewriteIteThen()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00205">CVC3::ArrayTheoremProducer::rewriteRedundantWrite1()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l02366">CVC3::TheoryBitvector::simplifyPendingEq()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00425">CVC3::TheoryDatatype::solve()</a>, <a class="el" href="theory__core_8cpp_source.html#l01248">CVC3::TheoryCore::solve()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l02818">CVC3::TheoryBitvector::solve()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03547">CVC3::TheoryArithOld::solve()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01805">CVC3::TheoryArithNew::solve()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02569">CVC3::TheoryArith3::solve()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l01017">CVC3::TheoryArithOld::substAndCanonize()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00787">CVC3::TheoryArithNew::substAndCanonize()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l01038">CVC3::TheoryArith3::substAndCanonize()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00302">CVC3::CommonTheoremProducer::substitutivityRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00187">CVC3::CommonTheoremProducer::symmetryRule()</a>, and <a class="el" href="common__theorem__producer_8cpp_source.html#l00245">CVC3::CommonTheoremProducer::transitivityRule()</a>.</p>
</div>
</div>
<a class="anchor" id="a05282db6832afb4f198d8c6b2b67aeb1"></a><!-- doxytag: member="CVC3::Theorem::isAssump" ref="a05282db6832afb4f198d8c6b2b67aeb1" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem::isAssump </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00395">395</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem__value_8h_source.html#l00315">CVC3::TheoremValue::isAssump()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l04788">CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00429">CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08653">CVC3::TheoryQuant::findInstAssumptions()</a>, <a class="el" href="theorem_8cpp_source.html#l00320">getAssumptionsAndCongRec()</a>, <a class="el" href="vcl_8cpp_source.html#l00354">CVC3::VCL::getAssumptionsRec()</a>, <a class="el" href="theorem_8cpp_source.html#l00259">getAssumptionsRec()</a>, <a class="el" href="theorem_8cpp_source.html#l00288">GetSatAssumptionsRec()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00775">CVC3::CommonTheoremProducer::implIntro()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00085">CVC3::CommonTheoremProducer::implIntro3()</a>, <a class="el" href="theorem_8h_source.html#l00355">CVC3::Theorem3::isAssump()</a>, <a class="el" href="search__fast_8cpp_source.html#l01573">CVC3::SearchEngineFast::newIntAssumption()</a>, <a class="el" href="theorem_8cpp_source.html#l00580">print()</a>, and <a class="el" href="theorem_8cpp_source.html#l00516">recursivePrint()</a>.</p>
</div>
</div>
<a class="anchor" id="a16f074e60b9e076187efb478889d2c47"></a><!-- doxytag: member="CVC3::Theorem::isRefl" ref="a16f074e60b9e076187efb478889d2c47" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem::isRefl </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00171">171</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>Referenced by <a class="el" href="theory__array_8cpp_source.html#l00154">CVC3::TheoryArray::checkSat()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00429">CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems()</a>, <a class="el" href="theorem_8cpp_source.html#l00422">clearAllFlags()</a>, <a class="el" href="theory_8cpp_source.html#l00310">CVC3::Theory::find()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08653">CVC3::TheoryQuant::findInstAssumptions()</a>, <a class="el" href="theory_8cpp_source.html#l00327">CVC3::Theory::findReduce()</a>, <a class="el" href="theorem_8cpp_source.html#l00370">getAssumptionsAndCong()</a>, <a class="el" href="theorem_8cpp_source.html#l00320">getAssumptionsAndCongRec()</a>, <a class="el" href="vcl_8cpp_source.html#l00354">CVC3::VCL::getAssumptionsRec()</a>, <a class="el" href="theorem_8cpp_source.html#l00259">getAssumptionsRec()</a>, <a class="el" href="theorem_8cpp_source.html#l00385">getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00441">getCachedValue()</a>, <a class="el" href="theorem_8cpp_source.html#l00464">getExpandFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00274">getLeafAssumptions()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">getLHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00476">getLitFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">getProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00491">getQuantLevel()</a>, <a class="el" href="theorem_8cpp_source.html#l00497">getQuantLevelDebug()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">getRHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00309">GetSatAssumptions()</a>, <a class="el" href="theorem_8cpp_source.html#l00288">GetSatAssumptionsRec()</a>, <a class="el" href="theorem_8cpp_source.html#l00486">getScope()</a>, <a class="el" href="theorem_8cpp_source.html#l00395">isAssump()</a>, <a class="el" href="theorem_8cpp_source.html#l00416">isFlagged()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">isRewrite()</a>, <a class="el" href="theorem_8cpp_source.html#l00452">isSubst()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00334">CVC3::ExprTransform::newPPrec()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00079">CVC3::ExprTransform::preprocess()</a>, <a class="el" href="theorem_8cpp_source.html#l00580">print()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00699">CVC3::TheoryBitvector::pushNegationRec()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00074">SAT::CNF_Manager::replaceITErec()</a>, <a class="el" href="theory__core_8cpp_source.html#l00968">CVC3::TheoryCore::rewrite()</a>, <a class="el" href="theory__array_8cpp_source.html#l00368">CVC3::TheoryArray::rewrite()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00887">CVC3::TheoryBitvector::rewriteBV()</a>, <a class="el" href="theory__core_8cpp_source.html#l00455">CVC3::TheoryCore::rewriteCore()</a>, <a class="el" href="theorem_8cpp_source.html#l00435">setCachedValue()</a>, <a class="el" href="theorem_8cpp_source.html#l00458">setExpandFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00429">setFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00470">setLitFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00504">setQuantLevel()</a>, <a class="el" href="theorem_8cpp_source.html#l00447">setSubst()</a>, <a class="el" href="theory__core_8cpp_source.html#l00184">CVC3::TheoryCore::simplify()</a>, <a class="el" href="theory__core_8cpp_source.html#l01292">CVC3::TheoryCore::simplifyOp()</a>, <a class="el" href="theory_8cpp_source.html#l00053">CVC3::Theory::simplifyOp()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00476">CVC3::ExprTransform::simplifyWithCare()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00296">CVC3::ExprTransform::specialSimplify()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00434">CVC3::ExprTransform::substitute()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00302">CVC3::CommonTheoremProducer::substitutivityRule()</a>, <a class="el" href="theory__array_8cpp_source.html#l00550">CVC3::TheoryArray::update()</a>, <a class="el" href="theorem_8cpp_source.html#l00219">withAssumptions()</a>, and <a class="el" href="theorem_8cpp_source.html#l00214">withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="af2b97ae5d270ddf1013bf4f3867a7e5d"></a><!-- doxytag: member="CVC3::Theorem::getExpr" ref="af2b97ae5d270ddf1013bf4f3867a7e5d" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> CVC3::Theorem::getExpr </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00230">230</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l00929">CVC3::Expr::eqExpr()</a>, <a class="el" href="theorem_8h_source.html#l00132">exprValue()</a>, <a class="el" href="theorem__value_8h_source.html#l00297">CVC3::TheoremValue::getExpr()</a>, <a class="el" href="expr_8h_source.html#l00965">CVC3::Expr::iffExpr()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, <a class="el" href="expr_8h_source.html#l01021">CVC3::Expr::isTerm()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
<p>Referenced by <a class="el" href="cnf__manager_8cpp_source.html#l00623">SAT::CNF_Manager::addAssumption()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00218">CVC3::SearchImplBase::addCNFFact()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l04788">CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge()</a>, <a class="el" href="theory__core_8cpp_source.html#l03468">CVC3::TheoryCore::addFact()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00231">CVC3::SearchImplBase::addFact()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03016">CVC3::ArithTheoremProducerOld::addInequalities()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02814">CVC3::ArithTheoremProducer3::addInequalities()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02905">CVC3::ArithTheoremProducer::addInequalities()</a>, <a class="el" href="search__sat_8cpp_source.html#l00170">CVC3::SearchSat::addLemma()</a>, <a class="el" href="search__fast_8cpp_source.html#l01530">CVC3::SearchEngineFast::addLiteralFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l01445">CVC3::SearchEngineFast::addNonLiteralFact()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l01241">CVC3::TheoryArithOld::addToBuffer()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00829">CVC3::TheoryArithNew::addToBuffer()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l01126">CVC3::TheoryArith3::addToBuffer()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00723">CVC3::SearchImplBase::addToCNFCache()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00510">CVC3::QuantTheoremProducer::adjustVarUniv()</a>, <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00718">CVC3::CommonTheoremProducer::andElim()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00338">CVC3::ArrayTheoremProducer::arrayNotEq()</a>, <a class="el" href="theory__core_8cpp_source.html#l04093">CVC3::TheoryCore::assertEqualities()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00079">CVC3::TheoryUF::assertFact()</a>, <a class="el" href="theory__records_8cpp_source.html#l00129">CVC3::TheoryRecords::assertFact()</a>, <a class="el" href="theory__quant_8cpp_source.html#l03502">CVC3::TheoryQuant::assertFact()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00201">CVC3::TheoryDatatype::assertFact()</a>, <a class="el" href="theory__core_8cpp_source.html#l00960">CVC3::TheoryCore::assertFact()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l01861">CVC3::TheoryBitvector::assertFact()</a>, <a class="el" href="theory__array_8cpp_source.html#l00106">CVC3::TheoryArray::assertFact()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02481">CVC3::TheoryArithOld::assertFact()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l03138">CVC3::TheoryArithNew::assertFact()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02020">CVC3::TheoryArith3::assertFact()</a>, <a class="el" href="theory__core_8cpp_source.html#l00321">CVC3::TheoryCore::assertFactCore()</a>, <a class="el" href="theory__core_8cpp_source.html#l00385">CVC3::TheoryCore::assertFormula()</a>, <a class="el" href="theory__core_8cpp_source.html#l03734">CVC3::TheoryCore::assignValue()</a>, <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00164">CVC3::TheoryBitvector::bitBlastDisEqn()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00225">CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00927">CVC3::BitvectorTheoremProducer::bitExtractToExtract()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00066">CVC3::BitvectorTheoremProducer::bitvectorFalseRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00104">CVC3::BitvectorTheoremProducer::bitvectorTrueRule()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00748">CVC3::QuantTheoremProducer::boundVarElim()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00401">CVC3::TheoryArithOld::canonPred()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00279">CVC3::TheoryArithNew::canonPred()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00390">CVC3::TheoryArith3::canonPred()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00135">CVC3::SearchEngineTheoremProducer::caseSplit()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03621">CVC3::TheoryArithOld::checkAssertEqInvariant()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02643">CVC3::TheoryArith3::checkAssertEqInvariant()</a>, <a class="el" href="theory__core_8cpp_source.html#l01195">CVC3::TheoryCore::checkEquation()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02913">CVC3::TheoryArithOld::checkIntegerEquality()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l02574">CVC3::TheoryBitvector::checkSat()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02606">CVC3::TheoryArithOld::checkSat()</a>, <a class="el" href="theory__core_8cpp_source.html#l01220">CVC3::TheoryCore::checkSolved()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00429">CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems()</a>, <a class="el" href="search__simple_8cpp_source.html#l00165">CVC3::SearchSimple::checkValidInternal()</a>, <a class="el" href="search__simple_8cpp_source.html#l00126">CVC3::SearchSimple::checkValidMain()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, <a class="el" href="search__simple_8cpp_source.html#l00037">CVC3::SearchSimple::checkValidRec()</a>, <a class="el" href="circuit_8cpp_source.html#l00028">CVC3::Circuit::Circuit()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02976">CVC3::ArithTheoremProducerOld::clashingBounds()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02774">CVC3::ArithTheoremProducer3::clashingBounds()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02865">CVC3::ArithTheoremProducer::clashingBounds()</a>, <a class="el" href="clause_8cpp_source.html#l00035">CVC3::ClauseValue::ClauseValue()</a>, <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00311">CVC3::CNF_TheoremProducer::CNFAddUnit()</a>, <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00321">CVC3::CNF_TheoremProducer::CNFConvert()</a>, <a class="el" href="theory__core_8cpp_source.html#l03763">CVC3::TheoryCore::collectBasicVars()</a>, <a class="el" href="theory__core_8cpp_source.html#l03954">CVC3::TheoryCore::collectModelValues()</a>, <a class="el" href="theorem_8cpp_source.html#l00045">CVC3::compare()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l03345">CVC3::TheoryBitvector::computeModel()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l05111">CVC3::TheoryArithOld::DifferenceLogicGraph::computeModel()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l05535">CVC3::TheoryArithOld::computeTermBounds()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00744">CVC3::SearchEngineTheoremProducer::confAndrAF()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00711">CVC3::SearchEngineTheoremProducer::confAndrAT()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00834">CVC3::SearchEngineTheoremProducer::confIffr()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01059">CVC3::SearchEngineTheoremProducer::confIterIfThen()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01012">CVC3::SearchEngineTheoremProducer::confIterThenElse()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00221">CVC3::SearchEngineTheoremProducer::conflictClause()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01109">CVC3::SearchEngineTheoremProducer::conflictRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00561">CVC3::CommonTheoremProducer::contradictionRule()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00375">CVC3::SearchEngineTheoremProducer::cutRule()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01833">CVC3::ArithTheoremProducerOld::darkGrayShadow2ab()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01635">CVC3::ArithTheoremProducer3::darkGrayShadow2ab()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01678">CVC3::ArithTheoremProducer::darkGrayShadow2ab()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01926">CVC3::ArithTheoremProducerOld::darkGrayShadow2ba()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01726">CVC3::ArithTheoremProducer3::darkGrayShadow2ba()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01769">CVC3::ArithTheoremProducer::darkGrayShadow2ba()</a>, <a class="el" href="variable_8cpp_source.html#l00162">CVC3::Variable::deriveThmRec()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02931">CVC3::ArithTheoremProducerOld::diseqToIneq()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02729">CVC3::ArithTheoremProducer3::diseqToIneq()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02754">CVC3::ArithTheoremProducer::diseqToIneq()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00447">CVC3::TheoryArithOld::doSolve()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00331">CVC3::TheoryArithNew::doSolve()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00432">CVC3::TheoryArith3::doSolve()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00454">CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, <a class="el" href="theory__core_8cpp_source.html#l04213">CVC3::TheoryCore::enqueueFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l01031">CVC3::SearchEngineFast::enqueueFact()</a>, <a class="el" href="theory__quant_8cpp_source.html#l00633">CVC3::TheoryQuant::enqueueInst()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02708">CVC3::ArithTheoremProducerOld::eqElimIntRule()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02506">CVC3::ArithTheoremProducer3::eqElimIntRule()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02531">CVC3::ArithTheoremProducer::eqElimIntRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01911">CVC3::BitvectorTheoremProducer::eqToBits()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02014">CVC3::ArithTheoremProducerOld::expandDarkShadow()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01811">CVC3::ArithTheoremProducer3::expandDarkShadow()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01854">CVC3::ArithTheoremProducer::expandDarkShadow()</a>, <a class="el" href="records__theorem__producer_8cpp_source.html#l00205">CVC3::RecordsTheoremProducer::expandEq()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02091">CVC3::ArithTheoremProducerOld::expandGrayShadow()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01889">CVC3::ArithTheoremProducer3::expandGrayShadow()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01931">CVC3::ArithTheoremProducer::expandGrayShadow()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02029">CVC3::ArithTheoremProducerOld::expandGrayShadow0()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01826">CVC3::ArithTheoremProducer3::expandGrayShadow0()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01869">CVC3::ArithTheoremProducer::expandGrayShadow0()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02122">CVC3::ArithTheoremProducerOld::expandGrayShadowConst()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01920">CVC3::ArithTheoremProducer3::expandGrayShadowConst()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01962">CVC3::ArithTheoremProducer::expandGrayShadowConst()</a>, <a class="el" href="records__theorem__producer_8cpp_source.html#l00158">CVC3::RecordsTheoremProducer::expandNeq()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04294">CVC3::BitvectorTheoremProducer::expandTypePred()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02465">CVC3::BitvectorTheoremProducer::extractConcat()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00750">CVC3::SearchImplBase::findInCNFCache()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08653">CVC3::TheoryQuant::findInstAssumptions()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01769">CVC3::ArithTheoremProducerOld::finiteInterval()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01571">CVC3::ArithTheoremProducer3::finiteInterval()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01614">CVC3::ArithTheoremProducer::finiteInterval()</a>, <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l02409">CVC3::TheoryBitvector::generalBitBlast()</a>, <a class="el" href="theorem_8cpp_source.html#l00320">getAssumptionsAndCongRec()</a>, <a class="el" href="vcl_8cpp_source.html#l00354">CVC3::VCL::getAssumptionsRec()</a>, <a class="el" href="theorem_8cpp_source.html#l00259">getAssumptionsRec()</a>, <a class="el" href="theorem_8h_source.html#l00358">CVC3::Theorem3::getExpr()</a>, <a class="el" href="search__sat_8cpp_source.html#l00284">CVC3::SearchSat::getImplication()</a>, <a class="el" href="vcl_8cpp_source.html#l01904">CVC3::VCL::getImpliedLiteral()</a>, <a class="el" href="search__sat_8cpp_source.html#l01010">CVC3::SearchSat::getImpliedLiteral()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l03662">CVC3::TheoryArithNew::getLowerBoundExplanation()</a>, <a class="el" href="theorem_8cpp_source.html#l00288">GetSatAssumptionsRec()</a>, <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00049">CVC3::CNF_TheoremProducer::getSmartClauses()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l03749">CVC3::TheoryArithNew::getUpperBoundExplanation()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l03273">CVC3::TheoryArithNew::getVariableIntroThm()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02187">CVC3::ArithTheoremProducerOld::grayShadowConst()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01985">CVC3::ArithTheoremProducer3::grayShadowConst()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02027">CVC3::ArithTheoremProducer::grayShadowConst()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00641">CVC3::CommonTheoremProducer::iffContrapositive()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00667">CVC3::CommonTheoremProducer::iffMP()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00602">CVC3::CommonTheoremProducer::iffNotFalse()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01206">CVC3::SearchEngineTheoremProducer::iffToClauses()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00591">CVC3::CommonTheoremProducer::iffTrue()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00825">CVC3::CommonTheoremProducer::implContrapositive()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00775">CVC3::CommonTheoremProducer::implIntro()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00692">CVC3::CommonTheoremProducer::implMP()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l04613">CVC3::TheoryArithOld::inequalityToFind()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01330">CVC3::ArithTheoremProducerOld::intEqIrrational()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01260">CVC3::ArithTheoremProducer3::intEqIrrational()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01273">CVC3::ArithTheoremProducer::intEqIrrational()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03332">CVC3::ArithTheoremProducerOld::intEqualityRationalConstant()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02297">CVC3::ArithTheoremProducerOld::intVarEqnConst()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02095">CVC3::ArithTheoremProducer3::intVarEqnConst()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02138">CVC3::ArithTheoremProducer::intVarEqnConst()</a>, <a class="el" href="theorem_8cpp_source.html#l00482">isAbsLiteral()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00081">CVC3::TheoryArithOld::isIntegerDerive()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00076">CVC3::TheoryArithNew::isIntegerDerive()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00076">CVC3::TheoryArith3::isIntegerDerive()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02682">CVC3::ArithTheoremProducerOld::IsIntegerElim()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02480">CVC3::ArithTheoremProducer3::IsIntegerElim()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02505">CVC3::ArithTheoremProducer::IsIntegerElim()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l01499">CVC3::TheoryArithOld::isolateVariable()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l01150">CVC3::TheoryArith3::isolateVariable()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l01651">CVC3::TheoryArithOld::isStale()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l01290">CVC3::TheoryArith3::isStale()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01186">CVC3::SearchEngineTheoremProducer::iteToClauses()</a>, <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00106">CVC3::CNF_TheoremProducer::learnedClauses()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02245">CVC3::ArithTheoremProducerOld::lessThanToLE()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02043">CVC3::ArithTheoremProducer3::lessThanToLE()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02085">CVC3::ArithTheoremProducer::lessThanToLE()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03416">CVC3::ArithTheoremProducerOld::lessThanToLERewrite()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l03103">CVC3::ArithTheoremProducer3::lessThanToLERewrite()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l03152">CVC3::ArithTheoremProducer::lessThanToLERewrite()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00105">CVC3::SearchEngineTheoremProducer::negIntro()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00179">CVC3::SearchImplBase::newIntAssumption()</a>, <a class="el" href="search__fast_8cpp_source.html#l01573">CVC3::SearchEngineFast::newIntAssumption()</a>, <a class="el" href="search__sat_8cpp_source.html#l01064">CVC3::SearchSat::newUserAssumptionInt()</a>, <a class="el" href="search__sat_8cpp_source.html#l01042">CVC3::SearchSat::newUserAssumptionIntHelper()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03697">CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03070">CVC3::TheoryArithOld::normalize()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l01822">CVC3::TheoryArithOld::normalizeProjectIneqs()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l01449">CVC3::TheoryArith3::normalizeProjectIneqs()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08621">CVC3::TheoryQuant::notifyInconsistent()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00655">CVC3::CommonTheoremProducer::notNotElim()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00906">CVC3::CommonTheoremProducer::notToIff()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01226">CVC3::SearchEngineTheoremProducer::opCNFRule()</a>, <a class="el" href="theory__arith__new_8h_source.html#l00550">CVC3::TheoryArithNew::BoundInfo::operator<()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00054">CVC3::operator<<()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00568">CVC3::QuantTheoremProducer::packVar()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00408">CVC3::QuantTheoremProducer::partialUniversalInst()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l02594">CVC3::TheoryArithNew::pivot()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l03600">CVC3::TheoryArithNew::pivotRule()</a>, <a class="el" href="theorem_8cpp_source.html#l00209">pprintx()</a>, <a class="el" href="theorem_8cpp_source.html#l00210">pprintxnodag()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00120">CVC3::ExprTransform::preprocess()</a>, <a class="el" href="theorem_8cpp_source.html#l00580">print()</a>, <a class="el" href="theorem_8cpp_source.html#l00207">printx()</a>, <a class="el" href="theorem_8cpp_source.html#l00208">printxnodag()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l01037">CVC3::TheoryArithOld::processBuffer()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l01059">CVC3::TheoryArith3::processBuffer()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l05609">CVC3::BitvectorTheoremProducer::processExtract()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02373">CVC3::TheoryArithOld::processFiniteInterval()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01168">CVC3::TheoryArithNew::processFiniteInterval()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l01917">CVC3::TheoryArith3::processFiniteInterval()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00869">CVC3::TheoryArithOld::processIntEq()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00642">CVC3::TheoryArithNew::processIntEq()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00889">CVC3::TheoryArith3::processIntEq()</a>, <a class="el" href="search__fast_8cpp_source.html#l01108">processNode()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00615">CVC3::TheoryArithOld::processRealEq()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00317">CVC3::SearchImplBase::processResult()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00739">CVC3::TheoryArithOld::processSimpleIntEq()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00507">CVC3::TheoryArithNew::processSimpleIntEq()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00759">CVC3::TheoryArith3::processSimpleIntEq()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l01710">CVC3::TheoryArithOld::projectInequalities()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l01346">CVC3::TheoryArith3::projectInequalities()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00074">CVC3::SearchEngineTheoremProducer::proofByContradiction()</a>, <a class="el" href="circuit_8cpp_source.html#l00047">CVC3::Circuit::propagate()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l04000">CVC3::TheoryArithNew::propagateTheory()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00564">CVC3::SearchEngineTheoremProducer::propAndrAF()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00593">CVC3::SearchEngineTheoremProducer::propAndrAT()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00651">CVC3::SearchEngineTheoremProducer::propAndrLF()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00623">CVC3::SearchEngineTheoremProducer::propAndrLRT()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00681">CVC3::SearchEngineTheoremProducer::propAndrRF()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00782">CVC3::SearchEngineTheoremProducer::propIffr()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00923">CVC3::SearchEngineTheoremProducer::propIterIfThen()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00881">CVC3::SearchEngineTheoremProducer::propIterIte()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00970">CVC3::SearchEngineTheoremProducer::propIterThen()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00612">CVC3::QuantTheoremProducer::pullVarOut()</a>, <a class="el" href="decision__engine_8cpp_source.html#l00128">CVC3::DecisionEngine::pushDecision()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00055">CVC3::CommonTheoremProducer::queryTCC()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02953">CVC3::TheoryArithOld::rafineInequalityToInteger()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03253">CVC3::ArithTheoremProducerOld::rafineStrictInteger()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02970">CVC3::ArithTheoremProducer3::rafineStrictInteger()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l03068">CVC3::ArithTheoremProducer::rafineStrictInteger()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01702">CVC3::ArithTheoremProducerOld::realShadow()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01504">CVC3::ArithTheoremProducer3::realShadow()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01547">CVC3::ArithTheoremProducer::realShadow()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01737">CVC3::ArithTheoremProducerOld::realShadowEq()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01539">CVC3::ArithTheoremProducer3::realShadowEq()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01582">CVC3::ArithTheoremProducer::realShadowEq()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08466">CVC3::TheoryQuant::recInstantiate()</a>, <a class="el" href="search__fast_8cpp_source.html#l00549">CVC3::SearchEngineFast::recordFact()</a>, <a class="el" href="theorem_8cpp_source.html#l00516">recursivePrint()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l04662">CVC3::TheoryArithOld::registerAtom()</a>, <a class="el" href="uf__theorem__producer_8cpp_source.html#l00054">CVC3::UFTheoremProducer::relToClosure()</a>, <a class="el" href="uf__theorem__producer_8cpp_source.html#l00076">CVC3::UFTheoremProducer::relTrans()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00074">SAT::CNF_Manager::replaceITErec()</a>, <a class="el" href="theory__core_8cpp_source.html#l00968">CVC3::TheoryCore::rewrite()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01286">CVC3::CommonTheoremProducer::rewriteAnd()</a>, <a class="el" href="theory__records_8cpp_source.html#l00091">CVC3::TheoryRecords::rewriteAux()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00887">CVC3::TheoryBitvector::rewriteBV()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00161">CVC3::CoreTheoremProducer::rewriteIteElse()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00136">CVC3::CoreTheoremProducer::rewriteIteThen()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01292">CVC3::CommonTheoremProducer::rewriteOr()</a>, <a class="el" href="theory__quant_8cpp_source.html#l00998">CVC3::TheoryQuant::sendInstNew()</a>, <a class="el" href="theory__core_8cpp_source.html#l00509">CVC3::TheoryCore::setFindLiteral()</a>, <a class="el" href="theory__core_8cpp_source.html#l04245">CVC3::TheoryCore::setInconsistent()</a>, <a class="el" href="theory__core_8cpp_source.html#l04260">CVC3::TheoryCore::setupTerm()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02917">CVC3::TheoryQuant::setupTriggers()</a>, <a class="el" href="variable_8cpp_source.html#l00295">CVC3::VariableValue::setValue()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00437">CVC3::BitvectorTheoremProducer::signBVLTRule()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01508">CVC3::ArithTheoremProducerOld::simpleIneqInt()</a>, <a class="el" href="search__impl__base_8h_source.html#l00124">CVC3::SearchImplBase::simplify()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l02366">CVC3::TheoryBitvector::simplifyPendingEq()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01731">CVC3::CompleteInstPreProcessor::simplifyQuant()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01223">CVC3::CommonTheoremProducer::skolemize()</a>, <a class="el" href="theory__core_8cpp_source.html#l01248">CVC3::TheoryCore::solve()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l02818">CVC3::TheoryBitvector::solve()</a>, <a class="el" href="theory__array_8cpp_source.html#l00718">CVC3::TheoryArray::solve()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00912">CVC3::TheoryArithOld::solvedForm()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00681">CVC3::TheoryArithNew::solvedForm()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00932">CVC3::TheoryArith3::solvedForm()</a>, <a class="el" href="search__fast_8cpp_source.html#l00254">CVC3::SearchEngineFast::split()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02054">CVC3::ArithTheoremProducerOld::splitGrayShadow()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01852">CVC3::ArithTheoremProducer3::splitGrayShadow()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01894">CVC3::ArithTheoremProducer::splitGrayShadow()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03456">CVC3::ArithTheoremProducerOld::splitGrayShadowSmall()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l01017">CVC3::TheoryArithOld::substAndCanonize()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00787">CVC3::TheoryArithNew::substAndCanonize()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l01038">CVC3::TheoryArith3::substAndCanonize()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l03447">CVC3::TheoryArithNew::substAndCanonizeModTableaux()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l03524">CVC3::TheoryArithNew::substAndCanonizeTableaux()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00302">CVC3::CommonTheoremProducer::substitutivityRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00187">CVC3::CommonTheoremProducer::symmetryRule()</a>, <a class="el" href="search__fast_8cpp_source.html#l01096">TheoremEq()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02227">CVC3::TheoryArithOld::TheoryArithOld()</a>, <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00245">CVC3::CommonTheoremProducer::transitivityRule()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00510">SAT::CNF_Manager::translateExpr()</a>, <a class="el" href="vcl_8cpp_source.html#l02116">CVC3::VCL::tryModelGeneration()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00511">CVC3::SearchEngineTheoremProducer::unitProp()</a>, <a class="el" href="search__fast_8cpp_source.html#l00915">CVC3::SearchEngineFast::unitPropagation()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00154">CVC3::QuantTheoremProducer::universalInst()</a>, <a class="el" href="theory__quant_8cpp_source.html#l00419">CVC3::TheoryQuant::update()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l02695">CVC3::TheoryBitvector::update()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03390">CVC3::TheoryArithOld::update()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01769">CVC3::TheoryArithNew::update()</a>, and <a class="el" href="theory__arith3_8cpp_source.html#l02534">CVC3::TheoryArith3::update()</a>.</p>
</div>
</div>
<a class="anchor" id="a206c04f39fbbcacef2337148675553f4"></a><!-- doxytag: member="CVC3::Theorem::getLHS" ref="a206c04f39fbbcacef2337148675553f4" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & CVC3::Theorem::getLHS </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00240">240</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="theorem_8h_source.html#l00092">d_expr</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem__value_8h_source.html#l00298">CVC3::TheoremValue::getLHS()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00723">CVC3::SearchImplBase::addToCNFCache()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>, <a class="el" href="theory__core_8cpp_source.html#l04093">CVC3::TheoryCore::assertEqualities()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02020">CVC3::TheoryArith3::assertFact()</a>, <a class="el" href="theory__core_8cpp_source.html#l00321">CVC3::TheoryCore::assertFactCore()</a>, <a class="el" href="theory__core_8cpp_source.html#l03734">CVC3::TheoryCore::assignValue()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06407">CVC3::BitvectorTheoremProducer::bitblastBVPlus()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00164">CVC3::TheoryBitvector::bitBlastDisEqn()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00091">CVC3::TheoryBitvector::bitBlastEqn()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00359">CVC3::TheoryBitvector::bitBlastTerm()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01337">CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed()</a>, <a class="el" href="theory__core_8cpp_source.html#l03862">CVC3::TheoryCore::buildModel()</a>, <a class="el" href="theory__arith_8cpp_source.html#l00031">CVC3::TheoryArith::canonRec()</a>, <a class="el" href="theory__arith_8cpp_source.html#l00257">CVC3::TheoryArith::canonSimp()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03621">CVC3::TheoryArithOld::checkAssertEqInvariant()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02643">CVC3::TheoryArith3::checkAssertEqInvariant()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00178">CVC3::TheoryDatatypeLazy::checkSat()</a>, <a class="el" href="theorem_8cpp_source.html#l00045">CVC3::compare()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01406">CVC3::BitvectorTheoremProducer::computeCarryPreComputed()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00509">CVC3::TheoryUF::computeModel()</a>, <a class="el" href="theory__records_8cpp_source.html#l00281">CVC3::TheoryRecords::computeModel()</a>, <a class="el" href="theory__array_8cpp_source.html#l00939">CVC3::TheoryArray::computeModel()</a>, <a class="el" href="datatype__theorem__producer_8cpp_source.html#l00118">CVC3::DatatypeTheoremProducer::decompose()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, <a class="el" href="theory__core_8cpp_source.html#l04213">CVC3::TheoryCore::enqueueFact()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02708">CVC3::ArithTheoremProducerOld::eqElimIntRule()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02506">CVC3::ArithTheoremProducer3::eqElimIntRule()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02531">CVC3::ArithTheoremProducer::eqElimIntRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01911">CVC3::BitvectorTheoremProducer::eqToBits()</a>, <a class="el" href="records__theorem__producer_8cpp_source.html#l00205">CVC3::RecordsTheoremProducer::expandEq()</a>, <a class="el" href="theory_8cpp_source.html#l00310">CVC3::Theory::find()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00750">CVC3::SearchImplBase::findInCNFCache()</a>, <a class="el" href="theory_8cpp_source.html#l00295">CVC3::Theory::findRef()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l02409">CVC3::TheoryBitvector::generalBitBlast()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00762">CVC3::BitvectorTheoremProducer::generalIneqn()</a>, <a class="el" href="theorem_8cpp_source.html#l00320">getAssumptionsAndCongRec()</a>, <a class="el" href="theorem_8h_source.html#l00359">CVC3::Theorem3::getLHS()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00641">CVC3::CommonTheoremProducer::iffContrapositive()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00626">CVC3::CommonTheoremProducer::iffFalseElim()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00667">CVC3::CommonTheoremProducer::iffMP()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01206">CVC3::SearchEngineTheoremProducer::iffToClauses()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00612">CVC3::CommonTheoremProducer::iffTrueElim()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00615">CVC3::TheoryArithOld::processRealEq()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00420">CVC3::TheoryArithNew::processRealEq()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00642">CVC3::TheoryArith3::processRealEq()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00739">CVC3::TheoryArithOld::processSimpleIntEq()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00507">CVC3::TheoryArithNew::processSimpleIntEq()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00759">CVC3::TheoryArith3::processSimpleIntEq()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00388">CVC3::ArrayTheoremProducer::propagateIndexDiseq()</a>, <a class="el" href="theory__core_8cpp_source.html#l00968">CVC3::TheoryCore::rewrite()</a>, <a class="el" href="theory__records_8cpp_source.html#l00045">CVC3::TheoryRecords::rewriteAux()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l01638">CVC3::TheoryBitvector::rewriteBoolean()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00887">CVC3::TheoryBitvector::rewriteBV()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00161">CVC3::CoreTheoremProducer::rewriteIteElse()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00136">CVC3::CoreTheoremProducer::rewriteIteThen()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00205">CVC3::ArrayTheoremProducer::rewriteRedundantWrite1()</a>, <a class="el" href="expr_8h_source.html#l01416">CVC3::Expr::setEqNext()</a>, <a class="el" href="expr_8h_source.html#l01405">CVC3::Expr::setFind()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00437">CVC3::BitvectorTheoremProducer::signBVLTRule()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00812">CVC3::TheoryBitvector::simplifyOp()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l02366">CVC3::TheoryBitvector::simplifyPendingEq()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00425">CVC3::TheoryDatatype::solve()</a>, <a class="el" href="theory__core_8cpp_source.html#l01248">CVC3::TheoryCore::solve()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l02818">CVC3::TheoryBitvector::solve()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03547">CVC3::TheoryArithOld::solve()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01805">CVC3::TheoryArithNew::solve()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02569">CVC3::TheoryArith3::solve()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00302">CVC3::CommonTheoremProducer::substitutivityRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00187">CVC3::CommonTheoremProducer::symmetryRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00245">CVC3::CommonTheoremProducer::transitivityRule()</a>, <a class="el" href="theory__quant_8cpp_source.html#l00419">CVC3::TheoryQuant::update()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00267">CVC3::TheoryDatatypeLazy::update()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00359">CVC3::TheoryDatatype::update()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l02695">CVC3::TheoryBitvector::update()</a>, <a class="el" href="theory__array_8cpp_source.html#l00550">CVC3::TheoryArray::update()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03390">CVC3::TheoryArithOld::update()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01769">CVC3::TheoryArithNew::update()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02534">CVC3::TheoryArith3::update()</a>, <a class="el" href="theory_8cpp_source.html#l00417">CVC3::Theory::updateHelper()</a>, and <a class="el" href="theory__bitvector_8cpp_source.html#l02791">CVC3::TheoryBitvector::updateSubterms()</a>.</p>
</div>
</div>
<a class="anchor" id="a97d957fcbf9094480851b1d2e5d3729f"></a><!-- doxytag: member="CVC3::Theorem::getRHS" ref="a97d957fcbf9094480851b1d2e5d3729f" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & CVC3::Theorem::getRHS </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00246">246</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="theorem_8h_source.html#l00092">d_expr</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem__value_8h_source.html#l00305">CVC3::TheoremValue::getRHS()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
<p>Referenced by <a class="el" href="theory__arith__old_8cpp_source.html#l01241">CVC3::TheoryArithOld::addToBuffer()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00723">CVC3::SearchImplBase::addToCNFCache()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>, <a class="el" href="theory__core_8cpp_source.html#l04093">CVC3::TheoryCore::assertEqualities()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02020">CVC3::TheoryArith3::assertFact()</a>, <a class="el" href="theory__core_8cpp_source.html#l00321">CVC3::TheoryCore::assertFactCore()</a>, <a class="el" href="theory__core_8cpp_source.html#l03734">CVC3::TheoryCore::assignValue()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00164">CVC3::TheoryBitvector::bitBlastDisEqn()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00091">CVC3::TheoryBitvector::bitBlastEqn()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00240">CVC3::TheoryBitvector::bitBlastIneqn()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00359">CVC3::TheoryBitvector::bitBlastTerm()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01337">CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00380">CVC3::BitvectorTheoremProducer::bitExtractSXRule()</a>, <a class="el" href="theory__core_8cpp_source.html#l03817">CVC3::TheoryCore::buildModel()</a>, <a class="el" href="theory__core_8cpp_source.html#l00857">CVC3::TheoryCore::callTheoryPreprocess()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00218">CVC3::TheoryArithOld::canon()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00123">CVC3::TheoryArithNew::canon()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00212">CVC3::TheoryArith3::canon()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04770">CVC3::BitvectorTheoremProducer::canonBVMult()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l00957">CVC3::ArithTheoremProducerOld::canonDivide()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l00907">CVC3::ArithTheoremProducer3::canonDivide()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l00907">CVC3::ArithTheoremProducer::canonDivide()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l00232">CVC3::ArithTheoremProducerOld::canonMultConstPlus()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l00231">CVC3::ArithTheoremProducer3::canonMultConstPlus()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l00237">CVC3::ArithTheoremProducer::canonMultConstPlus()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00417">CVC3::TheoryArithOld::canonPredEquiv()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00295">CVC3::TheoryArithNew::canonPredEquiv()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00404">CVC3::TheoryArith3::canonPredEquiv()</a>, <a class="el" href="theory__arith_8cpp_source.html#l00031">CVC3::TheoryArith::canonRec()</a>, <a class="el" href="theory__arith_8cpp_source.html#l00257">CVC3::TheoryArith::canonSimp()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00371">CVC3::TheoryArithOld::canonSimplify()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00246">CVC3::TheoryArithNew::canonSimplify()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00360">CVC3::TheoryArith3::canonSimplify()</a>, <a class="el" href="theory__arith_8h_source.html#l00120">CVC3::TheoryArith::canonThm()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03621">CVC3::TheoryArithOld::checkAssertEqInvariant()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02643">CVC3::TheoryArith3::checkAssertEqInvariant()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02913">CVC3::TheoryArithOld::checkIntegerEquality()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00156">CVC3::TheoryUF::checkSat()</a>, <a class="el" href="theory__quant_8cpp_source.html#l07647">CVC3::TheoryQuant::checkSat()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00178">CVC3::TheoryDatatypeLazy::checkSat()</a>, <a class="el" href="theory__array_8cpp_source.html#l00154">CVC3::TheoryArray::checkSat()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02606">CVC3::TheoryArithOld::checkSat()</a>, <a class="el" href="search__simple_8cpp_source.html#l00165">CVC3::SearchSimple::checkValidInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, <a class="el" href="theory__core_8cpp_source.html#l03763">CVC3::TheoryCore::collectBasicVars()</a>, <a class="el" href="theory__core_8cpp_source.html#l03954">CVC3::TheoryCore::collectModelValues()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03692">CVC3::BitvectorTheoremProducer::collectOneTermOfPlus()</a>, <a class="el" href="theorem_8cpp_source.html#l00045">CVC3::compare()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l02512">CVC3::TheoryBitvector::comparebv()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01406">CVC3::BitvectorTheoremProducer::computeCarryPreComputed()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00509">CVC3::TheoryUF::computeModel()</a>, <a class="el" href="theory__records_8cpp_source.html#l00281">CVC3::TheoryRecords::computeModel()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l03345">CVC3::TheoryBitvector::computeModel()</a>, <a class="el" href="theory__array_8cpp_source.html#l00939">CVC3::TheoryArray::computeModel()</a>, <a class="el" href="theory__core_8cpp_source.html#l03449">CVC3::TheoryCore::computeModelBasic()</a>, <a class="el" href="theory__records_8cpp_source.html#l00261">CVC3::TheoryRecords::computeModelTerm()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00591">CVC3::TheoryUF::computeTCC()</a>, <a class="el" href="theory__simulate_8cpp_source.html#l00164">CVC3::TheorySimulate::computeTCC()</a>, <a class="el" href="theory__core_8cpp_source.html#l01650">CVC3::TheoryCore::computeTCC()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l05570">CVC3::TheoryBitvector::computeTCC()</a>, <a class="el" href="theory__array_8cpp_source.html#l01041">CVC3::TheoryArray::computeTCC()</a>, <a class="el" href="theory_8cpp_source.html#l00081">CVC3::Theory::computeTCC()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l05535">CVC3::TheoryArithOld::computeTermBounds()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03785">CVC3::BitvectorTheoremProducer::createNewPlusCollection()</a>, <a class="el" href="theory__quant_8cpp_source.html#l00343">CVC3::TheoryQuant::debug()</a>, <a class="el" href="datatype__theorem__producer_8cpp_source.html#l00118">CVC3::DatatypeTheoremProducer::decompose()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, <a class="el" href="theory__core_8cpp_source.html#l04213">CVC3::TheoryCore::enqueueFact()</a>, <a class="el" href="theory__quant_8cpp_source.html#l00633">CVC3::TheoryQuant::enqueueInst()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02708">CVC3::ArithTheoremProducerOld::eqElimIntRule()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02506">CVC3::ArithTheoremProducer3::eqElimIntRule()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02531">CVC3::ArithTheoremProducer::eqElimIntRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01911">CVC3::BitvectorTheoremProducer::eqToBits()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02816">CVC3::ArithTheoremProducerOld::equalLeaves1()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02614">CVC3::ArithTheoremProducer3::equalLeaves1()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02639">CVC3::ArithTheoremProducer::equalLeaves1()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02845">CVC3::ArithTheoremProducerOld::equalLeaves2()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02643">CVC3::ArithTheoremProducer3::equalLeaves2()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02668">CVC3::ArithTheoremProducer::equalLeaves2()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02874">CVC3::ArithTheoremProducerOld::equalLeaves3()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02672">CVC3::ArithTheoremProducer3::equalLeaves3()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02697">CVC3::ArithTheoremProducer::equalLeaves3()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02903">CVC3::ArithTheoremProducerOld::equalLeaves4()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02701">CVC3::ArithTheoremProducer3::equalLeaves4()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02726">CVC3::ArithTheoremProducer::equalLeaves4()</a>, <a class="el" href="records__theorem__producer_8cpp_source.html#l00205">CVC3::RecordsTheoremProducer::expandEq()</a>, <a class="el" href="theory_8cpp_source.html#l00310">CVC3::Theory::find()</a>, <a class="el" href="theory_8h_source.html#l00503">CVC3::Theory::findExpr()</a>, <a class="el" href="theory_8cpp_source.html#l00357">CVC3::Theory::findReduced()</a>, <a class="el" href="theory_8cpp_source.html#l00295">CVC3::Theory::findRef()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l02409">CVC3::TheoryBitvector::generalBitBlast()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00762">CVC3::BitvectorTheoremProducer::generalIneqn()</a>, <a class="el" href="theory__core_8cpp_source.html#l04320">CVC3::TheoryCore::getAssignment()</a>, <a class="el" href="theorem_8cpp_source.html#l00320">getAssumptionsAndCongRec()</a>, <a class="el" href="theorem_8h_source.html#l00360">CVC3::Theorem3::getRHS()</a>, <a class="el" href="theory__core_8cpp_source.html#l04333">CVC3::TheoryCore::getValue()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00641">CVC3::CommonTheoremProducer::iffContrapositive()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00626">CVC3::CommonTheoremProducer::iffFalseElim()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00667">CVC3::CommonTheoremProducer::iffMP()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01206">CVC3::SearchEngineTheoremProducer::iffToClauses()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00612">CVC3::CommonTheoremProducer::iffTrueElim()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l04613">CVC3::TheoryArithOld::inequalityToFind()</a>, <a class="el" href="theory_8cpp_source.html#l00557">CVC3::Theory::leavesAreSimp()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04075">CVC3::TheoryQuant::matchListOld()</a>, <a class="el" href="theory__quant_8cpp_source.html#l03950">CVC3::TheoryQuant::multMatchChild()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00282">CVC3::ExprTransform::newPP()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00334">CVC3::ExprTransform::newPPrec()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04592">CVC3::TheoryQuant::newTopMatch()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04671">CVC3::TheoryQuant::newTopMatchSig()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03070">CVC3::TheoryArithOld::normalize()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01537">CVC3::TheoryArithNew::normalize()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02382">CVC3::TheoryArith3::normalize()</a>, <a class="el" href="theory__arith__new_8h_source.html#l00550">CVC3::TheoryArithNew::BoundInfo::operator<()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00079">CVC3::ExprTransform::preprocess()</a>, <a class="el" href="translator_8cpp_source.html#l00072">CVC3::Translator::preprocessRec()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01168">CVC3::TheoryArithNew::processFiniteInterval()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l01917">CVC3::TheoryArith3::processFiniteInterval()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00615">CVC3::TheoryArithOld::processRealEq()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00420">CVC3::TheoryArithNew::processRealEq()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00642">CVC3::TheoryArith3::processRealEq()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00739">CVC3::TheoryArithOld::processSimpleIntEq()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00507">CVC3::TheoryArithNew::processSimpleIntEq()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00759">CVC3::TheoryArith3::processSimpleIntEq()</a>, <a class="el" href="theory__core_8cpp_source.html#l00291">CVC3::TheoryCore::processUpdates()</a>, <a class="el" href="theory__array_8cpp_source.html#l00345">CVC3::TheoryArray::pullIndex()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00699">CVC3::TheoryBitvector::pushNegationRec()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00225">CVC3::ExprTransform::pushNegationRec()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l02953">CVC3::TheoryArithOld::rafineInequalityToInteger()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01541">CVC3::TheoryArithNew::rafineIntegerConstraints()</a>, <a class="el" href="theory__quant_8cpp_source.html#l05587">CVC3::TheoryQuant::recMultMatch()</a>, <a class="el" href="theory__quant_8cpp_source.html#l05310">CVC3::TheoryQuant::recMultMatchDebug()</a>, <a class="el" href="theory__core_8cpp_source.html#l03541">CVC3::TheoryCore::registerAtom()</a>, <a class="el" href="theory_8cpp_source.html#l00935">CVC3::Theory::renameExpr()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00804">CVC3::SearchImplBase::replaceITE()</a>, <a class="el" href="search__simple_8cpp_source.html#l00207">CVC3::SearchSimple::restartInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01750">CVC3::SearchEngineFast::restartInternal()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00211">CVC3::TheoryUF::rewrite()</a>, <a class="el" href="theory__records_8cpp_source.html#l00161">CVC3::TheoryRecords::rewrite()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00320">CVC3::TheoryDatatype::rewrite()</a>, <a class="el" href="theory__core_8cpp_source.html#l00968">CVC3::TheoryCore::rewrite()</a>, <a class="el" href="theory__array_8cpp_source.html#l00368">CVC3::TheoryArray::rewrite()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03076">CVC3::TheoryArithOld::rewrite()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01570">CVC3::TheoryArithNew::rewrite()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02387">CVC3::TheoryArith3::rewrite()</a>, <a class="el" href="theory__records_8cpp_source.html#l00045">CVC3::TheoryRecords::rewriteAux()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l01638">CVC3::TheoryBitvector::rewriteBoolean()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00887">CVC3::TheoryBitvector::rewriteBV()</a>, <a class="el" href="theory__core_8cpp_source.html#l00257">CVC3::TheoryCore::rewriteCore()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00161">CVC3::CoreTheoremProducer::rewriteIteElse()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00136">CVC3::CoreTheoremProducer::rewriteIteThen()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00205">CVC3::ArrayTheoremProducer::rewriteRedundantWrite1()</a>, <a class="el" href="theory__core_8cpp_source.html#l00509">CVC3::TheoryCore::setFindLiteral()</a>, <a class="el" href="theory__records_8cpp_source.html#l00508">CVC3::TheoryRecords::setup()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00437">CVC3::BitvectorTheoremProducer::signBVLTRule()</a>, <a class="el" href="theory__core_8cpp_source.html#l00184">CVC3::TheoryCore::simplify()</a>, <a class="el" href="theory_8h_source.html#l00430">CVC3::Theory::simplifyExpr()</a>, <a class="el" href="theory__core_8cpp_source.html#l01292">CVC3::TheoryCore::simplifyOp()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00812">CVC3::TheoryBitvector::simplifyOp()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l02366">CVC3::TheoryBitvector::simplifyPendingEq()</a>, <a class="el" href="vcl_8cpp_source.html#l01919">CVC3::VCL::simplifyThm()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00425">CVC3::TheoryDatatype::solve()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03547">CVC3::TheoryArithOld::solve()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01805">CVC3::TheoryArithNew::solve()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02569">CVC3::TheoryArith3::solve()</a>, <a class="el" href="search__fast_8cpp_source.html#l00254">CVC3::SearchEngineFast::split()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00966">CVC3::TheoryArithOld::substAndCanonize()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00736">CVC3::TheoryArithNew::substAndCanonize()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00987">CVC3::TheoryArith3::substAndCanonize()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l03447">CVC3::TheoryArithNew::substAndCanonizeModTableaux()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l03524">CVC3::TheoryArithNew::substAndCanonizeTableaux()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00302">CVC3::CommonTheoremProducer::substitutivityRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00187">CVC3::CommonTheoremProducer::symmetryRule()</a>, <a class="el" href="theory__quant_8cpp_source.html#l07258">CVC3::TheoryQuant::synNewInst()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00245">CVC3::CommonTheoremProducer::transitivityRule()</a>, <a class="el" href="cnf__manager_8cpp_source.html#l00147">SAT::CNF_Manager::translateExprRec()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l05039">CVC3::TheoryArithOld::tryPropagate()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00257">CVC3::TheoryUF::update()</a>, <a class="el" href="theory__records_8cpp_source.html#l00561">CVC3::TheoryRecords::update()</a>, <a class="el" href="theory__quant_8cpp_source.html#l00419">CVC3::TheoryQuant::update()</a>, <a class="el" href="theory__datatype__lazy_8cpp_source.html#l00267">CVC3::TheoryDatatypeLazy::update()</a>, <a class="el" href="theory__datatype_8cpp_source.html#l00359">CVC3::TheoryDatatype::update()</a>, <a class="el" href="theory__core_8cpp_source.html#l01141">CVC3::TheoryCore::update()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l02695">CVC3::TheoryBitvector::update()</a>, <a class="el" href="theory__array_8cpp_source.html#l00550">CVC3::TheoryArray::update()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l03390">CVC3::TheoryArithOld::update()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l01769">CVC3::TheoryArithNew::update()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l02534">CVC3::TheoryArith3::update()</a>, <a class="el" href="theory_8cpp_source.html#l00473">CVC3::Theory::updateCC()</a>, <a class="el" href="theory_8cpp_source.html#l00417">CVC3::Theory::updateHelper()</a>, and <a class="el" href="theory__bitvector_8cpp_source.html#l02791">CVC3::TheoryBitvector::updateSubterms()</a>.</p>
</div>
</div>
<a class="anchor" id="aad446d2963572258f7b8f0c74fb9e299"></a><!-- doxytag: member="CVC3::Theorem::GetSatAssumptions" ref="aad446d2963572258f7b8f0c74fb9e299" args="(std::vector< Theorem > &assumptions) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::GetSatAssumptions </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>assumptions</em></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00309">309</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00151">CVC3::Assumptions::begin()</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="assumptions_8h_source.html#l00152">CVC3::Assumptions::end()</a>, <a class="el" href="theorem_8cpp_source.html#l00385">getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00416">isFlagged()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, and <a class="el" href="theorem_8cpp_source.html#l00429">setFlag()</a>.</p>
<p>Referenced by <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00049">CVC3::CNF_TheoremProducer::getSmartClauses()</a>.</p>
</div>
</div>
<a class="anchor" id="a524b4dafa4fb8f14742baa856612d92b"></a><!-- doxytag: member="CVC3::Theorem::getLeafAssumptions" ref="a524b4dafa4fb8f14742baa856612d92b" args="(std::vector< Expr > &assumptions, bool negate=false) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::getLeafAssumptions </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>assumptions</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>negate</em> = <code>false</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00274">274</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="theorem_8cpp_source.html#l00422">clearAllFlags()</a>, <a class="el" href="theorem_8cpp_source.html#l00259">getAssumptionsRec()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, and <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l03862">CVC3::TheoryCore::buildModel()</a>, <a class="el" href="search__simple_8cpp_source.html#l00126">CVC3::SearchSimple::checkValidMain()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, <a class="el" href="vcl_8cpp_source.html#l02085">CVC3::VCL::getAssumptionsUsed()</a>, <a class="el" href="search_8cpp_source.html#l00091">CVC3::SearchEngine::getConcreteModel()</a>, <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00106">CVC3::CNF_TheoremProducer::learnedClauses()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08621">CVC3::TheoryQuant::notifyInconsistent()</a>, <a class="el" href="theory__core_8cpp_source.html#l03429">CVC3::TheoryCore::refineCounterExample()</a>, and <a class="el" href="vcl_8cpp_source.html#l02116">CVC3::VCL::tryModelGeneration()</a>.</p>
</div>
</div>
<a class="anchor" id="a69c948a7ecc79597eac8eb816e8d76a1"></a><!-- doxytag: member="CVC3::Theorem::getAssumptionsAndCong" ref="a69c948a7ecc79597eac8eb816e8d76a1" args="(std::vector< Expr > &assumptions, std::vector< Expr > &congruences, bool negate=false) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::getAssumptionsAndCong </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>assumptions</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>congruences</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>negate</em> = <code>false</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00370">370</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="theorem_8cpp_source.html#l00422">clearAllFlags()</a>, <a class="el" href="theorem_8cpp_source.html#l00320">getAssumptionsAndCongRec()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, and <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>.</p>
</div>
</div>
<a class="anchor" id="a5e9ab00a613df15cc02f55edb55a67b3"></a><!-- doxytag: member="CVC3::Theorem::getAssumptionsRef" ref="a5e9ab00a613df15cc02f55edb55a67b3" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & CVC3::Theorem::getAssumptionsRef </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00385">385</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="classCVC3_1_1TheoremValue.html#a375f504a8a9844005b2eb8e055483829">CVC3::TheoremValue::getAssumptionsRef()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
<p>Referenced by <a class="el" href="assumptions_8cpp_source.html#l00190">CVC3::Assumptions::add()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00510">CVC3::QuantTheoremProducer::adjustVarUniv()</a>, <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, <a class="el" href="assumptions_8cpp_source.html#l00149">CVC3::Assumptions::Assumptions()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00225">CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00927">CVC3::BitvectorTheoremProducer::bitExtractToExtract()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00066">CVC3::BitvectorTheoremProducer::bitvectorFalseRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00104">CVC3::BitvectorTheoremProducer::bitvectorTrueRule()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00748">CVC3::QuantTheoremProducer::boundVarElim()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00135">CVC3::SearchEngineTheoremProducer::caseSplit()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00429">CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems()</a>, <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00311">CVC3::CNF_TheoremProducer::CNFAddUnit()</a>, <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00321">CVC3::CNF_TheoremProducer::CNFConvert()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00375">CVC3::SearchEngineTheoremProducer::cutRule()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02931">CVC3::ArithTheoremProducerOld::diseqToIneq()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02729">CVC3::ArithTheoremProducer3::diseqToIneq()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02754">CVC3::ArithTheoremProducer::diseqToIneq()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00454">CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01911">CVC3::BitvectorTheoremProducer::eqToBits()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02816">CVC3::ArithTheoremProducerOld::equalLeaves1()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02614">CVC3::ArithTheoremProducer3::equalLeaves1()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02639">CVC3::ArithTheoremProducer::equalLeaves1()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02845">CVC3::ArithTheoremProducerOld::equalLeaves2()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02643">CVC3::ArithTheoremProducer3::equalLeaves2()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02668">CVC3::ArithTheoremProducer::equalLeaves2()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02874">CVC3::ArithTheoremProducerOld::equalLeaves3()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02672">CVC3::ArithTheoremProducer3::equalLeaves3()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02697">CVC3::ArithTheoremProducer::equalLeaves3()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02903">CVC3::ArithTheoremProducerOld::equalLeaves4()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02701">CVC3::ArithTheoremProducer3::equalLeaves4()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02726">CVC3::ArithTheoremProducer::equalLeaves4()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02014">CVC3::ArithTheoremProducerOld::expandDarkShadow()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01811">CVC3::ArithTheoremProducer3::expandDarkShadow()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01854">CVC3::ArithTheoremProducer::expandDarkShadow()</a>, <a class="el" href="records__theorem__producer_8cpp_source.html#l00205">CVC3::RecordsTheoremProducer::expandEq()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02091">CVC3::ArithTheoremProducerOld::expandGrayShadow()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01889">CVC3::ArithTheoremProducer3::expandGrayShadow()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01931">CVC3::ArithTheoremProducer::expandGrayShadow()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02029">CVC3::ArithTheoremProducerOld::expandGrayShadow0()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01826">CVC3::ArithTheoremProducer3::expandGrayShadow0()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01869">CVC3::ArithTheoremProducer::expandGrayShadow0()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02122">CVC3::ArithTheoremProducerOld::expandGrayShadowConst()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01920">CVC3::ArithTheoremProducer3::expandGrayShadowConst()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01962">CVC3::ArithTheoremProducer::expandGrayShadowConst()</a>, <a class="el" href="records__theorem__producer_8cpp_source.html#l00158">CVC3::RecordsTheoremProducer::expandNeq()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04294">CVC3::BitvectorTheoremProducer::expandTypePred()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08653">CVC3::TheoryQuant::findInstAssumptions()</a>, <a class="el" href="assumptions_8cpp_source.html#l00034">CVC3::Assumptions::findTheorem()</a>, <a class="el" href="theorem_8cpp_source.html#l00320">getAssumptionsAndCongRec()</a>, <a class="el" href="vcl_8cpp_source.html#l00354">CVC3::VCL::getAssumptionsRec()</a>, <a class="el" href="theorem_8cpp_source.html#l00259">getAssumptionsRec()</a>, <a class="el" href="theorem_8h_source.html#l00365">CVC3::Theorem3::getAssumptionsRef()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00297">CVC3::SearchImplBase::getAssumptionsUsed()</a>, <a class="el" href="theorem_8cpp_source.html#l00309">GetSatAssumptions()</a>, <a class="el" href="theorem_8cpp_source.html#l00288">GetSatAssumptionsRec()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02187">CVC3::ArithTheoremProducerOld::grayShadowConst()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01985">CVC3::ArithTheoremProducer3::grayShadowConst()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02027">CVC3::ArithTheoremProducer::grayShadowConst()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01206">CVC3::SearchEngineTheoremProducer::iffToClauses()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00775">CVC3::CommonTheoremProducer::implIntro()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01330">CVC3::ArithTheoremProducerOld::intEqIrrational()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01260">CVC3::ArithTheoremProducer3::intEqIrrational()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01273">CVC3::ArithTheoremProducer::intEqIrrational()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03332">CVC3::ArithTheoremProducerOld::intEqualityRationalConstant()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02297">CVC3::ArithTheoremProducerOld::intVarEqnConst()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02095">CVC3::ArithTheoremProducer3::intVarEqnConst()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02138">CVC3::ArithTheoremProducer::intVarEqnConst()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01186">CVC3::SearchEngineTheoremProducer::iteToClauses()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00105">CVC3::SearchEngineTheoremProducer::negIntro()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08621">CVC3::TheoryQuant::notifyInconsistent()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01226">CVC3::SearchEngineTheoremProducer::opCNFRule()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00568">CVC3::QuantTheoremProducer::packVar()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00408">CVC3::QuantTheoremProducer::partialUniversalInst()</a>, <a class="el" href="theorem_8cpp_source.html#l00580">print()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00074">CVC3::SearchEngineTheoremProducer::proofByContradiction()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00612">CVC3::QuantTheoremProducer::pullVarOut()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00055">CVC3::CommonTheoremProducer::queryTCC()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03253">CVC3::ArithTheoremProducerOld::rafineStrictInteger()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02970">CVC3::ArithTheoremProducer3::rafineStrictInteger()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l03068">CVC3::ArithTheoremProducer::rafineStrictInteger()</a>, <a class="el" href="theorem_8cpp_source.html#l00516">recursivePrint()</a>, <a class="el" href="uf__theorem__producer_8cpp_source.html#l00054">CVC3::UFTheoremProducer::relToClosure()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00161">CVC3::CoreTheoremProducer::rewriteIteElse()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00136">CVC3::CoreTheoremProducer::rewriteIteThen()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00205">CVC3::ArrayTheoremProducer::rewriteRedundantWrite1()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02054">CVC3::ArithTheoremProducerOld::splitGrayShadow()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01852">CVC3::ArithTheoremProducer3::splitGrayShadow()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01894">CVC3::ArithTheoremProducer::splitGrayShadow()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03456">CVC3::ArithTheoremProducerOld::splitGrayShadowSmall()</a>, <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00154">CVC3::QuantTheoremProducer::universalInst()</a>, and <a class="el" href="search__theorem__producer_8cpp_source.html#l00192">CVC3::SearchEngineTheoremProducer::verifyConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="a2d8352c07a756c3837683a27a1e659ef"></a><!-- doxytag: member="CVC3::Theorem::getProof" ref="a2d8352c07a756c3837683a27a1e659ef" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Proof.html">Proof</a> CVC3::Theorem::getProof </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00402">402</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8h_source.html#l00132">exprValue()</a>, <a class="el" href="theorem__value_8h_source.html#l00316">CVC3::TheoremValue::getProof()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, <a class="el" href="kinds_8h_source.html#l00275">PF_APPLY</a>, <a class="el" href="theorem_8h_source.html#l00133">thm()</a>, and <a class="el" href="theorem_8cpp_source.html#l00214">withProof()</a>.</p>
<p>Referenced by <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03016">CVC3::ArithTheoremProducerOld::addInequalities()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02814">CVC3::ArithTheoremProducer3::addInequalities()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02905">CVC3::ArithTheoremProducer::addInequalities()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00510">CVC3::QuantTheoremProducer::adjustVarUniv()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00718">CVC3::CommonTheoremProducer::andElim()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00338">CVC3::ArrayTheoremProducer::arrayNotEq()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00225">CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00927">CVC3::BitvectorTheoremProducer::bitExtractToExtract()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00066">CVC3::BitvectorTheoremProducer::bitvectorFalseRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00104">CVC3::BitvectorTheoremProducer::bitvectorTrueRule()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00748">CVC3::QuantTheoremProducer::boundVarElim()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00135">CVC3::SearchEngineTheoremProducer::caseSplit()</a>, <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00311">CVC3::CNF_TheoremProducer::CNFAddUnit()</a>, <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00321">CVC3::CNF_TheoremProducer::CNFConvert()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00744">CVC3::SearchEngineTheoremProducer::confAndrAF()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00711">CVC3::SearchEngineTheoremProducer::confAndrAT()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00834">CVC3::SearchEngineTheoremProducer::confIffr()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01059">CVC3::SearchEngineTheoremProducer::confIterIfThen()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01012">CVC3::SearchEngineTheoremProducer::confIterThenElse()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00221">CVC3::SearchEngineTheoremProducer::conflictClause()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01109">CVC3::SearchEngineTheoremProducer::conflictRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00561">CVC3::CommonTheoremProducer::contradictionRule()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00375">CVC3::SearchEngineTheoremProducer::cutRule()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01833">CVC3::ArithTheoremProducerOld::darkGrayShadow2ab()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01635">CVC3::ArithTheoremProducer3::darkGrayShadow2ab()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01678">CVC3::ArithTheoremProducer::darkGrayShadow2ab()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01926">CVC3::ArithTheoremProducerOld::darkGrayShadow2ba()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01726">CVC3::ArithTheoremProducer3::darkGrayShadow2ba()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01769">CVC3::ArithTheoremProducer::darkGrayShadow2ba()</a>, <a class="el" href="datatype__theorem__producer_8cpp_source.html#l00118">CVC3::DatatypeTheoremProducer::decompose()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02931">CVC3::ArithTheoremProducerOld::diseqToIneq()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02729">CVC3::ArithTheoremProducer3::diseqToIneq()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02754">CVC3::ArithTheoremProducer::diseqToIneq()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00454">CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02708">CVC3::ArithTheoremProducerOld::eqElimIntRule()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02506">CVC3::ArithTheoremProducer3::eqElimIntRule()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02531">CVC3::ArithTheoremProducer::eqElimIntRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01911">CVC3::BitvectorTheoremProducer::eqToBits()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02816">CVC3::ArithTheoremProducerOld::equalLeaves1()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02614">CVC3::ArithTheoremProducer3::equalLeaves1()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02639">CVC3::ArithTheoremProducer::equalLeaves1()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02845">CVC3::ArithTheoremProducerOld::equalLeaves2()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02643">CVC3::ArithTheoremProducer3::equalLeaves2()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02668">CVC3::ArithTheoremProducer::equalLeaves2()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02874">CVC3::ArithTheoremProducerOld::equalLeaves3()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02672">CVC3::ArithTheoremProducer3::equalLeaves3()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02697">CVC3::ArithTheoremProducer::equalLeaves3()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02903">CVC3::ArithTheoremProducerOld::equalLeaves4()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02701">CVC3::ArithTheoremProducer3::equalLeaves4()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02726">CVC3::ArithTheoremProducer::equalLeaves4()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02014">CVC3::ArithTheoremProducerOld::expandDarkShadow()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01811">CVC3::ArithTheoremProducer3::expandDarkShadow()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01854">CVC3::ArithTheoremProducer::expandDarkShadow()</a>, <a class="el" href="records__theorem__producer_8cpp_source.html#l00205">CVC3::RecordsTheoremProducer::expandEq()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02091">CVC3::ArithTheoremProducerOld::expandGrayShadow()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01889">CVC3::ArithTheoremProducer3::expandGrayShadow()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01931">CVC3::ArithTheoremProducer::expandGrayShadow()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02029">CVC3::ArithTheoremProducerOld::expandGrayShadow0()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01826">CVC3::ArithTheoremProducer3::expandGrayShadow0()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01869">CVC3::ArithTheoremProducer::expandGrayShadow0()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02122">CVC3::ArithTheoremProducerOld::expandGrayShadowConst()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01920">CVC3::ArithTheoremProducer3::expandGrayShadowConst()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01962">CVC3::ArithTheoremProducer::expandGrayShadowConst()</a>, <a class="el" href="records__theorem__producer_8cpp_source.html#l00158">CVC3::RecordsTheoremProducer::expandNeq()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04294">CVC3::BitvectorTheoremProducer::expandTypePred()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01769">CVC3::ArithTheoremProducerOld::finiteInterval()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01571">CVC3::ArithTheoremProducer3::finiteInterval()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01614">CVC3::ArithTheoremProducer::finiteInterval()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00258">generateSatProof()</a>, <a class="el" href="theorem_8h_source.html#l00370">CVC3::Theorem3::getProof()</a>, <a class="el" href="search__sat_8cpp_source.html#l01178">CVC3::SearchSat::getProof()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00282">CVC3::SearchImplBase::getProof()</a>, <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00049">CVC3::CNF_TheoremProducer::getSmartClauses()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02187">CVC3::ArithTheoremProducerOld::grayShadowConst()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01985">CVC3::ArithTheoremProducer3::grayShadowConst()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02027">CVC3::ArithTheoremProducer::grayShadowConst()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00641">CVC3::CommonTheoremProducer::iffContrapositive()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00626">CVC3::CommonTheoremProducer::iffFalseElim()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00667">CVC3::CommonTheoremProducer::iffMP()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00602">CVC3::CommonTheoremProducer::iffNotFalse()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01206">CVC3::SearchEngineTheoremProducer::iffToClauses()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00591">CVC3::CommonTheoremProducer::iffTrue()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00612">CVC3::CommonTheoremProducer::iffTrueElim()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00825">CVC3::CommonTheoremProducer::implContrapositive()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00775">CVC3::CommonTheoremProducer::implIntro()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00085">CVC3::CommonTheoremProducer::implIntro3()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00692">CVC3::CommonTheoremProducer::implMP()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01330">CVC3::ArithTheoremProducerOld::intEqIrrational()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01260">CVC3::ArithTheoremProducer3::intEqIrrational()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01273">CVC3::ArithTheoremProducer::intEqIrrational()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03332">CVC3::ArithTheoremProducerOld::intEqualityRationalConstant()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02297">CVC3::ArithTheoremProducerOld::intVarEqnConst()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02095">CVC3::ArithTheoremProducer3::intVarEqnConst()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02138">CVC3::ArithTheoremProducer::intVarEqnConst()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02682">CVC3::ArithTheoremProducerOld::IsIntegerElim()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02480">CVC3::ArithTheoremProducer3::IsIntegerElim()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02505">CVC3::ArithTheoremProducer::IsIntegerElim()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01186">CVC3::SearchEngineTheoremProducer::iteToClauses()</a>, <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00106">CVC3::CNF_TheoremProducer::learnedClauses()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02245">CVC3::ArithTheoremProducerOld::lessThanToLE()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02043">CVC3::ArithTheoremProducer3::lessThanToLE()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02085">CVC3::ArithTheoremProducer::lessThanToLE()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03416">CVC3::ArithTheoremProducerOld::lessThanToLERewrite()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l03103">CVC3::ArithTheoremProducer3::lessThanToLERewrite()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l03152">CVC3::ArithTheoremProducer::lessThanToLERewrite()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00105">CVC3::SearchEngineTheoremProducer::negIntro()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03697">CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00655">CVC3::CommonTheoremProducer::notNotElim()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00906">CVC3::CommonTheoremProducer::notToIff()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01226">CVC3::SearchEngineTheoremProducer::opCNFRule()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00568">CVC3::QuantTheoremProducer::packVar()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00408">CVC3::QuantTheoremProducer::partialUniversalInst()</a>, <a class="el" href="theorem_8cpp_source.html#l00580">print()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00074">CVC3::SearchEngineTheoremProducer::proofByContradiction()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00388">CVC3::ArrayTheoremProducer::propagateIndexDiseq()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00564">CVC3::SearchEngineTheoremProducer::propAndrAF()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00593">CVC3::SearchEngineTheoremProducer::propAndrAT()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00651">CVC3::SearchEngineTheoremProducer::propAndrLF()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00623">CVC3::SearchEngineTheoremProducer::propAndrLRT()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00681">CVC3::SearchEngineTheoremProducer::propAndrRF()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00782">CVC3::SearchEngineTheoremProducer::propIffr()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00923">CVC3::SearchEngineTheoremProducer::propIterIfThen()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00881">CVC3::SearchEngineTheoremProducer::propIterIte()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00970">CVC3::SearchEngineTheoremProducer::propIterThen()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00612">CVC3::QuantTheoremProducer::pullVarOut()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00055">CVC3::CommonTheoremProducer::queryTCC()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03253">CVC3::ArithTheoremProducerOld::rafineStrictInteger()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02970">CVC3::ArithTheoremProducer3::rafineStrictInteger()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l03068">CVC3::ArithTheoremProducer::rafineStrictInteger()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01702">CVC3::ArithTheoremProducerOld::realShadow()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01504">CVC3::ArithTheoremProducer3::realShadow()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01547">CVC3::ArithTheoremProducer::realShadow()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01737">CVC3::ArithTheoremProducerOld::realShadowEq()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01539">CVC3::ArithTheoremProducer3::realShadowEq()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01582">CVC3::ArithTheoremProducer::realShadowEq()</a>, <a class="el" href="uf__theorem__producer_8cpp_source.html#l00054">CVC3::UFTheoremProducer::relToClosure()</a>, <a class="el" href="uf__theorem__producer_8cpp_source.html#l00076">CVC3::UFTheoremProducer::relTrans()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00161">CVC3::CoreTheoremProducer::rewriteIteElse()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00136">CVC3::CoreTheoremProducer::rewriteIteThen()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00205">CVC3::ArrayTheoremProducer::rewriteRedundantWrite1()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01508">CVC3::ArithTheoremProducerOld::simpleIneqInt()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02054">CVC3::ArithTheoremProducerOld::splitGrayShadow()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01852">CVC3::ArithTheoremProducer3::splitGrayShadow()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01894">CVC3::ArithTheoremProducer::splitGrayShadow()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03456">CVC3::ArithTheoremProducerOld::splitGrayShadowSmall()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00302">CVC3::CommonTheoremProducer::substitutivityRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00187">CVC3::CommonTheoremProducer::symmetryRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00245">CVC3::CommonTheoremProducer::transitivityRule()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00511">CVC3::SearchEngineTheoremProducer::unitProp()</a>, and <a class="el" href="quant__theorem__producer_8cpp_source.html#l00154">CVC3::QuantTheoremProducer::universalInst()</a>.</p>
</div>
</div>
<a class="anchor" id="a112466d9793abcf97015233ffdc4ec5e"></a><!-- doxytag: member="CVC3::Theorem::getScope" ref="a112466d9793abcf97015233ffdc4ec5e" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CVC3::Theorem::getScope </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00486">486</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem__value_8h_source.html#l00164">CVC3::TheoremValue::getScope()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, <a class="el" href="theory__core_8cpp_source.html#l04213">CVC3::TheoryCore::enqueueFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>, <a class="el" href="theorem_8h_source.html#l00374">CVC3::Theorem3::getScope()</a>, <a class="el" href="theorem_8cpp_source.html#l00580">print()</a>, <a class="el" href="search__fast_8cpp_source.html#l00549">CVC3::SearchEngineFast::recordFact()</a>, <a class="el" href="theorem_8cpp_source.html#l00516">recursivePrint()</a>, <a class="el" href="variable_8h_source.html#l00153">CVC3::Literal::setValue()</a>, <a class="el" href="variable_8cpp_source.html#l00134">CVC3::Variable::setValue()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="a26b6f0af9e9b2f2a8c22a7dcb9fbb0b1"></a><!-- doxytag: member="CVC3::Theorem::getQuantLevel" ref="a26b6f0af9e9b2f2a8c22a7dcb9fbb0b1" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::Theorem::getQuantLevel </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Return quantification level for this theorem. </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00491">491</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem__value_8h_source.html#l00168">CVC3::TheoremValue::getQuantLevel()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, <a class="el" href="theorem_8h_source.html#l00133">thm()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
<p>Referenced by <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00049">CVC3::CNF_TheoremProducer::getSmartClauses()</a>, <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00106">CVC3::CNF_TheoremProducer::learnedClauses()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00408">CVC3::QuantTheoremProducer::partialUniversalInst()</a>, <a class="el" href="theory__core_8cpp_source.html#l04260">CVC3::TheoryCore::setupTerm()</a>, and <a class="el" href="quant__theorem__producer_8cpp_source.html#l00154">CVC3::QuantTheoremProducer::universalInst()</a>.</p>
</div>
</div>
<a class="anchor" id="abd3642f4230db7cd61aab78fdcc329e3"></a><!-- doxytag: member="CVC3::Theorem::getQuantLevelDebug" ref="abd3642f4230db7cd61aab78fdcc329e3" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::Theorem::getQuantLevelDebug </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00497">497</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem__value_8h_source.html#l00170">CVC3::TheoremValue::getQuantLevelDebug()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, <a class="el" href="theorem_8h_source.html#l00133">thm()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
</div>
</div>
<a class="anchor" id="ab3309c937f827595d1d92fa48cb5a471"></a><!-- doxytag: member="CVC3::Theorem::setQuantLevel" ref="ab3309c937f827595d1d92fa48cb5a471" args="(unsigned level)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::setQuantLevel </td>
<td>(</td>
<td class="paramtype">unsigned </td>
<td class="paramname"><em>level</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Set the quantification level for this theorem. </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00504">504</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, <a class="el" href="theorem__value_8h_source.html#l00175">CVC3::TheoremValue::setQuantLevel()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
<p>Referenced by <a class="el" href="search__sat_8cpp_source.html#l00193">CVC3::SearchSat::assertLit()</a>, <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00049">CVC3::CNF_TheoremProducer::getSmartClauses()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00170">CVC3::SearchImplBase::newIntAssumption()</a>, <a class="el" href="quant__theorem__producer_8cpp_source.html#l00408">CVC3::QuantTheoremProducer::partialUniversalInst()</a>, and <a class="el" href="quant__theorem__producer_8cpp_source.html#l00154">CVC3::QuantTheoremProducer::universalInst()</a>.</p>
</div>
</div>
<a class="anchor" id="abe268eaf2b89ffdc4ccb291c0a2eaeb9"></a><!-- doxytag: member="CVC3::Theorem::hash" ref="abe268eaf2b89ffdc4ccb291c0a2eaeb9" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">size_t CVC3::Theorem::hash </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00511">511</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="theorem_8h_source.html#l00091">d_thm</a>.</p>
<p>Referenced by <a class="el" href="theorem_8h_source.html#l00444">Hash::hash< CVC3::Theorem >::operator()()</a>.</p>
</div>
</div>
<a class="anchor" id="ac4b1c9570ffb9cc901627ef2abb9ff77"></a><!-- doxytag: member="CVC3::Theorem::toString" ref="ac4b1c9570ffb9cc901627ef2abb9ff77" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string CVC3::Theorem::toString </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00404">404</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01530">CVC3::SearchEngineFast::addLiteralFact()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00718">CVC3::CommonTheoremProducer::andElim()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00338">CVC3::ArrayTheoremProducer::arrayNotEq()</a>, <a class="el" href="theory__records_8cpp_source.html#l00129">CVC3::TheoryRecords::assertFact()</a>, <a class="el" href="theory__quant_8cpp_source.html#l03502">CVC3::TheoryQuant::assertFact()</a>, <a class="el" href="theory__core_8cpp_source.html#l00960">CVC3::TheoryCore::assertFact()</a>, <a class="el" href="theory__core_8cpp_source.html#l00385">CVC3::TheoryCore::assertFormula()</a>, <a class="el" href="theory__core_8cpp_source.html#l03734">CVC3::TheoryCore::assignValue()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00164">CVC3::TheoryBitvector::bitBlastDisEqn()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00225">CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00240">CVC3::TheoryBitvector::bitBlastIneqn()</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l00359">CVC3::TheoryBitvector::bitBlastTerm()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01575">CVC3::BitvectorTheoremProducer::bitExtractBitwise()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01337">CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00401">CVC3::TheoryArithOld::canonPred()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00279">CVC3::TheoryArithNew::canonPred()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00390">CVC3::TheoryArith3::canonPred()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00417">CVC3::TheoryArithOld::canonPredEquiv()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00295">CVC3::TheoryArithNew::canonPredEquiv()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00404">CVC3::TheoryArith3::canonPredEquiv()</a>, <a class="el" href="clause_8cpp_source.html#l00035">CVC3::ClauseValue::ClauseValue()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01109">CVC3::SearchEngineTheoremProducer::conflictRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00561">CVC3::CommonTheoremProducer::contradictionRule()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01833">CVC3::ArithTheoremProducerOld::darkGrayShadow2ab()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01635">CVC3::ArithTheoremProducer3::darkGrayShadow2ab()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01678">CVC3::ArithTheoremProducer::darkGrayShadow2ab()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01926">CVC3::ArithTheoremProducerOld::darkGrayShadow2ba()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01726">CVC3::ArithTheoremProducer3::darkGrayShadow2ba()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01769">CVC3::ArithTheoremProducer::darkGrayShadow2ba()</a>, <a class="el" href="variable_8cpp_source.html#l00162">CVC3::Variable::deriveThmRec()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00447">CVC3::TheoryArithOld::doSolve()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00331">CVC3::TheoryArithNew::doSolve()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00432">CVC3::TheoryArith3::doSolve()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, <a class="el" href="theory__core_8cpp_source.html#l04213">CVC3::TheoryCore::enqueueFact()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02708">CVC3::ArithTheoremProducerOld::eqElimIntRule()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02506">CVC3::ArithTheoremProducer3::eqElimIntRule()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02531">CVC3::ArithTheoremProducer::eqElimIntRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01911">CVC3::BitvectorTheoremProducer::eqToBits()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00762">CVC3::BitvectorTheoremProducer::generalIneqn()</a>, <a class="el" href="vcl_8cpp_source.html#l00354">CVC3::VCL::getAssumptionsRec()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00641">CVC3::CommonTheoremProducer::iffContrapositive()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00626">CVC3::CommonTheoremProducer::iffFalseElim()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00667">CVC3::CommonTheoremProducer::iffMP()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00612">CVC3::CommonTheoremProducer::iffTrueElim()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00692">CVC3::CommonTheoremProducer::implMP()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l01499">CVC3::TheoryArithOld::isolateVariable()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l01150">CVC3::TheoryArith3::isolateVariable()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00105">CVC3::SearchEngineTheoremProducer::negIntro()</a>, <a class="el" href="search__fast_8cpp_source.html#l01573">CVC3::SearchEngineFast::newIntAssumption()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08621">CVC3::TheoryQuant::notifyInconsistent()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00655">CVC3::CommonTheoremProducer::notNotElim()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00906">CVC3::CommonTheoremProducer::notToIff()</a>, <a class="el" href="theorem_8cpp_source.html#l00211">print()</a>, <a class="el" href="search__fast_8cpp_source.html#l01108">processNode()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00615">CVC3::TheoryArithOld::processRealEq()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00420">CVC3::TheoryArithNew::processRealEq()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00642">CVC3::TheoryArith3::processRealEq()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00317">CVC3::SearchImplBase::processResult()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00739">CVC3::TheoryArithOld::processSimpleIntEq()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00759">CVC3::TheoryArith3::processSimpleIntEq()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l01710">CVC3::TheoryArithOld::projectInequalities()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l01346">CVC3::TheoryArith3::projectInequalities()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00074">CVC3::SearchEngineTheoremProducer::proofByContradiction()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l04000">CVC3::TheoryArithNew::propagateTheory()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00225">CVC3::ExprTransform::pushNegationRec()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01702">CVC3::ArithTheoremProducerOld::realShadow()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01504">CVC3::ArithTheoremProducer3::realShadow()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01547">CVC3::ArithTheoremProducer::realShadow()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l01737">CVC3::ArithTheoremProducerOld::realShadowEq()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l01539">CVC3::ArithTheoremProducer3::realShadowEq()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l01582">CVC3::ArithTheoremProducer::realShadowEq()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08466">CVC3::TheoryQuant::recInstantiate()</a>, <a class="el" href="theory_8cpp_source.html#l00935">CVC3::Theory::renameExpr()</a>, <a class="el" href="theory__core_8cpp_source.html#l00257">CVC3::TheoryCore::rewriteCore()</a>, <a class="el" href="theory__core_8cpp_source.html#l04260">CVC3::TheoryCore::setupTerm()</a>, <a class="el" href="variable_8cpp_source.html#l00295">CVC3::VariableValue::setValue()</a>, and <a class="el" href="search__theorem__producer_8cpp_source.html#l00511">CVC3::SearchEngineTheoremProducer::unitProp()</a>.</p>
</div>
</div>
<a class="anchor" id="aeb41e125749338e05d680beca6df9ee4"></a><!-- doxytag: member="CVC3::Theorem::printx" ref="aeb41e125749338e05d680beca6df9ee4" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::printx </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00207">207</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="theorem_8cpp_source.html#l00230">getExpr()</a>, and <a class="el" href="expr_8cpp_source.html#l00362">CVC3::Expr::print()</a>.</p>
<p>Referenced by <a class="el" href="theorem_8h_source.html#l00384">CVC3::Theorem3::printx()</a>.</p>
</div>
</div>
<a class="anchor" id="a44f518efb0307d256450628cbc6085d2"></a><!-- doxytag: member="CVC3::Theorem::printxnodag" ref="a44f518efb0307d256450628cbc6085d2" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::printxnodag </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00208">208</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="theorem_8cpp_source.html#l00230">getExpr()</a>, and <a class="el" href="expr_8cpp_source.html#l00394">CVC3::Expr::printnodag()</a>.</p>
</div>
</div>
<a class="anchor" id="ab188a2869b745cb0d5f0e1f0d9081dfa"></a><!-- doxytag: member="CVC3::Theorem::pprintx" ref="ab188a2869b745cb0d5f0e1f0d9081dfa" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::pprintx </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00209">209</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="theorem_8cpp_source.html#l00230">getExpr()</a>, and <a class="el" href="expr_8cpp_source.html#l00373">CVC3::Expr::pprint()</a>.</p>
</div>
</div>
<a class="anchor" id="a2ccfcbaed17e735e3e008900d5a06e78"></a><!-- doxytag: member="CVC3::Theorem::pprintxnodag" ref="a2ccfcbaed17e735e3e008900d5a06e78" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::pprintxnodag </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00210">210</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="theorem_8cpp_source.html#l00230">getExpr()</a>, and <a class="el" href="expr_8cpp_source.html#l00383">CVC3::Expr::pprintnodag()</a>.</p>
</div>
</div>
<a class="anchor" id="af412e1fca4a31f24a63c948f85c18358"></a><!-- doxytag: member="CVC3::Theorem::print" ref="af412e1fca4a31f24a63c948f85c18358" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::print </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00211">211</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, and <a class="el" href="theorem_8h_source.html#l00404">toString()</a>.</p>
<p>Referenced by <a class="el" href="theorem_8h_source.html#l00385">CVC3::Theorem3::print()</a>.</p>
</div>
</div>
<a class="anchor" id="a1695c9afc9a5c1f8cd000d40b9e2a9cd"></a><!-- doxytag: member="CVC3::Theorem::isFlagged" ref="a1695c9afc9a5c1f8cd000d40b9e2a9cd" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem::isFlagged </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Check if the flag attribute is set. </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00416">416</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="expr__value_8h_source.html#l00132">CVC3::ExprValue::d_em</a>, <a class="el" href="theorem_8h_source.html#l00092">d_expr</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8h_source.html#l00132">exprValue()</a>, <a class="el" href="expr__manager_8h_source.html#l00331">CVC3::ExprManager::getTM()</a>, <a class="el" href="theorem__value_8h_source.html#l00125">CVC3::TheoremValue::isFlagged()</a>, <a class="el" href="theorem__manager_8h_source.html#l00100">CVC3::TheoremManager::isFlagged()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
<p>Referenced by <a class="el" href="search__theorem__producer_8cpp_source.html#l00429">CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08653">CVC3::TheoryQuant::findInstAssumptions()</a>, <a class="el" href="theorem_8cpp_source.html#l00320">getAssumptionsAndCongRec()</a>, <a class="el" href="vcl_8cpp_source.html#l00354">CVC3::VCL::getAssumptionsRec()</a>, <a class="el" href="theorem_8cpp_source.html#l00259">getAssumptionsRec()</a>, <a class="el" href="theorem_8cpp_source.html#l00309">GetSatAssumptions()</a>, <a class="el" href="theorem_8cpp_source.html#l00288">GetSatAssumptionsRec()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01108">processNode()</a>.</p>
</div>
</div>
<a class="anchor" id="a621ab2150eedc0e3b38d34275ac206cd"></a><!-- doxytag: member="CVC3::Theorem::clearAllFlags" ref="a621ab2150eedc0e3b38d34275ac206cd" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::clearAllFlags </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Clear the flag attribute in all the theorems. </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00422">422</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00129">CVC3::TheoremValue::clearAllFlags()</a>, <a class="el" href="theorem__manager_8h_source.html#l00086">CVC3::TheoremManager::clearAllFlags()</a>, <a class="el" href="expr__value_8h_source.html#l00132">CVC3::ExprValue::d_em</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8h_source.html#l00132">exprValue()</a>, <a class="el" href="expr__manager_8h_source.html#l00331">CVC3::ExprManager::getTM()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00221">CVC3::SearchEngineTheoremProducer::conflictClause()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00454">CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms()</a>, <a class="el" href="theorem_8cpp_source.html#l00370">getAssumptionsAndCong()</a>, <a class="el" href="theorem_8cpp_source.html#l00274">getLeafAssumptions()</a>, <a class="el" href="cnf__theorem__producer_8cpp_source.html#l00049">CVC3::CNF_TheoremProducer::getSmartClauses()</a>, <a class="el" href="assumptions_8cpp_source.html#l00263">CVC3::Assumptions::operator[]()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="af83d6b4d71bfb558296a1c296a69c3d7"></a><!-- doxytag: member="CVC3::Theorem::setFlag" ref="af83d6b4d71bfb558296a1c296a69c3d7" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::setFlag </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Set the flag attribute. </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00429">429</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="expr__value_8h_source.html#l00132">CVC3::ExprValue::d_em</a>, <a class="el" href="theorem_8h_source.html#l00092">d_expr</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8h_source.html#l00132">exprValue()</a>, <a class="el" href="expr__manager_8h_source.html#l00331">CVC3::ExprManager::getTM()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, <a class="el" href="theorem__value_8h_source.html#l00133">CVC3::TheoremValue::setFlag()</a>, <a class="el" href="theorem__manager_8h_source.html#l00099">CVC3::TheoremManager::setFlag()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
<p>Referenced by <a class="el" href="search__theorem__producer_8cpp_source.html#l00429">CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08653">CVC3::TheoryQuant::findInstAssumptions()</a>, <a class="el" href="assumptions_8cpp_source.html#l00034">CVC3::Assumptions::findTheorem()</a>, <a class="el" href="theorem_8cpp_source.html#l00320">getAssumptionsAndCongRec()</a>, <a class="el" href="vcl_8cpp_source.html#l00354">CVC3::VCL::getAssumptionsRec()</a>, <a class="el" href="theorem_8cpp_source.html#l00259">getAssumptionsRec()</a>, <a class="el" href="theorem_8cpp_source.html#l00309">GetSatAssumptions()</a>, <a class="el" href="theorem_8cpp_source.html#l00288">GetSatAssumptionsRec()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01108">processNode()</a>.</p>
</div>
</div>
<a class="anchor" id="a979f97355a4ecd2d8d8b96b679df5240"></a><!-- doxytag: member="CVC3::Theorem::setSubst" ref="a979f97355a4ecd2d8d8b96b679df5240" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::setSubst </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Set flag stating that theorem is an instance of substitution. </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00447">447</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, <a class="el" href="theorem__value_8h_source.html#l00145">CVC3::TheoremValue::setSubst()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l00302">CVC3::CommonTheoremProducer::substitutivityRule()</a>.</p>
</div>
</div>
<a class="anchor" id="ad413df893f7cc81cd2e0a59178b981db"></a><!-- doxytag: member="CVC3::Theorem::isSubst" ref="ad413df893f7cc81cd2e0a59178b981db" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem::isSubst </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Is theorem an instance of substitution. </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00452">452</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, <a class="el" href="theorem__value_8h_source.html#l00146">CVC3::TheoremValue::isSubst()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00320">getAssumptionsAndCongRec()</a>, and <a class="el" href="theorem_8cpp_source.html#l00516">recursivePrint()</a>.</p>
</div>
</div>
<a class="anchor" id="a30644e9241516daa6483f5d9c0be4caf"></a><!-- doxytag: member="CVC3::Theorem::setExpandFlag" ref="a30644e9241516daa6483f5d9c0be4caf" args="(bool val) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::setExpandFlag </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>val</em></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Set the "expand" attribute. </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00458">458</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="expr__value_8h_source.html#l00132">CVC3::ExprValue::d_em</a>, <a class="el" href="theorem_8h_source.html#l00092">d_expr</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8h_source.html#l00132">exprValue()</a>, <a class="el" href="expr__manager_8h_source.html#l00331">CVC3::ExprManager::getTM()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, <a class="el" href="theorem__value_8h_source.html#l00148">CVC3::TheoremValue::setExpandFlag()</a>, <a class="el" href="theorem__manager_8h_source.html#l00107">CVC3::TheoremManager::setExpandFlag()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="a2eefa550b2e04a012adc03ba456af38b"></a><!-- doxytag: member="CVC3::Theorem::getExpandFlag" ref="a2eefa550b2e04a012adc03ba456af38b" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem::getExpandFlag </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Check the "expand" attribute. </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00464">464</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="expr__value_8h_source.html#l00132">CVC3::ExprValue::d_em</a>, <a class="el" href="theorem_8h_source.html#l00092">d_expr</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8h_source.html#l00132">exprValue()</a>, <a class="el" href="theorem__value_8h_source.html#l00152">CVC3::TheoremValue::getExpandFlag()</a>, <a class="el" href="theorem__manager_8h_source.html#l00108">CVC3::TheoremManager::getExpandFlag()</a>, <a class="el" href="expr__manager_8h_source.html#l00331">CVC3::ExprManager::getTM()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01108">processNode()</a>.</p>
</div>
</div>
<a class="anchor" id="a575a8519a298b25db8b728f4c273972c"></a><!-- doxytag: member="CVC3::Theorem::setLitFlag" ref="a575a8519a298b25db8b728f4c273972c" args="(bool val) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::setLitFlag </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>val</em></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Set the "literal" attribute. </p>
<p>The expression of this theorem will be added as a conflict clause literal </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00470">470</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="expr__value_8h_source.html#l00132">CVC3::ExprValue::d_em</a>, <a class="el" href="theorem_8h_source.html#l00092">d_expr</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8h_source.html#l00132">exprValue()</a>, <a class="el" href="expr__manager_8h_source.html#l00331">CVC3::ExprManager::getTM()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, <a class="el" href="theorem__value_8h_source.html#l00156">CVC3::TheoremValue::setLitFlag()</a>, <a class="el" href="theorem__manager_8h_source.html#l00113">CVC3::TheoremManager::setLitFlag()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
</div>
</div>
<a class="anchor" id="a8442e9bc88086d84648ccea5b373cdb0"></a><!-- doxytag: member="CVC3::Theorem::getLitFlag" ref="a8442e9bc88086d84648ccea5b373cdb0" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem::getLitFlag </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Check the "literal" attribute. </p>
<p>The expression of this theorem will be added as a conflict clause literal </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00476">476</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="expr__value_8h_source.html#l00132">CVC3::ExprValue::d_em</a>, <a class="el" href="theorem_8h_source.html#l00092">d_expr</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8h_source.html#l00132">exprValue()</a>, <a class="el" href="theorem__value_8h_source.html#l00160">CVC3::TheoremValue::getLitFlag()</a>, <a class="el" href="theorem__manager_8h_source.html#l00114">CVC3::TheoremManager::getLitFlag()</a>, <a class="el" href="expr__manager_8h_source.html#l00331">CVC3::ExprManager::getTM()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01108">processNode()</a>.</p>
</div>
</div>
<a class="anchor" id="aed1590a02166f6099e5538dbf681a60c"></a><!-- doxytag: member="CVC3::Theorem::isAbsLiteral" ref="aed1590a02166f6099e5538dbf681a60c" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem::isAbsLiteral </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Check if the theorem is a literal. </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00482">482</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="theorem_8cpp_source.html#l00230">getExpr()</a>, and <a class="el" href="expr_8h_source.html#l00406">CVC3::Expr::isAbsLiteral()</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00218">CVC3::SearchImplBase::addCNFFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l01530">CVC3::SearchEngineFast::addLiteralFact()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, <a class="el" href="search__fast_8cpp_source.html#l01031">CVC3::SearchEngineFast::enqueueFact()</a>, <a class="el" href="theorem_8h_source.html#l00388">CVC3::Theorem3::isAbsLiteral()</a>, <a class="el" href="search__fast_8cpp_source.html#l01108">processNode()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00915">CVC3::SearchEngineFast::unitPropagation()</a>.</p>
</div>
</div>
<a class="anchor" id="a657f0037f907743988443bffdf2e505c"></a><!-- doxytag: member="CVC3::Theorem::refutes" ref="a657f0037f907743988443bffdf2e505c" args="(const Expr &e) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem::refutes </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Check if the flag attribute is set. </p>
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00252">252</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>.</p>
<p>Referenced by <a class="el" href="search__theorem__producer_8cpp_source.html#l00744">CVC3::SearchEngineTheoremProducer::confAndrAF()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00711">CVC3::SearchEngineTheoremProducer::confAndrAT()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00834">CVC3::SearchEngineTheoremProducer::confIffr()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01059">CVC3::SearchEngineTheoremProducer::confIterIfThen()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01012">CVC3::SearchEngineTheoremProducer::confIterThenElse()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00564">CVC3::SearchEngineTheoremProducer::propAndrAF()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00651">CVC3::SearchEngineTheoremProducer::propAndrLF()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00681">CVC3::SearchEngineTheoremProducer::propAndrRF()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00782">CVC3::SearchEngineTheoremProducer::propIffr()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00923">CVC3::SearchEngineTheoremProducer::propIterIfThen()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00881">CVC3::SearchEngineTheoremProducer::propIterIte()</a>, and <a class="el" href="search__theorem__producer_8cpp_source.html#l00970">CVC3::SearchEngineTheoremProducer::propIterThen()</a>.</p>
</div>
</div>
<a class="anchor" id="afd8511ead1dfc424a75089f4b4afb95d"></a><!-- doxytag: member="CVC3::Theorem::proves" ref="afd8511ead1dfc424a75089f4b4afb95d" args="(const Expr &e) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem::proves </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Check if the flag attribute is set. </p>
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00259">259</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>Referenced by <a class="el" href="search__theorem__producer_8cpp_source.html#l00744">CVC3::SearchEngineTheoremProducer::confAndrAF()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00711">CVC3::SearchEngineTheoremProducer::confAndrAT()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00834">CVC3::SearchEngineTheoremProducer::confIffr()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01059">CVC3::SearchEngineTheoremProducer::confIterIfThen()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01012">CVC3::SearchEngineTheoremProducer::confIterThenElse()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00593">CVC3::SearchEngineTheoremProducer::propAndrAT()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00651">CVC3::SearchEngineTheoremProducer::propAndrLF()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00623">CVC3::SearchEngineTheoremProducer::propAndrLRT()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00681">CVC3::SearchEngineTheoremProducer::propAndrRF()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00782">CVC3::SearchEngineTheoremProducer::propIffr()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00923">CVC3::SearchEngineTheoremProducer::propIterIfThen()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00881">CVC3::SearchEngineTheoremProducer::propIterIte()</a>, and <a class="el" href="search__theorem__producer_8cpp_source.html#l00970">CVC3::SearchEngineTheoremProducer::propIterThen()</a>.</p>
</div>
</div>
<a class="anchor" id="a1d50e47a6c0a1dc6ac9328c5b8e63d1c"></a><!-- doxytag: member="CVC3::Theorem::matches" ref="a1d50e47a6c0a1dc6ac9328c5b8e63d1c" args="(const Expr &e) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem::matches </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Check if the flag attribute is set. </p>
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00264">264</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
</div>
</div>
<a class="anchor" id="a293ebbc3162763fbbeaa9fbd8ea1c657"></a><!-- doxytag: member="CVC3::Theorem::setCachedValue" ref="a293ebbc3162763fbbeaa9fbd8ea1c657" args="(int value) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem::setCachedValue </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>value</em></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Check if the flag attribute is set. </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00435">435</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="expr__value_8h_source.html#l00132">CVC3::ExprValue::d_em</a>, <a class="el" href="theorem_8h_source.html#l00092">d_expr</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8h_source.html#l00132">exprValue()</a>, <a class="el" href="expr__manager_8h_source.html#l00331">CVC3::ExprManager::getTM()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, <a class="el" href="theorem__value_8h_source.html#l00137">CVC3::TheoremValue::setCachedValue()</a>, <a class="el" href="theorem__manager_8h_source.html#l00101">CVC3::TheoremManager::setCachedValue()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01108">processNode()</a>, <a class="el" href="theorem_8cpp_source.html#l00516">recursivePrint()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="a0062fd610006e5bc0b4093ae72943342"></a><!-- doxytag: member="CVC3::Theorem::getCachedValue" ref="a0062fd610006e5bc0b4093ae72943342" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CVC3::Theorem::getCachedValue </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Check if the flag attribute is set. </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00441">441</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="expr__value_8h_source.html#l00132">CVC3::ExprValue::d_em</a>, <a class="el" href="theorem_8h_source.html#l00092">d_expr</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8h_source.html#l00132">exprValue()</a>, <a class="el" href="theorem__value_8h_source.html#l00141">CVC3::TheoremValue::getCachedValue()</a>, <a class="el" href="theorem__manager_8h_source.html#l00102">CVC3::TheoremManager::getCachedValue()</a>, <a class="el" href="expr__manager_8h_source.html#l00331">CVC3::ExprManager::getTM()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, and <a class="el" href="theorem_8h_source.html#l00133">thm()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01108">processNode()</a>, and <a class="el" href="theorem_8cpp_source.html#l00516">recursivePrint()</a>.</p>
</div>
</div>
<a class="anchor" id="a6ead218343fdbf3e92c26d8c76b9d399"></a><!-- doxytag: member="CVC3::Theorem::print" ref="a6ead218343fdbf3e92c26d8c76b9d399" args="(std::ostream &os, const std::string &name) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">ostream & CVC3::Theorem::print </td>
<td>(</td>
<td class="paramtype">std::ostream & </td>
<td class="paramname"><em>os</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>name</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Printing a theorem to a stream, calling it "name". </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00580">580</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
<p>References <a class="el" href="theorem__value_8h_source.html#l00074">CVC3::TheoremValue::d_refcount</a>, <a class="el" href="theorem_8cpp_source.html#l00385">getAssumptionsRef()</a>, <a class="el" href="expr_8h_source.html#l01156">CVC3::Expr::getEM()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">getProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00486">getScope()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00345">CVC3::ExprManager::incIndent()</a>, <a class="el" href="expr__manager_8h_source.html#l00354">CVC3::ExprManager::indent()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00184">CVC3::ExprManager::isActive()</a>, <a class="el" href="theorem_8cpp_source.html#l00395">isAssump()</a>, <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00171">isRefl()</a>, <a class="el" href="theorem_8h_source.html#l00133">thm()</a>, <a class="el" href="theorem_8cpp_source.html#l00219">withAssumptions()</a>, and <a class="el" href="theorem_8cpp_source.html#l00214">withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="aaf9a1a9a97d765b069eac3d3460545be"></a><!-- doxytag: member="CVC3::Theorem::TheoremEq" ref="aaf9a1a9a97d765b069eac3d3460545be" args="(const Theorem &t1, const Theorem &t2)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">static bool CVC3::Theorem::TheoremEq </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>t1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>t2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline, static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00281">281</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="theorem_8h_source.html#l00164">isNull()</a>.</p>
</div>
</div>
<hr/><h2>Friends And Related Function Documentation</h2>
<a class="anchor" id="adb16a6e6bad96912c4150299576eaf9a"></a><!-- doxytag: member="CVC3::Theorem::TheoremProducer" ref="adb16a6e6bad96912c4150299576eaf9a" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1TheoremProducer.html">TheoremProducer</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00080">80</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
</div>
</div>
<a class="anchor" id="acc3b40272a636c6365e02a387cfc4c82"></a><!-- doxytag: member="CVC3::Theorem::Theorem3" ref="acc3b40272a636c6365e02a387cfc4c82" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1Theorem3.html">Theorem3</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00082">82</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
</div>
</div>
<a class="anchor" id="a2fc7fcb35dcb6d97f101ffb632ac1dcd"></a><!-- doxytag: member="CVC3::Theorem::RegTheoremValue" ref="a2fc7fcb35dcb6d97f101ffb632ac1dcd" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1RegTheoremValue.html">RegTheoremValue</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00084">84</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
</div>
</div>
<a class="anchor" id="add1e5fec863ffafbd22cac7aa0d1b689"></a><!-- doxytag: member="CVC3::Theorem::RWTheoremValue" ref="add1e5fec863ffafbd22cac7aa0d1b689" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1RWTheoremValue.html">RWTheoremValue</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00085">85</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
</div>
</div>
<a class="anchor" id="a4b6ae0abb7c60306b856e52d64c774c0"></a><!-- doxytag: member="CVC3::Theorem::compare" ref="a4b6ae0abb7c60306b856e52d64c774c0" args="(const Theorem &t1, const Theorem &t2)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int compare </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>t1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>t2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Compare Theorems by their expressions. Return -1, 0, or 1. </p>
<p>This is an arbitrary total ordering on Theorems. For simplicity, we define rewrite theorems (e1 = e2 or e1 <=> e2) to be smaller than other theorems. </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00045">45</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="ab15840d10f28308594233c883b5662bb"></a><!-- doxytag: member="CVC3::Theorem::compare" ref="ab15840d10f28308594233c883b5662bb" args="(const Theorem &t1, const Expr &e2)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int compare </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>t1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Compare a <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> with an <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> (as if <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> is a <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>) </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00065">65</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="ad1783549762b1401c0ec14c39099196d"></a><!-- doxytag: member="CVC3::Theorem::compareByPtr" ref="ad1783549762b1401c0ec14c39099196d" args="(const Theorem &t1, const Theorem &t2)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int compareByPtr </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>t1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>t2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Compare Theorems by <a class="el" href="classCVC3_1_1TheoremValue.html">TheoremValue</a> pointers. Return -1, 0, or 1. </p>
<p>Definition at line <a class="el" href="theorem_8cpp_source.html#l00083">83</a> of file <a class="el" href="theorem_8cpp_source.html">theorem.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a6f08e5df7b32fccb7bba2e689518569e"></a><!-- doxytag: member="CVC3::Theorem::operator==" ref="a6f08e5df7b32fccb7bba2e689518569e" args="(const Theorem &t1, const Theorem &t2)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool operator== </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>t1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>t2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Equality is w.r.t. <a class="el" href="classCVC3_1_1Theorem.html#a4b6ae0abb7c60306b856e52d64c774c0" title="Compare Theorems by their expressions. Return -1, 0, or 1.">compare()</a> </p>
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00102">102</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
</div>
</div>
<a class="anchor" id="acf65eea626a36c24c83abcee026ec205"></a><!-- doxytag: member="CVC3::Theorem::operator!=" ref="acf65eea626a36c24c83abcee026ec205" args="(const Theorem &t1, const Theorem &t2)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool operator!= </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>t1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>t2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Disequality is w.r.t. <a class="el" href="classCVC3_1_1Theorem.html#a4b6ae0abb7c60306b856e52d64c774c0" title="Compare Theorems by their expressions. Return -1, 0, or 1.">compare()</a> </p>
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00105">105</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
</div>
</div>
<a class="anchor" id="afde7ac3dde23e989a6df667b6836ecfa"></a><!-- doxytag: member="CVC3::Theorem::operator<<" ref="afde7ac3dde23e989a6df667b6836ecfa" args="(std::ostream &os, const Theorem &t)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::ostream& operator<< </td>
<td>(</td>
<td class="paramtype">std::ostream & </td>
<td class="paramname"><em>os</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>t</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00277">277</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="a696e2281069af317ec3fb6510845ca6c"></a><!-- doxytag: member="CVC3::Theorem::d_thm" ref="a696e2281069af317ec3fb6510845ca6c" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">intptr_t <a class="el" href="classCVC3_1_1Theorem.html#a696e2281069af317ec3fb6510845ca6c">CVC3::Theorem::d_thm</a></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00091">91</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00045">CVC3::compare()</a>, <a class="el" href="theorem_8cpp_source.html#l00083">CVC3::compareByPtr()</a>, <a class="el" href="theorem_8cpp_source.html#l00511">hash()</a>, <a class="el" href="theorem_8cpp_source.html#l00091">operator=()</a>, <a class="el" href="theorem_8cpp_source.html#l00170">Theorem()</a>, and <a class="el" href="theorem_8cpp_source.html#l00188">~Theorem()</a>.</p>
</div>
</div>
<a class="anchor" id="a798f8085ec077b69aae198a155077774"></a><!-- doxytag: member="CVC3::Theorem::d_expr" ref="a798f8085ec077b69aae198a155077774" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprValue.html">ExprValue</a>* <a class="el" href="classCVC3_1_1Theorem.html#a798f8085ec077b69aae198a155077774">CVC3::Theorem::d_expr</a></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00092">92</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00441">getCachedValue()</a>, <a class="el" href="theorem_8cpp_source.html#l00464">getExpandFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">getLHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00476">getLitFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">getRHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00416">isFlagged()</a>, <a class="el" href="theorem_8cpp_source.html#l00435">setCachedValue()</a>, <a class="el" href="theorem_8cpp_source.html#l00458">setExpandFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00429">setFlag()</a>, <a class="el" href="theorem_8cpp_source.html#l00470">setLitFlag()</a>, and <a class="el" href="theorem_8cpp_source.html#l00182">Theorem()</a>.</p>
</div>
</div>
<a class="anchor" id="ad18bcb483567d152757b4412793be53d"></a><!-- doxytag: member="CVC3::Theorem::@2" ref="ad18bcb483567d152757b4412793be53d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">union { ... } <code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="theorem_8h_source.html">theorem.h</a></li>
<li><a class="el" href="theorem_8cpp_source.html">theorem.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>
