<!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::SearchEngineTheoremProducer 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_1SearchEngineTheoremProducer.html">SearchEngineTheoremProducer</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> </div>
<div class="headertitle">
<div class="title">CVC3::SearchEngineTheoremProducer Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::SearchEngineTheoremProducer" --><!-- doxytag: inherits="CVC3::SearchEngineRules,CVC3::TheoremProducer" -->
<p><code>#include <<a class="el" href="search__theorem__producer_8h_source.html">search_theorem_producer.h</a>></code></p>
<div class="dynheader">
Inheritance diagram for CVC3::SearchEngineTheoremProducer:</div>
<div class="dyncontent">
<div class="center">
<img src="classCVC3_1_1SearchEngineTheoremProducer.png" usemap="#CVC3::SearchEngineTheoremProducer_map" alt=""/>
<map id="CVC3::SearchEngineTheoremProducer_map" name="CVC3::SearchEngineTheoremProducer_map">
<area href="classCVC3_1_1SearchEngineRules.html" title="API to the proof rules for the Search Engines." alt="CVC3::SearchEngineRules" shape="rect" coords="0,0,234,24"/>
<area href="classCVC3_1_1TheoremProducer.html" alt="CVC3::TheoremProducer" shape="rect" coords="244,0,478,24"/>
</map>
</div></div>
<p><a href="classCVC3_1_1SearchEngineTheoremProducer-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#ad09ba717299f8684495e218548a43533">SearchEngineTheoremProducer</a> (<a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> *tm)
<li>virtual <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a4a91c61608f1df10cfd4b114986327c9">~SearchEngineTheoremProducer</a> ()
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a671a24b65b564dff6588925ecfcb5f60">proofByContradiction</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &a, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &pfFalse)
<dl class="el"><dd class="mdescRight"><a class="el" href="classCVC3_1_1Proof.html">Proof</a> by contradiction: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma, \neg A \vdash\mathrm{FALSE}}{\Gamma \vdash A}\]" src="form_293.png"/>
</p>
<p>. <a href="#a671a24b65b564dff6588925ecfcb5f60"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a7f69d40a18ab9b66200d24ccc92c2ae9">negIntro</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &not_a, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &pfFalse)
<dl class="el"><dd class="mdescRight">Negation introduction: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma, A \vdash\mathrm{FALSE}}{\Gamma\vdash\neg A}\]" src="form_296.png"/>
</p>
<p>. <a href="#a7f69d40a18ab9b66200d24ccc92c2ae9"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a68990fddbfff890590e69e239a3110fe">caseSplit</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &a, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &a_proves_c, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &not_a_proves_c)
<dl class="el"><dd class="mdescRight">Case split: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_1, A\vdash C \quad \Gamma_2, \neg A\vdash C} {\Gamma_1\cup\Gamma_2\vdash C}\]" src="form_298.png"/>
</p>
<p>. <a href="#a68990fddbfff890590e69e239a3110fe"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#ac980b63fbd08b0e29b1092ed4aeb95e8">eliminateSkolemAxioms</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &tFalse, const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &delta)
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#abf46962b0eb1ff204a5b321828139713">conflictClause</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm, const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &lits, const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &gamma)
<dl class="el"><dd class="mdescRight">Conflict clause rule: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma,A_1,\ldots,A_n\vdash\mathrm{FALSE}} {\Gamma\vdash\neg A_1\vee\cdots\vee \neg A_n}\]" src="form_301.png"/>
</p>
<p>. <a href="#abf46962b0eb1ff204a5b321828139713"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a9be0036e770d071001f7afab845f0473">cutRule</a> (const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &thmsA, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &as_prove_b)
<dl class="el"><dd class="mdescRight">Cut rule: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_1\vdash A_1\quad\cdots\quad\Gamma_n\vdash A_n \quad \Gamma', A_1,\ldots,A_n\vdash B} {\bigcup_{i=1}^n\Gamma_i\cup\Gamma'\vdash B}\]" src="form_303.png"/>
</p>
<p>. <a href="#a9be0036e770d071001f7afab845f0473"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#af764cf6eae285f0dbd3d430b76c5e19d">unitProp</a> (const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &thms, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &clause, unsigned i)
<dl class="el"><dd class="mdescRight">Unit propagation rule: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_j\vdash\neg A_j\mbox{ for }j\in[1\ldots n]-\{i\} \quad \Gamma\vdash A_1\vee\cdots\vee A_n} {\bigcup_{j\in[1\ldots n]-\{i\}}\Gamma_j\cup\Gamma\vdash A_i}\]" src="form_306.png"/>
</p>
<p>. <a href="#af764cf6eae285f0dbd3d430b76c5e19d"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a55bf4e865a7a76e82c23d5fba566b853">conflictRule</a> (const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &thms, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &clause)
<dl class="el"><dd class="mdescRight">"Conflict" rule (all literals in a clause become FALSE) </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_j\vdash\neg A_j\mbox{ for }j\in[1\ldots n] \quad \Gamma\vdash A_1\vee\cdots\vee A_n} {\bigcup_{j\in[1\ldots n]}\Gamma_j\cup\Gamma \vdash\mathrm{FALSE}}\]" src="form_309.png"/>
</p>
<a href="#a55bf4e865a7a76e82c23d5fba566b853"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a1d0f21b895fc25bff5dc653490a775c0">propAndrAF</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &andr_th, bool left, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &b_th)
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a22c592b3807cddf270b7be995594d58a">propAndrAT</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &andr_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &l_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &r_th)
<li>virtual void <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a1bdf01b6d0e85d8c91a2fa3aaf0704c6">propAndrLRT</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &andr_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &a_th, <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> *l_th, <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> *r_th)
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a373b85c528799a04c9997f8f0b1349d6">propAndrLF</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &andr_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &a_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &r_th)
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a948eaf2519eb12dd8f76c3c890babd78">propAndrRF</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &andr_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &a_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &l_th)
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a8b6dd7f1001b52a5be21914e1ecf6da0">confAndrAT</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &andr_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &a_th, bool left, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &b_th)
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a09acd80b1c336ac225de0a71bee0d4c8">confAndrAF</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &andr_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &a_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &l_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &r_th)
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#afb6d1f50a0b2cf48bf98517731160595">propIffr</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &iffr_th, int p, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &a_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &b_th)
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#afc1db7951ca830c313d2cef522e45f25">confIffr</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &iffr_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &i_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &l_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &r_th)
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a9964535eb830bbc87e91f40e71333dfa">propIterIte</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &iter_th, bool left, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &if_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &then_th)
<li>virtual void <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a9c5271d8f47048c4573e21bfd21bc8a7">propIterIfThen</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &iter_th, bool left, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &ite_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &then_th, <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> *if_th, <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> *else_th)
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#aa3a9dce562278a5383f4551d95b12c3a">propIterThen</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &iter_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &ite_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &if_th)
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#aaf56546de0c7c7bbe0b573477d412bf7">confIterThenElse</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &iter_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &ite_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &then_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &else_th)
<li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#aad519346f53864cc21109200379a3698">confIterIfThen</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &iter_th, bool left, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &ite_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &if_th, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &then_th)
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#af38d03174800bca0baba91f4e8288b0f">andCNFRule</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<dl class="el"><dd class="mdescRight">AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v]. <a href="#af38d03174800bca0baba91f4e8288b0f"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a3cf33a58eee64dc744015e8657adc40a">orCNFRule</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<dl class="el"><dd class="mdescRight">OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v]. <a href="#a3cf33a58eee64dc744015e8657adc40a"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a15cbb86a5a77422c7d8c59384488f9e1">impCNFRule</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<dl class="el"><dd class="mdescRight">(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v] <a href="#a15cbb86a5a77422c7d8c59384488f9e1"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a47468ab81771bdb7af900bd2f907f818">iffCNFRule</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<dl class="el"><dd class="mdescRight">(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v] <a href="#a47468ab81771bdb7af900bd2f907f818"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a1c37ba3237f04f7536164166c7f0156e">iteCNFRule</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<dl class="el"><dd class="mdescRight">ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v]. <a href="#a1c37ba3237f04f7536164166c7f0156e"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a9ec94eac3bdabe251a4147b2830a2f50">iteToClauses</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &ite)
<dl class="el"><dd class="mdescRight">ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2) <a href="#a9ec94eac3bdabe251a4147b2830a2f50"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#ab608d81ddbbce71638fcce0d119c63d1">iffToClauses</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &iff)
<dl class="el"><dd class="mdescRight">e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2) <a href="#ab608d81ddbbce71638fcce0d119c63d1"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a211e687727973cff1b055a7302d562ae">satProof</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &queryExpr, const <a class="el" href="classCVC3_1_1Proof.html">Proof</a> &satProof)
</ul>
<h2><a name="pri-methods"></a>
Private Member Functions</h2>
<ul>
<li>void <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#acaa4dd5cb5be1e9844e03c82feea84b6">verifyConflict</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm, <a class="el" href="namespaceCVC3.html#ae8220d283ddfdaa8f4e0da0a03fa7ff4">TheoremMap</a> &m)
<li>void <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#aa12792d6b382598a0f5aeea983568a23">checkSoundNoSkolems</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > &visited, const <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > &skolems)
<li>void <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#aecd6425dded4edb62daefa858e969cf8">checkSoundNoSkolems</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t, <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > &visited, const <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > &skolems)
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#afd9835d232286f451200d637ba995e75">opCNFRule</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm, int kind, const std::string &ruleName)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a8ad94f1a94fd5bf8fa10dbf26e04ee58">convertToCNF</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &v, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &phi)
<dl class="el"><dd class="mdescRight">produces the CNF for the formula v <==> phi <a href="#a8ad94f1a94fd5bf8fa10dbf26e04ee58"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#a4af17425aaf7d8a28aaf1d8a09241535">findInLocalCache</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &i, <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &localCache, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &boundVars)
<dl class="el"><dd class="mdescRight">checks if phi has v in local cache of opCNFRule, if so reuse v. <a href="#a4af17425aaf7d8a28aaf1d8a09241535"></a><br/></dl></ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li><a class="el" href="classCVC3_1_1CommonProofRules.html">CommonProofRules</a> * <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#abb70faf5bb0eccda31e8ff06a46f2b65">d_commonRules</a>
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="search__theorem__producer_8h_source.html#l00032">32</a> of file <a class="el" href="search__theorem__producer_8h_source.html">search_theorem_producer.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="ad09ba717299f8684495e218548a43533"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::SearchEngineTheoremProducer" ref="ad09ba717299f8684495e218548a43533" args="(TheoremManager *tm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">SearchEngineTheoremProducer::SearchEngineTheoremProducer </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoremManager.html">TheoremManager</a> * </td>
<td class="paramname"><em>tm</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00062">62</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a4a91c61608f1df10cfd4b114986327c9"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::~SearchEngineTheoremProducer" ref="a4a91c61608f1df10cfd4b114986327c9" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">virtual CVC3::SearchEngineTheoremProducer::~SearchEngineTheoremProducer </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="search__theorem__producer_8h_source.html#l00048">48</a> of file <a class="el" href="search__theorem__producer_8h_source.html">search_theorem_producer.h</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="acaa4dd5cb5be1e9844e03c82feea84b6"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::verifyConflict" ref="acaa4dd5cb5be1e9844e03c82feea84b6" args="(const Theorem &thm, TheoremMap &m)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineTheoremProducer::verifyConflict </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="namespaceCVC3.html#ae8220d283ddfdaa8f4e0da0a03fa7ff4">TheoremMap</a> & </td>
<td class="paramname"><em>m</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00192">192</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, and <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>.</p>
<p>Referenced by <a class="el" href="search__theorem__producer_8cpp_source.html#l00221">conflictClause()</a>.</p>
</div>
</div>
<a class="anchor" id="aa12792d6b382598a0f5aeea983568a23"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems" ref="aa12792d6b382598a0f5aeea983568a23" args="(const Expr &e, ExprMap< bool > &visited, const ExprMap< bool > &skolems)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineTheoremProducer::checkSoundNoSkolems </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>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > & </td>
<td class="paramname"><em>visited</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > & </td>
<td class="paramname"><em>skolems</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00411">411</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="expr__map_8h_source.html#l00173">CVC3::ExprMap< Data >::count()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="kinds_8h_source.html#l00085">EXISTS</a>, <a class="el" href="kinds_8h_source.html#l00084">FORALL</a>, <a class="el" href="expr_8h_source.html#l01069">CVC3::Expr::getBody()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
<p>Referenced by <a class="el" href="search__theorem__producer_8cpp_source.html#l00429">checkSoundNoSkolems()</a>, and <a class="el" href="search__theorem__producer_8cpp_source.html#l00454">eliminateSkolemAxioms()</a>.</p>
</div>
</div>
<a class="anchor" id="aecd6425dded4edb62daefa858e969cf8"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems" ref="aecd6425dded4edb62daefa858e969cf8" args="(const Theorem &t, ExprMap< bool > &visited, const ExprMap< bool > &skolems)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineTheoremProducer::checkSoundNoSkolems </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 class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > & </td>
<td class="paramname"><em>visited</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > & </td>
<td class="paramname"><em>skolems</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00429">429</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="search__theorem__producer_8cpp_source.html#l00411">checkSoundNoSkolems()</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00395">CVC3::Theorem::isAssump()</a>, <a class="el" href="theorem_8cpp_source.html#l00416">CVC3::Theorem::isFlagged()</a>, <a class="el" href="theorem_8h_source.html#l00171">CVC3::Theorem::isRefl()</a>, and <a class="el" href="theorem_8cpp_source.html#l00429">CVC3::Theorem::setFlag()</a>.</p>
</div>
</div>
<a class="anchor" id="a671a24b65b564dff6588925ecfcb5f60"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::proofByContradiction" ref="a671a24b65b564dff6588925ecfcb5f60" args="(const Expr &a, const Theorem &pfFalse)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::proofByContradiction </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>a</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>pfFalse</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><a class="el" href="classCVC3_1_1Proof.html">Proof</a> by contradiction: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma, \neg A \vdash\mathrm{FALSE}}{\Gamma \vdash A}\]" src="form_293.png"/>
</p>
<p>. </p>
<p><img class="formulaInl" alt="$\neg A$" src="form_294.png"/> does not have to be present in the assumptions. </p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">a</td><td>is the assumption <em>A</em> </td></tr>
<tr><td class="paramname">pfFalse</td><td>is the theorem <img class="formulaInl" alt="$\Gamma, \neg A \vdash\mathrm{FALSE}$" src="form_295.png"/> </td></tr>
</table>
</dd>
</dl>
<p>Implements <a class="el" href="group__SE__Rules.html#ga64c9fb7058e52c324ce76f15fcea37e2">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00074">74</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00052">lfsc_called</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01419">satProof()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a7f69d40a18ab9b66200d24ccc92c2ae9"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::negIntro" ref="a7f69d40a18ab9b66200d24ccc92c2ae9" args="(const Expr &not_a, const Theorem &pfFalse)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::negIntro </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>not_a</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>pfFalse</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Negation introduction: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma, A \vdash\mathrm{FALSE}}{\Gamma\vdash\neg A}\]" src="form_296.png"/>
</p>
<p>. </p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">not_a</td><td>is the formula <img class="formulaInl" alt="$\neg A$" src="form_294.png"/>. We pass the negation <img class="formulaInl" alt="$\neg A$" src="form_294.png"/>, and not just <em>A</em>, for efficiency: building <img class="formulaInl" alt="$\neg A$" src="form_294.png"/> is more expensive (due to uniquifying pointers in <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> package) than extracting <em>A</em> from <img class="formulaInl" alt="$\neg A$" src="form_294.png"/>.</td></tr>
<tr><td class="paramname">pfFalse</td><td>is the theorem <img class="formulaInl" alt="$\Gamma, A \vdash\mathrm{FALSE}$" src="form_297.png"/> </td></tr>
</table>
</dd>
</dl>
<p>Implements <a class="el" href="group__SE__Rules.html#ga846c2bdc33f6ff2080e76637ea618626">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00105">105</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a68990fddbfff890590e69e239a3110fe"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::caseSplit" ref="a68990fddbfff890590e69e239a3110fe" args="(const Expr &a, const Theorem &a_proves_c, const Theorem &not_a_proves_c)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::caseSplit </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>a</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>a_proves_c</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>not_a_proves_c</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Case split: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_1, A\vdash C \quad \Gamma_2, \neg A\vdash C} {\Gamma_1\cup\Gamma_2\vdash C}\]" src="form_298.png"/>
</p>
<p>. </p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">a</td><td>is the assumption A to split on</td></tr>
<tr><td class="paramname">a_proves_c</td><td>is the theorem <img class="formulaInl" alt="$\Gamma_1, A\vdash C$" src="form_299.png"/></td></tr>
<tr><td class="paramname">not_a_proves_c</td><td>is the theorem <img class="formulaInl" alt="$\Gamma_2, \neg A\vdash C$" src="form_300.png"/> </td></tr>
</table>
</dd>
</dl>
<p>Implements <a class="el" href="group__SE__Rules.html#ga7db620d19846bd5947321a8d6f9e7da4">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00135">135</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="ac980b63fbd08b0e29b1092ed4aeb95e8"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms" ref="ac980b63fbd08b0e29b1092ed4aeb95e8" args="(const Theorem &tFalse, const std::vector< Theorem > &delta)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::eliminateSkolemAxioms </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>tFalse</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>delta</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Eliminate skolem axioms: Gamma, Delta |- false => Gamma|- false where Delta is a set of skolem axioms {|-Exists(x) phi (x) => phi(c)} and gamma does not contain any of the skolem constants c. </p>
<p>Implements <a class="el" href="group__SE__Rules.html#ga3ddf95924d2ff2efb59e84dc78a19821">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00454">454</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr__map_8h_source.html#l00190">CVC3::ExprMap< Data >::begin()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00411">checkSoundNoSkolems()</a>, <a class="el" href="theorem_8cpp_source.html#l00422">CVC3::Theorem::clearAllFlags()</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="expr__manager_8h_source.html#l00454">CVC3::ExprManager::newLeafExpr()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="abf46962b0eb1ff204a5b321828139713"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::conflictClause" ref="abf46962b0eb1ff204a5b321828139713" args="(const Theorem &thm, const std::vector< Theorem > &lits, const std::vector< Theorem > &gamma)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::conflictClause </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>lits</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>gamma</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Conflict clause rule: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma,A_1,\ldots,A_n\vdash\mathrm{FALSE}} {\Gamma\vdash\neg A_1\vee\cdots\vee \neg A_n}\]" src="form_301.png"/>
</p>
<p>. </p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">thm</td><td>is the theorem <img class="formulaInl" alt="$\Gamma,A_1,\ldots,A_n\vdash\mathrm{FALSE}$" src="form_302.png"/></td></tr>
<tr><td class="paramname">lits</td><td>is the vector of literals <em>A<sub>i</sub></em>. They must be present in the set of assumptions of <em>thm</em>.</td></tr>
<tr><td class="paramname">gamma</td><td>FIXME: document this!! </td></tr>
</table>
</dd>
</dl>
<p>Implements <a class="el" href="group__SE__Rules.html#ga03be39f8ffe84a1bcc09bba60f45245c">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00221">221</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00422">CVC3::Theorem::clearAllFlags()</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__map_8h_source.html#l00305">CVC3::ExprHashMap< Data >::empty()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="proof_8h_source.html#l00046">CVC3::Proof::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="expr_8h_source.html#l01005">CVC3::Expr::isVar()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00052">CVC3::TheoremProducer::newLabel()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="kinds_8h_source.html#l00068">OR</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00192">verifyConflict()</a>, <a class="el" href="theorem__producer_8h_source.html#l00162">CVC3::TheoremProducer::withAssumptions()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a9be0036e770d071001f7afab845f0473"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::cutRule" ref="a9be0036e770d071001f7afab845f0473" args="(const std::vector< Theorem > &thmsA, const Theorem &as_prove_b)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::cutRule </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>thmsA</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>as_prove_b</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Cut rule: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_1\vdash A_1\quad\cdots\quad\Gamma_n\vdash A_n \quad \Gamma', A_1,\ldots,A_n\vdash B} {\bigcup_{i=1}^n\Gamma_i\cup\Gamma'\vdash B}\]" src="form_303.png"/>
</p>
<p>. </p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">thmsA</td><td>is a vector of theorems <img class="formulaInl" alt="$\Gamma_i\vdash A_i$" src="form_304.png"/></td></tr>
<tr><td class="paramname">as_prove_b</td><td>is the theorem <img class="formulaInl" alt="$\Gamma', A_1,\ldots,A_n\vdash B$" src="form_305.png"/> (the name means "A's prove B") </td></tr>
</table>
</dd>
</dl>
<p>Implements <a class="el" href="group__SE__Rules.html#gac1ef0687c058a3d4bd1d9ed88cd27abe">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00375">375</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8cpp_source.html#l00200">CVC3::Assumptions::add()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem__producer_8h_source.html#l00162">CVC3::TheoremProducer::withAssumptions()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="af764cf6eae285f0dbd3d430b76c5e19d"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::unitProp" ref="af764cf6eae285f0dbd3d430b76c5e19d" args="(const std::vector< Theorem > &thms, const Theorem &clause, unsigned i)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::unitProp </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>thms</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>clause</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">unsigned </td>
<td class="paramname"><em>i</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Unit propagation rule: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_j\vdash\neg A_j\mbox{ for }j\in[1\ldots n]-\{i\} \quad \Gamma\vdash A_1\vee\cdots\vee A_n} {\bigcup_{j\in[1\ldots n]-\{i\}}\Gamma_j\cup\Gamma\vdash A_i}\]" src="form_306.png"/>
</p>
<p>. </p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">clause</td><td>is the proof of the clause <img class="formulaInl" alt="$ \Gamma\vdash A_1\vee\cdots\vee A_n$" src="form_307.png"/></td></tr>
<tr><td class="paramname">i</td><td>is the index (0..n-1) of the literal to be unit-propagated</td></tr>
<tr><td class="paramname">thms</td><td>is the vector of theorems <img class="formulaInl" alt="$\Gamma_j\vdash\neg A_j$" src="form_308.png"/> for all literals except <em>A<sub>i</sub></em> </td></tr>
</table>
</dd>
</dl>
<p>Implements <a class="el" href="group__SE__Rules.html#gae7221bb8b77313a9b53a4beca9cc0aa0">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00511">511</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8cpp_source.html#l00200">CVC3::Assumptions::add()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a55bf4e865a7a76e82c23d5fba566b853"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::conflictRule" ref="a55bf4e865a7a76e82c23d5fba566b853" args="(const std::vector< Theorem > &thms, const Theorem &clause)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::conflictRule </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>thms</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>clause</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>"Conflict" rule (all literals in a clause become FALSE) </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_j\vdash\neg A_j\mbox{ for }j\in[1\ldots n] \quad \Gamma\vdash A_1\vee\cdots\vee A_n} {\bigcup_{j\in[1\ldots n]}\Gamma_j\cup\Gamma \vdash\mathrm{FALSE}}\]" src="form_309.png"/>
</p>
</p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">clause</td><td>is the proof of the clause <img class="formulaInl" alt="$ \Gamma\vdash A_1\vee\cdots\vee A_n$" src="form_307.png"/></td></tr>
<tr><td class="paramname">thms</td><td>is the vector of theorems <img class="formulaInl" alt="$\Gamma_j\vdash\neg A_j$" src="form_308.png"/> </td></tr>
</table>
</dd>
</dl>
<p>Implements <a class="el" href="group__SE__Rules.html#ga9c74425b4471d411f58f16781951c441">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l01109">1109</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8cpp_source.html#l00200">CVC3::Assumptions::add()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="expr__manager_8h_source.html#l00278">CVC3::ExprManager::falseExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a1d0f21b895fc25bff5dc653490a775c0"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::propAndrAF" ref="a1d0f21b895fc25bff5dc653490a775c0" args="(const Theorem &andr_th, bool left, const Theorem &b_th)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::propAndrAF </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>andr_th</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>left</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>b_th</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="group__SE__Rules.html#gaf5a18f8bcdc2f71632f05bcfe0bc533e">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00564">564</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00075">AND_R</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00252">CVC3::Theorem::refutes()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a22c592b3807cddf270b7be995594d58a"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::propAndrAT" ref="a22c592b3807cddf270b7be995594d58a" args="(const Theorem &andr_th, const Theorem &l_th, const Theorem &r_th)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::propAndrAT </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>andr_th</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>l_th</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>r_th</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="group__SE__Rules.html#gac7998bdcac234b0f3dc202d44b49c69c">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00593">593</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8cpp_source.html#l00200">CVC3::Assumptions::add()</a>, <a class="el" href="kinds_8h_source.html#l00075">AND_R</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00259">CVC3::Theorem::proves()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a1bdf01b6d0e85d8c91a2fa3aaf0704c6"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::propAndrLRT" ref="a1bdf01b6d0e85d8c91a2fa3aaf0704c6" args="(const Theorem &andr_th, const Theorem &a_th, Theorem *l_th, Theorem *r_th)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineTheoremProducer::propAndrLRT </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>andr_th</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>a_th</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> * </td>
<td class="paramname"><em>l_th</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> * </td>
<td class="paramname"><em>r_th</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="group__SE__Rules.html#gad0150b04c296a6b8e05579c1dbd365f8">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00623">623</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00075">AND_R</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00259">CVC3::Theorem::proves()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a373b85c528799a04c9997f8f0b1349d6"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::propAndrLF" ref="a373b85c528799a04c9997f8f0b1349d6" args="(const Theorem &andr_th, const Theorem &a_th, const Theorem &r_th)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::propAndrLF </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>andr_th</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>a_th</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>r_th</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="group__SE__Rules.html#ga8c8fc73c8b0413f5ca3fa7d72e687f5b">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00651">651</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8cpp_source.html#l00200">CVC3::Assumptions::add()</a>, <a class="el" href="kinds_8h_source.html#l00075">AND_R</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00259">CVC3::Theorem::proves()</a>, <a class="el" href="theorem_8h_source.html#l00252">CVC3::Theorem::refutes()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a948eaf2519eb12dd8f76c3c890babd78"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::propAndrRF" ref="a948eaf2519eb12dd8f76c3c890babd78" args="(const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::propAndrRF </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>andr_th</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>a_th</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>l_th</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="group__SE__Rules.html#ga1158c41e7b7ed199271391d4404ce1b2">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00681">681</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8cpp_source.html#l00200">CVC3::Assumptions::add()</a>, <a class="el" href="kinds_8h_source.html#l00075">AND_R</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00259">CVC3::Theorem::proves()</a>, <a class="el" href="theorem_8h_source.html#l00252">CVC3::Theorem::refutes()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a8b6dd7f1001b52a5be21914e1ecf6da0"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::confAndrAT" ref="a8b6dd7f1001b52a5be21914e1ecf6da0" args="(const Theorem &andr_th, const Theorem &a_th, bool left, const Theorem &b_th)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::confAndrAT </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>andr_th</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>a_th</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>left</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>b_th</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="group__SE__Rules.html#ga09d987f2d81c19d798d7185b125879b6">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00711">711</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8cpp_source.html#l00200">CVC3::Assumptions::add()</a>, <a class="el" href="kinds_8h_source.html#l00075">AND_R</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="expr__manager_8h_source.html#l00278">CVC3::ExprManager::falseExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00259">CVC3::Theorem::proves()</a>, <a class="el" href="theorem_8h_source.html#l00252">CVC3::Theorem::refutes()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a09acd80b1c336ac225de0a71bee0d4c8"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::confAndrAF" ref="a09acd80b1c336ac225de0a71bee0d4c8" args="(const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th, const Theorem &r_th)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::confAndrAF </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>andr_th</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>a_th</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>l_th</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>r_th</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="group__SE__Rules.html#gadb878db4f9d24a21b62f50df2713ecca">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00744">744</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8cpp_source.html#l00200">CVC3::Assumptions::add()</a>, <a class="el" href="kinds_8h_source.html#l00075">AND_R</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="expr__manager_8h_source.html#l00278">CVC3::ExprManager::falseExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00259">CVC3::Theorem::proves()</a>, <a class="el" href="theorem_8h_source.html#l00252">CVC3::Theorem::refutes()</a>, <a class="el" href="theorem__producer_8h_source.html#l00162">CVC3::TheoremProducer::withAssumptions()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="afb6d1f50a0b2cf48bf98517731160595"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::propIffr" ref="afb6d1f50a0b2cf48bf98517731160595" args="(const Theorem &iffr_th, int p, const Theorem &a_th, const Theorem &b_th)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::propIffr </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>iffr_th</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>p</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>a_th</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>b_th</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="group__SE__Rules.html#ga9bc3e3eab4b1fe4fb2c0a0172ca25ee9">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00782">782</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8cpp_source.html#l00200">CVC3::Assumptions::add()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="kinds_8h_source.html#l00076">IFF_R</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00259">CVC3::Theorem::proves()</a>, <a class="el" href="theorem_8h_source.html#l00252">CVC3::Theorem::refutes()</a>, <a class="el" href="theorem__producer_8h_source.html#l00162">CVC3::TheoremProducer::withAssumptions()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="afc1db7951ca830c313d2cef522e45f25"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::confIffr" ref="afc1db7951ca830c313d2cef522e45f25" args="(const Theorem &iffr_th, const Theorem &i_th, const Theorem &l_th, const Theorem &r_th)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::confIffr </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>iffr_th</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>i_th</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>l_th</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>r_th</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="group__SE__Rules.html#gaef31b1a5f6d6e9f270a1ab28ee361b14">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00834">834</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8cpp_source.html#l00200">CVC3::Assumptions::add()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="expr__manager_8h_source.html#l00278">CVC3::ExprManager::falseExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="kinds_8h_source.html#l00076">IFF_R</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00259">CVC3::Theorem::proves()</a>, <a class="el" href="theorem_8h_source.html#l00252">CVC3::Theorem::refutes()</a>, <a class="el" href="theorem__producer_8h_source.html#l00162">CVC3::TheoremProducer::withAssumptions()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a9964535eb830bbc87e91f40e71333dfa"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::propIterIte" ref="a9964535eb830bbc87e91f40e71333dfa" args="(const Theorem &iter_th, bool left, const Theorem &if_th, const Theorem &then_th)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::propIterIte </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>iter_th</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>left</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>if_th</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>then_th</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="group__SE__Rules.html#ga979ad08269cd2799993628eaaccc146f">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00881">881</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8cpp_source.html#l00200">CVC3::Assumptions::add()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="kinds_8h_source.html#l00077">ITE_R</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00259">CVC3::Theorem::proves()</a>, <a class="el" href="theorem_8h_source.html#l00252">CVC3::Theorem::refutes()</a>, <a class="el" href="theorem__producer_8h_source.html#l00162">CVC3::TheoremProducer::withAssumptions()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a9c5271d8f47048c4573e21bfd21bc8a7"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::propIterIfThen" ref="a9c5271d8f47048c4573e21bfd21bc8a7" args="(const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &then_th, Theorem *if_th, Theorem *else_th)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineTheoremProducer::propIterIfThen </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>iter_th</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>left</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>ite_th</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>then_th</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> * </td>
<td class="paramname"><em>if_th</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> * </td>
<td class="paramname"><em>else_th</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="group__SE__Rules.html#gad35217bbc9f4a27b4d23af173e9ea2c7">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00923">923</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8cpp_source.html#l00200">CVC3::Assumptions::add()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="kinds_8h_source.html#l00077">ITE_R</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00259">CVC3::Theorem::proves()</a>, <a class="el" href="theorem_8h_source.html#l00252">CVC3::Theorem::refutes()</a>, <a class="el" href="theorem__producer_8h_source.html#l00162">CVC3::TheoremProducer::withAssumptions()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="aa3a9dce562278a5383f4551d95b12c3a"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::propIterThen" ref="aa3a9dce562278a5383f4551d95b12c3a" args="(const Theorem &iter_th, const Theorem &ite_th, const Theorem &if_th)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::propIterThen </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>iter_th</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>ite_th</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>if_th</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="group__SE__Rules.html#gab7b07d3b350b2cc7f3f596233abb54ea">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00970">970</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8cpp_source.html#l00200">CVC3::Assumptions::add()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="kinds_8h_source.html#l00077">ITE_R</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00259">CVC3::Theorem::proves()</a>, <a class="el" href="theorem_8h_source.html#l00252">CVC3::Theorem::refutes()</a>, <a class="el" href="theorem__producer_8h_source.html#l00162">CVC3::TheoremProducer::withAssumptions()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="aaf56546de0c7c7bbe0b573477d412bf7"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::confIterThenElse" ref="aaf56546de0c7c7bbe0b573477d412bf7" args="(const Theorem &iter_th, const Theorem &ite_th, const Theorem &then_th, const Theorem &else_th)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::confIterThenElse </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>iter_th</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>ite_th</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>then_th</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>else_th</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="group__SE__Rules.html#gaae491d08949a1ec57981526c8e960119">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l01012">1012</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8cpp_source.html#l00200">CVC3::Assumptions::add()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="expr__manager_8h_source.html#l00278">CVC3::ExprManager::falseExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="kinds_8h_source.html#l00077">ITE_R</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00259">CVC3::Theorem::proves()</a>, <a class="el" href="theorem_8h_source.html#l00252">CVC3::Theorem::refutes()</a>, <a class="el" href="theorem__producer_8h_source.html#l00162">CVC3::TheoremProducer::withAssumptions()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="aad519346f53864cc21109200379a3698"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::confIterIfThen" ref="aad519346f53864cc21109200379a3698" args="(const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &if_th, const Theorem &then_th)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::confIterIfThen </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>iter_th</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>left</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>ite_th</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>if_th</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>then_th</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="group__SE__Rules.html#ga771471d7cbb2253bc32f2a8018bd7182">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l01059">1059</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8cpp_source.html#l00200">CVC3::Assumptions::add()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="expr__manager_8h_source.html#l00278">CVC3::ExprManager::falseExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="kinds_8h_source.html#l00077">ITE_R</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="theorem_8h_source.html#l00259">CVC3::Theorem::proves()</a>, <a class="el" href="theorem_8h_source.html#l00252">CVC3::Theorem::refutes()</a>, <a class="el" href="theorem__producer_8h_source.html#l00162">CVC3::TheoremProducer::withAssumptions()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="af38d03174800bca0baba91f4e8288b0f"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::andCNFRule" ref="af38d03174800bca0baba91f4e8288b0f" args="(const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::andCNFRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v]. </p>
<p>Implements <a class="el" href="group__SE__Rules.html#gab183ff7d1013729d0d3e2dbe28686e3c">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l01160">1160</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00067">AND</a>, and <a class="el" href="search__theorem__producer_8cpp_source.html#l01226">opCNFRule()</a>.</p>
</div>
</div>
<a class="anchor" id="a3cf33a58eee64dc744015e8657adc40a"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::orCNFRule" ref="a3cf33a58eee64dc744015e8657adc40a" args="(const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::orCNFRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v]. </p>
<p>Implements <a class="el" href="group__SE__Rules.html#ga7086aa693d2a3421bc349eca8e9938ba">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l01165">1165</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="search__theorem__producer_8cpp_source.html#l01226">opCNFRule()</a>, and <a class="el" href="kinds_8h_source.html#l00068">OR</a>.</p>
</div>
</div>
<a class="anchor" id="a15cbb86a5a77422c7d8c59384488f9e1"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::impCNFRule" ref="a15cbb86a5a77422c7d8c59384488f9e1" args="(const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::impCNFRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v] </p>
<p>Implements <a class="el" href="group__SE__Rules.html#ga25f7b95c8ebce2be117d03a1c93d715f">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l01170">1170</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00071">IMPLIES</a>, and <a class="el" href="search__theorem__producer_8cpp_source.html#l01226">opCNFRule()</a>.</p>
</div>
</div>
<a class="anchor" id="a47468ab81771bdb7af900bd2f907f818"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::iffCNFRule" ref="a47468ab81771bdb7af900bd2f907f818" args="(const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::iffCNFRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v] </p>
<p>Implements <a class="el" href="group__SE__Rules.html#ga4ab7606744594db9050cb83fe6b73668">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l01175">1175</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00070">IFF</a>, and <a class="el" href="search__theorem__producer_8cpp_source.html#l01226">opCNFRule()</a>.</p>
</div>
</div>
<a class="anchor" id="a1c37ba3237f04f7536164166c7f0156e"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::iteCNFRule" ref="a1c37ba3237f04f7536164166c7f0156e" args="(const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::iteCNFRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v]. </p>
<p>Implements <a class="el" href="group__SE__Rules.html#gae9263cbcedf5def99b3c49ee6978497a">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l01180">1180</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00081">ITE</a>, and <a class="el" href="search__theorem__producer_8cpp_source.html#l01226">opCNFRule()</a>.</p>
</div>
</div>
<a class="anchor" id="a9ec94eac3bdabe251a4147b2830a2f50"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::iteToClauses" ref="a9ec94eac3bdabe251a4147b2830a2f50" args="(const Theorem &ite)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::iteToClauses </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>ite</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2) </p>
<p>Implements <a class="el" href="group__SE__Rules.html#ga9b9c0fe62505477b6ec9774c1b5b2494">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l01186">1186</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr_8h_source.html#l00423">CVC3::Expr::isITE()</a>, <a class="el" href="expr_8h_source.html#l00937">CVC3::Expr::negate()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="ab608d81ddbbce71638fcce0d119c63d1"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::iffToClauses" ref="ab608d81ddbbce71638fcce0d119c63d1" args="(const Theorem &iff)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::iffToClauses </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>iff</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2) </p>
<p>Implements <a class="el" href="group__SE__Rules.html#ga356cd5a36ede50921fbaa3bc7e222d4f">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l01206">1206</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, <a class="el" href="expr_8h_source.html#l00937">CVC3::Expr::negate()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="a211e687727973cff1b055a7302d562ae"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::satProof" ref="a211e687727973cff1b055a7302d562ae" args="(const Expr &queryExpr, const Proof &satProof)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::satProof </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>queryExpr</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>satProof</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implements <a class="el" href="group__SE__Rules.html#ga55daf0bf95530208f5abf9484ded9055">CVC3::SearchEngineRules</a>.</p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l01419">1419</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="search__theorem__producer_8h_source.html#l00036">d_commonRules</a>, <a class="el" href="theorem__producer_8h_source.html#l00094">CVC3::TheoremProducer::d_tm</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="proof_8h_source.html#l00046">CVC3::Proof::getExpr()</a>, <a class="el" href="theorem__manager_8h_source.html#l00077">CVC3::TheoremManager::getFlags()</a>, <a class="el" href="group__SE.html#ga43f52699cddc6e0feffffaf22424fe47">CVC3::SearchEngine::getUserAssumptions()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00052">lfsc_called</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="LFSCPrinter_8cpp_source.html#l00026">LFSCPrinter::print_LFSC()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00053">search_engine</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
<p>Referenced by <a class="el" href="search__theorem__producer_8cpp_source.html#l00074">proofByContradiction()</a>.</p>
</div>
</div>
<a class="anchor" id="afd9835d232286f451200d637ba995e75"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::opCNFRule" ref="afd9835d232286f451200d637ba995e75" args="(const Theorem &thm, int kind, const std::string &ruleName)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineTheoremProducer::opCNFRule </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>kind</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>ruleName</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l01226">1226</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00945">CVC3::andExpr()</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr__map_8h_source.html#l00190">CVC3::ExprMap< Data >::begin()</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="theorem__producer_8h_source.html#l00087">CHECK_PROOFS</a>, <a class="el" href="theorem__producer_8h_source.html#l00083">CHECK_SOUND</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01309">convertToCNF()</a>, <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="kinds_8h_source.html#l00085">EXISTS</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01382">findInLocalCache()</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00405">CVC3::ExprManager::getKindName()</a>, <a class="el" href="expr_8h_source.html#l01183">CVC3::Expr::getOp()</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="expr_8h_source.html#l00424">CVC3::Expr::isIff()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="expr_8h_source.html#l00411">CVC3::Expr::isPropAtom()</a>, <a class="el" href="expr__manager_8h_source.html#l00506">CVC3::ExprManager::newClosureExpr()</a>, <a class="el" href="theorem__producer_8cpp_source.html#l00075">CVC3::TheoremProducer::newPf()</a>, <a class="el" href="theorem__producer_8h_source.html#l00107">CVC3::TheoremProducer::newTheorem()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, and <a class="el" href="theorem__producer_8h_source.html#l00159">CVC3::TheoremProducer::withProof()</a>.</p>
<p>Referenced by <a class="el" href="search__theorem__producer_8cpp_source.html#l01160">andCNFRule()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01175">iffCNFRule()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01170">impCNFRule()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01180">iteCNFRule()</a>, and <a class="el" href="search__theorem__producer_8cpp_source.html#l01165">orCNFRule()</a>.</p>
</div>
</div>
<a class="anchor" id="a8ad94f1a94fd5bf8fa10dbf26e04ee58"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::convertToCNF" ref="a8ad94f1a94fd5bf8fa10dbf26e04ee58" args="(const Expr &v, const Expr &phi)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> SearchEngineTheoremProducer::convertToCNF </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>v</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>phi</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>produces the CNF for the formula v <==> phi </p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l01309">1309</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00067">AND</a>, <a class="el" href="expr_8h_source.html#l00945">CVC3::andExpr()</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="kinds_8h_source.html#l00070">IFF</a>, <a class="el" href="kinds_8h_source.html#l00071">IMPLIES</a>, <a class="el" href="kinds_8h_source.html#l00081">ITE</a>, <a class="el" href="expr_8h_source.html#l00937">CVC3::Expr::negate()</a>, <a class="el" href="kinds_8h_source.html#l00068">OR</a>, <a class="el" href="expr_8h_source.html#l00951">CVC3::Expr::orExpr()</a>, <a class="el" href="expr_8h_source.html#l00955">CVC3::orExpr()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
<p>Referenced by <a class="el" href="search__theorem__producer_8cpp_source.html#l01226">opCNFRule()</a>.</p>
</div>
</div>
<a class="anchor" id="a4af17425aaf7d8a28aaf1d8a09241535"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::findInLocalCache" ref="a4af17425aaf7d8a28aaf1d8a09241535" args="(const Expr &i, ExprMap< Expr > &localCache, std::vector< Expr > &boundVars)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> SearchEngineTheoremProducer::findInLocalCache </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>i</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>localCache</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>boundVars</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>checks if phi has v in local cache of opCNFRule, if so reuse v. </p>
<p>similarly for ( ! ... ! (phi)) </p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l01382">1382</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="theorem__producer_8h_source.html#l00095">CVC3::TheoremProducer::d_em</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr__map_8h_source.html#l00194">CVC3::ExprMap< Data >::find()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="expr_8h_source.html#l00965">CVC3::Expr::iffExpr()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="expr__manager_8h_source.html#l00484">CVC3::ExprManager::newBoundVarExpr()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
<p>Referenced by <a class="el" href="search__theorem__producer_8cpp_source.html#l01226">opCNFRule()</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="abb70faf5bb0eccda31e8ff06a46f2b65"></a><!-- doxytag: member="CVC3::SearchEngineTheoremProducer::d_commonRules" ref="abb70faf5bb0eccda31e8ff06a46f2b65" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CommonProofRules.html">CommonProofRules</a>* <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#abb70faf5bb0eccda31e8ff06a46f2b65">CVC3::SearchEngineTheoremProducer::d_commonRules</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="search__theorem__producer_8h_source.html#l00036">36</a> of file <a class="el" href="search__theorem__producer_8h_source.html">search_theorem_producer.h</a>.</p>
<p>Referenced by <a class="el" href="search__theorem__producer_8cpp_source.html#l01419">satProof()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="search__theorem__producer_8h_source.html">search_theorem_producer.h</a></li>
<li><a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.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>
