<!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::Theorem3 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_1Theorem3.html">Theorem3</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#pub-methods">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::Theorem3 Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::Theorem3" -->
<p><a class="el" href="classCVC3_1_1Theorem3.html" title="Theorem3.">Theorem3</a>.
<a href="classCVC3_1_1Theorem3.html#details">More...</a></p>
<p><code>#include <<a class="el" href="theorem_8h_source.html">theorem.h</a>></code></p>
<p><a href="classCVC3_1_1Theorem3-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_1Theorem3.html#ab7984ea5eb9c9bdba751fc9ea9d6cc90">printDebug</a> () const
<li><a class="el" href="classCVC3_1_1Theorem3.html#ae64084287342d9fa9374a4db1981bbd5">Theorem3</a> ()
<li>virtual <a class="el" href="classCVC3_1_1Theorem3.html#a55e28790faec403ea8a9a0b5a718eab1">~Theorem3</a> ()
<li>bool <a class="el" href="classCVC3_1_1Theorem3.html#a1f2b0509853067114494079f955de741">isNull</a> () const
<li>bool <a class="el" href="classCVC3_1_1Theorem3.html#ace6f5dda051da7db8a4adf74a723852c">isRewrite</a> () const
<li>bool <a class="el" href="classCVC3_1_1Theorem3.html#aba6e80e63438ef74f027476ca085781a">isAssump</a> () const
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1Theorem3.html#a744788782cc996d5b914533fe7304352">getExpr</a> () const
<li>const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="classCVC3_1_1Theorem3.html#a86b1b2342e05df0b6c965df22ac6bdc5">getLHS</a> () const
<li>const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & <a class="el" href="classCVC3_1_1Theorem3.html#a1da681e13e1dd2bfefb0d21027e20eb6">getRHS</a> () const
<li>const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & <a class="el" href="classCVC3_1_1Theorem3.html#a3bf0a31a2adaabfd7a37d61e990fa9ea">getAssumptionsRef</a> () const
<li><a class="el" href="classCVC3_1_1Proof.html">Proof</a> <a class="el" href="classCVC3_1_1Theorem3.html#a05c74972ebc3932829fa32ca237880db">getProof</a> () const
<li>int <a class="el" href="classCVC3_1_1Theorem3.html#a153b7d792f901a481d1eb4c91c885330">getScope</a> () const
<li>bool <a class="el" href="classCVC3_1_1Theorem3.html#a099ac3dc23ce274b26a25cd9e5059502">withProof</a> () const
<li>bool <a class="el" href="classCVC3_1_1Theorem3.html#a49abf6d71c6190f1400b5146b61b0872">withAssumptions</a> () const
<li>std::string <a class="el" href="classCVC3_1_1Theorem3.html#a3712f50eb83d3b485aab55f660bed77a">toString</a> () const
<li>void <a class="el" href="classCVC3_1_1Theorem3.html#a4a2253b9fa2508aedd3dded623e283ad">printx</a> () const
<li>void <a class="el" href="classCVC3_1_1Theorem3.html#ababd51a0131a57f96c0316f7f8f2a6c9">print</a> () const
<li>bool <a class="el" href="classCVC3_1_1Theorem3.html#a31be5df9f946e3a6f2a75f673db863cb">isAbsLiteral</a> () const
<dl class="el"><dd class="mdescRight">Check if the theorem is a literal. <a href="#a31be5df9f946e3a6f2a75f673db863cb"></a><br/></dl></ul>
<h2><a name="pri-methods"></a>
Private Member Functions</h2>
<ul>
<li><a class="el" href="classCVC3_1_1Theorem3.html#a1986607c85de1a0550ebe7759bf5b6a4">Theorem3</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)
<li><a class="el" href="classCVC3_1_1Theorem3.html#a5495a662364c65492dceb1108a45d55c">Theorem3</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)
</ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">d_thm</a>
</ul>
<h2><a name="friends"></a>
Friends</h2>
<ul>
<li>class <a class="el" href="classCVC3_1_1Theorem3.html#adb16a6e6bad96912c4150299576eaf9a">TheoremProducer</a>
<li>bool <a class="el" href="classCVC3_1_1Theorem3.html#a1d12c9cc45e21f2bef8b4065f23b1ecd">operator==</a> (const <a class="el" href="classCVC3_1_1Theorem3.html">Theorem3</a> &t1, const <a class="el" href="classCVC3_1_1Theorem3.html">Theorem3</a> &t2)
<li>bool <a class="el" href="classCVC3_1_1Theorem3.html#a08914251eb8cbf0ced80d277a07b6827">operator!=</a> (const <a class="el" href="classCVC3_1_1Theorem3.html">Theorem3</a> &t1, const <a class="el" href="classCVC3_1_1Theorem3.html">Theorem3</a> &t2)
<li>std::ostream & <a class="el" href="classCVC3_1_1Theorem3.html#af5109554e84f3a7b92eea93606cbc7bc">operator<<</a> (std::ostream &os, const <a class="el" href="classCVC3_1_1Theorem3.html">Theorem3</a> &t)
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock"><p><a class="el" href="classCVC3_1_1Theorem3.html" title="Theorem3.">Theorem3</a>. </p>
<p>Author: Sergey Berezin</p>
<p>Created: Tue Nov 4 17:57:07 2003</p>
<p>Implements the 3-valued theorem used for the user assertions and the result of query. It is simply a wrapper around class <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>, but has a different semantic meaning: the formula may have partial functions and has the Kleene's 3-valued interpretation. The fact that a <a class="el" href="classCVC3_1_1Theorem3.html" title="Theorem3.">Theorem3</a> value is derived means that the TCCs for the formula and all of its assumptions are valid in the current context, and the proofs of TCCs contribute to the set of assumptions. </p>
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00308">308</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="a1986607c85de1a0550ebe7759bf5b6a4"></a><!-- doxytag: member="CVC3::Theorem3::Theorem3" ref="a1986607c85de1a0550ebe7759bf5b6a4" 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::Theorem3::Theorem3 </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> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00325">325</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
</div>
</div>
<a class="anchor" id="a5495a662364c65492dceb1108a45d55c"></a><!-- doxytag: member="CVC3::Theorem3::Theorem3" ref="a5495a662364c65492dceb1108a45d55c" args="(TheoremManager *tm, const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Theorem3::Theorem3 </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></td>
<td>)</td>
<td></td><td><code> [inline, private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00332">332</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
</div>
</div>
<a class="anchor" id="ae64084287342d9fa9374a4db1981bbd5"></a><!-- doxytag: member="CVC3::Theorem3::Theorem3" ref="ae64084287342d9fa9374a4db1981bbd5" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::Theorem3::Theorem3 </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#l00346">346</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
</div>
</div>
<a class="anchor" id="a55e28790faec403ea8a9a0b5a718eab1"></a><!-- doxytag: member="CVC3::Theorem3::~Theorem3" ref="a55e28790faec403ea8a9a0b5a718eab1" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual CVC3::Theorem3::~Theorem3 </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00349">349</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="ab7984ea5eb9c9bdba751fc9ea9d6cc90"></a><!-- doxytag: member="CVC3::Theorem3::printDebug" ref="ab7984ea5eb9c9bdba751fc9ea9d6cc90" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem3::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#l00341">341</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>References <a class="el" href="theorem_8h_source.html#l00314">d_thm</a>, and <a class="el" href="theorem_8h_source.html#l00140">CVC3::Theorem::printDebug()</a>.</p>
</div>
</div>
<a class="anchor" id="a1f2b0509853067114494079f955de741"></a><!-- doxytag: member="CVC3::Theorem3::isNull" ref="a1f2b0509853067114494079f955de741" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem3::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#l00351">351</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>References <a class="el" href="theorem_8h_source.html#l00314">d_thm</a>, and <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>.</p>
</div>
</div>
<a class="anchor" id="ace6f5dda051da7db8a4adf74a723852c"></a><!-- doxytag: member="CVC3::Theorem3::isRewrite" ref="ace6f5dda051da7db8a4adf74a723852c" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem3::isRewrite </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#l00354">354</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>References <a class="el" href="theorem_8h_source.html#l00314">d_thm</a>, and <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>.</p>
</div>
</div>
<a class="anchor" id="aba6e80e63438ef74f027476ca085781a"></a><!-- doxytag: member="CVC3::Theorem3::isAssump" ref="aba6e80e63438ef74f027476ca085781a" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem3::isAssump </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#l00355">355</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>References <a class="el" href="theorem_8h_source.html#l00314">d_thm</a>, and <a class="el" href="theorem_8cpp_source.html#l00395">CVC3::Theorem::isAssump()</a>.</p>
</div>
</div>
<a class="anchor" id="a744788782cc996d5b914533fe7304352"></a><!-- doxytag: member="CVC3::Theorem3::getExpr" ref="a744788782cc996d5b914533fe7304352" 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::Theorem3::getExpr </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#l00358">358</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>References <a class="el" href="theorem_8h_source.html#l00314">d_thm</a>, and <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l00085">CVC3::CommonTheoremProducer::implIntro3()</a>.</p>
</div>
</div>
<a class="anchor" id="a86b1b2342e05df0b6c965df22ac6bdc5"></a><!-- doxytag: member="CVC3::Theorem3::getLHS" ref="a86b1b2342e05df0b6c965df22ac6bdc5" 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::Theorem3::getLHS </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#l00359">359</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>References <a class="el" href="theorem_8h_source.html#l00314">d_thm</a>, and <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>.</p>
</div>
</div>
<a class="anchor" id="a1da681e13e1dd2bfefb0d21027e20eb6"></a><!-- doxytag: member="CVC3::Theorem3::getRHS" ref="a1da681e13e1dd2bfefb0d21027e20eb6" 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::Theorem3::getRHS </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#l00360">360</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>References <a class="el" href="theorem_8h_source.html#l00314">d_thm</a>, and <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>.</p>
</div>
</div>
<a class="anchor" id="a3bf0a31a2adaabfd7a37d61e990fa9ea"></a><!-- doxytag: member="CVC3::Theorem3::getAssumptionsRef" ref="a3bf0a31a2adaabfd7a37d61e990fa9ea" 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::Theorem3::getAssumptionsRef </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#l00365">365</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>References <a class="el" href="theorem_8h_source.html#l00314">d_thm</a>, and <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>.</p>
<p>Referenced by <a class="el" href="vcl_8cpp_source.html#l00311">CVC3::VCL::deriveClosure()</a>, and <a class="el" href="common__theorem__producer_8cpp_source.html#l00085">CVC3::CommonTheoremProducer::implIntro3()</a>.</p>
</div>
</div>
<a class="anchor" id="a05c74972ebc3932829fa32ca237880db"></a><!-- doxytag: member="CVC3::Theorem3::getProof" ref="a05c74972ebc3932829fa32ca237880db" 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::Theorem3::getProof </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#l00370">370</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>References <a class="el" href="theorem_8h_source.html#l00314">d_thm</a>, and <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l00085">CVC3::CommonTheoremProducer::implIntro3()</a>.</p>
</div>
</div>
<a class="anchor" id="a153b7d792f901a481d1eb4c91c885330"></a><!-- doxytag: member="CVC3::Theorem3::getScope" ref="a153b7d792f901a481d1eb4c91c885330" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int CVC3::Theorem3::getScope </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#l00374">374</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>References <a class="el" href="theorem_8h_source.html#l00314">d_thm</a>, and <a class="el" href="theorem_8cpp_source.html#l00486">CVC3::Theorem::getScope()</a>.</p>
</div>
</div>
<a class="anchor" id="a099ac3dc23ce274b26a25cd9e5059502"></a><!-- doxytag: member="CVC3::Theorem3::withProof" ref="a099ac3dc23ce274b26a25cd9e5059502" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem3::withProof </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#l00377">377</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>References <a class="el" href="theorem_8h_source.html#l00314">d_thm</a>, and <a class="el" href="theorem_8cpp_source.html#l00214">CVC3::Theorem::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a49abf6d71c6190f1400b5146b61b0872"></a><!-- doxytag: member="CVC3::Theorem3::withAssumptions" ref="a49abf6d71c6190f1400b5146b61b0872" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem3::withAssumptions </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#l00378">378</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>References <a class="el" href="theorem_8h_source.html#l00314">d_thm</a>, and <a class="el" href="theorem_8cpp_source.html#l00219">CVC3::Theorem::withAssumptions()</a>.</p>
</div>
</div>
<a class="anchor" id="a3712f50eb83d3b485aab55f660bed77a"></a><!-- doxytag: member="CVC3::Theorem3::toString" ref="a3712f50eb83d3b485aab55f660bed77a" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string CVC3::Theorem3::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#l00410">410</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
</div>
</div>
<a class="anchor" id="a4a2253b9fa2508aedd3dded623e283ad"></a><!-- doxytag: member="CVC3::Theorem3::printx" ref="a4a2253b9fa2508aedd3dded623e283ad" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem3::printx </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#l00384">384</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>References <a class="el" href="theorem_8h_source.html#l00314">d_thm</a>, and <a class="el" href="theorem_8cpp_source.html#l00207">CVC3::Theorem::printx()</a>.</p>
</div>
</div>
<a class="anchor" id="ababd51a0131a57f96c0316f7f8f2a6c9"></a><!-- doxytag: member="CVC3::Theorem3::print" ref="ababd51a0131a57f96c0316f7f8f2a6c9" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Theorem3::print </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#l00385">385</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>References <a class="el" href="theorem_8h_source.html#l00314">d_thm</a>, and <a class="el" href="theorem_8cpp_source.html#l00211">CVC3::Theorem::print()</a>.</p>
</div>
</div>
<a class="anchor" id="a31be5df9f946e3a6f2a75f673db863cb"></a><!-- doxytag: member="CVC3::Theorem3::isAbsLiteral" ref="a31be5df9f946e3a6f2a75f673db863cb" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Theorem3::isAbsLiteral </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></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_8h_source.html#l00388">388</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>References <a class="el" href="theorem_8h_source.html#l00314">d_thm</a>, and <a class="el" href="theorem_8cpp_source.html#l00482">CVC3::Theorem::isAbsLiteral()</a>.</p>
</div>
</div>
<hr/><h2>Friends And Related Function Documentation</h2>
<a class="anchor" id="adb16a6e6bad96912c4150299576eaf9a"></a><!-- doxytag: member="CVC3::Theorem3::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#l00312">312</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
</div>
</div>
<a class="anchor" id="a1d12c9cc45e21f2bef8b4065f23b1ecd"></a><!-- doxytag: member="CVC3::Theorem3::operator==" ref="a1d12c9cc45e21f2bef8b4065f23b1ecd" args="(const Theorem3 &t1, const Theorem3 &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_1Theorem3.html">Theorem3</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_1Theorem3.html">Theorem3</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>Definition at line <a class="el" href="theorem_8h_source.html#l00316">316</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
</div>
</div>
<a class="anchor" id="a08914251eb8cbf0ced80d277a07b6827"></a><!-- doxytag: member="CVC3::Theorem3::operator!=" ref="a08914251eb8cbf0ced80d277a07b6827" args="(const Theorem3 &t1, const Theorem3 &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_1Theorem3.html">Theorem3</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_1Theorem3.html">Theorem3</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>Definition at line <a class="el" href="theorem_8h_source.html#l00319">319</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
</div>
</div>
<a class="anchor" id="af5109554e84f3a7b92eea93606cbc7bc"></a><!-- doxytag: member="CVC3::Theorem3::operator<<" ref="af5109554e84f3a7b92eea93606cbc7bc" args="(std::ostream &os, const Theorem3 &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_1Theorem3.html">Theorem3</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#l00390">390</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="ab03f48bf3430eb93d82983dd2bc8a632"></a><!-- doxytag: member="CVC3::Theorem3::d_thm" ref="ab03f48bf3430eb93d82983dd2bc8a632" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1Theorem3.html#ab03f48bf3430eb93d82983dd2bc8a632">CVC3::Theorem3::d_thm</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theorem_8h_source.html#l00314">314</a> of file <a class="el" href="theorem_8h_source.html">theorem.h</a>.</p>
<p>Referenced by <a class="el" href="theorem_8h_source.html#l00365">getAssumptionsRef()</a>, <a class="el" href="theorem_8h_source.html#l00358">getExpr()</a>, <a class="el" href="theorem_8h_source.html#l00359">getLHS()</a>, <a class="el" href="theorem_8h_source.html#l00370">getProof()</a>, <a class="el" href="theorem_8h_source.html#l00360">getRHS()</a>, <a class="el" href="theorem_8h_source.html#l00374">getScope()</a>, <a class="el" href="theorem_8h_source.html#l00388">isAbsLiteral()</a>, <a class="el" href="theorem_8h_source.html#l00355">isAssump()</a>, <a class="el" href="theorem_8h_source.html#l00351">isNull()</a>, <a class="el" href="theorem_8h_source.html#l00354">isRewrite()</a>, <a class="el" href="theorem_8h_source.html#l00385">print()</a>, <a class="el" href="theorem_8h_source.html#l00341">printDebug()</a>, <a class="el" href="theorem_8h_source.html#l00384">printx()</a>, <a class="el" href="theorem_8h_source.html#l00378">withAssumptions()</a>, and <a class="el" href="theorem_8h_source.html#l00377">withProof()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following file:<ul>
<li><a class="el" href="theorem_8h_source.html">theorem.h</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>
