<!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: search_theorem_producer.cpp Source File</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><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div class="header">
<div class="headertitle">
<div class="title">search_theorem_producer.cpp</div> </div>
</div>
<div class="contents">
<a href="search__theorem__producer_8cpp.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00002"></a>00002 <span class="comment">/*!</span>
<a name="l00003"></a>00003 <span class="comment"> * \file search_theorem_producer.cpp</span>
<a name="l00004"></a>00004 <span class="comment"> * \brief Implementation of the proof rules for the simple search engine</span>
<a name="l00005"></a>00005 <span class="comment"> * </span>
<a name="l00006"></a>00006 <span class="comment"> * Author: Sergey Berezin</span>
<a name="l00007"></a>00007 <span class="comment"> * </span>
<a name="l00008"></a>00008 <span class="comment"> * Created: Mon Feb 24 14:51:51 2003</span>
<a name="l00009"></a>00009 <span class="comment"> *</span>
<a name="l00010"></a>00010 <span class="comment"> * <hr></span>
<a name="l00011"></a>00011 <span class="comment"> *</span>
<a name="l00012"></a>00012 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00013"></a>00013 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00014"></a>00014 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00015"></a>00015 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00016"></a>00016 <span class="comment"> * </span>
<a name="l00017"></a>00017 <span class="comment"> * <hr></span>
<a name="l00018"></a>00018 <span class="comment"> * </span>
<a name="l00019"></a>00019 <span class="comment"> */</span>
<a name="l00020"></a>00020 <span class="comment">/*****************************************************************************/</span>
<a name="l00021"></a>00021
<a name="l00022"></a>00022 <span class="preprocessor">#include "<a class="code" href="search_8h.html" title="Abstract API to the proof search engine.">search.h</a>"</span>
<a name="l00023"></a>00023 <span class="preprocessor">#include "<a class="code" href="theory__core_8h.html">theory_core.h</a>"</span>
<a name="l00024"></a>00024 <span class="preprocessor">#include "<a class="code" href="theorem__manager_8h.html">theorem_manager.h</a>"</span>
<a name="l00025"></a>00025 <span class="preprocessor">#include "<a class="code" href="common__proof__rules_8h.html">common_proof_rules.h</a>"</span>
<a name="l00026"></a>00026 <span class="preprocessor">#include "<a class="code" href="command__line__flags_8h.html">command_line_flags.h</a>"</span>
<a name="l00027"></a>00027 <span class="preprocessor">#include "<a class="code" href="theory__arith_8h.html">theory_arith.h</a>"</span>
<a name="l00028"></a>00028 <span class="comment">// UNCOMMENT THIS FOR LFSC</span>
<a name="l00029"></a>00029 <span class="preprocessor">#include "<a class="code" href="LFSCPrinter_8h.html">LFSCPrinter.h</a>"</span> <span class="comment">// by liana for LFSC conversion</span>
<a name="l00030"></a>00030
<a name="l00031"></a><a class="code" href="search__theorem__producer_8cpp.html#a8663c36bbf15bb5a0dcb01b97897fa95">00031</a> <span class="preprocessor">#define _CVC3_TRUSTED_</span>
<a name="l00032"></a>00032 <span class="preprocessor"></span><span class="preprocessor">#include "<a class="code" href="search__theorem__producer_8h.html" title="Implementation API to proof rules for the simple search engine.">search_theorem_producer.h</a>"</span>
<a name="l00033"></a>00033
<a name="l00034"></a>00034
<a name="l00035"></a>00035 <span class="keyword">using namespace </span>std;
<a name="l00036"></a>00036 <span class="keyword">using namespace </span>CVC3;
<a name="l00037"></a>00037
<a name="l00038"></a>00038 <span class="comment"></span>
<a name="l00039"></a>00039 <span class="comment">/////////////////////////////////////////////////////////////////////////////</span>
<a name="l00040"></a>00040 <span class="comment"></span><span class="comment">// class SearchEngine trusted methods</span><span class="comment"></span>
<a name="l00041"></a>00041 <span class="comment">/////////////////////////////////////////////////////////////////////////////</span>
<a name="l00042"></a>00042 <span class="comment"></span>
<a name="l00043"></a>00043
<a name="l00044"></a>00044
<a name="l00045"></a>00045 <a class="code" href="classCVC3_1_1SearchEngineRules.html" title="API to the proof rules for the Search Engines.">SearchEngineRules</a>*
<a name="l00046"></a><a class="code" href="group__SE.html#ga11dd236b3ba4ca5faad7563dfe6f3d72">00046</a> SearchEngine::createRules() {
<a name="l00047"></a>00047 <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html">SearchEngineTheoremProducer</a>(d_core->getTM());
<a name="l00048"></a>00048 }
<a name="l00049"></a>00049
<a name="l00050"></a>00050
<a name="l00051"></a>00051 <span class="comment">// hack for printing original assumptions in LFSC by liana</span>
<a name="l00052"></a><a class="code" href="search__theorem__producer_8cpp.html#ad48a265d67710c19ae70a239a42cc9f3">00052</a> <span class="keywordtype">bool</span> <a class="code" href="search__theorem__producer_8cpp.html#ad48a265d67710c19ae70a239a42cc9f3">lfsc_called</a> = <span class="keyword">false</span>;
<a name="l00053"></a><a class="code" href="search__theorem__producer_8cpp.html#a735bfac5de1621927af23c4fbc78c257">00053</a> <a class="code" href="classCVC3_1_1SearchEngine.html" title="API to to a generic proof search engine.">SearchEngine</a>* <a class="code" href="search__theorem__producer_8cpp.html#a735bfac5de1621927af23c4fbc78c257">search_engine</a>;
<a name="l00054"></a>00054
<a name="l00055"></a>00055 <a class="code" href="classCVC3_1_1SearchEngineRules.html" title="API to the proof rules for the Search Engines.">SearchEngineRules</a>*
<a name="l00056"></a><a class="code" href="group__SE.html#ga5ee040962725cff9a07cd33cbb6d6232">00056</a> SearchEngine::createRules(<a class="code" href="classCVC3_1_1SearchEngine.html" title="API to to a generic proof search engine.">SearchEngine</a>* s_eng) {
<a name="l00057"></a>00057 <a class="code" href="search__theorem__producer_8cpp.html#a735bfac5de1621927af23c4fbc78c257">search_engine</a> = s_eng;
<a name="l00058"></a>00058 <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html">SearchEngineTheoremProducer</a>(d_core->getTM());
<a name="l00059"></a>00059 }
<a name="l00060"></a>00060
<a name="l00061"></a>00061
<a name="l00062"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#ad09ba717299f8684495e218548a43533">00062</a> SearchEngineTheoremProducer::SearchEngineTheoremProducer(<a class="code" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>* tm)
<a name="l00063"></a>00063 : <a class="code" href="classCVC3_1_1TheoremProducer.html">TheoremProducer</a>(tm), d_commonRules(tm->getRules())
<a name="l00064"></a>00064 { }
<a name="l00065"></a>00065
<a name="l00066"></a>00066 <span class="comment"></span>
<a name="l00067"></a>00067 <span class="comment">/////////////////////////////////////////////////////////////////////////////</span>
<a name="l00068"></a>00068 <span class="comment"></span><span class="comment">// Proof rules</span><span class="comment"></span>
<a name="l00069"></a>00069 <span class="comment">/////////////////////////////////////////////////////////////////////////////</span>
<a name="l00070"></a>00070 <span class="comment"></span>
<a name="l00071"></a>00071 <span class="comment">// Proof by contradiction: !A |- FALSE ==> |- A. "!A" doesn't</span>
<a name="l00072"></a>00072 <span class="comment">// have to be present in the assumptions.</span>
<a name="l00073"></a>00073 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00074"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a671a24b65b564dff6588925ecfcb5f60">00074</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a671a24b65b564dff6588925ecfcb5f60" title="Proof by contradiction: .">SearchEngineTheoremProducer::proofByContradiction</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& a,
<a name="l00075"></a>00075 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& pfFalse) {
<a name="l00076"></a>00076 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>)
<a name="l00077"></a>00077 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(pfFalse.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#ga6173f64b22cba76472cd0c814bbf6dae">isFalse</a>(),
<a name="l00078"></a>00078 <span class="stringliteral">"proofByContradiction: pfFalse = : "</span> + pfFalse.<a class="code" href="classCVC3_1_1Theorem.html#ac4b1c9570ffb9cc901627ef2abb9ff77">toString</a>());
<a name="l00079"></a>00079 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> not_a(!a);
<a name="l00080"></a>00080 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> assump(pfFalse.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>() - not_a);
<a name="l00081"></a>00081 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00082"></a>00082 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l00083"></a>00083 <span class="comment">// TODO: optimize with 1 traversal?</span>
<a name="l00084"></a>00084 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm(pfFalse.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>()[not_a]);
<a name="l00085"></a>00085 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> u; <span class="comment">// proof label for !aLFSCL</span>
<a name="l00086"></a>00086 <span class="keywordflow">if</span>(!thm.isNull()) u = thm.getProof();
<a name="l00087"></a>00087 <span class="comment">// Proof compaction: if u is Null, use "FALSE => A" rule</span>
<a name="l00088"></a>00088 <span class="keywordflow">if</span>(u.isNull()){
<a name="l00089"></a>00089 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"false_implies_anything"</span>, a, pfFalse.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00090"></a>00090 <span class="keywordflow">if</span>(!<a class="code" href="search__theorem__producer_8cpp.html#ad48a265d67710c19ae70a239a42cc9f3">lfsc_called</a>){
<a name="l00091"></a>00091 <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a211e687727973cff1b055a7302d562ae">satProof</a>(a, pf);
<a name="l00092"></a>00092 }
<a name="l00093"></a>00093 }
<a name="l00094"></a>00094 <span class="keywordflow">else</span>
<a name="l00095"></a>00095 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"pf_by_contradiction"</span>, a,
<a name="l00096"></a>00096 <span class="comment">// LAMBDA-abstraction (LAMBDA (u: !a): pfFalse)</span>
<a name="l00097"></a>00097 <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(u, not_a, pfFalse.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>()));
<a name="l00098"></a>00098 }
<a name="l00099"></a>00099 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(a, assump, pf);
<a name="l00100"></a>00100 }
<a name="l00101"></a>00101
<a name="l00102"></a>00102 <span class="comment">// Similar rule, only negation introduction:</span>
<a name="l00103"></a>00103 <span class="comment">// A |- FALSE ==> !A</span>
<a name="l00104"></a>00104 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00105"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a7f69d40a18ab9b66200d24ccc92c2ae9">00105</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a7f69d40a18ab9b66200d24ccc92c2ae9" title="Negation introduction: .">SearchEngineTheoremProducer::negIntro</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& not_a,
<a name="l00106"></a>00106 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& pfFalse) {
<a name="l00107"></a>00107 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00108"></a>00108 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(pfFalse.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#ga6173f64b22cba76472cd0c814bbf6dae">isFalse</a>(),
<a name="l00109"></a>00109 <span class="stringliteral">"negIntro: pfFalse = : "</span> + pfFalse.<a class="code" href="classCVC3_1_1Theorem.html#ac4b1c9570ffb9cc901627ef2abb9ff77">toString</a>());
<a name="l00110"></a>00110 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(not_a.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>(), <span class="stringliteral">"negIntro: not_a = "</span>+not_a.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00111"></a>00111 }
<a name="l00112"></a>00112
<a name="l00113"></a>00113 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> a(not_a[0]);
<a name="l00114"></a>00114 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> assump(pfFalse.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>() - a);
<a name="l00115"></a>00115 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00116"></a>00116 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l00117"></a>00117 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> thm(pfFalse.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>()[a]);
<a name="l00118"></a>00118 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> u; <span class="comment">// proof label for 'a'</span>
<a name="l00119"></a>00119 <span class="keywordflow">if</span>(!thm.isNull()) u = thm.getProof();
<a name="l00120"></a>00120 <span class="comment">// Proof compaction: if u is Null, use "FALSE => !A" rule</span>
<a name="l00121"></a>00121 <span class="keywordflow">if</span>(u.isNull())
<a name="l00122"></a>00122 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"false_implies_anything"</span>, not_a, pfFalse.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00123"></a>00123
<a name="l00124"></a>00124 <span class="keywordflow">else</span>
<a name="l00125"></a>00125 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"neg_intro"</span>, not_a,
<a name="l00126"></a>00126 <span class="comment">// LAMBDA-abstraction (LAMBDA (u: a): pfFalse)</span>
<a name="l00127"></a>00127 <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(u, a, pfFalse.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>()));
<a name="l00128"></a>00128 }
<a name="l00129"></a>00129 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(not_a, assump, pf);
<a name="l00130"></a>00130 }
<a name="l00131"></a>00131
<a name="l00132"></a>00132
<a name="l00133"></a>00133 <span class="comment">// Case split: u1:A |- C, u2:!A |- C ==> |- C</span>
<a name="l00134"></a>00134 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00135"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a68990fddbfff890590e69e239a3110fe">00135</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a68990fddbfff890590e69e239a3110fe" title="Case split: .">SearchEngineTheoremProducer::caseSplit</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& a,
<a name="l00136"></a>00136 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& a_proves_c,
<a name="l00137"></a>00137 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& not_a_proves_c) {
<a name="l00138"></a>00138 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> c(a_proves_c.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00139"></a>00139
<a name="l00140"></a>00140 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00141"></a>00141 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(c == not_a_proves_c.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(),
<a name="l00142"></a>00142 <span class="stringliteral">"caseSplit: conclusions differ:\n positive case C = "</span>
<a name="l00143"></a>00143 + c.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>() + <span class="stringliteral">"\n negative case C = "</span>
<a name="l00144"></a>00144 + not_a_proves_c.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00145"></a>00145 <span class="comment">// The opposite assumption should not appear in the theorems</span>
<a name="l00146"></a>00146 <span class="comment">// Actually, this doesn't violate soundness, no reason to check</span>
<a name="l00147"></a>00147 <span class="comment">// CHECK_SOUND(a_proves_c.getAssumptions()[!a].isNull(), </span>
<a name="l00148"></a>00148 <span class="comment">// "caseSplit: wrong assumption: " + (!a).toString()</span>
<a name="l00149"></a>00149 <span class="comment">// +"\n in "+a_proves_c.toString());</span>
<a name="l00150"></a>00150 <span class="comment">// CHECK_SOUND(not_a_proves_c.getAssumptions()[a].isNull(), </span>
<a name="l00151"></a>00151 <span class="comment">// "caseSplit: wrong assumption: " + a.toString()</span>
<a name="l00152"></a>00152 <span class="comment">// +"\n in "+not_a_proves_c.toString());</span>
<a name="l00153"></a>00153 }
<a name="l00154"></a>00154
<a name="l00155"></a>00155 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>& a1(a_proves_c.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>());
<a name="l00156"></a>00156 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>& a2(not_a_proves_c.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>());
<a name="l00157"></a>00157 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> a3 = a1 - a;
<a name="l00158"></a>00158 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> a4 = a2 - !a;
<a name="l00159"></a>00159
<a name="l00160"></a>00160 <span class="comment">// Proof compaction: if either theorem proves C without a or !a,</span>
<a name="l00161"></a>00161 <span class="comment">// then just use that theorem. This only works if assumptions are</span>
<a name="l00162"></a>00162 <span class="comment">// active.</span>
<a name="l00163"></a>00163
<a name="l00164"></a>00164 <span class="keywordflow">if</span> (a1 == a3) <span class="keywordflow">return</span> a_proves_c;
<a name="l00165"></a>00165 <span class="keywordflow">if</span> (a2 == a4) <span class="keywordflow">return</span> not_a_proves_c;
<a name="l00166"></a>00166
<a name="l00167"></a>00167 <span class="comment">// No easy way out. Do the work.</span>
<a name="l00168"></a>00168 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00169"></a>00169 a3.add(a4);
<a name="l00170"></a>00170
<a name="l00171"></a>00171 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l00172"></a>00172 <span class="comment">// Create lambda-abstractions</span>
<a name="l00173"></a>00173 vector<Proof> pfs;
<a name="l00174"></a>00174 pfs.push_back(<a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(a1[a].getProof(),
<a name="l00175"></a>00175 a, a_proves_c.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>()));
<a name="l00176"></a>00176 pfs.push_back(<a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(a2[!a].getProof(),
<a name="l00177"></a>00177 !a, not_a_proves_c.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>()));
<a name="l00178"></a>00178 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"case_split"</span>, a, c, pfs);
<a name="l00179"></a>00179 }
<a name="l00180"></a>00180 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(c, a3, pf);
<a name="l00181"></a>00181 }
<a name="l00182"></a>00182
<a name="l00183"></a>00183 <span class="comment">// Conflict clause rule: </span>
<a name="l00184"></a>00184 <span class="comment">// Gamma, A_1,...,A_n |- B ==> Gamma |- (OR B A_1 ... A_n)</span>
<a name="l00185"></a>00185 <span class="comment">// The assumptions A_i are given by the vector 'lits'.</span>
<a name="l00186"></a>00186 <span class="comment">// If B==FALSE, it is omitted from the result.</span>
<a name="l00187"></a>00187
<a name="l00188"></a>00188 <span class="comment">// NOTE: here "!A_i" means an inverse of A_i, not just a negation.</span>
<a name="l00189"></a>00189 <span class="comment">// That is, if A_i is NOT C, then !A_i is C.</span>
<a name="l00190"></a>00190
<a name="l00191"></a>00191 <span class="comment">// verification function used by conflictClause</span>
<a name="l00192"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#acaa4dd5cb5be1e9844e03c82feea84b6">00192</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#acaa4dd5cb5be1e9844e03c82feea84b6">SearchEngineTheoremProducer::verifyConflict</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm,
<a name="l00193"></a>00193 <a class="code" href="namespaceCVC3.html#ae8220d283ddfdaa8f4e0da0a03fa7ff4">TheoremMap</a>& m) {
<a name="l00194"></a>00194 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>& a(thm.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>());
<a name="l00195"></a>00195 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions_1_1iterator.html" title="Iterator for the Assumptions: points to class Theorem.">Assumptions::iterator</a> iend = a.end();
<a name="l00196"></a>00196 <span class="keywordflow">for</span> (<a class="code" href="classCVC3_1_1Assumptions_1_1iterator.html" title="Iterator for the Assumptions: points to class Theorem.">Assumptions::iterator</a> i = a.begin();
<a name="l00197"></a>00197 i != iend; ++i) {
<a name="l00198"></a>00198 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(!i->isNull(),
<a name="l00199"></a>00199 <span class="stringliteral">"SearchEngineTheoremProducer::conflictClause: "</span>
<a name="l00200"></a>00200 <span class="stringliteral">"Found null theorem"</span>);
<a name="l00201"></a>00201 <span class="keywordflow">if</span> (!i->isRefl() && !i->isFlagged()) {
<a name="l00202"></a>00202 i->setFlag();
<a name="l00203"></a>00203 <span class="keywordflow">if</span> (m.count(*i) == 0) {
<a name="l00204"></a>00204 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(!i->isAssump(),
<a name="l00205"></a>00205 <span class="stringliteral">"SearchEngineTheoremProducer::conflictClause: "</span>
<a name="l00206"></a>00206 <span class="stringliteral">"literal and gamma sets do not form a complete "</span>
<a name="l00207"></a>00207 <span class="stringliteral">"cut of Theorem assumptions. Stray theorem: \n"</span>
<a name="l00208"></a>00208 +i->toString());
<a name="l00209"></a>00209 <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#acaa4dd5cb5be1e9844e03c82feea84b6">verifyConflict</a>(*i, m);
<a name="l00210"></a>00210 }
<a name="l00211"></a>00211 <span class="keywordflow">else</span> {
<a name="l00212"></a>00212 m[*i] = <span class="keyword">true</span>;
<a name="l00213"></a>00213 }
<a name="l00214"></a>00214 }
<a name="l00215"></a>00215 }
<a name="l00216"></a>00216 }
<a name="l00217"></a>00217
<a name="l00218"></a>00218
<a name="l00219"></a>00219 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00220"></a>00220 <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#abf46962b0eb1ff204a5b321828139713" title="Conflict clause rule: .">SearchEngineTheoremProducer::</a>
<a name="l00221"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#abf46962b0eb1ff204a5b321828139713">00221</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#abf46962b0eb1ff204a5b321828139713" title="Conflict clause rule: .">conflictClause</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm, <span class="keyword">const</span> vector<Theorem>& lits,
<a name="l00222"></a>00222 <span class="keyword">const</span> vector<Theorem>& gamma) {
<a name="l00223"></a>00223 <span class="comment">// TRACE("search proofs", "conflictClause(", thm.getExpr(), ") {");</span>
<a name="l00224"></a>00224 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<span class="keywordflow">if</span>(debugger.trace(<span class="stringliteral">"search proofs"</span>)) {
<a name="l00225"></a>00225 ostream& os = debugger.getOS();
<a name="l00226"></a>00226 os << <span class="stringliteral">"lits = ["</span>;
<a name="l00227"></a>00227 <span class="keywordflow">for</span>(vector<Theorem>::const_iterator i=lits.begin(), iend=lits.end();
<a name="l00228"></a>00228 i!=iend; ++i)
<a name="l00229"></a>00229 os << i->getExpr() << <span class="stringliteral">",\n"</span>;
<a name="l00230"></a>00230 os << <span class="stringliteral">"]\n\ngamma = ["</span>;
<a name="l00231"></a>00231 <span class="keywordflow">for</span>(vector<Theorem>::const_iterator i=gamma.begin(), iend=gamma.end();
<a name="l00232"></a>00232 i!=iend; ++i)
<a name="l00233"></a>00233 os << i->getExpr() << <span class="stringliteral">",\n"</span>;
<a name="l00234"></a>00234 os << <span class="stringliteral">"]"</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00235"></a>00235 });
<a name="l00236"></a>00236 <span class="keywordtype">bool</span> checkProofs(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>);
<a name="l00237"></a>00237 <span class="comment">// This rule only makes sense when runnnig with assumptions</span>
<a name="l00238"></a>00238 <span class="keywordflow">if</span>(checkProofs) {
<a name="l00239"></a>00239 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(<a class="code" href="classCVC3_1_1TheoremProducer.html#a32afe6d99e661b5c70082036e40d48bc" title="Testing whether to generate assumptions.">withAssumptions</a>(),
<a name="l00240"></a>00240 <span class="stringliteral">"conflictClause: called while running without assumptions"</span>);
<a name="l00241"></a>00241 }
<a name="l00242"></a>00242
<a name="l00243"></a>00243 <span class="comment">// Assumptions aOrig(thm.getAssumptions());</span>
<a name="l00244"></a>00244
<a name="l00245"></a>00245 vector<Expr> literals;
<a name="l00246"></a>00246 vector<Proof> u; <span class="comment">// Vector of proof labels</span>
<a name="l00247"></a>00247 literals.reserve(lits.size() + 1);
<a name="l00248"></a>00248 u.reserve(lits.size());
<a name="l00249"></a>00249 <span class="keyword">const</span> vector<Theorem>::const_iterator iend = lits.end();
<a name="l00250"></a>00250 <span class="keywordflow">for</span>(vector<Theorem>::const_iterator i=lits.begin(); i!=iend; ++i) {
<a name="l00251"></a>00251 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> neg(i->getExpr().negate());
<a name="l00252"></a>00252
<a name="l00253"></a>00253 literals.push_back(neg);
<a name="l00254"></a>00254 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) u.push_back(i->getProof());
<a name="l00255"></a>00255 }
<a name="l00256"></a>00256
<a name="l00257"></a>00257 <span class="keywordflow">if</span>(checkProofs) {
<a name="l00258"></a>00258 <a class="code" href="namespaceCVC3.html#ae8220d283ddfdaa8f4e0da0a03fa7ff4">TheoremMap</a> m;
<a name="l00259"></a>00259 <span class="comment">// TRACE_MSG("search proofs", "adding gamma to m: {");</span>
<a name="l00260"></a>00260 <span class="keywordflow">for</span>(vector<Theorem>::const_iterator i = gamma.begin();
<a name="l00261"></a>00261 i != gamma.end(); ++i) {
<a name="l00262"></a>00262 <span class="comment">// TRACE("search proofs", "m[", *i, "]");</span>
<a name="l00263"></a>00263 m[*i] = <span class="keyword">false</span>;
<a name="l00264"></a>00264 }
<a name="l00265"></a>00265 <span class="comment">// TRACE_MSG("search proofs", "}");</span>
<a name="l00266"></a>00266
<a name="l00267"></a>00267 <span class="keywordflow">for</span>(vector<Theorem>::const_iterator i = lits.begin(); i!=iend; ++i) {
<a name="l00268"></a>00268 <span class="comment">// TRACE("search proofs", "check lit: ", *i, "");</span>
<a name="l00269"></a>00269 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(m.count(*i) == 0,
<a name="l00270"></a>00270 <span class="stringliteral">"SearchEngineTheoremProducer::conflictClause: "</span>
<a name="l00271"></a>00271 <span class="stringliteral">"literal and gamma sets are not disjoint: lit = "</span>
<a name="l00272"></a>00272 +i->toString());
<a name="l00273"></a>00273 m[*i] = <span class="keyword">false</span>;
<a name="l00274"></a>00274 }
<a name="l00275"></a>00275 thm.<a class="code" href="classCVC3_1_1Theorem.html#a621ab2150eedc0e3b38d34275ac206cd" title="Clear the flag attribute in all the theorems.">clearAllFlags</a>();
<a name="l00276"></a>00276 <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#acaa4dd5cb5be1e9844e03c82feea84b6">verifyConflict</a>(thm, m);
<a name="l00277"></a>00277 TheoremMap::iterator t = m.begin(), tend = m.end();
<a name="l00278"></a>00278 <span class="keywordflow">for</span> (; t != tend; ++t) {
<a name="l00279"></a>00279 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(t->second == <span class="keyword">true</span>,
<a name="l00280"></a>00280 <span class="stringliteral">"SearchEngineTheoremProducer::conflictClause: "</span>
<a name="l00281"></a>00281 <span class="stringliteral">"literal or gamma set contains extra element : "</span>
<a name="l00282"></a>00282 + t->first.toString());
<a name="l00283"></a>00283 }
<a name="l00284"></a>00284 }
<a name="l00285"></a>00285
<a name="l00286"></a>00286 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> a(gamma);
<a name="l00287"></a>00287
<a name="l00288"></a>00288 <span class="keywordflow">if</span>(!thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#ga6173f64b22cba76472cd0c814bbf6dae">isFalse</a>())
<a name="l00289"></a>00289 literals.push_back(thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00290"></a>00290
<a name="l00291"></a>00291 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00292"></a>00292 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l00293"></a>00293 <span class="keywordflow">if</span>(lits.size()>0) {
<a name="l00294"></a>00294 vector<Expr> assump;
<a name="l00295"></a>00295 <span class="comment">// If assumptions are not leaves, we need to create new</span>
<a name="l00296"></a>00296 <span class="comment">// variables for them and substitute them for their proofs in</span>
<a name="l00297"></a>00297 <span class="comment">// the proof term</span>
<a name="l00298"></a>00298 <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<Expr></a> subst;
<a name="l00299"></a>00299 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(u.size() == lits.size(), <span class="stringliteral">""</span>);
<a name="l00300"></a>00300 <span class="keywordflow">for</span>(<span class="keywordtype">size_t</span> i=0, iend=lits.size(); i<iend; ++i) {
<a name="l00301"></a>00301 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e(lits[i].getExpr());
<a name="l00302"></a>00302 assump.push_back(e);
<a name="l00303"></a>00303 <a class="code" href="classCVC3_1_1Proof.html">Proof</a>& v = u[i];
<a name="l00304"></a>00304 <span class="keywordflow">if</span>(!v.<a class="code" href="classCVC3_1_1Proof.html#a20cd8a5db4f7f07155464880300fb4c9">getExpr</a>().<a class="code" href="group__ExprPkg.html#ga55b6a203b4375e64598306596851d9ae">isVar</a>()) {
<a name="l00305"></a>00305 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> label = <a class="code" href="classCVC3_1_1TheoremProducer.html#af4bdd16428b49f295b3d21208dffc0cd" title="Create a new proof label (bound variable) for an assumption (formula)">newLabel</a>(e);
<a name="l00306"></a>00306 subst[v.<a class="code" href="classCVC3_1_1Proof.html#a20cd8a5db4f7f07155464880300fb4c9">getExpr</a>()] = label.<a class="code" href="classCVC3_1_1Proof.html#a20cd8a5db4f7f07155464880300fb4c9">getExpr</a>();
<a name="l00307"></a>00307 v = label;
<a name="l00308"></a>00308 }
<a name="l00309"></a>00309 }
<a name="l00310"></a>00310 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> body(thm.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00311"></a>00311 <span class="keywordflow">if</span>(!subst.<a class="code" href="classCVC3_1_1ExprHashMap.html#acacf635065039ccea5acb5b91dbaa4bb">empty</a>())
<a name="l00312"></a>00312 body = <a class="code" href="classCVC3_1_1Proof.html">Proof</a>(body.getExpr().substExpr(subst));
<a name="l00313"></a>00313 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"conflict_clause"</span>, <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(u, assump, body));
<a name="l00314"></a>00314 }
<a name="l00315"></a>00315 <span class="keywordflow">else</span>
<a name="l00316"></a>00316 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"false_to_empty_or"</span>, thm.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00317"></a>00317 }
<a name="l00318"></a>00318 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> res(<a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>, literals, <a class="code" href="classCVC3_1_1TheoremProducer.html#a1b706238281ad141a57363a6890f14a5">d_em</a>), a, pf));
<a name="l00319"></a>00319 <span class="comment">// TRACE("search proofs", "conflictClause => ", res.getExpr(), " }");</span>
<a name="l00320"></a>00320 <span class="keywordflow">return</span> res;
<a name="l00321"></a>00321 }
<a name="l00322"></a>00322
<a name="l00323"></a>00323
<a name="l00324"></a>00324 <span class="comment">// Theorem</span>
<a name="l00325"></a>00325 <span class="comment">// SearchEngineTheoremProducer::</span>
<a name="l00326"></a>00326 <span class="comment">// conflictClause(const Theorem& thm, const vector<Expr>& lits) {</span>
<a name="l00327"></a>00327 <span class="comment">// bool checkProofs(CHECK_PROOFS);</span>
<a name="l00328"></a>00328 <span class="comment">// // This rule only makes sense when runnnig with assumptions</span>
<a name="l00329"></a>00329 <span class="comment">// if(checkProofs) {</span>
<a name="l00330"></a>00330 <span class="comment">// CHECK_SOUND(withAssumptions(),</span>
<a name="l00331"></a>00331 <span class="comment">// "conflictClause: called while running without assumptions");</span>
<a name="l00332"></a>00332 <span class="comment">// }</span>
<a name="l00333"></a>00333
<a name="l00334"></a>00334 <span class="comment">// Assumptions aOrig(thm.getAssumptions());</span>
<a name="l00335"></a>00335
<a name="l00336"></a>00336 <span class="comment">// vector<Expr> literals;</span>
<a name="l00337"></a>00337 <span class="comment">// vector<Expr> negations;</span>
<a name="l00338"></a>00338 <span class="comment">// vector<Proof> u; // Vector of proof labels</span>
<a name="l00339"></a>00339 <span class="comment">// literals.reserve(lits.size() + 1);</span>
<a name="l00340"></a>00340 <span class="comment">// negations.reserve(lits.size());</span>
<a name="l00341"></a>00341 <span class="comment">// u.reserve(lits.size());</span>
<a name="l00342"></a>00342 <span class="comment">// for(vector<Expr>::const_iterator i=lits.begin(), iend=lits.end();</span>
<a name="l00343"></a>00343 <span class="comment">// i!=iend; ++i) {</span>
<a name="l00344"></a>00344 <span class="comment">// Expr neg(i->isNot()? (*i)[0] : !(*i));</span>
<a name="l00345"></a>00345 <span class="comment">// if(checkProofs)</span>
<a name="l00346"></a>00346 <span class="comment">// CHECK_SOUND(!aOrig[neg].isNull(), </span>
<a name="l00347"></a>00347 <span class="comment">// "SearchEngineTheoremProducer::conflictClause: "</span>
<a name="l00348"></a>00348 <span class="comment">// "literal is not in the set of assumptions: neg = "</span>
<a name="l00349"></a>00349 <span class="comment">// +neg.toString() + "\n Theorem = " + thm.toString());</span>
<a name="l00350"></a>00350 <span class="comment">// literals.push_back(*i);</span>
<a name="l00351"></a>00351 <span class="comment">// negations.push_back(neg);</span>
<a name="l00352"></a>00352 <span class="comment">// if(withProof()) u.push_back(aOrig[neg].getProof());</span>
<a name="l00353"></a>00353 <span class="comment">// }</span>
<a name="l00354"></a>00354
<a name="l00355"></a>00355 <span class="comment">// Assumptions a = aOrig - negations;</span>
<a name="l00356"></a>00356
<a name="l00357"></a>00357 <span class="comment">// if(!thm.getExpr().isFalse())</span>
<a name="l00358"></a>00358 <span class="comment">// literals.push_back(thm.getExpr());</span>
<a name="l00359"></a>00359
<a name="l00360"></a>00360 <span class="comment">// Proof pf;</span>
<a name="l00361"></a>00361 <span class="comment">// if(withProof()) {</span>
<a name="l00362"></a>00362 <span class="comment">// if(lits.size()>0)</span>
<a name="l00363"></a>00363 <span class="comment">// pf = newPf("conflict_clause", newPf(u, literals, thm.getProof()));</span>
<a name="l00364"></a>00364 <span class="comment">// else</span>
<a name="l00365"></a>00365 <span class="comment">// pf = newPf("false_to_empty_or", thm.getProof());</span>
<a name="l00366"></a>00366 <span class="comment">// }</span>
<a name="l00367"></a>00367 <span class="comment">// // Use ExprManager in newExpr, since literals may be empty</span>
<a name="l00368"></a>00368 <span class="comment">// return newTheorem(Expr(d_em, OR, literals), a, pf);</span>
<a name="l00369"></a>00369 <span class="comment">// }</span>
<a name="l00370"></a>00370
<a name="l00371"></a>00371
<a name="l00372"></a>00372 <span class="comment">// "Cut" rule: { G_i |- A_i }; G', { A_i } |- B ==> union(G_i)+G' |- B.</span>
<a name="l00373"></a>00373 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00374"></a>00374 <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a9be0036e770d071001f7afab845f0473" title="Cut rule: .">SearchEngineTheoremProducer::</a>
<a name="l00375"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a9be0036e770d071001f7afab845f0473">00375</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a9be0036e770d071001f7afab845f0473" title="Cut rule: .">cutRule</a>(<span class="keyword">const</span> vector<Theorem>& thmsA,
<a name="l00376"></a>00376 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& as_prove_b) {
<a name="l00377"></a>00377 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>)
<a name="l00378"></a>00378 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(<a class="code" href="classCVC3_1_1TheoremProducer.html#a32afe6d99e661b5c70082036e40d48bc" title="Testing whether to generate assumptions.">withAssumptions</a>(),
<a name="l00379"></a>00379 <span class="stringliteral">"cutRule called without assumptions activated"</span>);
<a name="l00380"></a>00380 <span class="comment">// Optimization: use only those theorems that occur in B's assumptions.</span>
<a name="l00381"></a>00381 <span class="comment">// *** No, take it back, it's a mis-optimization. Most of the time,</span>
<a name="l00382"></a>00382 <span class="comment">// cutRule is applied when we *know* thmsA are present in the</span>
<a name="l00383"></a>00383 <span class="comment">// assumptions of 'as_proof_b'.</span>
<a name="l00384"></a>00384
<a name="l00385"></a>00385 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00386"></a>00386 vector<Expr> exprs;
<a name="l00387"></a>00387 exprs.reserve(thmsA.size() + 1);
<a name="l00388"></a>00388 <span class="keyword">const</span> vector<Theorem>::const_iterator iend = thmsA.end();
<a name="l00389"></a>00389 <span class="keywordflow">for</span>(vector<Theorem>::const_iterator i=thmsA.begin(); i!=iend; ++i) {
<a name="l00390"></a>00390 exprs.push_back(i->getExpr());
<a name="l00391"></a>00391 }
<a name="l00392"></a>00392
<a name="l00393"></a>00393 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> a(thmsA); <span class="comment">// add the As</span>
<a name="l00394"></a>00394 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(as_prove_b.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>() - exprs); <span class="comment">// Add G'</span>
<a name="l00395"></a>00395
<a name="l00396"></a>00396 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l00397"></a>00397 vector<Proof> pfs;
<a name="l00398"></a>00398 pfs.reserve(thmsA.size() + 1);
<a name="l00399"></a>00399 <span class="keywordflow">for</span>(vector<Theorem>::const_iterator i = thmsA.begin(); i != iend; ++i) {
<a name="l00400"></a>00400 pfs.push_back(i->getProof());
<a name="l00401"></a>00401 }
<a name="l00402"></a>00402 exprs.push_back(as_prove_b.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00403"></a>00403 pfs.push_back(as_prove_b.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00404"></a>00404 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"cut_rule"</span>,exprs,pfs);
<a name="l00405"></a>00405 }
<a name="l00406"></a>00406 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(as_prove_b.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(), a, pf);
<a name="l00407"></a>00407 }
<a name="l00408"></a>00408
<a name="l00409"></a>00409
<a name="l00410"></a>00410 <span class="keywordtype">void</span>
<a name="l00411"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#aa12792d6b382598a0f5aeea983568a23">00411</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#aa12792d6b382598a0f5aeea983568a23">SearchEngineTheoremProducer::checkSoundNoSkolems</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e,
<a name="l00412"></a>00412 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a>& visited,
<a name="l00413"></a>00413 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a>& skolems)
<a name="l00414"></a>00414 {
<a name="l00415"></a>00415 <span class="keywordflow">if</span>(visited.<a class="code" href="classCVC3_1_1ExprMap.html#aa96dfa3a54a131cdb0964ef4b80e324f">count</a>(e)>0)
<a name="l00416"></a>00416 <span class="keywordflow">return</span>;
<a name="l00417"></a>00417 <span class="keywordflow">else</span>
<a name="l00418"></a>00418 visited[e] = <span class="keyword">true</span>;
<a name="l00419"></a>00419 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(skolems.<a class="code" href="classCVC3_1_1ExprMap.html#aa96dfa3a54a131cdb0964ef4b80e324f">count</a>(e) == 0,
<a name="l00420"></a>00420 <span class="stringliteral">"skolem constant found in axioms of false theorem: "</span>
<a name="l00421"></a>00421 + e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00422"></a>00422 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> it = e.<a class="code" href="group__ExprPkg.html#gac890e13db184610276fc533fa4b4fe99" title="Begin iterator.">begin</a>(), end = e.<a class="code" href="group__ExprPkg.html#gaf6048a5030c8fa2511bf5dfee868e653" title="End iterator.">end</a>(); it!= end; ++it)
<a name="l00423"></a>00423 <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#aa12792d6b382598a0f5aeea983568a23">checkSoundNoSkolems</a>(*it, visited, skolems);
<a name="l00424"></a>00424 <span class="keywordflow">if</span>(e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7b7b6f6e2b88589bd4656a14bcb7eb94">FORALL</a> || e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3197625a1bb2264943f5a95f236d9973">EXISTS</a>)
<a name="l00425"></a>00425 <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#aa12792d6b382598a0f5aeea983568a23">checkSoundNoSkolems</a>(e.<a class="code" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940" title="Get the body of the closure Expr.">getBody</a>(), visited, skolems);
<a name="l00426"></a>00426 }
<a name="l00427"></a>00427
<a name="l00428"></a>00428 <span class="keywordtype">void</span>
<a name="l00429"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#aecd6425dded4edb62daefa858e969cf8">00429</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#aa12792d6b382598a0f5aeea983568a23">SearchEngineTheoremProducer::checkSoundNoSkolems</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t,
<a name="l00430"></a>00430 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a>& visited,
<a name="l00431"></a>00431 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a>& skolems)
<a name="l00432"></a>00432 {
<a name="l00433"></a>00433 <span class="keywordflow">if</span>(t.<a class="code" href="classCVC3_1_1Theorem.html#a16f074e60b9e076187efb478889d2c47">isRefl</a>() || t.<a class="code" href="classCVC3_1_1Theorem.html#a1695c9afc9a5c1f8cd000d40b9e2a9cd" title="Check if the flag attribute is set.">isFlagged</a>())
<a name="l00434"></a>00434 <span class="keywordflow">return</span>;
<a name="l00435"></a>00435 t.<a class="code" href="classCVC3_1_1Theorem.html#af83d6b4d71bfb558296a1c296a69c3d7" title="Set the flag attribute.">setFlag</a>();
<a name="l00436"></a>00436 <span class="keywordflow">if</span>(t.<a class="code" href="classCVC3_1_1Theorem.html#a05282db6832afb4f198d8c6b2b67aeb1">isAssump</a>())
<a name="l00437"></a>00437 <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#aa12792d6b382598a0f5aeea983568a23">checkSoundNoSkolems</a>(t.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(), visited, skolems);
<a name="l00438"></a>00438 <span class="keywordflow">else</span>
<a name="l00439"></a>00439 {
<a name="l00440"></a>00440 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>& a(t.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>());
<a name="l00441"></a>00441 <a class="code" href="classCVC3_1_1Assumptions_1_1iterator.html" title="Iterator for the Assumptions: points to class Theorem.">Assumptions::iterator</a> it = a.begin(), end = a.end();
<a name="l00442"></a>00442 <span class="keywordflow">for</span>(; it!=end; ++it)
<a name="l00443"></a>00443 <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#aa12792d6b382598a0f5aeea983568a23">checkSoundNoSkolems</a>(*it, visited, skolems);
<a name="l00444"></a>00444 }
<a name="l00445"></a>00445 }
<a name="l00446"></a>00446 <span class="comment"></span>
<a name="l00447"></a>00447 <span class="comment">/*! Eliminate skolem axioms: </span>
<a name="l00448"></a>00448 <span class="comment"> * Gamma, Delta |- false => Gamma|- false </span>
<a name="l00449"></a>00449 <span class="comment"> * where Delta is a set of skolem axioms {|-Exists(x) phi (x) => phi(c)}</span>
<a name="l00450"></a>00450 <span class="comment"> * and gamma does not contain any of the skolem constants c.</span>
<a name="l00451"></a>00451 <span class="comment"> */</span>
<a name="l00452"></a>00452
<a name="l00453"></a>00453 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00454"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#ac980b63fbd08b0e29b1092ed4aeb95e8">00454</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#ac980b63fbd08b0e29b1092ed4aeb95e8">SearchEngineTheoremProducer::eliminateSkolemAxioms</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& tFalse,
<a name="l00455"></a>00455 <span class="keyword">const</span> std::vector<Theorem>& delta)
<a name="l00456"></a>00456 {
<a name="l00457"></a>00457 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"skolem"</span>, <span class="stringliteral">"=>eliminateSkolemAxioms "</span>, delta.size(), <span class="stringliteral">"{"</span>);
<a name="l00458"></a>00458 <span class="keywordflow">if</span>(delta.empty())
<a name="l00459"></a>00459 {
<a name="l00460"></a>00460 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"skolem"</span>, <span class="stringliteral">"eliminateSkolemAxioms"</span>,<span class="stringliteral">""</span> , <span class="stringliteral">"}"</span>);
<a name="l00461"></a>00461 <span class="keywordflow">return</span> tFalse;
<a name="l00462"></a>00462 }
<a name="l00463"></a>00463 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& falseExpr = tFalse.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>();
<a name="l00464"></a>00464 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00465"></a>00465 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(falseExpr.<a class="code" href="group__ExprPkg.html#ga6173f64b22cba76472cd0c814bbf6dae">isFalse</a>(),
<a name="l00466"></a>00466 <span class="stringliteral">"eliminateSkolemAxiom called on non-false theorem"</span>);
<a name="l00467"></a>00467 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> visited;
<a name="l00468"></a>00468 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> skolems;
<a name="l00469"></a>00469 vector<Theorem>::const_iterator it = delta.<a class="code" href="classCVC3_1_1ExprMap.html#a3db85401f8535daf4054fde531cd46b1">begin</a>(), end = delta.end();
<a name="l00470"></a>00470 <span class="keywordflow">for</span>(; it!=end; ++it) {
<a name="l00471"></a>00471 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(it->isRewrite(),
<a name="l00472"></a>00472 <span class="stringliteral">"eliminateSkolemAxioms(): Skolem axiom is not "</span>
<a name="l00473"></a>00473 <span class="stringliteral">"an IFF: "</span>+it->toString());
<a name="l00474"></a>00474 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& ex = it->getLHS();
<a name="l00475"></a>00475 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(ex.isExists(),
<a name="l00476"></a>00476 <span class="stringliteral">"Did not receive skolem axioms in Delta"</span>
<a name="l00477"></a>00477 <span class="stringliteral">" of eliminateSkolemAxioms"</span> + it->toString());
<a name="l00478"></a>00478 <span class="comment">// Collect the Skolem constants for further soundness checks</span>
<a name="l00479"></a>00479 <span class="keywordflow">for</span>(<span class="keywordtype">unsigned</span> <span class="keywordtype">int</span> j=0; j<ex.getVars().size(); j++) {
<a name="l00480"></a>00480 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> sk_var(ex.skolemExpr(j));
<a name="l00481"></a>00481 <span class="keywordflow">if</span>(sk_var.getType().isBool()) {
<a name="l00482"></a>00482 sk_var = <a class="code" href="classCVC3_1_1TheoremProducer.html#a1b706238281ad141a57363a6890f14a5">d_em</a>-><a class="code" href="group__EM__Priv.html#gacd77df1dbcc429e06a75047e2f609822">newLeafExpr</a>(sk_var.mkOp());
<a name="l00483"></a>00483 }
<a name="l00484"></a>00484 skolems[sk_var] = <span class="keyword">true</span>;
<a name="l00485"></a>00485 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"skolem"</span>, <span class="stringliteral">">> Eliminating variable: "</span>, sk_var, <span class="stringliteral">"<<"</span>);
<a name="l00486"></a>00486 }
<a name="l00487"></a>00487 }
<a name="l00488"></a>00488 tFalse.<a class="code" href="classCVC3_1_1Theorem.html#a621ab2150eedc0e3b38d34275ac206cd" title="Clear the flag attribute in all the theorems.">clearAllFlags</a>();
<a name="l00489"></a>00489 <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#aa12792d6b382598a0f5aeea983568a23">checkSoundNoSkolems</a>(tFalse, visited, skolems);
<a name="l00490"></a>00490 }
<a name="l00491"></a>00491 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00492"></a>00492 <span class="keywordflow">if</span>(!<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) <span class="keywordflow">return</span> tFalse;
<a name="l00493"></a>00493 <span class="keywordflow">else</span>
<a name="l00494"></a>00494 {
<a name="l00495"></a>00495 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> origFalse = tFalse.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>();
<a name="l00496"></a>00496 std::vector<Proof>skolemizeLabels;
<a name="l00497"></a>00497 std::vector<Expr> exprs;
<a name="l00498"></a>00498 <span class="keywordflow">for</span>(<span class="keywordtype">unsigned</span> <span class="keywordtype">int</span> i=0; i<delta.size(); i++)
<a name="l00499"></a>00499 {
<a name="l00500"></a>00500 exprs.push_back(delta[i].getExpr());
<a name="l00501"></a>00501 skolemizeLabels.push_back(delta[i].getProof());
<a name="l00502"></a>00502 }
<a name="l00503"></a>00503 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(skolemizeLabels, exprs, origFalse);
<a name="l00504"></a>00504 }
<a name="l00505"></a>00505 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"skolem"</span>, <span class="stringliteral">"eliminateSkolemAxioms"</span>,<span class="stringliteral">""</span> , <span class="stringliteral">"}"</span>);
<a name="l00506"></a>00506 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(tFalse.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(), tFalse.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>(), pf);
<a name="l00507"></a>00507 }
<a name="l00508"></a>00508
<a name="l00509"></a>00509
<a name="l00510"></a>00510 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00511"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#af764cf6eae285f0dbd3d430b76c5e19d">00511</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#af764cf6eae285f0dbd3d430b76c5e19d" title="Unit propagation rule: .">SearchEngineTheoremProducer::unitProp</a>(<span class="keyword">const</span> std::vector<Theorem>& thms,
<a name="l00512"></a>00512 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& clause,
<a name="l00513"></a>00513 <span class="keywordtype">unsigned</span> i) {
<a name="l00514"></a>00514 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e(clause.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00515"></a>00515 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00516"></a>00516 <span class="comment">// Soundness check: first, check the form of the 'clause' theorem</span>
<a name="l00517"></a>00517 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(e.isOr() && e.arity() > (int)i,
<a name="l00518"></a>00518 <span class="stringliteral">"SearchEngineTheoremProducer::unitProp: bad theorem or i="</span>
<a name="l00519"></a>00519 +<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(i)+<span class="stringliteral">" > arity="</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(e.arity())
<a name="l00520"></a>00520 +<span class="stringliteral">" in clause = "</span> + clause.<a class="code" href="classCVC3_1_1Theorem.html#ac4b1c9570ffb9cc901627ef2abb9ff77">toString</a>());
<a name="l00521"></a>00521 <span class="comment">// Now, check correspondence of thms to the disjunction</span>
<a name="l00522"></a>00522 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(((<span class="keywordtype">int</span>)thms.size()) == e.arity() - 1,
<a name="l00523"></a>00523 <span class="stringliteral">"SearchEngineTheoremProducer::unitProp: "</span>
<a name="l00524"></a>00524 <span class="stringliteral">"wrong number of theorems"</span>
<a name="l00525"></a>00525 <span class="stringliteral">"\n thms.size = "</span> + <a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(thms.size())
<a name="l00526"></a>00526 +<span class="stringliteral">"\n clause.arity = "</span> + <a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(e.arity()));
<a name="l00527"></a>00527
<a name="l00528"></a>00528 <span class="keywordflow">for</span>(<span class="keywordtype">unsigned</span> j=0,k=0; j<thms.size(); j++) {
<a name="l00529"></a>00529 <span class="keywordflow">if</span>(j!=i) {
<a name="l00530"></a>00530 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> ej(e[j]), ek(thms[k].getExpr());
<a name="l00531"></a>00531 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>((ej.isNot() && ej[0] == ek) || (ek.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() && ej == ek[0]),
<a name="l00532"></a>00532 <span class="stringliteral">"SearchEngineTheoremProducer::unitProp: "</span>
<a name="l00533"></a>00533 <span class="stringliteral">"wrong theorem["</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(k)+<span class="stringliteral">"]"</span>
<a name="l00534"></a>00534 <span class="stringliteral">"\n thm = "</span> + thms[k].toString() +
<a name="l00535"></a>00535 <span class="stringliteral">"\n literal = "</span> + e[j].toString() +
<a name="l00536"></a>00536 <span class="stringliteral">"\n clause = "</span> + clause.<a class="code" href="classCVC3_1_1Theorem.html#ac4b1c9570ffb9cc901627ef2abb9ff77">toString</a>());
<a name="l00537"></a>00537 k++;
<a name="l00538"></a>00538 }
<a name="l00539"></a>00539 }
<a name="l00540"></a>00540 }
<a name="l00541"></a>00541
<a name="l00542"></a>00542 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> a(thms);
<a name="l00543"></a>00543 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(clause);
<a name="l00544"></a>00544 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00545"></a>00545
<a name="l00546"></a>00546 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l00547"></a>00547 vector<Proof> pfs;
<a name="l00548"></a>00548 vector<Expr> exprs;
<a name="l00549"></a>00549 exprs.reserve(thms.size() + 1);
<a name="l00550"></a>00550 pfs.reserve(thms.size()+1);
<a name="l00551"></a>00551 <span class="keyword">const</span> vector<Theorem>::const_iterator iend = thms.end();
<a name="l00552"></a>00552 <span class="keywordflow">for</span>(vector<Theorem>::const_iterator i=thms.begin(); i!=iend; ++i) {
<a name="l00553"></a>00553 exprs.push_back(i->getExpr());
<a name="l00554"></a>00554 pfs.push_back(i->getProof());
<a name="l00555"></a>00555 }
<a name="l00556"></a>00556 exprs.push_back(clause.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00557"></a>00557 pfs.push_back(clause.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00558"></a>00558 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"unit_prop"</span>, exprs, pfs);
<a name="l00559"></a>00559 }
<a name="l00560"></a>00560 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(e[i], a, pf);
<a name="l00561"></a>00561 }
<a name="l00562"></a>00562
<a name="l00563"></a>00563 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00564"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a1d0f21b895fc25bff5dc653490a775c0">00564</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a1d0f21b895fc25bff5dc653490a775c0">SearchEngineTheoremProducer::propAndrAF</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& andr_th,
<a name="l00565"></a>00565 <span class="keywordtype">bool</span> <a class="code" href="namespaceMiniSat.html#ad93cb56673487974071ed3b75bf4ea83">left</a>,
<a name="l00566"></a>00566 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& b_th) {
<a name="l00567"></a>00567 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& andr_e(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00568"></a>00568 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00569"></a>00569 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(andr_e.getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf18208f4921c8175373d32e4ce909d42">AND_R</a> &&
<a name="l00570"></a>00570 ((left && b_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(andr_e[1])) ||
<a name="l00571"></a>00571 (!left && b_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(andr_e[2]))),
<a name="l00572"></a>00572 <span class="stringliteral">"SearchEngineTheoremProducer::propAndrAF"</span>);
<a name="l00573"></a>00573 }
<a name="l00574"></a>00574
<a name="l00575"></a>00575 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> a(andr_th, b_th);
<a name="l00576"></a>00576 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00577"></a>00577
<a name="l00578"></a>00578 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l00579"></a>00579 vector<Proof> pfs;
<a name="l00580"></a>00580 vector<Expr> exprs;
<a name="l00581"></a>00581 exprs.push_back(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00582"></a>00582 exprs.push_back(b_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00583"></a>00583 pfs.push_back(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00584"></a>00584 pfs.push_back(b_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00585"></a>00585 <span class="comment">// can we note which branch to take?</span>
<a name="l00586"></a>00586 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"prop_andr_af"</span>, exprs, pfs);
<a name="l00587"></a>00587 }
<a name="l00588"></a>00588
<a name="l00589"></a>00589 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(andr_e[0].negate(), a, pf);
<a name="l00590"></a>00590 }
<a name="l00591"></a>00591
<a name="l00592"></a>00592 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00593"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a22c592b3807cddf270b7be995594d58a">00593</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a22c592b3807cddf270b7be995594d58a">SearchEngineTheoremProducer::propAndrAT</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& andr_th,
<a name="l00594"></a>00594 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& l_th,
<a name="l00595"></a>00595 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& r_th) {
<a name="l00596"></a>00596 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& andr_e(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00597"></a>00597 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00598"></a>00598 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(andr_e.getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf18208f4921c8175373d32e4ce909d42">AND_R</a> &&
<a name="l00599"></a>00599 l_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(andr_e[1]) && r_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(andr_e[2]),
<a name="l00600"></a>00600 <span class="stringliteral">"SearchEngineTheoremProducer::propAndrAT"</span>);
<a name="l00601"></a>00601 }
<a name="l00602"></a>00602
<a name="l00603"></a>00603 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> a(andr_th, l_th);
<a name="l00604"></a>00604 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(r_th);
<a name="l00605"></a>00605 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00606"></a>00606
<a name="l00607"></a>00607 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l00608"></a>00608 vector<Proof> pfs;
<a name="l00609"></a>00609 vector<Expr> exprs;
<a name="l00610"></a>00610 exprs.push_back(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00611"></a>00611 exprs.push_back(l_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00612"></a>00612 exprs.push_back(r_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00613"></a>00613 pfs.push_back(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00614"></a>00614 pfs.push_back(l_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00615"></a>00615 pfs.push_back(r_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00616"></a>00616 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"prop_andr_at"</span>, exprs, pfs);
<a name="l00617"></a>00617 }
<a name="l00618"></a>00618
<a name="l00619"></a>00619 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(andr_e[0], a, pf);
<a name="l00620"></a>00620 }
<a name="l00621"></a>00621
<a name="l00622"></a>00622 <span class="keywordtype">void</span>
<a name="l00623"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a1bdf01b6d0e85d8c91a2fa3aaf0704c6">00623</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a1bdf01b6d0e85d8c91a2fa3aaf0704c6">SearchEngineTheoremProducer::propAndrLRT</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& andr_th,
<a name="l00624"></a>00624 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& a_th,
<a name="l00625"></a>00625 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>* l_th,
<a name="l00626"></a>00626 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>* r_th) {
<a name="l00627"></a>00627 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& andr_e(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00628"></a>00628 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00629"></a>00629 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(andr_e.getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf18208f4921c8175373d32e4ce909d42">AND_R</a> && a_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(andr_e[0]),
<a name="l00630"></a>00630 <span class="stringliteral">"SearchEngineTheoremProducer::propAndrLRT"</span>);
<a name="l00631"></a>00631 }
<a name="l00632"></a>00632
<a name="l00633"></a>00633 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> a(andr_th, a_th);
<a name="l00634"></a>00634 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00635"></a>00635
<a name="l00636"></a>00636 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l00637"></a>00637 vector<Proof> pfs;
<a name="l00638"></a>00638 vector<Expr> exprs;
<a name="l00639"></a>00639 exprs.push_back(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00640"></a>00640 exprs.push_back(a_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00641"></a>00641 pfs.push_back(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00642"></a>00642 pfs.push_back(a_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00643"></a>00643 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"prop_andr_lrt"</span>, exprs, pfs);
<a name="l00644"></a>00644 }
<a name="l00645"></a>00645
<a name="l00646"></a>00646 <span class="keywordflow">if</span> (l_th) *l_th = <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(andr_e[1], a, pf);
<a name="l00647"></a>00647 <span class="keywordflow">if</span> (r_th) *r_th = <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(andr_e[2], a, pf);
<a name="l00648"></a>00648 }
<a name="l00649"></a>00649
<a name="l00650"></a>00650 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00651"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a373b85c528799a04c9997f8f0b1349d6">00651</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a373b85c528799a04c9997f8f0b1349d6">SearchEngineTheoremProducer::propAndrLF</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& andr_th,
<a name="l00652"></a>00652 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& a_th,
<a name="l00653"></a>00653 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& r_th) {
<a name="l00654"></a>00654 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& andr_e(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00655"></a>00655 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00656"></a>00656 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(andr_e.getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf18208f4921c8175373d32e4ce909d42">AND_R</a> &&
<a name="l00657"></a>00657 a_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(andr_e[0]) && r_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(andr_e[2]),
<a name="l00658"></a>00658 <span class="stringliteral">"SearchEngineTheoremProducer::propAndrLF"</span>);
<a name="l00659"></a>00659 }
<a name="l00660"></a>00660
<a name="l00661"></a>00661 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> a(andr_th, a_th);
<a name="l00662"></a>00662 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(r_th);
<a name="l00663"></a>00663 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00664"></a>00664
<a name="l00665"></a>00665 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l00666"></a>00666 vector<Proof> pfs;
<a name="l00667"></a>00667 vector<Expr> exprs;
<a name="l00668"></a>00668 exprs.push_back(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00669"></a>00669 exprs.push_back(a_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00670"></a>00670 exprs.push_back(r_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00671"></a>00671 pfs.push_back(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00672"></a>00672 pfs.push_back(a_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00673"></a>00673 pfs.push_back(r_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00674"></a>00674 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"prop_andr_lf"</span>, exprs, pfs);
<a name="l00675"></a>00675 }
<a name="l00676"></a>00676
<a name="l00677"></a>00677 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(andr_e[1].negate(), a, pf);
<a name="l00678"></a>00678 }
<a name="l00679"></a>00679
<a name="l00680"></a>00680 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00681"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a948eaf2519eb12dd8f76c3c890babd78">00681</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a948eaf2519eb12dd8f76c3c890babd78">SearchEngineTheoremProducer::propAndrRF</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& andr_th,
<a name="l00682"></a>00682 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& a_th,
<a name="l00683"></a>00683 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& l_th) {
<a name="l00684"></a>00684 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& andr_e(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00685"></a>00685 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00686"></a>00686 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(andr_e.getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf18208f4921c8175373d32e4ce909d42">AND_R</a> &&
<a name="l00687"></a>00687 a_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(andr_e[0]) && l_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(andr_e[1]),
<a name="l00688"></a>00688 <span class="stringliteral">"SearchEngineTheoremProducer::propAndrRF"</span>);
<a name="l00689"></a>00689 }
<a name="l00690"></a>00690
<a name="l00691"></a>00691 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> a(andr_th, a_th);
<a name="l00692"></a>00692 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(l_th);
<a name="l00693"></a>00693 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00694"></a>00694
<a name="l00695"></a>00695 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l00696"></a>00696 vector<Proof> pfs;
<a name="l00697"></a>00697 vector<Expr> exprs;
<a name="l00698"></a>00698 exprs.push_back(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00699"></a>00699 exprs.push_back(a_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00700"></a>00700 exprs.push_back(l_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00701"></a>00701 pfs.push_back(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00702"></a>00702 pfs.push_back(a_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00703"></a>00703 pfs.push_back(l_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00704"></a>00704 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"prop_andr_rf"</span>, exprs, pfs);
<a name="l00705"></a>00705 }
<a name="l00706"></a>00706
<a name="l00707"></a>00707 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(andr_e[2].negate(), a, pf);
<a name="l00708"></a>00708 }
<a name="l00709"></a>00709
<a name="l00710"></a>00710 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00711"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a8b6dd7f1001b52a5be21914e1ecf6da0">00711</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a8b6dd7f1001b52a5be21914e1ecf6da0">SearchEngineTheoremProducer::confAndrAT</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& andr_th,
<a name="l00712"></a>00712 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& a_th,
<a name="l00713"></a>00713 <span class="keywordtype">bool</span> <a class="code" href="namespaceMiniSat.html#ad93cb56673487974071ed3b75bf4ea83">left</a>,
<a name="l00714"></a>00714 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& b_th) {
<a name="l00715"></a>00715 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& andr_e(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00716"></a>00716 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00717"></a>00717 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(andr_e.getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf18208f4921c8175373d32e4ce909d42">AND_R</a> && a_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(andr_e[0]) &&
<a name="l00718"></a>00718 ((left && b_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(andr_e[1])) ||
<a name="l00719"></a>00719 (!left && b_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(andr_e[2]))),
<a name="l00720"></a>00720 <span class="stringliteral">"SearchEngineTheoremProducer::confAndrAT"</span>);
<a name="l00721"></a>00721 }
<a name="l00722"></a>00722
<a name="l00723"></a>00723 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> a(andr_th, a_th);
<a name="l00724"></a>00724 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(b_th);
<a name="l00725"></a>00725 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00726"></a>00726
<a name="l00727"></a>00727 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l00728"></a>00728 vector<Proof> pfs;
<a name="l00729"></a>00729 vector<Expr> exprs;
<a name="l00730"></a>00730 exprs.push_back(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00731"></a>00731 exprs.push_back(a_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00732"></a>00732 exprs.push_back(b_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00733"></a>00733 pfs.push_back(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00734"></a>00734 pfs.push_back(a_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00735"></a>00735 pfs.push_back(b_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00736"></a>00736 <span class="comment">// can we note which branch to take?</span>
<a name="l00737"></a>00737 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"conf_andr_at"</span>, exprs, pfs);
<a name="l00738"></a>00738 }
<a name="l00739"></a>00739
<a name="l00740"></a>00740 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(<a class="code" href="classCVC3_1_1TheoremProducer.html#a1b706238281ad141a57363a6890f14a5">d_em</a>-><a class="code" href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae" title="FALSE Expr.">falseExpr</a>(), a, pf);
<a name="l00741"></a>00741 }
<a name="l00742"></a>00742
<a name="l00743"></a>00743 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00744"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a09acd80b1c336ac225de0a71bee0d4c8">00744</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a09acd80b1c336ac225de0a71bee0d4c8">SearchEngineTheoremProducer::confAndrAF</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& andr_th,
<a name="l00745"></a>00745 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& a_th,
<a name="l00746"></a>00746 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& l_th,
<a name="l00747"></a>00747 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& r_th) {
<a name="l00748"></a>00748 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& andr_e(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00749"></a>00749 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00750"></a>00750 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(andr_e.getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5baf18208f4921c8175373d32e4ce909d42">AND_R</a> && a_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(andr_e[0]) &&
<a name="l00751"></a>00751 l_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(andr_e[1]) && r_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(andr_e[2]),
<a name="l00752"></a>00752 <span class="stringliteral">"SearchEngineTheoremProducer::confAndrAF"</span>);
<a name="l00753"></a>00753 }
<a name="l00754"></a>00754
<a name="l00755"></a>00755 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> a;
<a name="l00756"></a>00756 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00757"></a>00757 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#a32afe6d99e661b5c70082036e40d48bc" title="Testing whether to generate assumptions.">withAssumptions</a>()) {
<a name="l00758"></a>00758 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(andr_th);
<a name="l00759"></a>00759 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(a_th);
<a name="l00760"></a>00760 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(l_th);
<a name="l00761"></a>00761 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(r_th);
<a name="l00762"></a>00762 }
<a name="l00763"></a>00763
<a name="l00764"></a>00764 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l00765"></a>00765 vector<Proof> pfs;
<a name="l00766"></a>00766 vector<Expr> exprs;
<a name="l00767"></a>00767 exprs.push_back(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00768"></a>00768 exprs.push_back(a_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00769"></a>00769 exprs.push_back(l_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00770"></a>00770 exprs.push_back(r_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00771"></a>00771 pfs.push_back(andr_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00772"></a>00772 pfs.push_back(a_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00773"></a>00773 pfs.push_back(l_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00774"></a>00774 pfs.push_back(r_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00775"></a>00775 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"conf_andr_af"</span>, exprs, pfs);
<a name="l00776"></a>00776 }
<a name="l00777"></a>00777
<a name="l00778"></a>00778 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(<a class="code" href="classCVC3_1_1TheoremProducer.html#a1b706238281ad141a57363a6890f14a5">d_em</a>-><a class="code" href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae" title="FALSE Expr.">falseExpr</a>(), a, pf);
<a name="l00779"></a>00779 }
<a name="l00780"></a>00780
<a name="l00781"></a>00781 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00782"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#afb6d1f50a0b2cf48bf98517731160595">00782</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#afb6d1f50a0b2cf48bf98517731160595">SearchEngineTheoremProducer::propIffr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& iffr_th,
<a name="l00783"></a>00783 <span class="keywordtype">int</span> p,
<a name="l00784"></a>00784 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& a_th,
<a name="l00785"></a>00785 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& b_th)
<a name="l00786"></a>00786 {
<a name="l00787"></a>00787 <span class="keywordtype">int</span> a(-1), b(-1);
<a name="l00788"></a>00788 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>)
<a name="l00789"></a>00789 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(p == 0 || p == 1 || p == 2,
<a name="l00790"></a>00790 <span class="stringliteral">"SearchEngineTheoremProducer::propIffr: p="</span>
<a name="l00791"></a>00791 +<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(p));
<a name="l00792"></a>00792 <span class="keywordflow">switch</span> (p) {
<a name="l00793"></a>00793 <span class="keywordflow">case</span> 0: a = 1; b = 2; <span class="keywordflow">break</span>;
<a name="l00794"></a>00794 <span class="keywordflow">case</span> 1: a = 0; b = 2; <span class="keywordflow">break</span>;
<a name="l00795"></a>00795 <span class="keywordflow">case</span> 2: a = 0; b = 1; <span class="keywordflow">break</span>;
<a name="l00796"></a>00796 }
<a name="l00797"></a>00797
<a name="l00798"></a>00798 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& iffr_e(iffr_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00799"></a>00799
<a name="l00800"></a>00800 <span class="keywordtype">bool</span> v0 = a_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(iffr_e[a]);
<a name="l00801"></a>00801 <span class="keywordtype">bool</span> v1 = b_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(iffr_e[b]);
<a name="l00802"></a>00802
<a name="l00803"></a>00803 <span class="keywordflow">if</span> (<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00804"></a>00804 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(iffr_e.getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab3535bf1f1c26490d56f63dc20696fa6">IFF_R</a> &&
<a name="l00805"></a>00805 (v0 || a_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(iffr_e[a])) &&
<a name="l00806"></a>00806 (v1 || b_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(iffr_e[b])),
<a name="l00807"></a>00807 <span class="stringliteral">"SearchEngineTheoremProducer::propIffr"</span>);
<a name="l00808"></a>00808 }
<a name="l00809"></a>00809
<a name="l00810"></a>00810 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> aa;
<a name="l00811"></a>00811 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00812"></a>00812 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoremProducer.html#a32afe6d99e661b5c70082036e40d48bc" title="Testing whether to generate assumptions.">withAssumptions</a>()) {
<a name="l00813"></a>00813 aa.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(iffr_th);
<a name="l00814"></a>00814 aa.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(a_th);
<a name="l00815"></a>00815 aa.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(b_th);
<a name="l00816"></a>00816 }
<a name="l00817"></a>00817
<a name="l00818"></a>00818 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l00819"></a>00819 vector<Proof> pfs;
<a name="l00820"></a>00820 vector<Expr> exprs;
<a name="l00821"></a>00821 exprs.push_back(iffr_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00822"></a>00822 exprs.push_back(a_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00823"></a>00823 exprs.push_back(b_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00824"></a>00824 pfs.push_back(iffr_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00825"></a>00825 pfs.push_back(a_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00826"></a>00826 pfs.push_back(b_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00827"></a>00827 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"prop_iffr"</span>, exprs, pfs);
<a name="l00828"></a>00828 }
<a name="l00829"></a>00829
<a name="l00830"></a>00830 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(v0 == v1 ? iffr_e[p] : iffr_e[p].negate(), aa, pf);
<a name="l00831"></a>00831 }
<a name="l00832"></a>00832
<a name="l00833"></a>00833 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00834"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#afc1db7951ca830c313d2cef522e45f25">00834</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#afc1db7951ca830c313d2cef522e45f25">SearchEngineTheoremProducer::confIffr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& iffr_th,
<a name="l00835"></a>00835 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& i_th,
<a name="l00836"></a>00836 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& l_th,
<a name="l00837"></a>00837 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& r_th)
<a name="l00838"></a>00838 {
<a name="l00839"></a>00839 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& iffr_e(iffr_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00840"></a>00840
<a name="l00841"></a>00841 <span class="keywordtype">bool</span> v0 = i_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(iffr_e[0]);
<a name="l00842"></a>00842 <span class="keywordtype">bool</span> v1 = l_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(iffr_e[1]);
<a name="l00843"></a>00843 <span class="keywordtype">bool</span> v2 = r_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(iffr_e[2]);
<a name="l00844"></a>00844
<a name="l00845"></a>00845 <span class="keywordflow">if</span> (<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00846"></a>00846 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(iffr_e.getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5bab3535bf1f1c26490d56f63dc20696fa6">IFF_R</a> &&
<a name="l00847"></a>00847 (v0 || i_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(iffr_e[0])) &&
<a name="l00848"></a>00848 (v1 || l_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(iffr_e[1])) &&
<a name="l00849"></a>00849 (v2 || r_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(iffr_e[2])) &&
<a name="l00850"></a>00850 ((v0 && v1 != v2) || (!v0 && v1 == v2)),
<a name="l00851"></a>00851 <span class="stringliteral">"SearchEngineTheoremProducer::confIffr"</span>);
<a name="l00852"></a>00852 }
<a name="l00853"></a>00853
<a name="l00854"></a>00854 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> a;
<a name="l00855"></a>00855 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00856"></a>00856 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoremProducer.html#a32afe6d99e661b5c70082036e40d48bc" title="Testing whether to generate assumptions.">withAssumptions</a>()) {
<a name="l00857"></a>00857 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(iffr_th);
<a name="l00858"></a>00858 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(i_th);
<a name="l00859"></a>00859 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(l_th);
<a name="l00860"></a>00860 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(r_th);
<a name="l00861"></a>00861 }
<a name="l00862"></a>00862
<a name="l00863"></a>00863 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l00864"></a>00864 vector<Proof> pfs;
<a name="l00865"></a>00865 vector<Expr> exprs;
<a name="l00866"></a>00866 exprs.push_back(iffr_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00867"></a>00867 exprs.push_back(i_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00868"></a>00868 exprs.push_back(l_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00869"></a>00869 exprs.push_back(r_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00870"></a>00870 pfs.push_back(iffr_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00871"></a>00871 pfs.push_back(i_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00872"></a>00872 pfs.push_back(l_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00873"></a>00873 pfs.push_back(r_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00874"></a>00874 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"conf_iffr"</span>, exprs, pfs);
<a name="l00875"></a>00875 }
<a name="l00876"></a>00876
<a name="l00877"></a>00877 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(<a class="code" href="classCVC3_1_1TheoremProducer.html#a1b706238281ad141a57363a6890f14a5">d_em</a>-><a class="code" href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae" title="FALSE Expr.">falseExpr</a>(), a, pf);
<a name="l00878"></a>00878 }
<a name="l00879"></a>00879
<a name="l00880"></a>00880 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00881"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a9964535eb830bbc87e91f40e71333dfa">00881</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a9964535eb830bbc87e91f40e71333dfa">SearchEngineTheoremProducer::propIterIte</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& iter_th,
<a name="l00882"></a>00882 <span class="keywordtype">bool</span> <a class="code" href="namespaceMiniSat.html#ad93cb56673487974071ed3b75bf4ea83">left</a>,
<a name="l00883"></a>00883 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& if_th,
<a name="l00884"></a>00884 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& then_th)
<a name="l00885"></a>00885 {
<a name="l00886"></a>00886 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& iter_e(iter_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00887"></a>00887
<a name="l00888"></a>00888 <span class="keywordtype">bool</span> v0 = if_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(iter_e[1]);
<a name="l00889"></a>00889 <span class="keywordtype">bool</span> v1 = then_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(iter_e[left ? 2 : 3]);
<a name="l00890"></a>00890
<a name="l00891"></a>00891 <span class="keywordflow">if</span> (<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00892"></a>00892 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(iter_e.getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba096c0758089b7d7d0a596b1b4c89a084">ITE_R</a> &&
<a name="l00893"></a>00893 (v0 || if_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(iter_e[1])) &&
<a name="l00894"></a>00894 (v1 || then_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(iter_e[left ? 2 : 3])) &&
<a name="l00895"></a>00895 v0 == left,
<a name="l00896"></a>00896 <span class="stringliteral">"SearchEngineTheoremProducer::propIterIte"</span>);
<a name="l00897"></a>00897 }
<a name="l00898"></a>00898
<a name="l00899"></a>00899 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> a;
<a name="l00900"></a>00900 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00901"></a>00901 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoremProducer.html#a32afe6d99e661b5c70082036e40d48bc" title="Testing whether to generate assumptions.">withAssumptions</a>()) {
<a name="l00902"></a>00902 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(iter_th);
<a name="l00903"></a>00903 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(if_th);
<a name="l00904"></a>00904 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(then_th);
<a name="l00905"></a>00905 }
<a name="l00906"></a>00906
<a name="l00907"></a>00907 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l00908"></a>00908 vector<Proof> pfs;
<a name="l00909"></a>00909 vector<Expr> exprs;
<a name="l00910"></a>00910 exprs.push_back(iter_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00911"></a>00911 exprs.push_back(if_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00912"></a>00912 exprs.push_back(then_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00913"></a>00913 pfs.push_back(iter_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00914"></a>00914 pfs.push_back(if_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00915"></a>00915 pfs.push_back(then_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00916"></a>00916 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"prop_iter_ite"</span>, exprs, pfs);
<a name="l00917"></a>00917 }
<a name="l00918"></a>00918
<a name="l00919"></a>00919 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(v1 ? iter_e[0] : iter_e[0].negate(), a, pf);
<a name="l00920"></a>00920 }
<a name="l00921"></a>00921
<a name="l00922"></a>00922 <span class="keywordtype">void</span>
<a name="l00923"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a9c5271d8f47048c4573e21bfd21bc8a7">00923</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a9c5271d8f47048c4573e21bfd21bc8a7">SearchEngineTheoremProducer::propIterIfThen</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& iter_th,
<a name="l00924"></a>00924 <span class="keywordtype">bool</span> <a class="code" href="namespaceMiniSat.html#ad93cb56673487974071ed3b75bf4ea83">left</a>,
<a name="l00925"></a>00925 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& ite_th,
<a name="l00926"></a>00926 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& then_th,
<a name="l00927"></a>00927 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>* if_th,
<a name="l00928"></a>00928 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>* else_th)
<a name="l00929"></a>00929 {
<a name="l00930"></a>00930 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& iter_e(iter_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00931"></a>00931
<a name="l00932"></a>00932 <span class="keywordtype">bool</span> v0 = ite_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(iter_e[0]);
<a name="l00933"></a>00933 <span class="keywordtype">bool</span> v1 = then_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(iter_e[left ? 2 : 3]);
<a name="l00934"></a>00934
<a name="l00935"></a>00935 <span class="keywordflow">if</span> (<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00936"></a>00936 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(iter_e.getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba096c0758089b7d7d0a596b1b4c89a084">ITE_R</a> &&
<a name="l00937"></a>00937 (v0 || ite_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(iter_e[0])) &&
<a name="l00938"></a>00938 (v1 || then_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(iter_e[left ? 2 : 3])) &&
<a name="l00939"></a>00939 v0 != v1,
<a name="l00940"></a>00940 <span class="stringliteral">"SearchEngineTheoremProducer::propIterIfThen"</span>);
<a name="l00941"></a>00941 }
<a name="l00942"></a>00942
<a name="l00943"></a>00943 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> a;
<a name="l00944"></a>00944 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00945"></a>00945 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoremProducer.html#a32afe6d99e661b5c70082036e40d48bc" title="Testing whether to generate assumptions.">withAssumptions</a>()) {
<a name="l00946"></a>00946 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(iter_th);
<a name="l00947"></a>00947 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(ite_th);
<a name="l00948"></a>00948 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(then_th);
<a name="l00949"></a>00949 }
<a name="l00950"></a>00950
<a name="l00951"></a>00951 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l00952"></a>00952 vector<Proof> pfs;
<a name="l00953"></a>00953 vector<Expr> exprs;
<a name="l00954"></a>00954 exprs.push_back(iter_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00955"></a>00955 exprs.push_back(ite_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00956"></a>00956 exprs.push_back(then_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00957"></a>00957 pfs.push_back(iter_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00958"></a>00958 pfs.push_back(ite_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00959"></a>00959 pfs.push_back(then_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00960"></a>00960 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"prop_iter_if_then"</span>, exprs, pfs);
<a name="l00961"></a>00961 }
<a name="l00962"></a>00962
<a name="l00963"></a>00963 <span class="keywordflow">if</span> (if_th)
<a name="l00964"></a>00964 *if_th = <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(left ? iter_e[1].negate() : iter_e[1], a, pf);
<a name="l00965"></a>00965 <span class="keywordflow">if</span> (else_th)
<a name="l00966"></a>00966 *else_th = <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(v0 ? iter_e[left ? 3 : 2] : iter_e[left ? 3 : 2].negate(), a, pf);
<a name="l00967"></a>00967 }
<a name="l00968"></a>00968
<a name="l00969"></a>00969 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00970"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#aa3a9dce562278a5383f4551d95b12c3a">00970</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#aa3a9dce562278a5383f4551d95b12c3a">SearchEngineTheoremProducer::propIterThen</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& iter_th,
<a name="l00971"></a>00971 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& ite_th,
<a name="l00972"></a>00972 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& if_th)
<a name="l00973"></a>00973 {
<a name="l00974"></a>00974 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& iter_e(iter_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00975"></a>00975
<a name="l00976"></a>00976 <span class="keywordtype">bool</span> v0 = ite_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(iter_e[0]);
<a name="l00977"></a>00977 <span class="keywordtype">bool</span> v1 = if_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(iter_e[1]);
<a name="l00978"></a>00978
<a name="l00979"></a>00979 <span class="keywordflow">if</span> (<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00980"></a>00980 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(iter_e.getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba096c0758089b7d7d0a596b1b4c89a084">ITE_R</a> &&
<a name="l00981"></a>00981 (v0 || ite_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(iter_e[0])) &&
<a name="l00982"></a>00982 (v1 || if_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(iter_e[1])),
<a name="l00983"></a>00983 <span class="stringliteral">"SearchEngineTheoremProducer::propIterThen"</span>);
<a name="l00984"></a>00984 }
<a name="l00985"></a>00985
<a name="l00986"></a>00986 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> a;
<a name="l00987"></a>00987 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00988"></a>00988 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoremProducer.html#a32afe6d99e661b5c70082036e40d48bc" title="Testing whether to generate assumptions.">withAssumptions</a>()) {
<a name="l00989"></a>00989 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(iter_th);
<a name="l00990"></a>00990 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(ite_th);
<a name="l00991"></a>00991 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(if_th);
<a name="l00992"></a>00992 }
<a name="l00993"></a>00993
<a name="l00994"></a>00994 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l00995"></a>00995 vector<Proof> pfs;
<a name="l00996"></a>00996 vector<Expr> exprs;
<a name="l00997"></a>00997 exprs.push_back(iter_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00998"></a>00998 exprs.push_back(ite_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l00999"></a>00999 exprs.push_back(if_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l01000"></a>01000 pfs.push_back(iter_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l01001"></a>01001 pfs.push_back(ite_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l01002"></a>01002 pfs.push_back(if_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l01003"></a>01003 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"prop_iter_then"</span>, exprs, pfs);
<a name="l01004"></a>01004 }
<a name="l01005"></a>01005
<a name="l01006"></a>01006 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(v1 ?
<a name="l01007"></a>01007 (v0 ? iter_e[2] : iter_e[2].negate()) :
<a name="l01008"></a>01008 (v0 ? iter_e[3] : iter_e[3].negate()), a, pf);
<a name="l01009"></a>01009 }
<a name="l01010"></a>01010
<a name="l01011"></a>01011 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l01012"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#aaf56546de0c7c7bbe0b573477d412bf7">01012</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#aaf56546de0c7c7bbe0b573477d412bf7">SearchEngineTheoremProducer::confIterThenElse</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& iter_th,
<a name="l01013"></a>01013 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& ite_th,
<a name="l01014"></a>01014 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& then_th,
<a name="l01015"></a>01015 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& else_th)
<a name="l01016"></a>01016 {
<a name="l01017"></a>01017 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& iter_e(iter_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l01018"></a>01018
<a name="l01019"></a>01019 <span class="keywordtype">bool</span> v0 = ite_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(iter_e[0]);
<a name="l01020"></a>01020 <span class="keywordtype">bool</span> v1 = then_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(iter_e[2]);
<a name="l01021"></a>01021 <span class="keywordtype">bool</span> v2 = else_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(iter_e[3]);
<a name="l01022"></a>01022
<a name="l01023"></a>01023 <span class="keywordflow">if</span> (<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l01024"></a>01024 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(iter_e.getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba096c0758089b7d7d0a596b1b4c89a084">ITE_R</a> &&
<a name="l01025"></a>01025 (v0 || ite_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(iter_e[0])) &&
<a name="l01026"></a>01026 (v1 || then_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(iter_e[2])) &&
<a name="l01027"></a>01027 (v2 || else_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(iter_e[3])) &&
<a name="l01028"></a>01028 ((v0 && !v1 && !v2) || (!v0 && v1 && v2)),
<a name="l01029"></a>01029 <span class="stringliteral">"SearchEngineTheoremProducer::confIterThenElse"</span>);
<a name="l01030"></a>01030 }
<a name="l01031"></a>01031
<a name="l01032"></a>01032 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> a;
<a name="l01033"></a>01033 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l01034"></a>01034 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoremProducer.html#a32afe6d99e661b5c70082036e40d48bc" title="Testing whether to generate assumptions.">withAssumptions</a>()) {
<a name="l01035"></a>01035 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(iter_th);
<a name="l01036"></a>01036 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(ite_th);
<a name="l01037"></a>01037 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(then_th);
<a name="l01038"></a>01038 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(else_th);
<a name="l01039"></a>01039 }
<a name="l01040"></a>01040
<a name="l01041"></a>01041 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l01042"></a>01042 vector<Proof> pfs;
<a name="l01043"></a>01043 vector<Expr> exprs;
<a name="l01044"></a>01044 exprs.push_back(iter_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l01045"></a>01045 exprs.push_back(ite_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l01046"></a>01046 exprs.push_back(then_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l01047"></a>01047 exprs.push_back(else_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l01048"></a>01048 pfs.push_back(iter_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l01049"></a>01049 pfs.push_back(ite_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l01050"></a>01050 pfs.push_back(then_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l01051"></a>01051 pfs.push_back(else_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l01052"></a>01052 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"conf_iter_then_else"</span>, exprs, pfs);
<a name="l01053"></a>01053 }
<a name="l01054"></a>01054
<a name="l01055"></a>01055 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(<a class="code" href="classCVC3_1_1TheoremProducer.html#a1b706238281ad141a57363a6890f14a5">d_em</a>-><a class="code" href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae" title="FALSE Expr.">falseExpr</a>(), a, pf);
<a name="l01056"></a>01056 }
<a name="l01057"></a>01057
<a name="l01058"></a>01058 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l01059"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#aad519346f53864cc21109200379a3698">01059</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#aad519346f53864cc21109200379a3698">SearchEngineTheoremProducer::confIterIfThen</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& iter_th,
<a name="l01060"></a>01060 <span class="keywordtype">bool</span> <a class="code" href="namespaceMiniSat.html#ad93cb56673487974071ed3b75bf4ea83">left</a>,
<a name="l01061"></a>01061 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& ite_th,
<a name="l01062"></a>01062 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& if_th,
<a name="l01063"></a>01063 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& then_th)
<a name="l01064"></a>01064 {
<a name="l01065"></a>01065 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& iter_e(iter_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l01066"></a>01066
<a name="l01067"></a>01067 <span class="keywordtype">bool</span> v0 = ite_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(iter_e[0]);
<a name="l01068"></a>01068 <span class="keywordtype">bool</span> v1 = if_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(iter_e[1]);
<a name="l01069"></a>01069 <span class="keywordtype">bool</span> v2 = then_th.<a class="code" href="classCVC3_1_1Theorem.html#afd8511ead1dfc424a75089f4b4afb95d" title="Check if the flag attribute is set.">proves</a>(iter_e[left ? 2 : 3]);
<a name="l01070"></a>01070
<a name="l01071"></a>01071 <span class="keywordflow">if</span> (<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l01072"></a>01072 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(iter_e.getKind() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba096c0758089b7d7d0a596b1b4c89a084">ITE_R</a> &&
<a name="l01073"></a>01073 (v0 || ite_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(iter_e[0])) &&
<a name="l01074"></a>01074 (v1 || if_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(iter_e[1])) &&
<a name="l01075"></a>01075 (v2 || then_th.<a class="code" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c" title="Check if the flag attribute is set.">refutes</a>(iter_e[left ? 2 : 3])) &&
<a name="l01076"></a>01076 v1 == left && v0 != v2,
<a name="l01077"></a>01077 <span class="stringliteral">"SearchEngineTheoremProducer::confIterThenElse"</span>);
<a name="l01078"></a>01078 }
<a name="l01079"></a>01079
<a name="l01080"></a>01080 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> a;
<a name="l01081"></a>01081 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l01082"></a>01082 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoremProducer.html#a32afe6d99e661b5c70082036e40d48bc" title="Testing whether to generate assumptions.">withAssumptions</a>()) {
<a name="l01083"></a>01083 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(iter_th);
<a name="l01084"></a>01084 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(ite_th);
<a name="l01085"></a>01085 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(if_th);
<a name="l01086"></a>01086 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(then_th);
<a name="l01087"></a>01087 }
<a name="l01088"></a>01088
<a name="l01089"></a>01089 <span class="keywordflow">if</span> (<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l01090"></a>01090 vector<Proof> pfs;
<a name="l01091"></a>01091 vector<Expr> exprs;
<a name="l01092"></a>01092 exprs.push_back(iter_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l01093"></a>01093 exprs.push_back(ite_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l01094"></a>01094 exprs.push_back(if_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l01095"></a>01095 exprs.push_back(then_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l01096"></a>01096 pfs.push_back(iter_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l01097"></a>01097 pfs.push_back(ite_th.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l01098"></a>01098 pfs.push_back(if_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l01099"></a>01099 pfs.push_back(then_th.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l01100"></a>01100 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"conf_iter_then_else"</span>, exprs, pfs);
<a name="l01101"></a>01101 }
<a name="l01102"></a>01102
<a name="l01103"></a>01103 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(<a class="code" href="classCVC3_1_1TheoremProducer.html#a1b706238281ad141a57363a6890f14a5">d_em</a>-><a class="code" href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae" title="FALSE Expr.">falseExpr</a>(), a, pf);
<a name="l01104"></a>01104 }
<a name="l01105"></a>01105
<a name="l01106"></a>01106 <span class="comment">// "Conflict" rule (all literals in a clause become FALSE)</span>
<a name="l01107"></a>01107 <span class="comment">// { G_j |- !l_j, j in [1..n] } , G |- (OR l_1 ... l_n) ==> FALSE</span>
<a name="l01108"></a>01108 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l01109"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a55bf4e865a7a76e82c23d5fba566b853">01109</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a55bf4e865a7a76e82c23d5fba566b853" title=""Conflict" rule (all literals in a clause become FALSE) ">SearchEngineTheoremProducer::conflictRule</a>(<span class="keyword">const</span> std::vector<Theorem>& thms,
<a name="l01110"></a>01110 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& clause) {
<a name="l01111"></a>01111 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e(clause.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l01112"></a>01112 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l01113"></a>01113 <span class="comment">// Soundness check: first, check the form of the 'clause' theorem</span>
<a name="l01114"></a>01114 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(e.isOr(),
<a name="l01115"></a>01115 <span class="stringliteral">"SearchEngineTheoremProducer::unitProp: "</span>
<a name="l01116"></a>01116 <span class="stringliteral">"bad theorem in clause = "</span>+clause.<a class="code" href="classCVC3_1_1Theorem.html#ac4b1c9570ffb9cc901627ef2abb9ff77">toString</a>());
<a name="l01117"></a>01117 <span class="comment">// Now, check correspondence of thms to the disjunction</span>
<a name="l01118"></a>01118 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(((<span class="keywordtype">int</span>)thms.size()) == e.arity(),
<a name="l01119"></a>01119 <span class="stringliteral">"SearchEngineTheoremProducer::conflictRule: "</span>
<a name="l01120"></a>01120 <span class="stringliteral">"wrong number of theorems"</span>
<a name="l01121"></a>01121 <span class="stringliteral">"\n thms.size = "</span> + <a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(thms.size())
<a name="l01122"></a>01122 +<span class="stringliteral">"\n clause.arity = "</span> + <a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(e.arity()));
<a name="l01123"></a>01123
<a name="l01124"></a>01124 <span class="keywordflow">for</span>(<span class="keywordtype">unsigned</span> j=0; j<thms.size(); j++) {
<a name="l01125"></a>01125 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> ej(e[j]), ek(thms[j].getExpr());
<a name="l01126"></a>01126 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>((ej.isNot() && ej[0] == ek) || (ek.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() && ej == ek[0]),
<a name="l01127"></a>01127 <span class="stringliteral">"SearchEngineTheoremProducer::conflictRule: "</span>
<a name="l01128"></a>01128 <span class="stringliteral">"wrong theorem["</span>+<a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(j)+<span class="stringliteral">"]"</span>
<a name="l01129"></a>01129 <span class="stringliteral">"\n thm = "</span> + thms[j].toString() +
<a name="l01130"></a>01130 <span class="stringliteral">"\n literal = "</span> + e[j].toString() +
<a name="l01131"></a>01131 <span class="stringliteral">"\n clause = "</span> + clause.<a class="code" href="classCVC3_1_1Theorem.html#ac4b1c9570ffb9cc901627ef2abb9ff77">toString</a>());
<a name="l01132"></a>01132 }
<a name="l01133"></a>01133 }
<a name="l01134"></a>01134
<a name="l01135"></a>01135 <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a> a(thms);
<a name="l01136"></a>01136 a.<a class="code" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a>(clause);
<a name="l01137"></a>01137 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l01138"></a>01138 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>()) {
<a name="l01139"></a>01139 vector<Proof> pfs;
<a name="l01140"></a>01140 vector<Expr> exprs;
<a name="l01141"></a>01141 exprs.reserve(thms.size() + 1);
<a name="l01142"></a>01142 pfs.reserve(thms.size()+1);
<a name="l01143"></a>01143 <span class="keyword">const</span> vector<Theorem>::const_iterator iend = thms.end();
<a name="l01144"></a>01144 <span class="keywordflow">for</span>(vector<Theorem>::const_iterator i=thms.begin(); i!=iend; ++i) {
<a name="l01145"></a>01145 exprs.push_back(i->getExpr());
<a name="l01146"></a>01146 pfs.push_back(i->getProof());
<a name="l01147"></a>01147 }
<a name="l01148"></a>01148 exprs.push_back(clause.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>());
<a name="l01149"></a>01149 pfs.push_back(clause.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l01150"></a>01150 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"conflict"</span>, exprs, pfs);
<a name="l01151"></a>01151 }
<a name="l01152"></a>01152 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(<a class="code" href="classCVC3_1_1TheoremProducer.html#a1b706238281ad141a57363a6890f14a5">d_em</a>-><a class="code" href="group__EM__Priv.html#gaae9db4c93c67cbf8bbf5d1e60e94f1ae" title="FALSE Expr.">falseExpr</a>(), a, pf);
<a name="l01153"></a>01153 }
<a name="l01154"></a>01154
<a name="l01155"></a>01155 <span class="comment"></span>
<a name="l01156"></a>01156 <span class="comment">///////////////////////////////////////////////////////////////////////</span>
<a name="l01157"></a>01157 <span class="comment">//// Conjunctive Normal Form (CNF) proof rules</span>
<a name="l01158"></a>01158 <span class="comment">///////////////////////////////////////////////////////////////////////</span>
<a name="l01159"></a>01159 <span class="comment"></span><a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l01160"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#af38d03174800bca0baba91f4e8288b0f">01160</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#af38d03174800bca0baba91f4e8288b0f" title="AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v].">SearchEngineTheoremProducer::andCNFRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm) {
<a name="l01161"></a>01161 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#afd9835d232286f451200d637ba995e75">opCNFRule</a>(thm, <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba865555c9f2e0458a7078486aa1b3254f">AND</a>, <span class="stringliteral">"and_cnf_rule"</span>);
<a name="l01162"></a>01162 }
<a name="l01163"></a>01163
<a name="l01164"></a>01164 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l01165"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a3cf33a58eee64dc744015e8657adc40a">01165</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a3cf33a58eee64dc744015e8657adc40a" title="OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v].">SearchEngineTheoremProducer::orCNFRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm) {
<a name="l01166"></a>01166 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#afd9835d232286f451200d637ba995e75">opCNFRule</a>(thm, <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>, <span class="stringliteral">"or_cnf_rule"</span>);
<a name="l01167"></a>01167 }
<a name="l01168"></a>01168
<a name="l01169"></a>01169 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l01170"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a15cbb86a5a77422c7d8c59384488f9e1">01170</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a15cbb86a5a77422c7d8c59384488f9e1" title="(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v]">SearchEngineTheoremProducer::impCNFRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm) {
<a name="l01171"></a>01171 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#afd9835d232286f451200d637ba995e75">opCNFRule</a>(thm, <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7338bb59b9aa936104a6d2f631d4d8db">IMPLIES</a>, <span class="stringliteral">"implies_cnf_rule"</span>);
<a name="l01172"></a>01172 }
<a name="l01173"></a>01173
<a name="l01174"></a>01174 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l01175"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a47468ab81771bdb7af900bd2f907f818">01175</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a47468ab81771bdb7af900bd2f907f818" title="(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]">SearchEngineTheoremProducer::iffCNFRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm) {
<a name="l01176"></a>01176 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#afd9835d232286f451200d637ba995e75">opCNFRule</a>(thm, <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>, <span class="stringliteral">"iff_cnf_rule"</span>);
<a name="l01177"></a>01177 }
<a name="l01178"></a>01178
<a name="l01179"></a>01179 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l01180"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a1c37ba3237f04f7536164166c7f0156e">01180</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a1c37ba3237f04f7536164166c7f0156e" title="ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v].">SearchEngineTheoremProducer::iteCNFRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm) {
<a name="l01181"></a>01181 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#afd9835d232286f451200d637ba995e75">opCNFRule</a>(thm, <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc">ITE</a>, <span class="stringliteral">"ite_cnf_rule"</span>);
<a name="l01182"></a>01182 }
<a name="l01183"></a>01183
<a name="l01184"></a>01184
<a name="l01185"></a>01185 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l01186"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a9ec94eac3bdabe251a4147b2830a2f50">01186</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a9ec94eac3bdabe251a4147b2830a2f50" title="ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2)">SearchEngineTheoremProducer::iteToClauses</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& ite) {
<a name="l01187"></a>01187 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& iteExpr = ite.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>();
<a name="l01188"></a>01188
<a name="l01189"></a>01189 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l01190"></a>01190 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(iteExpr.<a class="code" href="group__ExprPkg.html#gaef13fa4752a1fb28e129a1efd0e26f01">isITE</a>() && iteExpr.<a class="code" href="group__ExprPkg.html#ga42929221eb172250697b72c28af6de07" title="Get the type. Recursively compute if necessary.">getType</a>().<a class="code" href="classCVC3_1_1Type.html#a38bba404056eadf3c283a67ab2347e02">isBool</a>(),
<a name="l01191"></a>01191 <span class="stringliteral">"SearchEngineTheoremProducer::iteToClauses("</span>+iteExpr.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>()
<a name="l01192"></a>01192 +<span class="stringliteral">")\n Argument must be a Boolean ITE"</span>);
<a name="l01193"></a>01193 }
<a name="l01194"></a>01194 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& cond = iteExpr[0];
<a name="l01195"></a>01195 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1 = iteExpr[1];
<a name="l01196"></a>01196 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2 = iteExpr[2];
<a name="l01197"></a>01197
<a name="l01198"></a>01198 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l01199"></a>01199 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>())
<a name="l01200"></a>01200 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"ite_to_clauses"</span>, iteExpr, ite.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l01201"></a>01201 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>((cond.<a class="code" href="group__ExprPkg.html#gab1ce461dc931af73bf04e88c8d37dcbc">negate</a>() || t1) && (cond || t2), ite.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>(), pf);
<a name="l01202"></a>01202 }
<a name="l01203"></a>01203
<a name="l01204"></a>01204
<a name="l01205"></a>01205 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l01206"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#ab608d81ddbbce71638fcce0d119c63d1">01206</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#ab608d81ddbbce71638fcce0d119c63d1" title="e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)">SearchEngineTheoremProducer::iffToClauses</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& iff) {
<a name="l01207"></a>01207 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l01208"></a>01208 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(iff.<a class="code" href="classCVC3_1_1Theorem.html#a362c1d70e03803d804bbe300e5f6dc87">isRewrite</a>() && iff.<a class="code" href="classCVC3_1_1Theorem.html#a206c04f39fbbcacef2337148675553f4">getLHS</a>().<a class="code" href="group__ExprPkg.html#ga42929221eb172250697b72c28af6de07" title="Get the type. Recursively compute if necessary.">getType</a>().<a class="code" href="classCVC3_1_1Type.html#a38bba404056eadf3c283a67ab2347e02">isBool</a>(),
<a name="l01209"></a>01209 <span class="stringliteral">"SearchEngineTheoremProducer::iffToClauses("</span>+iff.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>().<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>()
<a name="l01210"></a>01210 +<span class="stringliteral">")\n Argument must be a Boolean IFF"</span>);
<a name="l01211"></a>01211 }
<a name="l01212"></a>01212 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1 = iff.<a class="code" href="classCVC3_1_1Theorem.html#a206c04f39fbbcacef2337148675553f4">getLHS</a>();
<a name="l01213"></a>01213 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2 = iff.<a class="code" href="classCVC3_1_1Theorem.html#a97d957fcbf9094480851b1d2e5d3729f">getRHS</a>();
<a name="l01214"></a>01214
<a name="l01215"></a>01215 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l01216"></a>01216 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>())
<a name="l01217"></a>01217 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"iff_to_clauses"</span>, iff.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(), iff.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l01218"></a>01218 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>((t1.<a class="code" href="group__ExprPkg.html#gab1ce461dc931af73bf04e88c8d37dcbc">negate</a>() || t2) && (t1 || t2.<a class="code" href="group__ExprPkg.html#gab1ce461dc931af73bf04e88c8d37dcbc">negate</a>()), iff.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>(), pf);
<a name="l01219"></a>01219 }
<a name="l01220"></a>01220
<a name="l01221"></a>01221 <span class="comment"></span>
<a name="l01222"></a>01222 <span class="comment">/////////////////////////////////////////////////////////////////////////</span>
<a name="l01223"></a>01223 <span class="comment">//// helper functions for CNF (Conjunctive Normal Form) conversion</span>
<a name="l01224"></a>01224 <span class="comment">/////////////////////////////////////////////////////////////////////////</span>
<a name="l01225"></a>01225 <span class="comment"></span><a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l01226"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#afd9835d232286f451200d637ba995e75">01226</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#afd9835d232286f451200d637ba995e75">SearchEngineTheoremProducer::opCNFRule</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm,
<a name="l01227"></a>01227 <span class="keywordtype">int</span> kind,
<a name="l01228"></a>01228 <span class="keyword">const</span> <span class="keywordtype">string</span>& ruleName) {
<a name="l01229"></a>01229 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"opCNFRule["</span>+<a class="code" href="classCVC3_1_1TheoremProducer.html#a1b706238281ad141a57363a6890f14a5">d_em</a>-><a class="code" href="group__EM__Priv.html#gad129f2ecc362f60ca43e06ff46b8521b" title="Return the name associated with a kind. The kind must already be registered.">getKindName</a>(kind)+<span class="stringliteral">"]("</span>,
<a name="l01230"></a>01230 thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(), <span class="stringliteral">") {"</span>);
<a name="l01231"></a>01231 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> localCache;
<a name="l01232"></a>01232 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l01233"></a>01233 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> phiIffVar = thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>();
<a name="l01234"></a>01234 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(phiIffVar.<a class="code" href="group__ExprPkg.html#gabe385fb97505cccb75702378511c5375">isIff</a>(),
<a name="l01235"></a>01235 <span class="stringliteral">"SearchEngineTheoremProducer::opCNFRule("</span>
<a name="l01236"></a>01236 +<a class="code" href="classCVC3_1_1TheoremProducer.html#a1b706238281ad141a57363a6890f14a5">d_em</a>-><a class="code" href="group__EM__Priv.html#gad129f2ecc362f60ca43e06ff46b8521b" title="Return the name associated with a kind. The kind must already be registered.">getKindName</a>(kind)+<span class="stringliteral">"): "</span>
<a name="l01237"></a>01237 <span class="stringliteral">"input must be an IFF: thm = "</span> + phiIffVar.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l01238"></a>01238 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(phiIffVar[0].getKind() == kind,
<a name="l01239"></a>01239 <span class="stringliteral">"SearchEngineTheoremProducer::opCNFRule("</span>
<a name="l01240"></a>01240 +<a class="code" href="classCVC3_1_1TheoremProducer.html#a1b706238281ad141a57363a6890f14a5">d_em</a>-><a class="code" href="group__EM__Priv.html#gad129f2ecc362f60ca43e06ff46b8521b" title="Return the name associated with a kind. The kind must already be registered.">getKindName</a>(kind)+<span class="stringliteral">"): "</span>
<a name="l01241"></a>01241 <span class="stringliteral">"input phi has wrong kind: thm = "</span> + phiIffVar.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l01242"></a>01242 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(phiIffVar[0] != phiIffVar[1],
<a name="l01243"></a>01243 <span class="stringliteral">"SearchEngineTheoremProducer::opCNFRule("</span>
<a name="l01244"></a>01244 +<a class="code" href="classCVC3_1_1TheoremProducer.html#a1b706238281ad141a57363a6890f14a5">d_em</a>-><a class="code" href="group__EM__Priv.html#gad129f2ecc362f60ca43e06ff46b8521b" title="Return the name associated with a kind. The kind must already be registered.">getKindName</a>(kind)+<span class="stringliteral">"): "</span>
<a name="l01245"></a>01245 <span class="stringliteral">"wrong input thm = "</span> + phiIffVar.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l01246"></a>01246 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> it=phiIffVar[0].begin(), itend=phiIffVar[0].<a class="code" href="group__ExprPkg.html#gaf6048a5030c8fa2511bf5dfee868e653" title="End iterator.">end</a>();
<a name="l01247"></a>01247 it!=itend;++it){
<a name="l01248"></a>01248 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(phiIffVar[1] != *it,
<a name="l01249"></a>01249 <span class="stringliteral">"SearchEngineTheoremProducer::opCNFRule("</span>
<a name="l01250"></a>01250 +<a class="code" href="classCVC3_1_1TheoremProducer.html#a1b706238281ad141a57363a6890f14a5">d_em</a>-><a class="code" href="group__EM__Priv.html#gad129f2ecc362f60ca43e06ff46b8521b" title="Return the name associated with a kind. The kind must already be registered.">getKindName</a>(kind)+<span class="stringliteral">"): "</span>
<a name="l01251"></a>01251 <span class="stringliteral">"wrong input thm = "</span> + phiIffVar.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l01252"></a>01252 }
<a name="l01253"></a>01253 }
<a name="l01254"></a>01254 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& phi = thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>()[0];
<a name="l01255"></a>01255 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& phiVar = thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>()[1];
<a name="l01256"></a>01256
<a name="l01257"></a>01257 std::vector<Expr> boundVars;
<a name="l01258"></a>01258 std::vector<Expr> boundVarsAndLiterals;
<a name="l01259"></a>01259 std::vector<Expr> equivs;
<a name="l01260"></a>01260 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> i=phi.<a class="code" href="group__ExprPkg.html#gac890e13db184610276fc533fa4b4fe99" title="Begin iterator.">begin</a>(), iend=phi.<a class="code" href="group__ExprPkg.html#gaf6048a5030c8fa2511bf5dfee868e653" title="End iterator.">end</a>(); i != iend; i++) {
<a name="l01261"></a>01261 <span class="comment">// First, strip the negation and check if the formula is atomic</span>
<a name="l01262"></a>01262 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> tmp(*i);
<a name="l01263"></a>01263 <span class="keywordflow">while</span>(tmp.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>())
<a name="l01264"></a>01264 tmp = tmp[0];
<a name="l01265"></a>01265
<a name="l01266"></a>01266 <span class="keywordflow">if</span>(tmp.<a class="code" href="group__ExprPkg.html#gad8c63abfec9cc4a8319f3df1b47eee45" title="True iff expr is not a Bool connective.">isPropAtom</a>())
<a name="l01267"></a>01267 boundVarsAndLiterals.push_back(*i);
<a name="l01268"></a>01268 <span class="keywordflow">else</span>
<a name="l01269"></a>01269 boundVarsAndLiterals.push_back(<a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a4af17425aaf7d8a28aaf1d8a09241535" title="checks if phi has v in local cache of opCNFRule, if so reuse v.">findInLocalCache</a>(*i, localCache,
<a name="l01270"></a>01270 boundVars));
<a name="l01271"></a>01271 }
<a name="l01272"></a>01272
<a name="l01273"></a>01273 <span class="keywordflow">for</span>(<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr>::iterator</a> it=localCache.<a class="code" href="classCVC3_1_1ExprMap.html#a3db85401f8535daf4054fde531cd46b1">begin</a>(), itend=localCache.end();
<a name="l01274"></a>01274 it != itend; it++) {
<a name="l01275"></a>01275 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>((*it).second.isIff(),
<a name="l01276"></a>01276 <span class="stringliteral">"SearchEngineTheoremProducer::opCNFRule: "</span> +
<a name="l01277"></a>01277 (*it).second.toString());
<a name="l01278"></a>01278 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!(*it).second[0].isPropLiteral() &&
<a name="l01279"></a>01279 (*it).second[1].isAbsLiteral(),
<a name="l01280"></a>01280 <span class="stringliteral">"SearchEngineTheoremProducer::opCNFRule: "</span> +
<a name="l01281"></a>01281 (*it).second.toString());
<a name="l01282"></a>01282 equivs.push_back((*it).second);
<a name="l01283"></a>01283 }
<a name="l01284"></a>01284
<a name="l01285"></a>01285 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(boundVarsAndLiterals.size() == (unsigned)phi.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>(),
<a name="l01286"></a>01286 <span class="stringliteral">"SearchEngineTheoremProducer::opCNFRule: "</span>
<a name="l01287"></a>01287 <span class="stringliteral">"wrong size of boundvars: phi = "</span> + phi.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l01288"></a>01288
<a name="l01289"></a>01289 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(boundVars.size() == equivs.size(),
<a name="l01290"></a>01290 <span class="stringliteral">"SearchEngineTheoremProducer::opCNFRule: "</span>
<a name="l01291"></a>01291 <span class="stringliteral">"wrong size of boundvars: phi = "</span> + phi.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l01292"></a>01292
<a name="l01293"></a>01293 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> cnfInput = phi.<a class="code" href="group__ExprPkg.html#ga28b901d05e52a5c646f83a95cc74f94b">arity</a>() > 0 ? <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(phi.<a class="code" href="group__ExprPkg.html#gace479f04faca399219496195152f7806" title="Get operator from expression.">getOp</a>(), boundVarsAndLiterals) : phi;
<a name="l01294"></a>01294 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> result = <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a8ad94f1a94fd5bf8fa10dbf26e04ee58" title="produces the CNF for the formula v <==> phi">convertToCNF</a>(phiVar, cnfInput);
<a name="l01295"></a>01295 <span class="keywordflow">if</span>(boundVars.size() > 0)
<a name="l01296"></a>01296 result =
<a name="l01297"></a>01297 <a class="code" href="classCVC3_1_1TheoremProducer.html#a1b706238281ad141a57363a6890f14a5">d_em</a>-><a class="code" href="group__EM__Priv.html#ga0d2ff7603a249b30b2df4e549607ad6e">newClosureExpr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3197625a1bb2264943f5a95f236d9973">EXISTS</a>, boundVars, result.andExpr(<a class="code" href="namespaceCVC3.html#ad4258158bba138eb54b9080af7f8223a">andExpr</a>(equivs)));
<a name="l01298"></a>01298
<a name="l01299"></a>01299 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l01300"></a>01300 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>())
<a name="l01301"></a>01301 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(ruleName, thm.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(), thm.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l01302"></a>01302 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> res(<a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(result, thm.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>(), pf));
<a name="l01303"></a>01303 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"opCNFRule["</span>+<a class="code" href="classCVC3_1_1TheoremProducer.html#a1b706238281ad141a57363a6890f14a5">d_em</a>-><a class="code" href="group__EM__Priv.html#gad129f2ecc362f60ca43e06ff46b8521b" title="Return the name associated with a kind. The kind must already be registered.">getKindName</a>(kind)+<span class="stringliteral">"] => "</span>, res.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>(),
<a name="l01304"></a>01304 <span class="stringliteral">" }"</span>);
<a name="l01305"></a>01305 <span class="keywordflow">return</span> res;
<a name="l01306"></a>01306 }
<a name="l01307"></a>01307 <span class="comment"></span>
<a name="l01308"></a>01308 <span class="comment">//! produces the CNF for the formula v <==> phi </span>
<a name="l01309"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a8ad94f1a94fd5bf8fa10dbf26e04ee58">01309</a> <span class="comment"></span><a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a8ad94f1a94fd5bf8fa10dbf26e04ee58" title="produces the CNF for the formula v <==> phi">SearchEngineTheoremProducer::convertToCNF</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& v, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> & phi) {
<a name="l01310"></a>01310 <span class="comment">//we assume that v \iff phi. v is the newVar corresponding to phi</span>
<a name="l01311"></a>01311
<a name="l01312"></a>01312 <a class="code" href="classCVC3_1_1Expr_1_1iterator.html">Expr::iterator</a> i = phi.<a class="code" href="group__ExprPkg.html#gac890e13db184610276fc533fa4b4fe99" title="Begin iterator.">begin</a>(), iend = phi.<a class="code" href="group__ExprPkg.html#gaf6048a5030c8fa2511bf5dfee868e653" title="End iterator.">end</a>();
<a name="l01313"></a>01313 std::vector<Expr> clauses;
<a name="l01314"></a>01314 std::vector<Expr> lastClause;
<a name="l01315"></a>01315 <span class="keywordflow">switch</span>(phi.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>()) {
<a name="l01316"></a>01316 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba865555c9f2e0458a7078486aa1b3254f">AND</a>: {
<a name="l01317"></a>01317 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& negV = v.<a class="code" href="group__ExprPkg.html#gab1ce461dc931af73bf04e88c8d37dcbc">negate</a>();
<a name="l01318"></a>01318 lastClause.push_back(v);
<a name="l01319"></a>01319 <span class="keywordflow">for</span>(;i!=iend; ++i) {
<a name="l01320"></a>01320 lastClause.push_back(i->negate());
<a name="l01321"></a>01321 }
<a name="l01322"></a>01322 clauses.push_back(<a class="code" href="namespaceCVC3.html#a30f30b6e20c174f21ae63acea8618294">orExpr</a>(lastClause));
<a name="l01323"></a>01323 }
<a name="l01324"></a>01324 <span class="keywordflow">break</span>;
<a name="l01325"></a>01325 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>:{
<a name="l01326"></a>01326 lastClause.push_back(v.<a class="code" href="group__ExprPkg.html#gab1ce461dc931af73bf04e88c8d37dcbc">negate</a>());
<a name="l01327"></a>01327 <span class="keywordflow">for</span>(;i!=iend; ++i) {
<a name="l01328"></a>01328 clauses.push_back(v.<a class="code" href="group__ExprPkg.html#gaf310870d783fff343e77ba9c2277c626">orExpr</a>(i->negate()));
<a name="l01329"></a>01329 lastClause.push_back(*i);
<a name="l01330"></a>01330 }
<a name="l01331"></a>01331 clauses.push_back(<a class="code" href="namespaceCVC3.html#a30f30b6e20c174f21ae63acea8618294">orExpr</a>(lastClause));
<a name="l01332"></a>01332 }
<a name="l01333"></a>01333 <span class="keywordflow">break</span>;
<a name="l01334"></a>01334 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba527cb185631442655c4486d51522b5a7">IFF</a>: {
<a name="l01335"></a>01335 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& v1 = phi[0];
<a name="l01336"></a>01336 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& v2 = phi[1];
<a name="l01337"></a>01337 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> negV = v.<a class="code" href="group__ExprPkg.html#gab1ce461dc931af73bf04e88c8d37dcbc">negate</a>();
<a name="l01338"></a>01338 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> negv1 = v1.<a class="code" href="group__ExprPkg.html#gab1ce461dc931af73bf04e88c8d37dcbc">negate</a>();
<a name="l01339"></a>01339 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> negv2 = v2.<a class="code" href="group__ExprPkg.html#gab1ce461dc931af73bf04e88c8d37dcbc">negate</a>();
<a name="l01340"></a>01340 clauses.push_back(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>, negV, negv1, v2));
<a name="l01341"></a>01341 clauses.push_back(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>, negV, v1, negv2));
<a name="l01342"></a>01342 clauses.push_back(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>, v, v1, v2));
<a name="l01343"></a>01343 clauses.push_back(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>, v, negv1, negv2));
<a name="l01344"></a>01344 } <span class="keywordflow">break</span>;
<a name="l01345"></a>01345 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7338bb59b9aa936104a6d2f631d4d8db">IMPLIES</a>:{
<a name="l01346"></a>01346 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& v1 = phi[0];
<a name="l01347"></a>01347 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& v2 = phi[1];
<a name="l01348"></a>01348 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> negV = v.<a class="code" href="group__ExprPkg.html#gab1ce461dc931af73bf04e88c8d37dcbc">negate</a>();
<a name="l01349"></a>01349 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> negv1 = v1.<a class="code" href="group__ExprPkg.html#gab1ce461dc931af73bf04e88c8d37dcbc">negate</a>();
<a name="l01350"></a>01350 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> negv2 = v2.<a class="code" href="group__ExprPkg.html#gab1ce461dc931af73bf04e88c8d37dcbc">negate</a>();
<a name="l01351"></a>01351 clauses.push_back(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>, negV, negv1, v2));
<a name="l01352"></a>01352 clauses.push_back(v.<a class="code" href="group__ExprPkg.html#gaf310870d783fff343e77ba9c2277c626">orExpr</a>(v1));
<a name="l01353"></a>01353 clauses.push_back(v.<a class="code" href="group__ExprPkg.html#gaf310870d783fff343e77ba9c2277c626">orExpr</a>(negv2));
<a name="l01354"></a>01354 }
<a name="l01355"></a>01355 <span class="keywordflow">break</span>;
<a name="l01356"></a>01356 <span class="keywordflow">case</span> <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3a4cfaf3eae8eac1dc2fd27d9f0994dc">ITE</a>: {
<a name="l01357"></a>01357 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& v1 = phi[0];
<a name="l01358"></a>01358 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& v2 = phi[1];
<a name="l01359"></a>01359 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& v3 = phi[2];
<a name="l01360"></a>01360 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& negV = v.<a class="code" href="group__ExprPkg.html#gab1ce461dc931af73bf04e88c8d37dcbc">negate</a>();
<a name="l01361"></a>01361 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& negv1 = v1.<a class="code" href="group__ExprPkg.html#gab1ce461dc931af73bf04e88c8d37dcbc">negate</a>();
<a name="l01362"></a>01362 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& negv2 = v2.<a class="code" href="group__ExprPkg.html#gab1ce461dc931af73bf04e88c8d37dcbc">negate</a>();
<a name="l01363"></a>01363 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& negv3 = v3.<a class="code" href="group__ExprPkg.html#gab1ce461dc931af73bf04e88c8d37dcbc">negate</a>();
<a name="l01364"></a>01364 clauses.push_back(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>, negV, negv1, v2));
<a name="l01365"></a>01365 clauses.push_back(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>, negV, v1, v3));
<a name="l01366"></a>01366 clauses.push_back(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>, v, negv1, negv2));
<a name="l01367"></a>01367 clauses.push_back(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba96727447c0ad447987df1c6415aef074">OR</a>, v, v1, negv3));
<a name="l01368"></a>01368 }
<a name="l01369"></a>01369 <span class="keywordflow">break</span>;
<a name="l01370"></a>01370 <span class="keywordflow">default</span>:
<a name="l01371"></a>01371 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"SearchEngineTheoremProducer::convertToCNF: "</span>
<a name="l01372"></a>01372 <span class="stringliteral">"bad operator in phi = "</span>+phi.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l01373"></a>01373 <span class="keywordflow">break</span>;
<a name="l01374"></a>01374 }
<a name="l01375"></a>01375 <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#ad4258158bba138eb54b9080af7f8223a">andExpr</a>(clauses);
<a name="l01376"></a>01376 }
<a name="l01377"></a>01377 <span class="comment"></span>
<a name="l01378"></a>01378 <span class="comment">///////////////////////////////////////////////////////////////////////</span>
<a name="l01379"></a>01379 <span class="comment"></span><span class="comment">// helper functions for CNF converters</span><span class="comment"></span>
<a name="l01380"></a>01380 <span class="comment">///////////////////////////////////////////////////////////////////////</span>
<a name="l01381"></a>01381 <span class="comment"></span>
<a name="l01382"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a4af17425aaf7d8a28aaf1d8a09241535">01382</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a4af17425aaf7d8a28aaf1d8a09241535" title="checks if phi has v in local cache of opCNFRule, if so reuse v.">SearchEngineTheoremProducer::findInLocalCache</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& i,
<a name="l01383"></a>01383 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a>& localCache,
<a name="l01384"></a>01384 vector<Expr>& boundVars) {
<a name="l01385"></a>01385 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"findInLocalCache("</span>, i.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>(), <span class="stringliteral">") { "</span>);
<a name="l01386"></a>01386 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> boundVar;
<a name="l01387"></a>01387 <span class="keywordtype">unsigned</span> <span class="keywordtype">int</span> negationDepth = 0;
<a name="l01388"></a>01388 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr>::iterator</a> it;
<a name="l01389"></a>01389
<a name="l01390"></a>01390 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> phi = i;
<a name="l01391"></a>01391 <span class="keywordflow">while</span>(phi.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>()) {
<a name="l01392"></a>01392 phi = phi[0];
<a name="l01393"></a>01393 negationDepth++;
<a name="l01394"></a>01394 }
<a name="l01395"></a>01395
<a name="l01396"></a>01396 it = localCache.<a class="code" href="classCVC3_1_1ExprMap.html#ae50ab1874dd63b575553e7db769abe28">find</a>(phi);
<a name="l01397"></a>01397 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> v;
<a name="l01398"></a>01398 <span class="keywordflow">if</span>(it != localCache.<a class="code" href="classCVC3_1_1ExprMap.html#a283ae6c44308cbdda0d82da5a16e52c8">end</a>()) {
<a name="l01399"></a>01399 v = ((*it).second)[1];
<a name="l01400"></a>01400 <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(debugger.counter(<span class="stringliteral">"CNF Local Cache Hits"</span>)++;)
<a name="l01401"></a>01401 }
<a name="l01402"></a>01402 <span class="keywordflow">else</span> {
<a name="l01403"></a>01403 v = <a class="code" href="classCVC3_1_1TheoremProducer.html#a1b706238281ad141a57363a6890f14a5">d_em</a>-><a class="code" href="group__EM__Priv.html#ga22dbb23f716cc73378d4c69d564e38dd">newBoundVarExpr</a>(i.<a class="code" href="group__ExprPkg.html#ga42929221eb172250697b72c28af6de07" title="Get the type. Recursively compute if necessary.">getType</a>());
<a name="l01404"></a>01404 boundVars.push_back(v);
<a name="l01405"></a>01405 localCache[phi] = phi.<a class="code" href="group__ExprPkg.html#gaae017ca8e68af655ba285c985dd9fba5">iffExpr</a>(v);
<a name="l01406"></a>01406 }
<a name="l01407"></a>01407 <span class="keywordflow">if</span>(negationDepth % 2 != 0)
<a name="l01408"></a>01408 v = !v;
<a name="l01409"></a>01409 <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7fa27e82c6c4f69434225ed81e5d151e">TRACE</a>(<span class="stringliteral">"mycnf"</span>, <span class="stringliteral">"findInLocalCache => "</span>, v, <span class="stringliteral">" }"</span>);
<a name="l01410"></a>01410 <span class="keywordflow">return</span> v;
<a name="l01411"></a>01411 }
<a name="l01412"></a>01412
<a name="l01413"></a>01413
<a name="l01414"></a>01414
<a name="l01415"></a>01415 <span class="comment">// for LFSC proof style, by yeting</span>
<a name="l01416"></a>01416
<a name="l01417"></a>01417
<a name="l01418"></a>01418 <span class="comment">// theorem for minisat generated proofs, by yeting</span>
<a name="l01419"></a><a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a211e687727973cff1b055a7302d562ae">01419</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a211e687727973cff1b055a7302d562ae">SearchEngineTheoremProducer::satProof</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& queryExpr, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Proof.html">Proof</a>& <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#a211e687727973cff1b055a7302d562ae">satProof</a>) {
<a name="l01420"></a>01420 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l01421"></a>01421 <span class="keywordflow">if</span>(<a class="code" href="classCVC3_1_1TheoremProducer.html#aceb1eeebc6b491b3241f463488471f3a" title="Testing whether to generate proofs.">withProof</a>())
<a name="l01422"></a>01422 pf = <a class="code" href="classCVC3_1_1TheoremProducer.html#a9a8e67b1fb33d5dfe428a659d8c66651">newPf</a>(<span class="stringliteral">"minisat_proof"</span>, queryExpr, satProof);
<a name="l01423"></a>01423
<a name="l01424"></a>01424 <span class="keywordflow">if</span> ((<a class="code" href="classCVC3_1_1TheoremProducer.html#a27015759e6bdfced928fc5a2d9877b7d">d_tm</a>-><a class="code" href="classCVC3_1_1TheoremManager.html#aac1a2b8c8dbec2d6e92c08fb0eaf2ec7">getFlags</a>()[<span class="stringliteral">"lfsc-mode"</span>]).getInt()!= 0)
<a name="l01425"></a>01425 {
<a name="l01426"></a>01426 <span class="comment">// UNCOMMENT THIS FOR LFSC</span>
<a name="l01427"></a>01427
<a name="l01428"></a>01428 <span class="keywordflow">if</span>(!<a class="code" href="search__theorem__producer_8cpp.html#ad48a265d67710c19ae70a239a42cc9f3">lfsc_called</a>){
<a name="l01429"></a>01429 <span class="keywordtype">int</span> lfscm = (<a class="code" href="classCVC3_1_1TheoremProducer.html#a27015759e6bdfced928fc5a2d9877b7d">d_tm</a>-><a class="code" href="classCVC3_1_1TheoremManager.html#aac1a2b8c8dbec2d6e92c08fb0eaf2ec7">getFlags</a>()[<span class="stringliteral">"lfsc-mode"</span>]).getInt();
<a name="l01430"></a>01430 std::vector<Expr> assumps;
<a name="l01431"></a>01431 <a class="code" href="search__theorem__producer_8cpp.html#a735bfac5de1621927af23c4fbc78c257">search_engine</a>-><a class="code" href="group__SE.html#ga43f52699cddc6e0feffffaf22424fe47" title="Get all user assumptions made in this and all previous contexts.">getUserAssumptions</a>(assumps);
<a name="l01432"></a>01432
<a name="l01433"></a>01433 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> pf_expr = pf.<a class="code" href="classCVC3_1_1Proof.html#a20cd8a5db4f7f07155464880300fb4c9">getExpr</a>()[2] ;
<a name="l01434"></a>01434 <span class="keywordflow">if</span>( lfscm == -1 ){
<a name="l01435"></a>01435 cout << <span class="stringliteral">"CVC3 Proof: "</span>;
<a name="l01436"></a>01436 cout << pf.<a class="code" href="classCVC3_1_1Proof.html#a20cd8a5db4f7f07155464880300fb4c9">getExpr</a>() << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l01437"></a>01437 }<span class="keywordflow">else</span>{
<a name="l01438"></a>01438 <a class="code" href="classLFSCPrinter.html">LFSCPrinter</a>* lfsc_printer = <span class="keyword">new</span> <a class="code" href="classLFSCPrinter.html">LFSCPrinter</a>(pf_expr, queryExpr, assumps, lfscm, <a class="code" href="classCVC3_1_1SearchEngineTheoremProducer.html#abb70faf5bb0eccda31e8ff06a46f2b65">d_commonRules</a>);
<a name="l01439"></a>01439 lfsc_printer-><a class="code" href="classLFSCPrinter.html#a726e72561b6c3dc2257af189667c17a6">print_LFSC</a>(pf_expr);
<a name="l01440"></a>01440 <a class="code" href="search__theorem__producer_8cpp.html#ad48a265d67710c19ae70a239a42cc9f3">lfsc_called</a> = <span class="keyword">true</span>;
<a name="l01441"></a>01441 exit( 0 );
<a name="l01442"></a>01442 }
<a name="l01443"></a>01443 }
<a name="l01444"></a>01444
<a name="l01445"></a>01445 }
<a name="l01446"></a>01446
<a name="l01447"></a>01447 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1TheoremProducer.html#ab3afa2471d244b129865548afe06ca89" title="Create a new theorem. See also newRWTheorem() and newReflTheorem()">newTheorem</a>(queryExpr, <a class="code" href="classCVC3_1_1Assumptions.html#af309a39e2e013cc62b6d94c5812ad86b">Assumptions::emptyAssump</a>() , pf);
<a name="l01448"></a>01448 }
<a name="l01449"></a>01449
<a name="l01450"></a>01450
<a name="l01451"></a>01451 <span class="comment">// LocalWords: clc</span>
</pre></div></div>
</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>
