<!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: quant_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">quant_theorem_producer.cpp</div> </div>
</div>
<div class="contents">
<a href="quant__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 quant_theorem_producer.cpp</span>
<a name="l00004"></a>00004 <span class="comment"> *</span>
<a name="l00005"></a>00005 <span class="comment"> * Author: Daniel Wichs, Yeting Ge</span>
<a name="l00006"></a>00006 <span class="comment"> *</span>
<a name="l00007"></a>00007 <span class="comment"> * Created: Jul 07 22:22:38 GMT 2003</span>
<a name="l00008"></a>00008 <span class="comment"> *</span>
<a name="l00009"></a>00009 <span class="comment"> * <hr></span>
<a name="l00010"></a>00010 <span class="comment"> *</span>
<a name="l00011"></a>00011 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00012"></a>00012 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00013"></a>00013 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00014"></a>00014 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00015"></a>00015 <span class="comment"> *</span>
<a name="l00016"></a>00016 <span class="comment"> * <hr></span>
<a name="l00017"></a>00017 <span class="comment"> *</span>
<a name="l00018"></a>00018 <span class="comment"> * CLASS: QuantProofRules</span>
<a name="l00019"></a>00019 <span class="comment"> *</span>
<a name="l00020"></a>00020 <span class="comment"> *</span>
<a name="l00021"></a>00021 <span class="comment"> * Description: TRUSTED implementation of arithmetic proof rules.</span>
<a name="l00022"></a>00022 <span class="comment"> *</span>
<a name="l00023"></a>00023 <span class="comment"> */</span>
<a name="l00024"></a>00024 <span class="comment">/*****************************************************************************/</span>
<a name="l00025"></a>00025
<a name="l00026"></a>00026 <span class="comment">// This code is trusted</span>
<a name="l00027"></a><a class="code" href="quant__theorem__producer_8cpp.html#a8663c36bbf15bb5a0dcb01b97897fa95">00027</a> <span class="preprocessor">#define _CVC3_TRUSTED_</span>
<a name="l00028"></a>00028 <span class="preprocessor"></span>
<a name="l00029"></a>00029
<a name="l00030"></a>00030 <span class="preprocessor">#include "<a class="code" href="quant__theorem__producer_8h.html">quant_theorem_producer.h</a>"</span>
<a name="l00031"></a>00031 <span class="preprocessor">#include "<a class="code" href="theory__quant_8h.html">theory_quant.h</a>"</span>
<a name="l00032"></a>00032 <span class="preprocessor">#include "<a class="code" href="theory__core_8h.html">theory_core.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
<a name="l00039"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a493eb80061815c95bab507f41343b260">00039</a> <a class="code" href="classCVC3_1_1QuantProofRules.html">QuantProofRules</a>* TheoryQuant::createProofRules() {
<a name="l00040"></a>00040 <span class="keywordflow">return</span> <span class="keyword">new</span> <a class="code" href="classCVC3_1_1QuantTheoremProducer.html">QuantTheoremProducer</a>(theoryCore()->getTM(), <span class="keyword">this</span>);
<a name="l00041"></a>00041 }
<a name="l00042"></a>00042
<a name="l00043"></a>00043
<a name="l00044"></a><a class="code" href="quant__theorem__producer_8cpp.html#a79f2713d570c7065f61a160134ea765b">00044</a> <span class="preprocessor">#define CLASS_NAME "CVC3::QuantTheoremProducer"</span>
<a name="l00045"></a>00045 <span class="preprocessor"></span>
<a name="l00046"></a>00046 <span class="comment"></span>
<a name="l00047"></a>00047 <span class="comment">//! ==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e</span>
<a name="l00048"></a>00048 <span class="comment"></span><a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00049"></a><a class="code" href="classCVC3_1_1QuantTheoremProducer.html#af59e47a4b45f624d2d8e088d5668f596">00049</a> QuantTheoremProducer::rewriteNotForall(<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="l00050"></a>00050 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00051"></a>00051 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(e.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() && e[0].<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>(),
<a name="l00052"></a>00052 <span class="stringliteral">"rewriteNotForall: expr must be NOT FORALL:\n"</span>
<a name="l00053"></a>00053 +e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00054"></a>00054 }
<a name="l00055"></a>00055 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00056"></a>00056 <span class="keywordflow">if</span>(withProof())
<a name="l00057"></a>00057 pf = newPf(<span class="stringliteral">"rewrite_not_forall"</span>, e);
<a name="l00058"></a>00058 <span class="keywordflow">return</span> newRWTheorem(e, e.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga0d2ff7603a249b30b2df4e549607ad6e">newClosureExpr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3197625a1bb2264943f5a95f236d9973">EXISTS</a>, e[0].getVars(),
<a name="l00059"></a>00059 !e[0].getBody()),
<a name="l00060"></a>00060 Assumptions::emptyAssump(), pf);
<a name="l00061"></a>00061 }
<a name="l00062"></a>00062
<a name="l00063"></a>00063 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00064"></a><a class="code" href="classCVC3_1_1QuantTheoremProducer.html#a6a234dee95bb3059e0e651c838c9458b">00064</a> QuantTheoremProducer::addNewConst(<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="l00065"></a>00065 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00066"></a>00066 <span class="keywordflow">if</span>(withProof())
<a name="l00067"></a>00067 pf = newPf(<span class="stringliteral">"add_new_const"</span>, e);
<a name="l00068"></a>00068 <span class="keywordflow">return</span> newTheorem(e, Assumptions::emptyAssump(), pf);
<a name="l00069"></a>00069 }
<a name="l00070"></a>00070 <span class="comment"></span>
<a name="l00071"></a>00071 <span class="comment">///do not use this rule, this is for debug only</span>
<a name="l00072"></a>00072 <span class="comment"></span><a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00073"></a><a class="code" href="classCVC3_1_1QuantTheoremProducer.html#a93e4e3adc9c630a975631a823ec23fbf">00073</a> QuantTheoremProducer::newRWThm(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& newE) {
<a name="l00074"></a>00074 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00075"></a>00075 <span class="keywordflow">if</span>(withProof())
<a name="l00076"></a>00076 pf = newPf(<span class="stringliteral">"from cache"</span>, e);
<a name="l00077"></a>00077 <span class="keywordflow">return</span> newRWTheorem(e, newE,Assumptions::emptyAssump(), pf);
<a name="l00078"></a>00078 }
<a name="l00079"></a>00079
<a name="l00080"></a>00080
<a name="l00081"></a>00081 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>
<a name="l00082"></a><a class="code" href="classCVC3_1_1QuantTheoremProducer.html#a31d81dce768ab5c942dedcac88977469">00082</a> QuantTheoremProducer::normalizeQuant(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& quant) {
<a name="l00083"></a>00083 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00084"></a>00084 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(quant.<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>()||quant.<a class="code" href="group__ExprPkg.html#ga1c922163af59ed6bc101728d65e04d16">isExists</a>(),
<a name="l00085"></a>00085 <span class="stringliteral">"normalizeQuant: expr must be FORALL or EXISTS\n"</span>
<a name="l00086"></a>00086 +quant.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00087"></a>00087 }
<a name="l00088"></a>00088
<a name="l00089"></a>00089
<a name="l00090"></a>00090 std::map<Expr,int>::iterator typeIter;
<a name="l00091"></a>00091 std::string base(<span class="stringliteral">"_BD"</span>);
<a name="l00092"></a>00092 <span class="keywordtype">int</span> counter(0);
<a name="l00093"></a>00093
<a name="l00094"></a>00094 vector<Expr> newVars;
<a name="l00095"></a>00095 <span class="keyword">const</span> std::vector<Expr>& cur_vars = quant.<a class="code" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd" title="Get bound variables from a closure Expr.">getVars</a>();
<a name="l00096"></a>00096 <span class="keywordflow">for</span>(<span class="keywordtype">size_t</span> j =0; j<cur_vars.size(); j++){
<a name="l00097"></a>00097 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> t = cur_vars[j].getType();
<a name="l00098"></a>00098 <span class="keywordtype">int</span> typeIndex ;
<a name="l00099"></a>00099
<a name="l00100"></a>00100 typeIter = d_typeFound.find(t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>());
<a name="l00101"></a>00101
<a name="l00102"></a>00102 <span class="keywordflow">if</span>(d_typeFound.end() == typeIter){
<a name="l00103"></a>00103 typeIndex = d_typeFound.size();
<a name="l00104"></a>00104 d_typeFound[t.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>()] = typeIndex;
<a name="l00105"></a>00105 }
<a name="l00106"></a>00106 <span class="keywordflow">else</span>{
<a name="l00107"></a>00107 typeIndex = typeIter->second;
<a name="l00108"></a>00108 }
<a name="l00109"></a>00109
<a name="l00110"></a>00110 counter++;
<a name="l00111"></a>00111 std::stringstream stringType;
<a name="l00112"></a>00112 stringType << counter << <span class="stringliteral">"TY"</span> << typeIndex ;
<a name="l00113"></a>00113 std::string out_str = base + stringType.str();
<a name="l00114"></a>00114 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newExpr = d_theoryQuant-><a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga22dbb23f716cc73378d4c69d564e38dd">newBoundVarExpr</a>(out_str, <a class="code" href="namespaceCVC3.html#af69618103f1f0f2eadada0796a2a940c">int2string</a>(counter));
<a name="l00115"></a>00115 newExpr.<a class="code" href="group__ExprPkg.html#ga07d47f902598e00097086deabf04d9c5" title="Set the cached type.">setType</a>(t);
<a name="l00116"></a>00116 newVars.push_back(newExpr);
<a name="l00117"></a>00117 }
<a name="l00118"></a>00118
<a name="l00119"></a>00119 vector<vector<Expr> > trigs = quant.<a class="code" href="group__ExprPkg.html#gae4cffec57be4b7d81e8486328c2396fc" title="Get the manual triggers of the closure Expr.">getTriggers</a>();
<a name="l00120"></a>00120 <span class="keywordflow">for</span>(<span class="keywordtype">size_t</span> i = 0 ; i < trigs.size(); i++){
<a name="l00121"></a>00121 <span class="keywordflow">for</span>(<span class="keywordtype">size_t</span> j = 0 ; j < trigs[i].size(); j++){
<a name="l00122"></a>00122 trigs[i][j] = trigs[i][j].substExpr(cur_vars,newVars);
<a name="l00123"></a>00123 }
<a name="l00124"></a>00124 }
<a name="l00125"></a>00125
<a name="l00126"></a>00126 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> normBody = quant.<a class="code" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940" title="Get the body of the closure Expr.">getBody</a>().<a class="code" href="group__ExprPkg.html#ga95e18015860195a80b317bf756055786">substExpr</a>(cur_vars,newVars);
<a name="l00127"></a>00127 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> normQuant = d_theoryQuant-><a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga0d2ff7603a249b30b2df4e549607ad6e">newClosureExpr</a>(quant.<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>()?<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7b7b6f6e2b88589bd4656a14bcb7eb94">FORALL</a>:<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3197625a1bb2264943f5a95f236d9973">EXISTS</a>, newVars, normBody, trigs);
<a name="l00128"></a>00128
<a name="l00129"></a>00129 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00130"></a>00130 <span class="keywordflow">if</span>(withProof())
<a name="l00131"></a>00131 pf = newPf(<span class="stringliteral">"normalizeQuant"</span>, quant, normQuant);
<a name="l00132"></a>00132
<a name="l00133"></a>00133 <span class="keywordflow">return</span> newRWTheorem(quant, normQuant, Assumptions::emptyAssump(), pf);
<a name="l00134"></a>00134
<a name="l00135"></a>00135 }
<a name="l00136"></a>00136
<a name="l00137"></a>00137 <span class="comment"></span>
<a name="l00138"></a>00138 <span class="comment">//! ==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e</span>
<a name="l00139"></a><a class="code" href="classCVC3_1_1QuantTheoremProducer.html#a658fde1235cb9668d454cbe9144b1da9">00139</a> <span class="comment"></span><a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> QuantTheoremProducer::rewriteNotExists(<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="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>(e.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() && e[0].<a class="code" href="group__ExprPkg.html#ga1c922163af59ed6bc101728d65e04d16">isExists</a>(),
<a name="l00142"></a>00142 <span class="stringliteral">"rewriteNotExists: expr must be NOT FORALL:\n"</span>
<a name="l00143"></a>00143 +e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00144"></a>00144 }
<a name="l00145"></a>00145 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00146"></a>00146 <span class="keywordflow">if</span>(withProof())
<a name="l00147"></a>00147 pf = newPf(<span class="stringliteral">"rewrite_not_exists"</span>, e);
<a name="l00148"></a>00148 <span class="keywordflow">return</span> newRWTheorem(e, e.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga0d2ff7603a249b30b2df4e549607ad6e">newClosureExpr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7b7b6f6e2b88589bd4656a14bcb7eb94">FORALL</a>, e[0].getVars(),
<a name="l00149"></a>00149 !e[0].getBody()),
<a name="l00150"></a>00150 Assumptions::emptyAssump(), pf);
<a name="l00151"></a>00151 }
<a name="l00152"></a>00152
<a name="l00153"></a>00153
<a name="l00154"></a><a class="code" href="classCVC3_1_1QuantTheoremProducer.html#a3cb05ffcc0b75525969c925fea988235">00154</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> QuantTheoremProducer::universalInst(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1, <span class="keyword">const</span> vector<Expr>& terms, <span class="keywordtype">int</span> quantLevel, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> gterm){
<a name="l00155"></a>00155 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e = t1.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>();
<a name="l00156"></a>00156 <span class="keyword">const</span> vector<Expr>& boundVars = e.<a class="code" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd" title="Get bound variables from a closure Expr.">getVars</a>();
<a name="l00157"></a>00157
<a name="l00158"></a>00158 <span class="keywordflow">for</span>(<span class="keywordtype">unsigned</span> <span class="keywordtype">int</span> i=0; i<terms.size(); i++){
<a name="l00159"></a>00159 <span class="keywordflow">if</span> (d_theoryQuant->getBaseType(boundVars[i]) !=
<a name="l00160"></a>00160 d_theoryQuant->getBaseType(terms[i])){
<a name="l00161"></a>00161 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00162"></a>00162 <span class="keywordflow">return</span> newRWTheorem(terms[i],terms[i],
<a name="l00163"></a>00163 Assumptions::emptyAssump(), pf);
<a name="l00164"></a>00164 }
<a name="l00165"></a>00165 <span class="comment">//this is the same as return a TRUE theorem, which will be ignored immeridatele. So, this is just return doing nothing. </span>
<a name="l00166"></a>00166 }
<a name="l00167"></a>00167
<a name="l00168"></a>00168
<a name="l00169"></a>00169 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00170"></a>00170 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(boundVars.size() == terms.size(),
<a name="l00171"></a>00171 <span class="stringliteral">"Universal instantiation: size of terms array does "</span>
<a name="l00172"></a>00172 <span class="stringliteral">"not match quanitfied variables array size"</span>);
<a name="l00173"></a>00173 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(e.<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>(),
<a name="l00174"></a>00174 <span class="stringliteral">"universal instantiation: expr must be FORALL:\n"</span>
<a name="l00175"></a>00175 +e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00176"></a>00176
<a name="l00177"></a>00177 <span class="keywordflow">for</span>(<span class="keywordtype">unsigned</span> <span class="keywordtype">int</span> i=0; i<terms.size(); i++)
<a name="l00178"></a>00178 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(d_theoryQuant->getBaseType(boundVars[i]) ==
<a name="l00179"></a>00179 d_theoryQuant->getBaseType(terms[i]),
<a name="l00180"></a>00180 <span class="stringliteral">"Universal instantiation: type mismatch"</span>);
<a name="l00181"></a>00181 }
<a name="l00182"></a>00182
<a name="l00183"></a>00183 <span class="comment">//build up a conjunction of type predicates for expression</span>
<a name="l00184"></a>00184 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> tr = e.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4471fca49c2acbb7b4cf71e72bc55d6a" title="TRUE Expr.">trueExpr</a>();
<a name="l00185"></a>00185 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> typePred = tr;
<a name="l00186"></a>00186 <span class="comment">// unsigned qlevel, qlevelMax = 0;</span>
<a name="l00187"></a>00187 <span class="keywordflow">for</span>(<span class="keywordtype">unsigned</span> <span class="keywordtype">int</span> i=0; i<terms.size(); i++) {
<a name="l00188"></a>00188 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> p = d_theoryQuant->getTypePred(boundVars[i].getType(),terms[i]);
<a name="l00189"></a>00189 <span class="keywordflow">if</span>(p!=tr) {
<a name="l00190"></a>00190 <span class="keywordflow">if</span>(typePred==tr)
<a name="l00191"></a>00191 typePred = p;
<a name="l00192"></a>00192 <span class="keywordflow">else</span>
<a name="l00193"></a>00193 typePred = typePred.<a class="code" href="group__ExprPkg.html#ga6c3651465ce69ed5f4e6fd461b9acf3c">andExpr</a>(p);
<a name="l00194"></a>00194 }
<a name="l00195"></a>00195 <span class="comment">// qlevel = d_theoryQuant->theoryCore()->getQuantLevelForTerm(terms[i]);</span>
<a name="l00196"></a>00196 <span class="comment">// if (qlevel > qlevelMax) qlevel = qlevelMax;</span>
<a name="l00197"></a>00197 }
<a name="l00198"></a>00198
<a name="l00199"></a>00199
<a name="l00200"></a>00200 <span class="comment">// Expr inst = e.getBody().substExprQuant(e.getVars(), terms);</span>
<a name="l00201"></a>00201 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> inst = e.<a class="code" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940" title="Get the body of the closure Expr.">getBody</a>().<a class="code" href="group__ExprPkg.html#ga95e18015860195a80b317bf756055786">substExpr</a>(e.<a class="code" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd" title="Get bound variables from a closure Expr.">getVars</a>(), terms);
<a name="l00202"></a>00202
<a name="l00203"></a>00203 <span class="comment">// Expr inst = e.getBody().substExpr(e.getVars(), terms);</span>
<a name="l00204"></a>00204
<a name="l00205"></a>00205
<a name="l00206"></a>00206 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00207"></a>00207 <span class="keywordflow">if</span>(withProof()) {
<a name="l00208"></a>00208 vector<Proof> pfs;
<a name="l00209"></a>00209 vector<Expr> es;
<a name="l00210"></a>00210 pfs.push_back(t1.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00211"></a>00211 es.push_back(e);
<a name="l00212"></a>00212 es.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#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a>,terms));
<a name="l00213"></a>00213 <span class="comment">// es.insert(es.end(), terms.begin(), terms.end());</span>
<a name="l00214"></a>00214 es.push_back(inst);
<a name="l00215"></a>00215 <span class="keywordflow">if</span> (gterm.<a class="code" href="group__ExprPkg.html#ga0265d1ca42fa59c95aaff3ca675b6504">isNull</a>()) {
<a name="l00216"></a>00216 es.push_back( d_theoryQuant->getEM()->newRatExpr(0));
<a name="l00217"></a>00217 }
<a name="l00218"></a>00218 <span class="keywordflow">else</span> {es.push_back(gterm);
<a name="l00219"></a>00219 }
<a name="l00220"></a>00220 pf= newPf(<span class="stringliteral">"universal_elimination1"</span>, es, pfs);
<a name="l00221"></a>00221 }
<a name="l00222"></a>00222
<a name="l00223"></a>00223
<a name="l00224"></a>00224 <span class="comment">// Expr inst = e.getBody().substExpr(e.getVars(), terms);</span>
<a name="l00225"></a>00225
<a name="l00226"></a>00226
<a name="l00227"></a>00227 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> imp;
<a name="l00228"></a>00228 <span class="keywordflow">if</span>(typePred == tr ) <span class="comment">//just for a easy life, yeting, change this assp</span>
<a name="l00229"></a>00229 imp = inst;
<a name="l00230"></a>00230 <span class="keywordflow">else</span>
<a name="l00231"></a>00231 imp = typePred.<a class="code" href="group__ExprPkg.html#ga8dd97bcdeb9d8870238f94a263fd083b">impExpr</a>(inst);
<a name="l00232"></a>00232 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> ret = newTheorem(imp, t1.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>(), pf);
<a name="l00233"></a>00233
<a name="l00234"></a>00234 <span class="keywordtype">int</span> thmLevel = t1.<a class="code" href="classCVC3_1_1Theorem.html#a26b6f0af9e9b2f2a8c22a7dcb9fbb0b1" title="Return quantification level for this theorem.">getQuantLevel</a>();
<a name="l00235"></a>00235 <span class="keywordflow">if</span>(quantLevel >= thmLevel) {
<a name="l00236"></a>00236 ret.<a class="code" href="classCVC3_1_1Theorem.html#ab3309c937f827595d1d92fa48cb5a471" title="Set the quantification level for this theorem.">setQuantLevel</a>(quantLevel+1);
<a name="l00237"></a>00237 }
<a name="l00238"></a>00238 <span class="keywordflow">else</span>{
<a name="l00239"></a>00239 ret.<a class="code" href="classCVC3_1_1Theorem.html#ab3309c937f827595d1d92fa48cb5a471" title="Set the quantification level for this theorem.">setQuantLevel</a>(thmLevel+1);
<a name="l00240"></a>00240 }
<a name="l00241"></a>00241
<a name="l00242"></a>00242 <span class="comment">// ret.setQuantLevel(quantLevel+1);</span>
<a name="l00243"></a>00243 <span class="keywordflow">return</span> ret;
<a name="l00244"></a>00244 }
<a name="l00245"></a>00245
<a name="l00246"></a>00246 <span class="comment"></span>
<a name="l00247"></a>00247 <span class="comment">//! Instantiate a universally quantified formula</span>
<a name="l00248"></a>00248 <span class="comment"></span><span class="comment">/*! From T|-FORALL(var): e generate T|-psi => e' where e' is obtained</span>
<a name="l00249"></a>00249 <span class="comment"> * from e by instantiating bound variables with terms in</span>
<a name="l00250"></a>00250 <span class="comment"> * vector<Expr>& terms. The vector of terms should be the same</span>
<a name="l00251"></a>00251 <span class="comment"> * size as the vector of bound variables in e. Also elements in</span>
<a name="l00252"></a>00252 <span class="comment"> * each position i need to have matching base types. psi is the conjunction of</span>
<a name="l00253"></a>00253 <span class="comment"> * subtype predicates for the bound variables of the quanitfied expression.</span>
<a name="l00254"></a>00254 <span class="comment"> * \param t1 the quantifier (a Theorem)</span>
<a name="l00255"></a>00255 <span class="comment"> * \param terms the terms to instantiate.</span>
<a name="l00256"></a>00256 <span class="comment"> * \param quantLevel the quantification level for the formula</span>
<a name="l00257"></a>00257 <span class="comment"> */</span>
<a name="l00258"></a><a class="code" href="classCVC3_1_1QuantTheoremProducer.html#a1122f38e6d7ea2caeab8a0cd0d68d044">00258</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> QuantTheoremProducer::universalInst(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1, <span class="keyword">const</span> vector<Expr>& terms, <span class="keywordtype">int</span> quantLevel){
<a name="l00259"></a>00259
<a name="l00260"></a>00260 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e = t1.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>();
<a name="l00261"></a>00261 <span class="keyword">const</span> vector<Expr>& boundVars = e.<a class="code" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd" title="Get bound variables from a closure Expr.">getVars</a>();
<a name="l00262"></a>00262 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00263"></a>00263 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(boundVars.size() == terms.size(),
<a name="l00264"></a>00264 <span class="stringliteral">"Universal instantiation: size of terms array does "</span>
<a name="l00265"></a>00265 <span class="stringliteral">"not match quanitfied variables array size"</span>);
<a name="l00266"></a>00266 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(e.<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>(),
<a name="l00267"></a>00267 <span class="stringliteral">"universal instantiation: expr must be FORALL:\n"</span>
<a name="l00268"></a>00268 +e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00269"></a>00269 <span class="keywordflow">for</span>(<span class="keywordtype">unsigned</span> <span class="keywordtype">int</span> i=0; i<terms.size(); i++)
<a name="l00270"></a>00270 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(d_theoryQuant->getBaseType(boundVars[i]) ==
<a name="l00271"></a>00271 d_theoryQuant->getBaseType(terms[i]),
<a name="l00272"></a>00272 <span class="stringliteral">"Universal instantiation: type mismatch"</span>);
<a name="l00273"></a>00273 }
<a name="l00274"></a>00274
<a name="l00275"></a>00275 <span class="comment">//build up a conjunction of type predicates for expression</span>
<a name="l00276"></a>00276 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> tr = e.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4471fca49c2acbb7b4cf71e72bc55d6a" title="TRUE Expr.">trueExpr</a>();
<a name="l00277"></a>00277 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> typePred = tr;
<a name="l00278"></a>00278 <span class="comment">// unsigned qlevel, qlevelMax = 0;</span>
<a name="l00279"></a>00279 <span class="keywordflow">for</span>(<span class="keywordtype">unsigned</span> <span class="keywordtype">int</span> i=0; i<terms.size(); i++) {
<a name="l00280"></a>00280 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> p = d_theoryQuant->getTypePred(boundVars[i].getType(),terms[i]);
<a name="l00281"></a>00281 <span class="keywordflow">if</span>(p!=tr) {
<a name="l00282"></a>00282 <span class="keywordflow">if</span>(typePred==tr)
<a name="l00283"></a>00283 typePred = p;
<a name="l00284"></a>00284 <span class="keywordflow">else</span>
<a name="l00285"></a>00285 typePred = typePred.<a class="code" href="group__ExprPkg.html#ga6c3651465ce69ed5f4e6fd461b9acf3c">andExpr</a>(p);
<a name="l00286"></a>00286 }
<a name="l00287"></a>00287 <span class="comment">// qlevel = d_theoryQuant->theoryCore()->getQuantLevelForTerm(terms[i]);</span>
<a name="l00288"></a>00288 <span class="comment">// if (qlevel > qlevelMax) qlevel = qlevelMax;</span>
<a name="l00289"></a>00289 }
<a name="l00290"></a>00290
<a name="l00291"></a>00291 <span class="comment">//Expr inst = e.getBody().substExprQuant(e.getVars(), terms);</span>
<a name="l00292"></a>00292 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> inst = e.<a class="code" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940" title="Get the body of the closure Expr.">getBody</a>().<a class="code" href="group__ExprPkg.html#ga95e18015860195a80b317bf756055786">substExpr</a>(e.<a class="code" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd" title="Get bound variables from a closure Expr.">getVars</a>(), terms);
<a name="l00293"></a>00293
<a name="l00294"></a>00294
<a name="l00295"></a>00295 <span class="comment">// Expr inst = e.getBody().substExpr(e.getVars(), terms);</span>
<a name="l00296"></a>00296
<a name="l00297"></a>00297
<a name="l00298"></a>00298 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00299"></a>00299 <span class="keywordflow">if</span>(withProof()) {
<a name="l00300"></a>00300 vector<Proof> pfs;
<a name="l00301"></a>00301 vector<Expr> es;
<a name="l00302"></a>00302 pfs.push_back(t1.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00303"></a>00303 es.push_back(e);
<a name="l00304"></a>00304 es.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#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a>,terms));
<a name="l00305"></a>00305 <span class="comment">// es.insert(es.end(), terms.begin(), terms.end());</span>
<a name="l00306"></a>00306 es.push_back(inst);
<a name="l00307"></a>00307 pf= newPf(<span class="stringliteral">"universal_elimination2"</span>, es, pfs);
<a name="l00308"></a>00308 }
<a name="l00309"></a>00309
<a name="l00310"></a>00310 <span class="comment">// Expr inst = e.getBody().substExpr(e.getVars(), terms);</span>
<a name="l00311"></a>00311
<a name="l00312"></a>00312
<a name="l00313"></a>00313 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> imp;
<a name="l00314"></a>00314 <span class="keywordflow">if</span>(typePred == tr) <span class="comment">//just for a easy life, yeting, change this assp</span>
<a name="l00315"></a>00315 imp = inst;
<a name="l00316"></a>00316 <span class="keywordflow">else</span>
<a name="l00317"></a>00317 imp = typePred.<a class="code" href="group__ExprPkg.html#ga8dd97bcdeb9d8870238f94a263fd083b">impExpr</a>(inst);
<a name="l00318"></a>00318 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> ret = newTheorem(imp, t1.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>(), pf);
<a name="l00319"></a>00319
<a name="l00320"></a>00320 <span class="keywordtype">int</span> thmLevel = t1.<a class="code" href="classCVC3_1_1Theorem.html#a26b6f0af9e9b2f2a8c22a7dcb9fbb0b1" title="Return quantification level for this theorem.">getQuantLevel</a>();
<a name="l00321"></a>00321 <span class="keywordflow">if</span>(quantLevel >= thmLevel) {
<a name="l00322"></a>00322 ret.<a class="code" href="classCVC3_1_1Theorem.html#ab3309c937f827595d1d92fa48cb5a471" title="Set the quantification level for this theorem.">setQuantLevel</a>(quantLevel+1);
<a name="l00323"></a>00323 }
<a name="l00324"></a>00324 <span class="keywordflow">else</span>{
<a name="l00325"></a>00325 ret.<a class="code" href="classCVC3_1_1Theorem.html#ab3309c937f827595d1d92fa48cb5a471" title="Set the quantification level for this theorem.">setQuantLevel</a>(thmLevel+1);
<a name="l00326"></a>00326 }
<a name="l00327"></a>00327
<a name="l00328"></a>00328 <span class="comment">// ret.setQuantLevel(quantLevel+1);</span>
<a name="l00329"></a>00329 <span class="keywordflow">return</span> ret;
<a name="l00330"></a>00330 }
<a name="l00331"></a>00331
<a name="l00332"></a><a class="code" href="classCVC3_1_1QuantTheoremProducer.html#ae47e344bc2d5bcd2665cdbd2e010c456">00332</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> QuantTheoremProducer::universalInst(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1, <span class="keyword">const</span> vector<Expr>& terms){
<a name="l00333"></a>00333
<a name="l00334"></a>00334 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e = t1.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>();
<a name="l00335"></a>00335 <span class="keyword">const</span> vector<Expr>& boundVars = e.<a class="code" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd" title="Get bound variables from a closure Expr.">getVars</a>();
<a name="l00336"></a>00336 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00337"></a>00337 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(boundVars.size() == terms.size(),
<a name="l00338"></a>00338 <span class="stringliteral">"Universal instantiation: size of terms array does "</span>
<a name="l00339"></a>00339 <span class="stringliteral">"not match quanitfied variables array size"</span>);
<a name="l00340"></a>00340 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(e.<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>(),
<a name="l00341"></a>00341 <span class="stringliteral">"universal instantiation: expr must be FORALL:\n"</span>
<a name="l00342"></a>00342 +e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00343"></a>00343 <span class="keywordflow">for</span>(<span class="keywordtype">unsigned</span> <span class="keywordtype">int</span> i=0; i<terms.size(); i++)
<a name="l00344"></a>00344 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(d_theoryQuant->getBaseType(boundVars[i]) ==
<a name="l00345"></a>00345 d_theoryQuant->getBaseType(terms[i]),
<a name="l00346"></a>00346 <span class="stringliteral">"Universal instantiation: type mismatch"</span>);
<a name="l00347"></a>00347 }
<a name="l00348"></a>00348
<a name="l00349"></a>00349 <span class="comment">//build up a conjunction of type predicates for expression</span>
<a name="l00350"></a>00350 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> tr = e.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4471fca49c2acbb7b4cf71e72bc55d6a" title="TRUE Expr.">trueExpr</a>();
<a name="l00351"></a>00351 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> typePred = tr;
<a name="l00352"></a>00352 <span class="keywordtype">unsigned</span> qlevel=0, qlevelMax = 0;
<a name="l00353"></a>00353 <span class="keywordflow">for</span>(<span class="keywordtype">unsigned</span> <span class="keywordtype">int</span> i=0; i<terms.size(); i++) {
<a name="l00354"></a>00354 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> p = d_theoryQuant->getTypePred(boundVars[i].getType(),terms[i]);
<a name="l00355"></a>00355 <span class="keywordflow">if</span>(p!=tr) {
<a name="l00356"></a>00356 <span class="keywordflow">if</span>(typePred==tr)
<a name="l00357"></a>00357 typePred = p;
<a name="l00358"></a>00358 <span class="keywordflow">else</span>
<a name="l00359"></a>00359 typePred = typePred.<a class="code" href="group__ExprPkg.html#ga6c3651465ce69ed5f4e6fd461b9acf3c">andExpr</a>(p);
<a name="l00360"></a>00360 }
<a name="l00361"></a>00361 qlevel = d_theoryQuant->theoryCore()->getQuantLevelForTerm(terms[i]);
<a name="l00362"></a>00362 <span class="keywordflow">if</span> (qlevel > qlevelMax) qlevel = qlevelMax;
<a name="l00363"></a>00363 }
<a name="l00364"></a>00364
<a name="l00365"></a>00365 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> inst = e.<a class="code" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940" title="Get the body of the closure Expr.">getBody</a>().<a class="code" href="group__ExprPkg.html#ga95e18015860195a80b317bf756055786">substExpr</a>(e.<a class="code" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd" title="Get bound variables from a closure Expr.">getVars</a>(), terms);
<a name="l00366"></a>00366 <span class="comment">// Expr inst = e.getBody().substExprQuant(e.getVars(), terms);</span>
<a name="l00367"></a>00367
<a name="l00368"></a>00368
<a name="l00369"></a>00369 <span class="comment">// Expr inst = e.getBody().substExpr(e.getVars(), terms);</span>
<a name="l00370"></a>00370
<a name="l00371"></a>00371 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00372"></a>00372 <span class="keywordflow">if</span>(withProof()) {
<a name="l00373"></a>00373 vector<Proof> pfs;
<a name="l00374"></a>00374 vector<Expr> es;
<a name="l00375"></a>00375 pfs.push_back(t1.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00376"></a>00376 es.push_back(e);
<a name="l00377"></a>00377 es.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#aa10c9e8951b8ccf714a59ec321bdac5ba60238049e233c8d68fc58e4d5ceb55e2">RAW_LIST</a>,terms));
<a name="l00378"></a>00378 <span class="comment">// es.insert(es.end(), terms.begin(), terms.end());</span>
<a name="l00379"></a>00379 es.push_back(inst);
<a name="l00380"></a>00380 pf= newPf(<span class="stringliteral">"universal_elimination3"</span>, es, pfs);
<a name="l00381"></a>00381 }
<a name="l00382"></a>00382
<a name="l00383"></a>00383 <span class="comment">// Expr inst = e.getBody().substExpr(e.getVars(), terms);</span>
<a name="l00384"></a>00384
<a name="l00385"></a>00385 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> imp;
<a name="l00386"></a>00386 <span class="keywordflow">if</span>( typePred == tr ) <span class="comment">//just for easy life, yeting, change this asap</span>
<a name="l00387"></a>00387 imp = inst;
<a name="l00388"></a>00388 <span class="keywordflow">else</span>
<a name="l00389"></a>00389 imp = typePred.<a class="code" href="group__ExprPkg.html#ga8dd97bcdeb9d8870238f94a263fd083b">impExpr</a>(inst);
<a name="l00390"></a>00390 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> ret = newTheorem(imp, t1.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>(), pf);
<a name="l00391"></a>00391
<a name="l00392"></a>00392
<a name="l00393"></a>00393 <span class="keywordtype">unsigned</span> thmLevel = t1.<a class="code" href="classCVC3_1_1Theorem.html#a26b6f0af9e9b2f2a8c22a7dcb9fbb0b1" title="Return quantification level for this theorem.">getQuantLevel</a>();
<a name="l00394"></a>00394 <span class="keywordflow">if</span>(qlevel >= thmLevel) {
<a name="l00395"></a>00395 ret.<a class="code" href="classCVC3_1_1Theorem.html#ab3309c937f827595d1d92fa48cb5a471" title="Set the quantification level for this theorem.">setQuantLevel</a>(qlevel+1);
<a name="l00396"></a>00396 }
<a name="l00397"></a>00397 <span class="keywordflow">else</span>{
<a name="l00398"></a>00398 <span class="comment">// ret.setQuantLevel(thmLevel+1);</span>
<a name="l00399"></a>00399 ret.<a class="code" href="classCVC3_1_1Theorem.html#ab3309c937f827595d1d92fa48cb5a471" title="Set the quantification level for this theorem.">setQuantLevel</a>(thmLevel+1);
<a name="l00400"></a>00400 }
<a name="l00401"></a>00401
<a name="l00402"></a>00402
<a name="l00403"></a>00403 <span class="comment">// ret.setQuantLevel(qlevel+1);</span>
<a name="l00404"></a>00404 <span class="keywordflow">return</span> ret;
<a name="l00405"></a>00405 }
<a name="l00406"></a>00406
<a name="l00407"></a>00407
<a name="l00408"></a><a class="code" href="classCVC3_1_1QuantTheoremProducer.html#aebf21764bafce44cff11c631f1378afc">00408</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> QuantTheoremProducer::partialUniversalInst(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1, <span class="keyword">const</span> vector<Expr>& terms, <span class="keywordtype">int</span> quantLevel){
<a name="l00409"></a>00409 cout<<<span class="stringliteral">"error in partial inst"</span> << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">endl</a>;
<a name="l00410"></a>00410 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e = t1.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>();
<a name="l00411"></a>00411 <span class="keyword">const</span> vector<Expr>& boundVars = e.<a class="code" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd" title="Get bound variables from a closure Expr.">getVars</a>();
<a name="l00412"></a>00412 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00413"></a>00413 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(boundVars.size() >= terms.size(),
<a name="l00414"></a>00414 <span class="stringliteral">"Universal instantiation: size of terms array does "</span>
<a name="l00415"></a>00415 <span class="stringliteral">"not match quanitfied variables array size"</span>);
<a name="l00416"></a>00416 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(e.<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>(),
<a name="l00417"></a>00417 <span class="stringliteral">"universal instantiation: expr must be FORALL:\n"</span>
<a name="l00418"></a>00418 +e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00419"></a>00419 <span class="keywordflow">for</span>(<span class="keywordtype">unsigned</span> <span class="keywordtype">int</span> i=0; i<terms.size(); i++){
<a name="l00420"></a>00420 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(d_theoryQuant->getBaseType(boundVars[i]) ==
<a name="l00421"></a>00421 d_theoryQuant->getBaseType(terms[i]),
<a name="l00422"></a>00422 <span class="stringliteral">"partial Universal instantiation: type mismatch"</span>);
<a name="l00423"></a>00423 }
<a name="l00424"></a>00424 }
<a name="l00425"></a>00425
<a name="l00426"></a>00426 <span class="comment">//build up a conjunction of type predicates for expression</span>
<a name="l00427"></a>00427 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> tr = e.<a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga4471fca49c2acbb7b4cf71e72bc55d6a" title="TRUE Expr.">trueExpr</a>();
<a name="l00428"></a>00428 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> typePred = tr;
<a name="l00429"></a>00429 <span class="keywordflow">for</span>(<span class="keywordtype">unsigned</span> <span class="keywordtype">int</span> i=0; i<terms.size(); i++) {
<a name="l00430"></a>00430 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> p = d_theoryQuant->getTypePred(boundVars[i].getType(),terms[i]);
<a name="l00431"></a>00431 <span class="keywordflow">if</span>(p!=tr) {
<a name="l00432"></a>00432 <span class="keywordflow">if</span>(typePred==tr)
<a name="l00433"></a>00433 typePred = p;
<a name="l00434"></a>00434 <span class="keywordflow">else</span>
<a name="l00435"></a>00435 typePred = typePred.<a class="code" href="group__ExprPkg.html#ga6c3651465ce69ed5f4e6fd461b9acf3c">andExpr</a>(p);
<a name="l00436"></a>00436 }
<a name="l00437"></a>00437 }
<a name="l00438"></a>00438 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00439"></a>00439 <span class="keywordflow">if</span>(withProof()) {
<a name="l00440"></a>00440 vector<Proof> pfs;
<a name="l00441"></a>00441 vector<Expr> es;
<a name="l00442"></a>00442 pfs.push_back(t1.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00443"></a>00443 es.push_back(e);
<a name="l00444"></a>00444 es.insert(es.end(), terms.begin(), terms.end());
<a name="l00445"></a>00445 pf= newPf(<span class="stringliteral">"partial_universal_instantiation"</span>, es, pfs);
<a name="l00446"></a>00446 }
<a name="l00447"></a>00447
<a name="l00448"></a>00448
<a name="l00449"></a>00449 <span class="keywordflow">if</span>(terms.size() == boundVars.size()){
<a name="l00450"></a>00450 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> inst = e.<a class="code" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940" title="Get the body of the closure Expr.">getBody</a>().<a class="code" href="group__ExprPkg.html#ga95e18015860195a80b317bf756055786">substExpr</a>(e.<a class="code" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd" title="Get bound variables from a closure Expr.">getVars</a>(), terms);
<a name="l00451"></a>00451 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> imp;
<a name="l00452"></a>00452 <span class="keywordflow">if</span>(typePred == tr)
<a name="l00453"></a>00453 imp = inst;
<a name="l00454"></a>00454 <span class="keywordflow">else</span>
<a name="l00455"></a>00455 imp = typePred.<a class="code" href="group__ExprPkg.html#ga8dd97bcdeb9d8870238f94a263fd083b">impExpr</a>(inst);
<a name="l00456"></a>00456 <span class="keywordflow">return</span>(newTheorem(imp, t1.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>(), pf));
<a name="l00457"></a>00457 }
<a name="l00458"></a>00458 <span class="keywordflow">else</span>{
<a name="l00459"></a>00459 vector<Expr> newBoundVars;
<a name="l00460"></a>00460 <span class="keywordflow">for</span>(<span class="keywordtype">size_t</span> i=0; i<terms.size(); i++) {
<a name="l00461"></a>00461 newBoundVars.push_back(boundVars[i]);
<a name="l00462"></a>00462 }
<a name="l00463"></a>00463
<a name="l00464"></a>00464 vector<Expr>leftBoundVars;
<a name="l00465"></a>00465 <span class="keywordflow">for</span>(<span class="keywordtype">size_t</span> i=terms.size(); i<boundVars.size(); i++) {
<a name="l00466"></a>00466 leftBoundVars.push_back(boundVars[i]);
<a name="l00467"></a>00467 }
<a name="l00468"></a>00468
<a name="l00469"></a>00469 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> tempinst = e.<a class="code" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940" title="Get the body of the closure Expr.">getBody</a>().<a class="code" href="group__ExprPkg.html#ga95e18015860195a80b317bf756055786">substExpr</a>(newBoundVars, terms);
<a name="l00470"></a>00470 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> inst = d_theoryQuant-><a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga0d2ff7603a249b30b2df4e549607ad6e">newClosureExpr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7b7b6f6e2b88589bd4656a14bcb7eb94">FORALL</a>, leftBoundVars, tempinst);
<a name="l00471"></a>00471
<a name="l00472"></a>00472 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> imp;
<a name="l00473"></a>00473 <span class="keywordflow">if</span>(typePred == tr)
<a name="l00474"></a>00474 imp = inst;
<a name="l00475"></a>00475 <span class="keywordflow">else</span>
<a name="l00476"></a>00476 imp = typePred.<a class="code" href="group__ExprPkg.html#ga8dd97bcdeb9d8870238f94a263fd083b">impExpr</a>(inst);
<a name="l00477"></a>00477
<a name="l00478"></a>00478 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> res = (newTheorem(imp, t1.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>(), pf));
<a name="l00479"></a>00479 <span class="keywordtype">int</span> thmLevel = t1.<a class="code" href="classCVC3_1_1Theorem.html#a26b6f0af9e9b2f2a8c22a7dcb9fbb0b1" title="Return quantification level for this theorem.">getQuantLevel</a>();
<a name="l00480"></a>00480 <span class="keywordflow">if</span>(quantLevel >= thmLevel) {
<a name="l00481"></a>00481 res.<a class="code" href="classCVC3_1_1Theorem.html#ab3309c937f827595d1d92fa48cb5a471" title="Set the quantification level for this theorem.">setQuantLevel</a>(quantLevel+1);
<a name="l00482"></a>00482 }
<a name="l00483"></a>00483 <span class="keywordflow">else</span>{
<a name="l00484"></a>00484 <span class="comment">//k ret.setQuantLevel(thmLevel+1);</span>
<a name="l00485"></a>00485 res.<a class="code" href="classCVC3_1_1Theorem.html#ab3309c937f827595d1d92fa48cb5a471" title="Set the quantification level for this theorem.">setQuantLevel</a>(thmLevel);
<a name="l00486"></a>00486 }
<a name="l00487"></a>00487 <span class="keywordflow">return</span> res;
<a name="l00488"></a>00488
<a name="l00489"></a>00489 }
<a name="l00490"></a>00490 }
<a name="l00491"></a>00491 <span class="comment"></span>
<a name="l00492"></a>00492 <span class="comment">//! find all bound variables in e and maps them to true in boundVars</span>
<a name="l00493"></a><a class="code" href="classCVC3_1_1QuantTheoremProducer.html#a8ab1be71db5a5816f69eb45aa8c2009f">00493</a> <span class="comment"></span><span class="keywordtype">void</span> QuantTheoremProducer::recFindBoundVars(<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="l00494"></a>00494 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> & boundVars, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> &visited)
<a name="l00495"></a>00495 {
<a name="l00496"></a>00496 <span class="keywordflow">if</span>(visited.<a class="code" href="classCVC3_1_1ExprMap.html#aa96dfa3a54a131cdb0964ef4b80e324f">count</a>(e)>0)
<a name="l00497"></a>00497 <span class="keywordflow">return</span>;
<a name="l00498"></a>00498 <span class="keywordflow">else</span>
<a name="l00499"></a>00499 visited[e] = <span class="keyword">true</span>;
<a name="l00500"></a>00500 <span class="keywordflow">if</span>(e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba462c38186c36e12c2f38a6d0d43feddf">BOUND_VAR</a>)
<a name="l00501"></a>00501 boundVars[e] = <span class="keyword">true</span>;
<a name="l00502"></a>00502 <span class="keywordflow">if</span>(e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3197625a1bb2264943f5a95f236d9973">EXISTS</a> || e.<a class="code" href="group__ExprPkg.html#ga7814e4f55f65c7ca860c637413df5f4d">getKind</a>() == <a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7b7b6f6e2b88589bd4656a14bcb7eb94">FORALL</a>)
<a name="l00503"></a>00503 recFindBoundVars(e.<a class="code" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940" title="Get the body of the closure Expr.">getBody</a>(), boundVars, visited);
<a name="l00504"></a>00504 <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>(); it!=e.<a class="code" href="group__ExprPkg.html#gaf6048a5030c8fa2511bf5dfee868e653" title="End iterator.">end</a>(); ++it)
<a name="l00505"></a>00505 recFindBoundVars(*it, boundVars, visited);
<a name="l00506"></a>00506
<a name="l00507"></a>00507 }
<a name="l00508"></a>00508 <span class="comment"></span>
<a name="l00509"></a>00509 <span class="comment">//!adjust the order of bound vars, newBvs begin first</span>
<a name="l00510"></a><a class="code" href="classCVC3_1_1QuantTheoremProducer.html#ac9f94901d86fe0b3cf90ad109e45db21">00510</a> <span class="comment"></span><a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> QuantTheoremProducer::adjustVarUniv(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1, <span class="keyword">const</span> std::vector<Expr>& newBvs){
<a name="l00511"></a>00511 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e=t1.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>();
<a name="l00512"></a>00512 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> body = e.<a class="code" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940" title="Get the body of the closure Expr.">getBody</a>();
<a name="l00513"></a>00513 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00514"></a>00514 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(e.<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>(),
<a name="l00515"></a>00515 <span class="stringliteral">"adjustVarUniv: "</span>
<a name="l00516"></a>00516 +e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00517"></a>00517 }
<a name="l00518"></a>00518
<a name="l00519"></a>00519 <span class="keyword">const</span> vector<Expr>& origVars = e.<a class="code" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd" title="Get bound variables from a closure Expr.">getVars</a>();
<a name="l00520"></a>00520
<a name="l00521"></a>00521
<a name="l00522"></a>00522 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> oldmap;
<a name="l00523"></a>00523 <span class="keywordflow">for</span>(vector<Expr>::const_iterator it = origVars.begin(),
<a name="l00524"></a>00524 iend=origVars.end(); it!=iend; ++it) {
<a name="l00525"></a>00525 oldmap[*it]=<span class="keyword">true</span>;
<a name="l00526"></a>00526 }
<a name="l00527"></a>00527
<a name="l00528"></a>00528 vector<Expr> quantVars;
<a name="l00529"></a>00529 <span class="keywordflow">for</span>(vector<Expr>::const_iterator it = newBvs.begin(),
<a name="l00530"></a>00530 iend=newBvs.end(); it!=iend; ++it) {
<a name="l00531"></a>00531 <span class="keywordflow">if</span>(oldmap.<a class="code" href="classCVC3_1_1ExprMap.html#aa96dfa3a54a131cdb0964ef4b80e324f">count</a>(*it) > 0)
<a name="l00532"></a>00532 quantVars.push_back(*it);
<a name="l00533"></a>00533 }
<a name="l00534"></a>00534
<a name="l00535"></a>00535 <span class="keywordflow">if</span>(quantVars.size() == origVars.size())
<a name="l00536"></a>00536 <span class="keywordflow">return</span> t1;
<a name="l00537"></a>00537
<a name="l00538"></a>00538 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> newmap;
<a name="l00539"></a>00539 <span class="keywordflow">for</span>(vector<Expr>::const_iterator it = newBvs.begin(),
<a name="l00540"></a>00540 iend=newBvs.end(); it!=iend; ++it) {
<a name="l00541"></a>00541 newmap[*it]=<span class="keyword">true</span>;
<a name="l00542"></a>00542 }
<a name="l00543"></a>00543
<a name="l00544"></a>00544 <span class="keywordflow">for</span>(vector<Expr>::const_iterator it = origVars.begin(),
<a name="l00545"></a>00545 iend=origVars.end(); it!=iend; ++it) {
<a name="l00546"></a>00546 <span class="keywordflow">if</span>(newmap.<a class="code" href="classCVC3_1_1ExprMap.html#aa96dfa3a54a131cdb0964ef4b80e324f">count</a>(*it)<=0){
<a name="l00547"></a>00547 quantVars.push_back(*it);
<a name="l00548"></a>00548 };
<a name="l00549"></a>00549 }
<a name="l00550"></a>00550
<a name="l00551"></a>00551 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00552"></a>00552 <span class="keywordflow">if</span>(withProof()) {
<a name="l00553"></a>00553 vector<Expr> es;
<a name="l00554"></a>00554 vector<Proof> pfs;
<a name="l00555"></a>00555 es.push_back(e);
<a name="l00556"></a>00556 es.insert(es.end(), quantVars.begin(), quantVars.end());
<a name="l00557"></a>00557 pfs.push_back(t1.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00558"></a>00558 pf= newPf(<span class="stringliteral">"adjustVarUniv"</span>, es, pfs);
<a name="l00559"></a>00559 }
<a name="l00560"></a>00560
<a name="l00561"></a>00561 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newQuantExpr;
<a name="l00562"></a>00562 newQuantExpr = d_theoryQuant-><a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga0d2ff7603a249b30b2df4e549607ad6e">newClosureExpr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7b7b6f6e2b88589bd4656a14bcb7eb94">FORALL</a>, quantVars, body);
<a name="l00563"></a>00563
<a name="l00564"></a>00564 <span class="keywordflow">return</span>(newTheorem(newQuantExpr, t1.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>(), pf));
<a name="l00565"></a>00565 }
<a name="l00566"></a>00566 <span class="comment"></span>
<a name="l00567"></a>00567 <span class="comment">//!pack (forall (x) forall (y)) into (forall (x y))</span>
<a name="l00568"></a><a class="code" href="classCVC3_1_1QuantTheoremProducer.html#af08b01f92622d3f9d4e8070907ce5062">00568</a> <span class="comment"></span><a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> QuantTheoremProducer::packVar(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1){
<a name="l00569"></a>00569 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> out_forall =t1.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>();
<a name="l00570"></a>00570
<a name="l00571"></a>00571 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00572"></a>00572 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(out_forall.<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>(),
<a name="l00573"></a>00573 <span class="stringliteral">"packVar: "</span>
<a name="l00574"></a>00574 +out_forall.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00575"></a>00575 }
<a name="l00576"></a>00576
<a name="l00577"></a>00577 vector<Expr> bVars = out_forall.<a class="code" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd" title="Get bound variables from a closure Expr.">getVars</a>();
<a name="l00578"></a>00578
<a name="l00579"></a>00579 <span class="keywordflow">if</span>(!out_forall.<a class="code" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940" title="Get the body of the closure Expr.">getBody</a>().<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>()){
<a name="l00580"></a>00580 <span class="keywordflow">return</span> t1;
<a name="l00581"></a>00581 }
<a name="l00582"></a>00582
<a name="l00583"></a>00583 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> cur_body = out_forall.<a class="code" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940" title="Get the body of the closure Expr.">getBody</a>();
<a name="l00584"></a>00584
<a name="l00585"></a>00585 <span class="keywordflow">while</span>(cur_body.<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>()){
<a name="l00586"></a>00586 vector<Expr> bVarsLeft = cur_body.<a class="code" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd" title="Get bound variables from a closure Expr.">getVars</a>();
<a name="l00587"></a>00587 <span class="keywordflow">for</span>(vector<Expr>::iterator i=bVarsLeft.begin(), iend=bVarsLeft.end(); i!=iend; i++){
<a name="l00588"></a>00588 bVars.push_back(*i);
<a name="l00589"></a>00589 }
<a name="l00590"></a>00590 cur_body=cur_body.<a class="code" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940" title="Get the body of the closure Expr.">getBody</a>();
<a name="l00591"></a>00591 }
<a name="l00592"></a>00592
<a name="l00593"></a>00593 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00594"></a>00594 <span class="keywordflow">if</span>(withProof()) {
<a name="l00595"></a>00595 vector<Expr> es;
<a name="l00596"></a>00596 vector<Proof> pfs;
<a name="l00597"></a>00597 es.push_back(out_forall);
<a name="l00598"></a>00598 es.insert(es.end(), bVars.begin(), bVars.end());
<a name="l00599"></a>00599 pfs.push_back(t1.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00600"></a>00600 pf= newPf(<span class="stringliteral">"packVar"</span>, es, pfs);
<a name="l00601"></a>00601 }
<a name="l00602"></a>00602
<a name="l00603"></a>00603 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newQuantExpr;
<a name="l00604"></a>00604 newQuantExpr = d_theoryQuant-><a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga0d2ff7603a249b30b2df4e549607ad6e">newClosureExpr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7b7b6f6e2b88589bd4656a14bcb7eb94">FORALL</a>, bVars, cur_body);
<a name="l00605"></a>00605
<a name="l00606"></a>00606 <span class="keywordflow">return</span> (newTheorem(newQuantExpr, t1.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>(), pf));
<a name="l00607"></a>00607 <span class="comment">// return (newRWTheorem(t1,newQuantExpr, t1.getAssumptionsRef(), pf));</span>
<a name="l00608"></a>00608 }
<a name="l00609"></a>00609 <span class="comment"></span>
<a name="l00610"></a>00610 <span class="comment">//! convert (forall (x) ... forall (y)) into (forall (x y)...)</span>
<a name="l00611"></a>00611 <span class="comment">//! convert (exists (x) ... exists (y)) into (exists (x y)...)</span>
<a name="l00612"></a><a class="code" href="classCVC3_1_1QuantTheoremProducer.html#a7f3fea7c5c13305de2da0b1ac3700503">00612</a> <span class="comment"></span><a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> QuantTheoremProducer::pullVarOut(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1){
<a name="l00613"></a>00613 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> thm_expr=t1.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>();
<a name="l00614"></a>00614
<a name="l00615"></a>00615 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00616"></a>00616 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(thm_expr.<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>() || thm_expr.<a class="code" href="group__ExprPkg.html#ga1c922163af59ed6bc101728d65e04d16">isExists</a>(),
<a name="l00617"></a>00617 <span class="stringliteral">"pullVarOut: "</span>
<a name="l00618"></a>00618 +thm_expr.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00619"></a>00619 }
<a name="l00620"></a>00620
<a name="l00621"></a>00621 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> outBody = thm_expr.<a class="code" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940" title="Get the body of the closure Expr.">getBody</a>();
<a name="l00622"></a>00622
<a name="l00623"></a>00623 <span class="comment">// if(((outBody.isAnd() && outBody[1].isForall()) ||</span>
<a name="l00624"></a>00624 <span class="comment">// (outBody.isImpl() && outBody[1].isForall()) ||</span>
<a name="l00625"></a>00625 <span class="comment">// (outBody.isNot() && outBody[0].isAnd() && outBody[0][1].isExists()) )){</span>
<a name="l00626"></a>00626 <span class="comment">// return t1;</span>
<a name="l00627"></a>00627 <span class="comment">// }</span>
<a name="l00628"></a>00628
<a name="l00629"></a>00629 <span class="keywordflow">if</span> (thm_expr.<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>()){
<a name="l00630"></a>00630 <span class="keywordflow">if</span>((outBody.<a class="code" href="group__ExprPkg.html#ga1a898858ccadce833df5a294c7740f11">isNot</a>() && outBody[0].<a class="code" href="group__ExprPkg.html#ga383260cf4f8919728e2712e6e11f21fa">isAnd</a>() && outBody[0][1].<a class="code" href="group__ExprPkg.html#ga1c922163af59ed6bc101728d65e04d16">isExists</a>())){
<a name="l00631"></a>00631
<a name="l00632"></a>00632 vector<Expr> bVarsOut = thm_expr.<a class="code" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd" title="Get bound variables from a closure Expr.">getVars</a>();
<a name="l00633"></a>00633
<a name="l00634"></a>00634 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> innerExists =outBody[0][1];
<a name="l00635"></a>00635 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> innerBody = innerExists.<a class="code" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940" title="Get the body of the closure Expr.">getBody</a>();
<a name="l00636"></a>00636 vector<Expr> bVarsIn = innerExists.<a class="code" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd" title="Get bound variables from a closure Expr.">getVars</a>();
<a name="l00637"></a>00637
<a name="l00638"></a>00638 <span class="keywordflow">for</span>(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){
<a name="l00639"></a>00639 bVarsOut.push_back(*i);
<a name="l00640"></a>00640 }
<a name="l00641"></a>00641
<a name="l00642"></a>00642 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00643"></a>00643 <span class="keywordflow">if</span>(withProof()) {
<a name="l00644"></a>00644 vector<Expr> es;
<a name="l00645"></a>00645 vector<Proof> pfs;
<a name="l00646"></a>00646 es.push_back(thm_expr);
<a name="l00647"></a>00647 es.insert(es.end(), bVarsIn.begin(), bVarsIn.end());
<a name="l00648"></a>00648 pfs.push_back(t1.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00649"></a>00649 pf= newPf(<span class="stringliteral">"pullVarOut"</span>, es, pfs);
<a name="l00650"></a>00650 }
<a name="l00651"></a>00651
<a name="l00652"></a>00652 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newbody;
<a name="l00653"></a>00653
<a name="l00654"></a>00654 newbody=(outBody[0][0].<a class="code" href="group__ExprPkg.html#ga59d07586d68ba39eadd98c86492acdac">notExpr</a>()).<a class="code" href="namespaceCVC3.html#a30f30b6e20c174f21ae63acea8618294">orExpr</a>(innerBody.<a class="code" href="group__ExprPkg.html#ga59d07586d68ba39eadd98c86492acdac">notExpr</a>());
<a name="l00655"></a>00655
<a name="l00656"></a>00656 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newQuantExpr;
<a name="l00657"></a>00657 newQuantExpr = d_theoryQuant-><a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga0d2ff7603a249b30b2df4e549607ad6e">newClosureExpr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7b7b6f6e2b88589bd4656a14bcb7eb94">FORALL</a>, bVarsOut, newbody);
<a name="l00658"></a>00658
<a name="l00659"></a>00659 <span class="keywordflow">return</span>(newTheorem(newQuantExpr, t1.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>(), pf));
<a name="l00660"></a>00660 }
<a name="l00661"></a>00661
<a name="l00662"></a>00662 <span class="keywordflow">else</span> <span class="keywordflow">if</span> ((outBody.<a class="code" href="group__ExprPkg.html#ga383260cf4f8919728e2712e6e11f21fa">isAnd</a>() && outBody[1].<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>()) ||
<a name="l00663"></a>00663 (outBody.<a class="code" href="group__ExprPkg.html#ga9067c706c6454ea1761ace7d7837af46">isImpl</a>() && outBody[1].<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>())){
<a name="l00664"></a>00664
<a name="l00665"></a>00665 vector<Expr> bVarsOut = thm_expr.<a class="code" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd" title="Get bound variables from a closure Expr.">getVars</a>();
<a name="l00666"></a>00666
<a name="l00667"></a>00667 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> innerForall=outBody[1];
<a name="l00668"></a>00668 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> innerBody = innerForall.<a class="code" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940" title="Get the body of the closure Expr.">getBody</a>();
<a name="l00669"></a>00669 vector<Expr> bVarsIn = innerForall.<a class="code" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd" title="Get bound variables from a closure Expr.">getVars</a>();
<a name="l00670"></a>00670
<a name="l00671"></a>00671 <span class="keywordflow">for</span>(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){
<a name="l00672"></a>00672 bVarsOut.push_back(*i);
<a name="l00673"></a>00673 }
<a name="l00674"></a>00674
<a name="l00675"></a>00675 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00676"></a>00676 <span class="keywordflow">if</span>(withProof()) {
<a name="l00677"></a>00677 vector<Expr> es;
<a name="l00678"></a>00678 vector<Proof> pfs;
<a name="l00679"></a>00679 es.push_back(thm_expr);
<a name="l00680"></a>00680 es.insert(es.end(), bVarsIn.begin(), bVarsIn.end());
<a name="l00681"></a>00681 pfs.push_back(t1.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00682"></a>00682 pf= newPf(<span class="stringliteral">"pullVarOut"</span>, es, pfs);
<a name="l00683"></a>00683 }
<a name="l00684"></a>00684
<a name="l00685"></a>00685 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newbody;
<a name="l00686"></a>00686 <span class="keywordflow">if</span>(outBody.<a class="code" href="group__ExprPkg.html#ga383260cf4f8919728e2712e6e11f21fa">isAnd</a>()){
<a name="l00687"></a>00687 newbody=outBody[0].<a class="code" href="group__ExprPkg.html#ga6c3651465ce69ed5f4e6fd461b9acf3c">andExpr</a>(innerBody);
<a name="l00688"></a>00688 }
<a name="l00689"></a>00689 <span class="keywordflow">else</span> <span class="keywordflow">if</span>(outBody.<a class="code" href="group__ExprPkg.html#ga9067c706c6454ea1761ace7d7837af46">isImpl</a>()){
<a name="l00690"></a>00690 newbody=outBody[0].<a class="code" href="group__ExprPkg.html#ga8dd97bcdeb9d8870238f94a263fd083b">impExpr</a>(innerBody);
<a name="l00691"></a>00691 }
<a name="l00692"></a>00692
<a name="l00693"></a>00693 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newQuantExpr;
<a name="l00694"></a>00694 newQuantExpr = d_theoryQuant-><a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga0d2ff7603a249b30b2df4e549607ad6e">newClosureExpr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7b7b6f6e2b88589bd4656a14bcb7eb94">FORALL</a>, bVarsOut, newbody);
<a name="l00695"></a>00695
<a name="l00696"></a>00696 <span class="keywordflow">return</span>(newTheorem(newQuantExpr, t1.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>(), pf));
<a name="l00697"></a>00697 }
<a name="l00698"></a>00698 <span class="keywordflow">return</span> t1; <span class="comment">// case cannot be handled now. </span>
<a name="l00699"></a>00699 }
<a name="l00700"></a>00700
<a name="l00701"></a>00701 <span class="keywordflow">else</span> <span class="keywordflow">if</span> (thm_expr.<a class="code" href="group__ExprPkg.html#ga1c922163af59ed6bc101728d65e04d16">isExists</a>()){
<a name="l00702"></a>00702 <span class="keywordflow">if</span> ((outBody.<a class="code" href="group__ExprPkg.html#ga383260cf4f8919728e2712e6e11f21fa">isAnd</a>() && outBody[1].<a class="code" href="group__ExprPkg.html#ga1c922163af59ed6bc101728d65e04d16">isExists</a>()) ||
<a name="l00703"></a>00703 (outBody.<a class="code" href="group__ExprPkg.html#ga9067c706c6454ea1761ace7d7837af46">isImpl</a>() && outBody[1].<a class="code" href="group__ExprPkg.html#ga1c922163af59ed6bc101728d65e04d16">isExists</a>())){
<a name="l00704"></a>00704
<a name="l00705"></a>00705 vector<Expr> bVarsOut = thm_expr.<a class="code" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd" title="Get bound variables from a closure Expr.">getVars</a>();
<a name="l00706"></a>00706
<a name="l00707"></a>00707 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> innerExists = outBody[1];
<a name="l00708"></a>00708 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> innerBody = innerExists.<a class="code" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940" title="Get the body of the closure Expr.">getBody</a>();
<a name="l00709"></a>00709 vector<Expr> bVarsIn = innerExists.<a class="code" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd" title="Get bound variables from a closure Expr.">getVars</a>();
<a name="l00710"></a>00710
<a name="l00711"></a>00711 <span class="keywordflow">for</span>(vector<Expr>::iterator i=bVarsIn.begin(), iend=bVarsIn.end(); i!=iend; i++){
<a name="l00712"></a>00712 bVarsOut.push_back(*i);
<a name="l00713"></a>00713 }
<a name="l00714"></a>00714
<a name="l00715"></a>00715 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00716"></a>00716 <span class="keywordflow">if</span>(withProof()) {
<a name="l00717"></a>00717 vector<Expr> es;
<a name="l00718"></a>00718 vector<Proof> pfs;
<a name="l00719"></a>00719 es.push_back(thm_expr);
<a name="l00720"></a>00720 es.insert(es.end(), bVarsIn.begin(), bVarsIn.end());
<a name="l00721"></a>00721 pfs.push_back(t1.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00722"></a>00722 pf= newPf(<span class="stringliteral">"pullVarOut"</span>, es, pfs);
<a name="l00723"></a>00723 }
<a name="l00724"></a>00724
<a name="l00725"></a>00725 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newbody;
<a name="l00726"></a>00726 <span class="keywordflow">if</span>(outBody.<a class="code" href="group__ExprPkg.html#ga383260cf4f8919728e2712e6e11f21fa">isAnd</a>()){
<a name="l00727"></a>00727 newbody=outBody[0].<a class="code" href="group__ExprPkg.html#ga6c3651465ce69ed5f4e6fd461b9acf3c">andExpr</a>(innerBody);
<a name="l00728"></a>00728 }
<a name="l00729"></a>00729 <span class="keywordflow">else</span> <span class="keywordflow">if</span>(outBody.<a class="code" href="group__ExprPkg.html#ga9067c706c6454ea1761ace7d7837af46">isImpl</a>()){
<a name="l00730"></a>00730 newbody=outBody[0].<a class="code" href="group__ExprPkg.html#ga8dd97bcdeb9d8870238f94a263fd083b">impExpr</a>(innerBody);
<a name="l00731"></a>00731 }
<a name="l00732"></a>00732
<a name="l00733"></a>00733 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newQuantExpr;
<a name="l00734"></a>00734 newQuantExpr = d_theoryQuant-><a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga0d2ff7603a249b30b2df4e549607ad6e">newClosureExpr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3197625a1bb2264943f5a95f236d9973">EXISTS</a>, bVarsOut, newbody);
<a name="l00735"></a>00735
<a name="l00736"></a>00736 <span class="keywordflow">return</span>(newTheorem(newQuantExpr, t1.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>(), pf));
<a name="l00737"></a>00737 }
<a name="l00738"></a>00738 }
<a name="l00739"></a>00739 <span class="keywordflow">return</span> t1;
<a name="l00740"></a>00740 }
<a name="l00741"></a>00741
<a name="l00742"></a>00742
<a name="l00743"></a>00743 <span class="comment"></span>
<a name="l00744"></a>00744 <span class="comment">/*! @brief From T|- QUANTIFIER (vars): e we get T|-QUANTIFIER(vars') e</span>
<a name="l00745"></a>00745 <span class="comment"> * where vars' is obtained from vars by removing all bound variables</span>
<a name="l00746"></a>00746 <span class="comment"> * not used in e. If vars' is empty the produced theorem is just T|-e</span>
<a name="l00747"></a>00747 <span class="comment"> */</span>
<a name="l00748"></a><a class="code" href="classCVC3_1_1QuantTheoremProducer.html#a822c41475a24cf1f4bd558dcbdf90d66">00748</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> QuantTheoremProducer::boundVarElim(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& t1)
<a name="l00749"></a>00749 {
<a name="l00750"></a>00750 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e=t1.<a class="code" href="classCVC3_1_1Theorem.html#af2b97ae5d270ddf1013bf4f3867a7e5d">getExpr</a>();
<a name="l00751"></a>00751 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> body = e.<a class="code" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940" title="Get the body of the closure Expr.">getBody</a>();
<a name="l00752"></a>00752 <span class="keywordflow">if</span>(<a class="code" href="theorem__producer_8h.html#a74a97b789e1a9e6c016291960c657445">CHECK_PROOFS</a>) {
<a name="l00753"></a>00753 <a class="code" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND</a>(e.<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>() || e.<a class="code" href="group__ExprPkg.html#ga1c922163af59ed6bc101728d65e04d16">isExists</a>(),
<a name="l00754"></a>00754 <span class="stringliteral">"bound var elimination: "</span>
<a name="l00755"></a>00755 +e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>());
<a name="l00756"></a>00756 }
<a name="l00757"></a>00757 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> boundVars; <span class="comment">//a mapping of bound variables in the body to true</span>
<a name="l00758"></a>00758 <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> visited; <span class="comment">//to make sure expressions aren't traversed</span>
<a name="l00759"></a>00759 <span class="comment">//multiple times</span>
<a name="l00760"></a>00760 recFindBoundVars(body, boundVars, visited);
<a name="l00761"></a>00761 vector<Expr> quantVars;
<a name="l00762"></a>00762 <span class="keyword">const</span> vector<Expr>& origVars = e.<a class="code" href="group__ExprPkg.html#gaad22e223d0e273780557aca9d87620cd" title="Get bound variables from a closure Expr.">getVars</a>();
<a name="l00763"></a>00763 <span class="keywordflow">for</span>(vector<Expr>::const_iterator it = origVars.begin(),
<a name="l00764"></a>00764 iend=origVars.end(); it!=iend; ++it)
<a name="l00765"></a>00765 {
<a name="l00766"></a>00766 <span class="keywordflow">if</span>(boundVars.<a class="code" href="classCVC3_1_1ExprMap.html#aa96dfa3a54a131cdb0964ef4b80e324f">count</a>(*it) > 0)
<a name="l00767"></a>00767 quantVars.push_back(*it);
<a name="l00768"></a>00768 }
<a name="l00769"></a>00769
<a name="l00770"></a>00770 <span class="comment">// If all variables are used, just return the original theorem</span>
<a name="l00771"></a>00771 <span class="keywordflow">if</span>(quantVars.size() == origVars.size())
<a name="l00772"></a>00772 <span class="keywordflow">return</span> t1;
<a name="l00773"></a>00773
<a name="l00774"></a>00774 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> pf;
<a name="l00775"></a>00775 <span class="keywordflow">if</span>(withProof()) {
<a name="l00776"></a>00776 vector<Expr> es;
<a name="l00777"></a>00777 vector<Proof> pfs;
<a name="l00778"></a>00778 es.push_back(e);
<a name="l00779"></a>00779 es.insert(es.end(), quantVars.begin(), quantVars.end());
<a name="l00780"></a>00780 pfs.push_back(t1.<a class="code" href="classCVC3_1_1Theorem.html#a2d8352c07a756c3837683a27a1e659ef">getProof</a>());
<a name="l00781"></a>00781 pf= newPf(<span class="stringliteral">"bound_variable_elimination"</span>, es, pfs);
<a name="l00782"></a>00782 }
<a name="l00783"></a>00783 <span class="keywordflow">if</span>(quantVars.size() == 0)
<a name="l00784"></a>00784 <span class="keywordflow">return</span>(newTheorem(e.<a class="code" href="group__ExprPkg.html#ga9060193194020fee3dac69ed1876a940" title="Get the body of the closure Expr.">getBody</a>(), t1.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>(), pf));
<a name="l00785"></a>00785
<a name="l00786"></a>00786 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newQuantExpr;
<a name="l00787"></a>00787 <span class="keywordflow">if</span>(e.<a class="code" href="group__ExprPkg.html#gaad6095e1d8b1551a006602d9421fb988">isForall</a>())
<a name="l00788"></a>00788 newQuantExpr = d_theoryQuant-><a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga0d2ff7603a249b30b2df4e549607ad6e">newClosureExpr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba7b7b6f6e2b88589bd4656a14bcb7eb94">FORALL</a>, quantVars, body);
<a name="l00789"></a>00789 <span class="keywordflow">else</span>
<a name="l00790"></a>00790 newQuantExpr = d_theoryQuant-><a class="code" href="group__ExprPkg.html#gab57ce3dfa78947a906241d090c7cf34d">getEM</a>()-><a class="code" href="group__EM__Priv.html#ga0d2ff7603a249b30b2df4e549607ad6e">newClosureExpr</a>(<a class="code" href="kinds_8h.html#aa10c9e8951b8ccf714a59ec321bdac5ba3197625a1bb2264943f5a95f236d9973">EXISTS</a>, quantVars, body);
<a name="l00791"></a>00791
<a name="l00792"></a>00792 <span class="keywordflow">return</span>(newTheorem(newQuantExpr, t1.<a class="code" href="classCVC3_1_1Theorem.html#a5e9ab00a613df15cc02f55edb55a67b3">getAssumptionsRef</a>(), pf));
<a name="l00793"></a>00793 }
</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>
