<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: Member List</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="inherits.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a></li><li class="navelem"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">CVC3::Theorem Member List</div> </div>
</div><!--header-->
<div class="contents">
<p>This is the complete list of members for <a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a>, including all inherited members.</p>
<table class="directory">
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a621ab2150eedc0e3b38d34275ac206cd">clearAllFlags</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a4b6ae0abb7c60306b856e52d64c774c0">compare</a>(const Theorem &t1, const Theorem &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#ab15840d10f28308594233c883b5662bb">compare</a>(const Theorem &t1, const Expr &e2)</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#ad1783549762b1401c0ec14c39099196d">compareByPtr</a>(const Theorem &t1, const Theorem &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a798f8085ec077b69aae198a155077774">d_expr</a></td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a696e2281069af317ec3fb6510845ca6c">d_thm</a></td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a67e2a295b1598057cfbb51120a0c1ad6">exprValue</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a69c948a7ecc79597eac8eb816e8d76a1">getAssumptionsAndCong</a>(std::vector< Expr > &assumptions, std::vector< Expr > &congruences, bool negate=false) const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a0c8eec45e649b4608ba1c88ca5f2e617">getAssumptionsAndCongRec</a>(std::set< Expr > &assumptions, std::vector< Expr > &congruences) const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#ab3e8c740e4da0bd7ae74754ef25af049">getAssumptionsRec</a>(std::set< Expr > &assumptions) const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a0062fd610006e5bc0b4093ae72943342">getCachedValue</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a2eefa550b2e04a012adc03ba456af38b">getExpandFlag</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a524b4dafa4fb8f14742baa856612d92b">getLeafAssumptions</a>(std::vector< Expr > &assumptions, bool negate=false) const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a206c04f39fbbcacef2337148675553f4">getLHS</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a8442e9bc88086d84648ccea5b373cdb0">getLitFlag</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a26b6f0af9e9b2f2a8c22a7dcb9fbb0b1">getQuantLevel</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#abd3642f4230db7cd61aab78fdcc329e3">getQuantLevelDebug</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#aad446d2963572258f7b8f0c74fb9e299">GetSatAssumptions</a>(std::vector< Theorem > &assumptions) const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#adf7fd8a76fe1052914bc88ed3a303660">GetSatAssumptionsRec</a>(std::vector< Theorem > &assumptions) const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a112466d9793abcf97015233ffdc4ec5e">getScope</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#abe268eaf2b89ffdc4ccb291c0a2eaeb9">hash</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#aed1590a02166f6099e5538dbf681a60c">isAbsLiteral</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a05282db6832afb4f198d8c6b2b67aeb1">isAssump</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a1695c9afc9a5c1f8cd000d40b9e2a9cd">isFlagged</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#afc6fdb0507eb3669e28d9be5ed0bd333">isNull</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a16f074e60b9e076187efb478889d2c47">isRefl</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a362c1d70e03803d804bbe300e5f6dc87">isRewrite</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#ad413df893f7cc81cd2e0a59178b981db">isSubst</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a1d50e47a6c0a1dc6ac9328c5b8e63d1c">matches</a>(const Expr &e) const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#acf65eea626a36c24c83abcee026ec205">operator!=</a>(const Theorem &t1, const Theorem &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#afde7ac3dde23e989a6df667b6836ecfa">operator<<</a>(std::ostream &os, const Theorem &t)</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#adacab84dc4dc38aeb12ddabcb3c4a51d">operator=</a>(const Theorem &th)</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a6f08e5df7b32fccb7bba2e689518569e">operator==</a>(const Theorem &t1, const Theorem &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#ab188a2869b745cb0d5f0e1f0d9081dfa">pprintx</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a2ccfcbaed17e735e3e008900d5a06e78">pprintxnodag</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#af412e1fca4a31f24a63c948f85c18358">print</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a6ead218343fdbf3e92c26d8c76b9d399">print</a>(std::ostream &os, const std::string &name) const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#ad9da69b34ab2bab4192e5977e5c10498">printDebug</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#aeb41e125749338e05d680beca6df9ee4">printx</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a44f518efb0307d256450628cbc6085d2">printxnodag</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d">proves</a>(const Expr &e) const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a472f420688e07c506969a4ed6b9a110e">recursivePrint</a>(int &i) const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c">refutes</a>(const Expr &e) const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a2fc7fcb35dcb6d97f101ffb632ac1dcd">RegTheoremValue</a> class</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#add1e5fec863ffafbd22cac7aa0d1b689">RWTheoremValue</a> class</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a293ebbc3162763fbbeaa9fbd8ea1c657">setCachedValue</a>(int value) const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a30644e9241516daa6483f5d9c0be4caf">setExpandFlag</a>(bool val) const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#af83d6b4d71bfb558296a1c296a69c3d7">setFlag</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a575a8519a298b25db8b728f4c273972c">setLitFlag</a>(bool val) const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#ab3309c937f827595d1d92fa48cb5a471">setQuantLevel</a>(unsigned level)</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a979f97355a4ecd2d8d8b96b679df5240">setSubst</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a2fefec275dfdf6d8932c6f74b03bec4d">Theorem</a>(TheoremValue *thm)</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#ae7e657235650f951a2e61affb3a55ef2">Theorem</a>(TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump=false, int scope=-1)</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a1e1b1005316fefef5d78a7c4d3ae6060">Theorem</a>(TheoremManager *tm, const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf, bool isAssump=false, int scope=-1)</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#ab27afa1904c73f44a38dae8945749a6a">Theorem</a>(const Expr &e)</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a4b7574a16eed728fac6e37d2404fdbf8">Theorem</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a43974f559b8faa8db89d81993e911881">Theorem</a>(const Theorem &th)</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#acc3b40272a636c6365e02a387cfc4c82">Theorem3</a> class</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#aaf9a1a9a97d765b069eac3d3460545be">TheoremEq</a>(const Theorem &t1, const Theorem &t2)</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">static</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#adb16a6e6bad96912c4150299576eaf9a">TheoremProducer</a> class</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">friend</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a12de358e2b6cb67415f508ceca6913d1">thm</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">private</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#ac4b1c9570ffb9cc901627ef2abb9ff77">toString</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#a90349125fe644e8a075e1a47a49872c7">withAssumptions</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#ad4573ca6be017cab3c83d28c2dbcebd8">withProof</a>() const </td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html#ad72ac2b7be75f1b2848e9d6199c01c83">~Theorem</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a></td><td class="entry"></td></tr>
</table></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:18 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
