<!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: theory_quant.h 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">theory_quant.h</div> </div>
</div>
<div class="contents">
<a href="theory__quant_8h.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 theory_quant.h</span>
<a name="l00004"></a>00004 <span class="comment"> * </span>
<a name="l00005"></a>00005 <span class="comment"> * Author: Sergey Berezin, Yeting Ge</span>
<a name="l00006"></a>00006 <span class="comment"> * </span>
<a name="l00007"></a>00007 <span class="comment"> * Created: Jun 24 21:13:59 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"> * ! Author: Daniel Wichs</span>
<a name="l00019"></a>00019 <span class="comment"> * ! Created: Wednesday July 2, 2003</span>
<a name="l00020"></a>00020 <span class="comment"> *</span>
<a name="l00021"></a>00021 <span class="comment"> * </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="preprocessor">#ifndef _cvc3__include__theory_quant_h_</span>
<a name="l00025"></a>00025 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__theory_quant_h_</span>
<a name="l00026"></a>00026 <span class="preprocessor"></span>
<a name="l00027"></a>00027 <span class="preprocessor">#include "<a class="code" href="theory_8h.html" title="Generic API for Theories plus methods commonly used by theories.">theory.h</a>"</span>
<a name="l00028"></a>00028 <span class="preprocessor">#include "<a class="code" href="cdmap_8h.html">cdmap.h</a>"</span>
<a name="l00029"></a>00029 <span class="preprocessor">#include "<a class="code" href="statistics_8h.html" title="Description: Counters and flags for collecting run-time statistics.">statistics.h</a>"</span>
<a name="l00030"></a>00030 <span class="preprocessor">#include<queue></span>
<a name="l00031"></a>00031
<a name="l00032"></a>00032 <span class="keyword">namespace </span>CVC3 {
<a name="l00033"></a>00033
<a name="l00034"></a>00034 <span class="keyword">class </span>QuantProofRules;
<a name="l00035"></a>00035
<a name="l00036"></a>00036 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00037"></a>00037 <span class="comment">/*!</span>
<a name="l00038"></a>00038 <span class="comment"> *\class TheoryQuant</span>
<a name="l00039"></a>00039 <span class="comment"> *\ingroup Theories</span>
<a name="l00040"></a>00040 <span class="comment"> *\brief This theory handles quantifiers.</span>
<a name="l00041"></a>00041 <span class="comment"> *</span>
<a name="l00042"></a>00042 <span class="comment"> * Author: Daniel Wichs</span>
<a name="l00043"></a>00043 <span class="comment"> *</span>
<a name="l00044"></a>00044 <span class="comment"> * Created: Wednesday July 2, 2003</span>
<a name="l00045"></a>00045 <span class="comment"> */</span>
<a name="l00046"></a>00046 <span class="comment">/*****************************************************************************/</span>
<a name="l00047"></a>00047
<a name="l00048"></a><a class="code" href="namespaceCVC3.html#aa6262a73c1109f35a6c533421f5dd393aa36f330d6c384df84029d036339d875e">00048</a> <span class="keyword">typedef</span> <span class="keyword">enum</span>{ <a class="code" href="namespaceCVC3.html#aa6262a73c1109f35a6c533421f5dd393aa36f330d6c384df84029d036339d875e">Ukn</a>, <a class="code" href="namespaceCVC3.html#aa6262a73c1109f35a6c533421f5dd393a0f862de84bb11f8a43eea9d18ae19048">Pos</a>, <a class="code" href="namespaceCVC3.html#aa6262a73c1109f35a6c533421f5dd393a83243e1548208082db5b8db82ec5cbe0">Neg</a>, <a class="code" href="namespaceCVC3.html#aa6262a73c1109f35a6c533421f5dd393aa4ce5dc85e02b6d569624c6ac46370fb">PosNeg</a>} <a class="code" href="namespaceCVC3.html#aa6262a73c1109f35a6c533421f5dd393">Polarity</a>;
<a name="l00049"></a>00049
<a name="l00050"></a><a class="code" href="classCVC3_1_1Trigger.html">00050</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Trigger.html">Trigger</a> {
<a name="l00051"></a>00051 <span class="keyword">public</span>:
<a name="l00052"></a><a class="code" href="classCVC3_1_1Trigger.html#a4e021ea47393a20e2a5ed518547b6cc5">00052</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1Trigger.html#a4e021ea47393a20e2a5ed518547b6cc5">trig</a>;
<a name="l00053"></a><a class="code" href="classCVC3_1_1Trigger.html#a072357cd5b19a3c255274a10c2e65ae1">00053</a> <a class="code" href="namespaceCVC3.html#aa6262a73c1109f35a6c533421f5dd393">Polarity</a> <a class="code" href="classCVC3_1_1Trigger.html#a072357cd5b19a3c255274a10c2e65ae1">polarity</a>;
<a name="l00054"></a>00054
<a name="l00055"></a><a class="code" href="classCVC3_1_1Trigger.html#a0316ac0451c9906e1ffa14269bca4822">00055</a> std::vector<Expr> <a class="code" href="classCVC3_1_1Trigger.html#a0316ac0451c9906e1ffa14269bca4822">bvs</a>;
<a name="l00056"></a><a class="code" href="classCVC3_1_1Trigger.html#a872b399bef4cb0181eef18c043dcf7c0">00056</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1Trigger.html#a872b399bef4cb0181eef18c043dcf7c0">head</a>;
<a name="l00057"></a><a class="code" href="classCVC3_1_1Trigger.html#a1b9f95a061179c63bb5c4a6572525149">00057</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#a1b9f95a061179c63bb5c4a6572525149">hasRWOp</a>;
<a name="l00058"></a><a class="code" href="classCVC3_1_1Trigger.html#ad27afc7a2fc903e53a03ab91a91ab2bb">00058</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#ad27afc7a2fc903e53a03ab91a91ab2bb">hasTrans</a>;
<a name="l00059"></a><a class="code" href="classCVC3_1_1Trigger.html#a164f72606a374f8bf9b1a86394df8e5a">00059</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#a164f72606a374f8bf9b1a86394df8e5a">hasT2</a>; <span class="comment">//if has trans of 2,</span>
<a name="l00060"></a><a class="code" href="classCVC3_1_1Trigger.html#a91aa68f794175b4a3d587bc735d90db1">00060</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#a91aa68f794175b4a3d587bc735d90db1">isSimple</a>; <span class="comment">//if of the form g(x,a);</span>
<a name="l00061"></a><a class="code" href="classCVC3_1_1Trigger.html#a1da964c1eddeeca162f2ad07084a519a">00061</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#a1da964c1eddeeca162f2ad07084a519a">isSuperSimple</a>; <span class="comment">//if of the form g(x,y);</span>
<a name="l00062"></a><a class="code" href="classCVC3_1_1Trigger.html#a263a81925c4e496b2db59a5c46c716da">00062</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#a263a81925c4e496b2db59a5c46c716da">isMulti</a>;
<a name="l00063"></a><a class="code" href="classCVC3_1_1Trigger.html#a7030f34d847ed61e24838c23b12e33f1">00063</a> <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1Trigger.html#a7030f34d847ed61e24838c23b12e33f1">multiIndex</a>;
<a name="l00064"></a><a class="code" href="classCVC3_1_1Trigger.html#aca45e27343e0e829d3515bb5e5614811">00064</a> <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1Trigger.html#aca45e27343e0e829d3515bb5e5614811">multiId</a>;
<a name="l00065"></a>00065
<a name="l00066"></a>00066 <a class="code" href="classCVC3_1_1Trigger.html#a1c729c6d36b3082f91432909c2e54409">Trigger</a>(<a class="code" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">TheoryCore</a>* core, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e, <a class="code" href="namespaceCVC3.html#aa6262a73c1109f35a6c533421f5dd393">Polarity</a> pol, std::set<Expr>);
<a name="l00067"></a>00067 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#aa5a20c74a358c4c9a83cf9f92f6e32da">isPos</a>();
<a name="l00068"></a>00068 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#ab6de8624e192483eca4c6af43ccdf0ae">isNeg</a>();
<a name="l00069"></a>00069 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1Trigger.html#a7ce47406ef7c80b30bfe72f01ca7427a">getEx</a>();
<a name="l00070"></a>00070 std::vector<Expr> <a class="code" href="classCVC3_1_1Trigger.html#af93f5d8aab866ffa559363feedcd50e3">getBVs</a>();
<a name="l00071"></a>00071 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Trigger.html#a038eeb6966002433652cd9ae30854be2">setHead</a>(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> h);
<a name="l00072"></a>00072 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1Trigger.html#a94a53eecac006205c1469d035472b9c2">getHead</a>();
<a name="l00073"></a>00073 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Trigger.html#a8dc23a790de84038e254b3b1677405f1">setRWOp</a>(<span class="keywordtype">bool</span> b);
<a name="l00074"></a>00074 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#aba631f56bfe8dac2b9833e4e692e6333">hasRW</a>();
<a name="l00075"></a>00075 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Trigger.html#ab28f10324850f03d8dd2d711d2084d42">setTrans</a>(<span class="keywordtype">bool</span> b);
<a name="l00076"></a>00076 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#a0302d9d47d4c5ca8f19796e4848f458d">hasTr</a>();
<a name="l00077"></a>00077 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Trigger.html#a677feb42871ff81f92c5070b455f4692">setTrans2</a>(<span class="keywordtype">bool</span> b);
<a name="l00078"></a>00078 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#aefbd02bbe97a369587ef7dcb07521adb">hasTr2</a>();
<a name="l00079"></a>00079 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Trigger.html#a3340abe4247b968ae8c2d6d76dbdad7a">setSimp</a>();
<a name="l00080"></a>00080 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#a7fd4df8cdf6f965b6560a7859d3e3cfb">isSimp</a>();
<a name="l00081"></a>00081 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Trigger.html#ac49043dc15a503a32759cf4538809e6e">setSuperSimp</a>();
<a name="l00082"></a>00082 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#a010f25f800a4abf9bbf242886f7d790b">isSuperSimp</a>();
<a name="l00083"></a>00083 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Trigger.html#ab86a9c01de2cf98869b3952d823603aa">setMultiTrig</a>();
<a name="l00084"></a>00084 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#a5fcf09b60025ebbfe31d5b659312681d">isMultiTrig</a>();
<a name="l00085"></a>00085
<a name="l00086"></a>00086
<a name="l00087"></a>00087 };
<a name="l00088"></a>00088
<a name="l00089"></a><a class="code" href="structCVC3_1_1dynTrig.html">00089</a> <span class="keyword">typedef</span> <span class="keyword">struct </span><a class="code" href="structCVC3_1_1dynTrig.html">dynTrig</a>{
<a name="l00090"></a><a class="code" href="structCVC3_1_1dynTrig.html#ab9c6198f3d1bbe415ff1a92ccb1c760c">00090</a> <a class="code" href="classCVC3_1_1Trigger.html">Trigger</a> <a class="code" href="structCVC3_1_1dynTrig.html#ab9c6198f3d1bbe415ff1a92ccb1c760c">trig</a>;
<a name="l00091"></a><a class="code" href="structCVC3_1_1dynTrig.html#ab8473d4aa20bfbcb9120043818cd319f">00091</a> <span class="keywordtype">size_t</span> <a class="code" href="structCVC3_1_1dynTrig.html#ab8473d4aa20bfbcb9120043818cd319f">univ_id</a>;
<a name="l00092"></a><a class="code" href="structCVC3_1_1dynTrig.html#a724a541dbe2ffe257a30b5931c786d4a">00092</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> <a class="code" href="structCVC3_1_1dynTrig.html#a724a541dbe2ffe257a30b5931c786d4a">binds</a>;
<a name="l00093"></a>00093 <a class="code" href="structCVC3_1_1dynTrig.html#aa4165e34609b668b909672389dc33501">dynTrig</a>(<a class="code" href="classCVC3_1_1Trigger.html">Trigger</a> t, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> b, <span class="keywordtype">size_t</span> <span class="keywordtype">id</span>);
<a name="l00094"></a>00094 } <a class="code" href="namespaceCVC3.html#adbf44ec4d7f9e553da5d876964266546">dynTrig</a>;
<a name="l00095"></a>00095
<a name="l00096"></a>00096
<a name="l00097"></a><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html">00097</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html">CompleteInstPreProcessor</a> {
<a name="l00098"></a>00098
<a name="l00099"></a><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#ad41c79afe0059463b226d9a60cd9d39d">00099</a> <a class="code" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">TheoryCore</a>* <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#ad41c79afe0059463b226d9a60cd9d39d">d_theoryCore</a>; <span class="comment">//needed by plusOne and minusOne;</span>
<a name="l00100"></a><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a135b1e372b6f3a33941c6fa2ecc93d3e">00100</a> <a class="code" href="classCVC3_1_1QuantProofRules.html">QuantProofRules</a>* <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a135b1e372b6f3a33941c6fa2ecc93d3e">d_quant_rules</a>;
<a name="l00101"></a>00101
<a name="l00102"></a><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a3837998b3df09387a2a162258ef6b2db">00102</a> std::set<Expr> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a3837998b3df09387a2a162258ef6b2db">d_allIndex</a>; <span class="comment">//a set contains all index</span>
<a name="l00103"></a>00103
<a name="l00104"></a><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#af4ab970a26f5f10316e10b88cd88f5ed">00104</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Polarity></a> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#af4ab970a26f5f10316e10b88cd88f5ed">d_expr_pol</a> ;<span class="comment">//map a expr to its polarity</span>
<a name="l00105"></a>00105
<a name="l00106"></a><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a8c3444e4e7e06812e1823c4b0d323034">00106</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a8c3444e4e7e06812e1823c4b0d323034">d_quant_equiv_map</a> ; <span class="comment">//map a quant to its equivalent form</span>
<a name="l00107"></a>00107
<a name="l00108"></a><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#ae0b4227a71a7d717dd55cc141a638eb1">00108</a> std::vector<Expr> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#ae0b4227a71a7d717dd55cc141a638eb1">d_gnd_cache</a>; <span class="comment">//cache of all ground formulas, before index can be collected, all such ground terms must be put into d_expr_pol.</span>
<a name="l00109"></a>00109
<a name="l00110"></a><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a40a454874f53c168f0e05cffe5d3d853">00110</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a40a454874f53c168f0e05cffe5d3d853">d_is_macro_def</a>;<span class="comment">//if a quant is a macro quant</span>
<a name="l00111"></a>00111
<a name="l00112"></a><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a7a68974e437e44e62cc3020f51f881cc">00112</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a7a68974e437e44e62cc3020f51f881cc">d_macro_quant</a>;<span class="comment">//map a macro to its macro quant.</span>
<a name="l00113"></a>00113
<a name="l00114"></a><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a316d10c5eb6ecb1b11fb212d4835a735">00114</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a316d10c5eb6ecb1b11fb212d4835a735">d_macro_def</a>;<span class="comment">//map a macro head to its def.</span>
<a name="l00115"></a>00115
<a name="l00116"></a><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#ad488e4d5e4340e0401a201a7afcb45f5">00116</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#ad488e4d5e4340e0401a201a7afcb45f5">d_macro_lhs</a>;<span class="comment">//map a macro to its lhs.</span>
<a name="l00117"></a>00117 <span class="comment"></span>
<a name="l00118"></a>00118 <span class="comment"> //! if all formulas checked so far are good</span>
<a name="l00119"></a><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a99f6e270ce292ce04b1dea58cf5b95c3">00119</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a99f6e270ce292ce04b1dea58cf5b95c3" title="if all formulas checked so far are good">d_all_good</a> ;
<a name="l00120"></a>00120 <span class="comment"></span>
<a name="l00121"></a>00121 <span class="comment"> //! if e satisfies the shiled property, that is all bound vars are parameters of uninterpreted functions/predicates and array reads/writes</span>
<a name="l00122"></a>00122 <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#abcd7e5d5717e70de631ccd00d463a3f1" title="if e satisfies the shiled property, that is all bound vars are parameters of uninterpreted functions/...">isShield</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="l00123"></a>00123
<a name="l00124"></a>00124 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a93f995fdf562c93aac2cb2f3f74d6a41">hasShieldVar</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="l00125"></a>00125 <span class="comment"></span>
<a name="l00126"></a>00126 <span class="comment"> //! insert an index</span>
<a name="l00127"></a>00127 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a2bc25f5c5c2a9203936185dbc8fe3a1f" title="insert an index">addIndex</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="l00128"></a>00128
<a name="l00129"></a>00129 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a002b629954b04ffe3a2c5c4d118e220b">collect_shield_index</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="l00130"></a>00130
<a name="l00131"></a>00131 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#aac890a5593abc885fc710614b79a71b0">collect_forall_index</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& forall_quant);
<a name="l00132"></a>00132 <span class="comment"></span>
<a name="l00133"></a>00133 <span class="comment"> //! if e is a quant in the array property fragmenet</span>
<a name="l00134"></a>00134 <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a8bfd959ae7f2e79a9991a8f9229e8d14" title="if e is a quant in the array property fragmenet">isGoodQuant</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="l00135"></a>00135 <span class="comment"></span>
<a name="l00136"></a>00136 <span class="comment"> //! return e+1</span>
<a name="l00137"></a>00137 <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_1CompleteInstPreProcessor.html#a18fc7bd5b8710c016c92a28f1557f5dd" title="return e+1">plusOne</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="l00138"></a>00138 <span class="comment"></span>
<a name="l00139"></a>00139 <span class="comment"> //! return e-1</span>
<a name="l00140"></a>00140 <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_1CompleteInstPreProcessor.html#a8229594b976a7bee92940c1a8ebec1bf" title="return e-1">minusOne</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="l00141"></a>00141
<a name="l00142"></a>00142 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a7c9d388dcb5846892ccc3d42d859c151">collectHeads</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& assert, std::set<Expr>& heads);
<a name="l00143"></a>00143 <span class="comment"></span>
<a name="l00144"></a>00144 <span class="comment"> //! if assert is a macro definition</span>
<a name="l00145"></a>00145 <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#afba1bd2e5c7db9460329c57e63bd0ca4" title="if assert is a macro definition">isMacro</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& assert);
<a name="l00146"></a>00146
<a name="l00147"></a>00147 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a91a6a2cc72569859fe20fbe3f1f7b69a">recInstMacros</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& assert);
<a name="l00148"></a>00148
<a name="l00149"></a>00149 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a7d1616efce19baa76e85ba1f0d14633c">substMacro</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>&);
<a name="l00150"></a>00150
<a name="l00151"></a>00151 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#ae7bef3316e99205836a6c490ce97d0e5">recRewriteNot</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>&, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Polarity></a>&);
<a name="l00152"></a>00152 <span class="comment"></span>
<a name="l00153"></a>00153 <span class="comment"> //! rewrite neg polarity forall / exists to pos polarity</span>
<a name="l00154"></a>00154 <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_1CompleteInstPreProcessor.html#a0d86f8e44226c42e5c9f35ec866a7459" title="rewrite neg polarity forall / exists to pos polarity">rewriteNot</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> &);
<a name="l00155"></a>00155
<a name="l00156"></a>00156 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a26a13f237507dfff8de68bbba747246a">recSkolemize</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> &, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Polarity></a>&);
<a name="l00157"></a>00157
<a name="l00158"></a>00158 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#af229547753572cd602fa29b72dd4b8c4">pullVarOut</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>&);
<a name="l00159"></a>00159
<a name="l00160"></a>00160 <span class="keyword">public</span> :
<a name="l00161"></a>00161
<a name="l00162"></a>00162 <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a43966b9849fccf7dad80f3ea726142ab">CompleteInstPreProcessor</a>(<a class="code" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">TheoryCore</a> * , <a class="code" href="classCVC3_1_1QuantProofRules.html">QuantProofRules</a>*);
<a name="l00163"></a>00163 <span class="comment"></span>
<a name="l00164"></a>00164 <span class="comment"> //! if e is a formula in the array property fragment </span>
<a name="l00165"></a>00165 <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#acaa35692151e48b945ed672248a37a04" title="if e is a formula in the array property fragment">isGood</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="l00166"></a>00166 <span class="comment"></span>
<a name="l00167"></a>00167 <span class="comment"> //! collect index for instantiation</span>
<a name="l00168"></a>00168 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a2d131cd947f7d1f4a4128e9145fefd76" title="collect index for instantiation">collectIndex</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="l00169"></a>00169 <span class="comment"></span>
<a name="l00170"></a>00170 <span class="comment"> //! inst forall quant using index from collectIndex</span>
<a name="l00171"></a>00171 <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_1CompleteInstPreProcessor.html#a40ad81f71a9660025478bdfa3e0faba3" title="inst forall quant using index from collectIndex">inst</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="l00172"></a>00172 <span class="comment"></span>
<a name="l00173"></a>00173 <span class="comment"> //! if there are macros</span>
<a name="l00174"></a>00174 <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a9c4d23bdb98082eb4ed1ad4823e9ae84" title="if there are macros">hasMacros</a>(<span class="keyword">const</span> std::vector<Expr>& asserts);
<a name="l00175"></a>00175 <span class="comment"></span>
<a name="l00176"></a>00176 <span class="comment"> //! substitute a macro in assert</span>
<a name="l00177"></a>00177 <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_1CompleteInstPreProcessor.html#a7446d08768323eeaa24ddc647b872f63" title="substitute a macro in assert">instMacros</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& , <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> );
<a name="l00178"></a>00178 <span class="comment"></span>
<a name="l00179"></a>00179 <span class="comment"> //! simplify a=a to True</span>
<a name="l00180"></a>00180 <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_1CompleteInstPreProcessor.html#a56ee0c6a3da8f909c63b1b6c8927b871" title="simplify a=a to True">simplifyEq</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> &);
<a name="l00181"></a>00181 <span class="comment"></span>
<a name="l00182"></a>00182 <span class="comment"> //! put all quants in postive form and then skolemize all exists </span>
<a name="l00183"></a>00183 <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_1CompleteInstPreProcessor.html#aabf49f82cbf8008c81eef01dd8b66666" title="put all quants in postive form and then skolemize all exists">simplifyQuant</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> &);
<a name="l00184"></a>00184 };
<a name="l00185"></a>00185
<a name="l00186"></a><a class="code" href="classCVC3_1_1TheoryQuant.html">00186</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1TheoryQuant.html" title="This theory handles quantifiers.">TheoryQuant</a> :<span class="keyword">public</span> <a class="code" href="classCVC3_1_1Theory.html" title="Base class for theories.">Theory</a> {
<a name="l00187"></a>00187
<a name="l00188"></a>00188 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#aaed061533566d5aa74f4195a6eece020" title="Theory-specific rewrite rules.">rewrite</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="l00189"></a>00189
<a name="l00190"></a>00190 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a2d5e93e866382db19e0675f693d14c32" title="Theory-specific preprocessing.">theoryPreprocess</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="l00191"></a>00191
<a name="l00192"></a><a class="code" href="classCVC3_1_1TheoryQuant_1_1TypeComp.html">00192</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1TheoryQuant_1_1TypeComp.html">TypeComp</a> { <span class="comment">//!< needed for typeMap</span>
<a name="l00193"></a>00193 <span class="comment"></span> <span class="keyword">public</span>:
<a name="l00194"></a><a class="code" href="classCVC3_1_1TheoryQuant_1_1TypeComp.html#adeafb5c7ebe3a272107f25d0fd695940">00194</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant_1_1TypeComp.html#adeafb5c7ebe3a272107f25d0fd695940" title="< needed for typeMap">operator() </a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> t2)<span class="keyword"> const</span>
<a name="l00195"></a>00195 <span class="keyword"> </span>{<span class="keywordflow">return</span> (t1.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>() < t2.<a class="code" href="classCVC3_1_1Type.html#a0bc1eebf8dbd9d2880e1f18d7804e5c2">getExpr</a>()); }
<a name="l00196"></a>00196 };
<a name="l00197"></a>00197 <span class="comment"></span>
<a name="l00198"></a>00198 <span class="comment"> //! used to facilitate instantiation of universal quantifiers</span>
<a name="l00199"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a9530e1a16572ad8b35d7c3bd08c9803a">00199</a> <span class="comment"></span> <span class="keyword">typedef</span> std::map<Type, std::vector<size_t>, <a class="code" href="classCVC3_1_1TheoryQuant_1_1TypeComp.html">TypeComp</a> > <a class="code" href="classCVC3_1_1TheoryQuant.html#a9530e1a16572ad8b35d7c3bd08c9803a" title="used to facilitate instantiation of universal quantifiers">typeMap</a>;
<a name="l00200"></a>00200 <span class="comment"></span>
<a name="l00201"></a>00201 <span class="comment"> //! database of universally quantified theorems</span>
<a name="l00202"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a8c837bb9045c09ceb44d135e13f1788a">00202</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Theorem></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a8c837bb9045c09ceb44d135e13f1788a" title="database of universally quantified theorems">d_univs</a>;
<a name="l00203"></a>00203
<a name="l00204"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a98562e5cbaac2c2abec9a0814726e990">00204</a> <a class="code" href="classCVC3_1_1CDList.html">CDList<Theorem></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a98562e5cbaac2c2abec9a0814726e990">d_rawUnivs</a>;
<a name="l00205"></a>00205
<a name="l00206"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a6ed4dff6a76e12a20c1b11cf2080106f">00206</a> <a class="code" href="classCVC3_1_1CDList.html">CDList<dynTrig></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a6ed4dff6a76e12a20c1b11cf2080106f">d_arrayTrigs</a>;
<a name="l00207"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a8182fa76e03957abb77e540861c4db40">00207</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a8182fa76e03957abb77e540861c4db40">d_lastArrayPos</a>;
<a name="l00208"></a>00208 <span class="comment"></span>
<a name="l00209"></a>00209 <span class="comment"> //! universally quantified formulas to be instantiated, the var bindings is in d_bingQueue and the ground term matched with the trigger is in d_gtermQueue </span>
<a name="l00210"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a216345a29be8f6c9e135b656e16fd4ca">00210</a> <span class="comment"></span> std::queue<Theorem> <a class="code" href="classCVC3_1_1TheoryQuant.html#a216345a29be8f6c9e135b656e16fd4ca" title="universally quantified formulas to be instantiated, the var bindings is in d_bingQueue and the ground...">d_univsQueue</a>;
<a name="l00211"></a>00211
<a name="l00212"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a20237cf6afe027d65533f121fa9baa8d">00212</a> std::queue<Theorem> <a class="code" href="classCVC3_1_1TheoryQuant.html#a20237cf6afe027d65533f121fa9baa8d">d_simplifiedThmQueue</a>;
<a name="l00213"></a>00213
<a name="l00214"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#adced7c9130c7f24e53f2553eae73246c">00214</a> std::queue<Theorem> <a class="code" href="classCVC3_1_1TheoryQuant.html#adced7c9130c7f24e53f2553eae73246c">d_gUnivQueue</a>;
<a name="l00215"></a>00215
<a name="l00216"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a7f68f552fa0794f221bbceeb7918c167">00216</a> std::queue<Expr> <a class="code" href="classCVC3_1_1TheoryQuant.html#a7f68f552fa0794f221bbceeb7918c167">d_gBindQueue</a>;
<a name="l00217"></a>00217
<a name="l00218"></a>00218
<a name="l00219"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#afa26420c222cf2a7f47c09842b164307">00219</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<std::set<std::vector<Expr></a> > > <a class="code" href="classCVC3_1_1TheoryQuant.html#afa26420c222cf2a7f47c09842b164307">d_tempBinds</a>;
<a name="l00220"></a>00220 <span class="comment"></span>
<a name="l00221"></a>00221 <span class="comment"> //!tracks the possition of preds </span>
<a name="l00222"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ad1c890b18078d4c9ce5ef49517f539c4">00222</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#ad1c890b18078d4c9ce5ef49517f539c4" title="tracks the possition of preds">d_lastPredsPos</a>;<span class="comment"></span>
<a name="l00223"></a>00223 <span class="comment"> //!tracks the possition of terms </span>
<a name="l00224"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ada0a9362e554f531636059ba0f128ac9">00224</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#ada0a9362e554f531636059ba0f128ac9" title="tracks the possition of terms">d_lastTermsPos</a>;
<a name="l00225"></a>00225 <span class="comment"></span>
<a name="l00226"></a>00226 <span class="comment"> //!tracks the positions of preds for partial instantiation</span>
<a name="l00227"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ac84aea59c42a90500d10f8604e7eb822">00227</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#ac84aea59c42a90500d10f8604e7eb822" title="tracks the positions of preds for partial instantiation">d_lastPartPredsPos</a>;<span class="comment"></span>
<a name="l00228"></a>00228 <span class="comment"> //!tracks the possition of terms for partial instantiation</span>
<a name="l00229"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a9141a0d67cecc9180e1838b1e03f2062">00229</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a9141a0d67cecc9180e1838b1e03f2062" title="tracks the possition of terms for partial instantiation">d_lastPartTermsPos</a>;<span class="comment"></span>
<a name="l00230"></a>00230 <span class="comment"> //!tracks a possition in the database of universals for partial instantiation</span>
<a name="l00231"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a49b552d6d70733a9c6dd60eee5a2a646">00231</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a49b552d6d70733a9c6dd60eee5a2a646" title="tracks a possition in the database of universals for partial instantiation">d_univsPartSavedPos</a>;
<a name="l00232"></a>00232 <span class="comment"></span>
<a name="l00233"></a>00233 <span class="comment"> //! the last decision level on which partial instantion is called</span>
<a name="l00234"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#adb2db1fc47d328213e2f8bef1de71b88">00234</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#adb2db1fc47d328213e2f8bef1de71b88" title="the last decision level on which partial instantion is called">d_lastPartLevel</a>;
<a name="l00235"></a>00235
<a name="l00236"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a777ab16b886b05ea63180e44bd62fe43">00236</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<bool></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a777ab16b886b05ea63180e44bd62fe43">d_partCalled</a>;
<a name="l00237"></a>00237 <span class="comment"></span>
<a name="l00238"></a>00238 <span class="comment"> //! the max instantiation level reached</span>
<a name="l00239"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a5c321d21dbbf2e23a772dec478dd6ade">00239</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<bool></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a5c321d21dbbf2e23a772dec478dd6ade" title="the max instantiation level reached">d_maxILReached</a>;
<a name="l00240"></a>00240
<a name="l00241"></a>00241
<a name="l00242"></a>00242 <span class="comment"></span>
<a name="l00243"></a>00243 <span class="comment"> //!useful gterms for matching</span>
<a name="l00244"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ae2aa24cf865298deb21463f1c64cefed">00244</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#ae2aa24cf865298deb21463f1c64cefed" title="useful gterms for matching">d_usefulGterms</a>;
<a name="l00245"></a>00245 <span class="comment"></span>
<a name="l00246"></a>00246 <span class="comment"> //!tracks the position in d_usefulGterms</span>
<a name="l00247"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a949092aaf1aba7329ab512031f8399cc">00247</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a949092aaf1aba7329ab512031f8399cc" title="tracks the position in d_usefulGterms">d_lastUsefulGtermsPos</a>;
<a name="l00248"></a>00248 <span class="comment"></span>
<a name="l00249"></a>00249 <span class="comment"> //!tracks a possition in the savedTerms map</span>
<a name="l00250"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a12325d3d4d8cd79170c4cf3ec61a511f">00250</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a12325d3d4d8cd79170c4cf3ec61a511f" title="tracks a possition in the savedTerms map">d_savedTermsPos</a>;<span class="comment"></span>
<a name="l00251"></a>00251 <span class="comment"> //!tracks a possition in the database of universals</span>
<a name="l00252"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a78e66cea83a0bd258f7c7064bac4808c">00252</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a78e66cea83a0bd258f7c7064bac4808c" title="tracks a possition in the database of universals">d_univsSavedPos</a>;
<a name="l00253"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a54e9b1c666a443f2fd4b8abf48077f5b">00253</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a54e9b1c666a443f2fd4b8abf48077f5b">d_rawUnivsSavedPos</a>;<span class="comment"></span>
<a name="l00254"></a>00254 <span class="comment"> //!tracks a possition in the database of universals</span>
<a name="l00255"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a8b5e246c61121a22421d550d4376d3f0">00255</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a8b5e246c61121a22421d550d4376d3f0" title="tracks a possition in the database of universals">d_univsPosFull</a>;<span class="comment"></span>
<a name="l00256"></a>00256 <span class="comment"> //!tracks a possition in the database of universals if fulleffort mode, the d_univsSavedPos now uesed when fulleffort=0 only.</span>
<a name="l00257"></a>00257 <span class="comment"></span>
<a name="l00258"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a0388d31f826f4786e14d252726c8c26a">00258</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a0388d31f826f4786e14d252726c8c26a" title="tracks a possition in the database of universals if fulleffort mode, the d_univsSavedPos now uesed wh...">d_univsContextPos</a>;
<a name="l00259"></a>00259
<a name="l00260"></a>00260
<a name="l00261"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a9bc78df3616eacf20e564a08c8a9896f">00261</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<int></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a9bc78df3616eacf20e564a08c8a9896f" title="number of instantiations made in given context">d_instCount</a>; <span class="comment">//!< number of instantiations made in given context</span>
<a name="l00262"></a>00262 <span class="comment"></span><span class="comment"></span>
<a name="l00263"></a>00263 <span class="comment"> //! set if the fullEffort = 1</span>
<a name="l00264"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a97c18d8746ce2afdd83a9e12c84cdd24">00264</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a97c18d8746ce2afdd83a9e12c84cdd24" title="set if the fullEffort = 1">d_inEnd</a>;
<a name="l00265"></a>00265
<a name="l00266"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a6c0bfa341c282227a4a94e27d997bf01">00266</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a6c0bfa341c282227a4a94e27d997bf01">d_allout</a>;
<a name="l00267"></a>00267 <span class="comment"></span>
<a name="l00268"></a>00268 <span class="comment"> //! a map of types to posisitions in the d_contextTerms list</span>
<a name="l00269"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a9f6efeac1026260673ddbf7f083504da">00269</a> <span class="comment"></span> std::map<Type, CDList<size_t>* ,<a class="code" href="classCVC3_1_1TheoryQuant_1_1TypeComp.html">TypeComp</a>> <a class="code" href="classCVC3_1_1TheoryQuant.html#a9f6efeac1026260673ddbf7f083504da" title="a map of types to posisitions in the d_contextTerms list">d_contextMap</a>;<span class="comment"></span>
<a name="l00270"></a>00270 <span class="comment"> //! a list of all the terms appearing in the current context</span>
<a name="l00271"></a>00271 <span class="comment"></span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#aa859e8e5d08c4c4a64c110f956209b72" title="a list of all the terms appearing in the current context">d_contextTerms</a>;<span class="comment"></span>
<a name="l00272"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#aa859e8e5d08c4c4a64c110f956209b72">00272</a> <span class="comment"> //!< chache of expressions</span>
<a name="l00273"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ab4a7ed7a25824178d2a60fb9d2645632">00273</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, bool></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#ab4a7ed7a25824178d2a60fb9d2645632">d_contextCache</a>;
<a name="l00274"></a>00274 <span class="comment"></span>
<a name="l00275"></a>00275 <span class="comment"> //! a map of types to positions in the d_savedTerms vector</span>
<a name="l00276"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a151130d7ab3011be448ea16b0eb96156">00276</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a9530e1a16572ad8b35d7c3bd08c9803a" title="used to facilitate instantiation of universal quantifiers">typeMap</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a151130d7ab3011be448ea16b0eb96156" title="a map of types to positions in the d_savedTerms vector">d_savedMap</a>;
<a name="l00277"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a2090a926ff4120c1f417693974afd49e">00277</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a2090a926ff4120c1f417693974afd49e">d_savedCache</a>; <span class="comment">//!< cache of expressions</span>
<a name="l00278"></a>00278 <span class="comment"></span><span class="comment"> //! a vector of all of the terms that have produced conflicts.</span>
<a name="l00279"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ab8eafb65bdcded93b43a311e65d80051">00279</a> <span class="comment"></span> std::vector<Expr> <a class="code" href="classCVC3_1_1TheoryQuant.html#ab8eafb65bdcded93b43a311e65d80051" title="a vector of all of the terms that have produced conflicts.">d_savedTerms</a>;
<a name="l00280"></a>00280 <span class="comment"></span>
<a name="l00281"></a>00281 <span class="comment"> //! a map of instantiated universals to a vector of their instantiations</span>
<a name="l00282"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#afbc66a1d0e321ce140c1db73d22d2551">00282</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<std::vector<Expr></a> > <a class="code" href="classCVC3_1_1TheoryQuant.html#afbc66a1d0e321ce140c1db73d22d2551" title="a map of instantiated universals to a vector of their instantiations">d_insts</a>;
<a name="l00283"></a>00283 <span class="comment"></span>
<a name="l00284"></a>00284 <span class="comment"> //! quantifier theorem production rules</span>
<a name="l00285"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a402f8b86c479687a21ff3e71581e9cd4">00285</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1QuantProofRules.html">QuantProofRules</a>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a402f8b86c479687a21ff3e71581e9cd4" title="quantifier theorem production rules">d_rules</a>;
<a name="l00286"></a>00286
<a name="l00287"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#aad0370d3aabc256eb298dfcc27229e72">00287</a> <span class="keyword">const</span> <span class="keywordtype">int</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#aad0370d3aabc256eb298dfcc27229e72" title="Command line option.">d_maxQuantInst</a>; <span class="comment">//!< Command line option</span>
<a name="l00288"></a>00288 <span class="comment"></span><span class="comment"></span>
<a name="l00289"></a>00289 <span class="comment"> /*! \brief categorizes all the terms contained in an expressions by</span>
<a name="l00290"></a>00290 <span class="comment"> *type.</span>
<a name="l00291"></a>00291 <span class="comment"> *</span>
<a name="l00292"></a>00292 <span class="comment"> * Updates d_contextTerms, d_contextMap, d_contextCache accordingly.</span>
<a name="l00293"></a>00293 <span class="comment"> * returns true if the expression does not contain bound variables, false</span>
<a name="l00294"></a>00294 <span class="comment"> * otherwise.</span>
<a name="l00295"></a>00295 <span class="comment"> */</span>
<a name="l00296"></a>00296 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a184ff0daa00e9777c766aec5e1fc3015" title="categorizes all the terms contained in an expressions by type.">recursiveMap</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& term);
<a name="l00297"></a>00297 <span class="comment"></span>
<a name="l00298"></a>00298 <span class="comment"> /*! \brief categorizes all the terms contained in a vector of expressions by</span>
<a name="l00299"></a>00299 <span class="comment"> * type.</span>
<a name="l00300"></a>00300 <span class="comment"> *</span>
<a name="l00301"></a>00301 <span class="comment"> * Updates d_contextTerms, d_contextMap, d_contextCache accordingly.</span>
<a name="l00302"></a>00302 <span class="comment"> */</span>
<a name="l00303"></a>00303 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a151e98ce89abebbe306580f7fcd06704" title="categorizes all the terms contained in a vector of expressions by type.">mapTermsByType</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& terms);
<a name="l00304"></a>00304 <span class="comment"></span>
<a name="l00305"></a>00305 <span class="comment"> /*! \brief Queues up all possible instantiations of bound</span>
<a name="l00306"></a>00306 <span class="comment"> * variables.</span>
<a name="l00307"></a>00307 <span class="comment"> *</span>
<a name="l00308"></a>00308 <span class="comment"> * The savedMap boolean indicates whether to use savedMap or</span>
<a name="l00309"></a>00309 <span class="comment"> * d_contextMap the all boolean indicates weather to use all</span>
<a name="l00310"></a>00310 <span class="comment"> * instantiation or only new ones and newIndex is the index where</span>
<a name="l00311"></a>00311 <span class="comment"> * new instantiations begin.</span>
<a name="l00312"></a>00312 <span class="comment"> */</span>
<a name="l00313"></a>00313 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a501db08125b03768f4f270c3d4a251e0" title="Queues up all possible instantiations of bound variables.">instantiate</a>(<a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> univ, <span class="keywordtype">bool</span> all, <span class="keywordtype">bool</span> savedMap,
<a name="l00314"></a>00314 <span class="keywordtype">size_t</span> newIndex);<span class="comment"></span>
<a name="l00315"></a>00315 <span class="comment"> //! does most of the work of the instantiate function.</span>
<a name="l00316"></a>00316 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a9e3bb4497a71d84322a8f97a86d2b11c" title="does most of the work of the instantiate function.">recInstantiate</a>(<a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& univ , <span class="keywordtype">bool</span> all, <span class="keywordtype">bool</span> savedMap,<span class="keywordtype">size_t</span> newIndex,
<a name="l00317"></a>00317 std::vector<Expr>& varReplacements);
<a name="l00318"></a>00318 <span class="comment"></span>
<a name="l00319"></a>00319 <span class="comment"> /*! \brief A recursive function used to find instantiated universals</span>
<a name="l00320"></a>00320 <span class="comment"> * in the hierarchy of assumptions.</span>
<a name="l00321"></a>00321 <span class="comment"> */</span>
<a name="l00322"></a>00322 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a652fbf4d1d2a11fc048e0cedcb8d69e1" title="A recursive function used to find instantiated universals in the hierarchy of assumptions.">findInstAssumptions</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);
<a name="l00323"></a>00323
<a name="l00324"></a>00324 <span class="comment">// CDO<bool> usedup;</span>
<a name="l00325"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a941345e490bc23ed9454bc98513fafb2">00325</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a941345e490bc23ed9454bc98513fafb2">d_useNew</a>;<span class="comment">//!use new way of instantiation</span>
<a name="l00326"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a71f7265b98a79dff4f924fa84c6720d5">00326</a> <span class="comment"></span> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a71f7265b98a79dff4f924fa84c6720d5" title="use new way of instantiation">d_useLazyInst</a>;<span class="comment">//!use lazy instantiation</span>
<a name="l00327"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a6849ba1ee187928b1c254722525f8c5e">00327</a> <span class="comment"></span> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a6849ba1ee187928b1c254722525f8c5e" title="use lazy instantiation">d_useSemMatch</a>;<span class="comment">//!use semantic matching</span>
<a name="l00328"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a307d487df3c5ba9770f4f2c99a1ce912">00328</a> <span class="comment"></span> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a307d487df3c5ba9770f4f2c99a1ce912" title="use semantic matching">d_useCompleteInst</a>; <span class="comment">//! Try complete instantiation </span>
<a name="l00329"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#affe271f96919ed4bb74e331159573d03">00329</a> <span class="comment"></span> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#affe271f96919ed4bb74e331159573d03" title="Try complete instantiation.">d_translate</a>;<span class="comment">//!translate only</span>
<a name="l00330"></a>00330 <span class="comment"></span>
<a name="l00331"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#aa6c894d36bb697a93713950312593e53">00331</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#aa6c894d36bb697a93713950312593e53" title="translate only">d_usePart</a>;<span class="comment">//!use partial instantiaion</span>
<a name="l00332"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ad0bf093cc6fe61456b2d186333fa1476">00332</a> <span class="comment"></span> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#ad0bf093cc6fe61456b2d186333fa1476" title="use partial instantiaion">d_useMult</a>;<span class="comment">//use </span>
<a name="l00333"></a>00333 <span class="comment">// const bool* d_useInstEnd;</span>
<a name="l00334"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ae18bcd5e6dd77c740c08a37a90face8d">00334</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#ae18bcd5e6dd77c740c08a37a90face8d">d_useInstLCache</a>;
<a name="l00335"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#aed3aa4f475cb2d920dcc137009aa208c">00335</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#aed3aa4f475cb2d920dcc137009aa208c">d_useInstGCache</a>;
<a name="l00336"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a0cb98a0e60550b47b6cf62d58ef7526c">00336</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a0cb98a0e60550b47b6cf62d58ef7526c">d_useInstThmCache</a>;
<a name="l00337"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a26af226b922851112e91577ca7e3b452">00337</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a26af226b922851112e91577ca7e3b452">d_useInstTrue</a>;
<a name="l00338"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a40f07b217c6934bba4480207f798eea2">00338</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a40f07b217c6934bba4480207f798eea2">d_usePullVar</a>;
<a name="l00339"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a8f7f76c25794e58a8bbd35bbb37e3aed">00339</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a8f7f76c25794e58a8bbd35bbb37e3aed">d_useExprScore</a>;
<a name="l00340"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a1f1f4c18fe0c68dfb7eea0d3bd0220db">00340</a> <span class="keyword">const</span> <span class="keywordtype">int</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a1f1f4c18fe0c68dfb7eea0d3bd0220db">d_useTrigLoop</a>;
<a name="l00341"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a5f3ae02fd56df2f401da18b10ffc068b">00341</a> <span class="keyword">const</span> <span class="keywordtype">int</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a5f3ae02fd56df2f401da18b10ffc068b">d_maxInst</a>;
<a name="l00342"></a>00342 <span class="comment">// const int* d_maxUserScore;</span>
<a name="l00343"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#aa223ccaf4a6297fbe9243905f2fa1cd3">00343</a> <span class="keyword">const</span> <span class="keywordtype">int</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#aa223ccaf4a6297fbe9243905f2fa1cd3">d_maxIL</a>;
<a name="l00344"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a6bde73c972d4bfc46683279e6c18b7df">00344</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a6bde73c972d4bfc46683279e6c18b7df">d_useTrans</a>;
<a name="l00345"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a596216803168d232d335c3a2e7b35a02">00345</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a596216803168d232d335c3a2e7b35a02">d_useTrans2</a>;
<a name="l00346"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a2a8534b65e4c74e2c28c98f297b931e0">00346</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a2a8534b65e4c74e2c28c98f297b931e0">d_useManTrig</a>;
<a name="l00347"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a2dc4c4cd98dd966b17a705399db80bd4">00347</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a2dc4c4cd98dd966b17a705399db80bd4">d_useGFact</a>;
<a name="l00348"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a343bd1867fbb824c16f2bc376d031234">00348</a> <span class="keyword">const</span> <span class="keywordtype">int</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a343bd1867fbb824c16f2bc376d031234">d_gfactLimit</a>;
<a name="l00349"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a1caf0d9c2c9ff8ac77123921158e781c">00349</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a1caf0d9c2c9ff8ac77123921158e781c">d_useInstAll</a>;
<a name="l00350"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a7285a10b61c56f1abd386d15da664341">00350</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a7285a10b61c56f1abd386d15da664341">d_usePolarity</a>;
<a name="l00351"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ab6987761a0573b5a1f96be74f5be6594">00351</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#ab6987761a0573b5a1f96be74f5be6594">d_useEqu</a>;
<a name="l00352"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ad7cb228fd0c997d6d0cb92ebdf36f0d4">00352</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#ad7cb228fd0c997d6d0cb92ebdf36f0d4">d_useNewEqu</a>;
<a name="l00353"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ac5ecfdb795d8741da3942e7e4ec19928">00353</a> <span class="keyword">const</span> <span class="keywordtype">int</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#ac5ecfdb795d8741da3942e7e4ec19928">d_maxNaiveCall</a>;
<a name="l00354"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ae3655c358b7c2b206c7a467eb7cc4880">00354</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#ae3655c358b7c2b206c7a467eb7cc4880">d_useNaiveInst</a>;
<a name="l00355"></a>00355
<a name="l00356"></a>00356
<a name="l00357"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a0353fa5170be84ed1feffc0adaea61b6">00357</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<int></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a0353fa5170be84ed1feffc0adaea61b6">d_curMaxExprScore</a>;
<a name="l00358"></a>00358
<a name="l00359"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ae765160d5df0404da2d869a19ce3392d">00359</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#ae765160d5df0404da2d869a19ce3392d">d_useFullTrig</a>;
<a name="l00360"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a43d925d46b17106af6676a693bb3e81c">00360</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a43d925d46b17106af6676a693bb3e81c">d_usePartTrig</a>;
<a name="l00361"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a94cdc6b5d40ea0d468176829f3b7cc7f">00361</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a94cdc6b5d40ea0d468176829f3b7cc7f">d_useMultTrig</a>;
<a name="l00362"></a>00362
<a name="l00363"></a>00363 <span class="comment">//ExprMap<std::vector<Expr> > d_arrayIndic; //map array name to a list of indics</span>
<a name="l00364"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a42bf4d8a8865547e765374f47c89a42d">00364</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, std::vector<Expr></a> > <a class="code" href="classCVC3_1_1TheoryQuant.html#a42bf4d8a8865547e765374f47c89a42d">d_arrayIndic</a>; <span class="comment">//map array name to a list of indics</span>
<a name="l00365"></a>00365 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#acad8f385272425eabffcc518eacefbb4">arrayIndexName</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="l00366"></a>00366
<a name="l00367"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a257fa05e1227011338ff18b07bbd8ea7">00367</a> std::vector<Expr> <a class="code" href="classCVC3_1_1TheoryQuant.html#a257fa05e1227011338ff18b07bbd8ea7">d_allInsts</a>; <span class="comment">//! all instantiations</span>
<a name="l00368"></a>00368 <span class="comment"></span>
<a name="l00369"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a7e5a0fbbbe03ac62ae2fe52ea6768988">00369</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a7e5a0fbbbe03ac62ae2fe52ea6768988" title="all instantiations">d_initMaxScore</a>;
<a name="l00370"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#adb5ce0ce6808f4d60284a2658256a772">00370</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#adb5ce0ce6808f4d60284a2658256a772">d_offset_multi_trig</a> ;
<a name="l00371"></a>00371
<a name="l00372"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a42b268e32a020cedcca5c58efd84c114">00372</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a42b268e32a020cedcca5c58efd84c114">d_instThisRound</a>;
<a name="l00373"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a0615dcf3f868ddbd02984a29e482427e">00373</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a0615dcf3f868ddbd02984a29e482427e">d_callThisRound</a>;
<a name="l00374"></a>00374
<a name="l00375"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#aa60a22e8795e5046cd17d016d40705b2">00375</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#aa60a22e8795e5046cd17d016d40705b2">partial_called</a>;
<a name="l00376"></a>00376
<a name="l00377"></a>00377 <span class="comment">// ExprMap<std::vector<Expr> > d_fullTriggers;</span>
<a name="l00378"></a>00378 <span class="comment">//for multi-triggers, now we only have one set of multi-triggers.</span>
<a name="l00379"></a>00379
<a name="l00380"></a>00380
<a name="l00381"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ac1f7a57f263b0bbc3d2bd87e7a931598">00381</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<std::vector<Expr></a> > <a class="code" href="classCVC3_1_1TheoryQuant.html#ac1f7a57f263b0bbc3d2bd87e7a931598">d_multTriggers</a>;
<a name="l00382"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ab00d303da385069d53e20c8fe52248b0">00382</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<std::vector<Expr></a> > <a class="code" href="classCVC3_1_1TheoryQuant.html#ab00d303da385069d53e20c8fe52248b0">d_partTriggers</a>;
<a name="l00383"></a>00383
<a name="l00384"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a590efa99276b0b530def7c750931f0e0">00384</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<std::vector<Trigger></a> > <a class="code" href="classCVC3_1_1TheoryQuant.html#a590efa99276b0b530def7c750931f0e0">d_fullTrigs</a>;
<a name="l00385"></a>00385 <span class="comment">//for multi-triggers, now we only have one set of multi-triggers.</span>
<a name="l00386"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ab3d76fe9a84814d0493dc47928450be1">00386</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<std::vector<Trigger></a> > <a class="code" href="classCVC3_1_1TheoryQuant.html#ab3d76fe9a84814d0493dc47928450be1">d_multTrigs</a>;
<a name="l00387"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a9b64987d5098fd227f10b45e0365da63">00387</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<std::vector<Trigger></a> > <a class="code" href="classCVC3_1_1TheoryQuant.html#a9b64987d5098fd227f10b45e0365da63">d_partTrigs</a>;
<a name="l00388"></a>00388
<a name="l00389"></a>00389
<a name="l00390"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ad9e2ac11111d8068cd47101e914400ec">00390</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#ad9e2ac11111d8068cd47101e914400ec">d_exprLastUpdatedPos</a> ;<span class="comment">//the position of the last expr updated in d_exprUpdate </span>
<a name="l00391"></a>00391
<a name="l00392"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a8acfdb59fc63cde21b7d9ec22796756d">00392</a> std::map<ExprIndex, int> <a class="code" href="classCVC3_1_1TheoryQuant.html#a8acfdb59fc63cde21b7d9ec22796756d">d_indexScore</a>;
<a name="l00393"></a>00393
<a name="l00394"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a712b1f8b6128c2f5290b02b16285fac4">00394</a> std::map<ExprIndex, Expr> <a class="code" href="classCVC3_1_1TheoryQuant.html#a712b1f8b6128c2f5290b02b16285fac4">d_indexExpr</a>;
<a name="l00395"></a>00395
<a name="l00396"></a>00396 <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a8e31abf45d65f6893471be5611aa9f2e">getExprScore</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="l00397"></a>00397 <span class="comment"></span>
<a name="l00398"></a>00398 <span class="comment"> //!the score for a full trigger</span>
<a name="l00399"></a>00399 <span class="comment"></span>
<a name="l00400"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#aa0f0f35f81aad33349edb9a4ae1f50c2">00400</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#aa0f0f35f81aad33349edb9a4ae1f50c2" title="the score for a full trigger">d_hasTriggers</a>;
<a name="l00401"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a149311d8fb4973ba78aaef0b49fcdeb3">00401</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a149311d8fb4973ba78aaef0b49fcdeb3">d_hasMoreBVs</a>;
<a name="l00402"></a>00402
<a name="l00403"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a32a16dc1f3abd4bb2923512863dad2e3">00403</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a32a16dc1f3abd4bb2923512863dad2e3">d_trans_num</a>;
<a name="l00404"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a21177e07fa85adab68a40245f7b56dc7">00404</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a21177e07fa85adab68a40245f7b56dc7">d_trans2_num</a>;
<a name="l00405"></a>00405
<a name="l00406"></a><a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html">00406</a> <span class="keyword">typedef</span> <span class="keyword">struct</span>{
<a name="l00407"></a><a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#a30585771f9ea7ba104b9b0e96aae8f58">00407</a> std::vector<std::vector<size_t> > <a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#a30585771f9ea7ba104b9b0e96aae8f58">common_pos</a>;
<a name="l00408"></a><a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#aa9a7e0ca5f85e46d2a87574d31340882">00408</a> std::vector<std::vector<size_t> > <a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#aa9a7e0ca5f85e46d2a87574d31340882">var_pos</a>;
<a name="l00409"></a>00409
<a name="l00410"></a><a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#ae8069d3960f8fca170b24437747be5be">00410</a> std::vector<CDMap<Expr, bool>* > <a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#ae8069d3960f8fca170b24437747be5be">var_binds_found</a>;
<a name="l00411"></a>00411
<a name="l00412"></a><a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#adb3cde79421ada753728f06749d81a26">00412</a> std::vector<ExprMap<CDList<Expr>* >* > <a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#adb3cde79421ada753728f06749d81a26">uncomm_list</a>; <span class="comment">//</span>
<a name="l00413"></a><a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#a1bb00c7646f04ef7a7b1effe16afbf47">00413</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#a1bb00c7646f04ef7a7b1effe16afbf47">univThm</a>; <span class="comment">// for test only</span>
<a name="l00414"></a><a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#a96287846947610728257c05150e830a0">00414</a> <span class="keywordtype">size_t</span> <a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#a96287846947610728257c05150e830a0">univ_id</a>; <span class="comment">// for test only</span>
<a name="l00415"></a>00415 } <a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html">multTrigsInfo</a> ;
<a name="l00416"></a>00416
<a name="l00417"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#abe536d22495efd45fcb3c35cadc3f417">00417</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<multTrigsInfo></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#abe536d22495efd45fcb3c35cadc3f417">d_multitrigs_maps</a>;
<a name="l00418"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a5ba728c791a6e156c1e1252698656154">00418</a> std::vector<multTrigsInfo> <a class="code" href="classCVC3_1_1TheoryQuant.html#a5ba728c791a6e156c1e1252698656154">d_all_multTrigsInfo</a>;
<a name="l00419"></a>00419
<a name="l00420"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a5988b551d392a2675afe20061c374387">00420</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<CDList<Expr></a>* > <a class="code" href="classCVC3_1_1TheoryQuant.html#a5988b551d392a2675afe20061c374387">d_trans_back</a>;
<a name="l00421"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a09130b8c278fc53d6b978144fc060b88">00421</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<CDList<Expr></a>* > <a class="code" href="classCVC3_1_1TheoryQuant.html#a09130b8c278fc53d6b978144fc060b88">d_trans_forw</a>;
<a name="l00422"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a40d9d2a6ac497d8925d85b1534f927fe">00422</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,bool ></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a40d9d2a6ac497d8925d85b1534f927fe">d_trans_found</a>;
<a name="l00423"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a1c1cea4c4d5aa9cd0e85233daf082a14">00423</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,bool ></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a1c1cea4c4d5aa9cd0e85233daf082a14">d_trans2_found</a>;
<a name="l00424"></a>00424
<a name="l00425"></a>00425
<a name="l00426"></a>00426 <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a192cb414dac910cbd803f82ad39df82e">transFound</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& comb);
<a name="l00427"></a>00427
<a name="l00428"></a>00428 <span class="keyword">inline</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a2839204961cc646d22f8dfd3c1c53575">setTransFound</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& comb);
<a name="l00429"></a>00429
<a name="l00430"></a>00430 <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a2c9aee5ef245bdf1536f58c17414f4f0">trans2Found</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& comb);
<a name="l00431"></a>00431
<a name="l00432"></a>00432 <span class="keyword">inline</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a9ed056909d84ff32d1768bce20ba3480">setTrans2Found</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& comb);
<a name="l00433"></a>00433
<a name="l00434"></a>00434
<a name="l00435"></a>00435 <span class="keyword">inline</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a> & <a class="code" href="classCVC3_1_1TheoryQuant.html#ac4aaca08cc3081e899b3f771a8a37a37">backList</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& ex);
<a name="l00436"></a>00436
<a name="l00437"></a>00437 <span class="keyword">inline</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a> & <a class="code" href="classCVC3_1_1TheoryQuant.html#a009ef12073c14fb4f18c0d05fd166c11">forwList</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& ex);
<a name="l00438"></a>00438
<a name="l00439"></a>00439 <span class="keywordtype">void</span> <span class="keyword">inline</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#aa695cc36069a55cb32ed84963093bd9d">iterFWList</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& sr, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& dt, <span class="keywordtype">size_t</span> univ_id, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm);
<a name="l00440"></a>00440 <span class="keywordtype">void</span> <span class="keyword">inline</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a2b83e2b6ed406fab48b51aad5bed441b">iterBKList</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& sr, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& dt, <span class="keywordtype">size_t</span> univ_id, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm);
<a name="l00441"></a>00441
<a name="l00442"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a8c198e6cf92b67913a4c2eeba3049591">00442</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a8c198e6cf92b67913a4c2eeba3049591">defaultWriteExpr</a>;
<a name="l00443"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ac3c6c90503e2a63b01cb71aec8e67959">00443</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#ac3c6c90503e2a63b01cb71aec8e67959">defaultReadExpr</a>;
<a name="l00444"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ae722d51a41c8bbfb71262033b5366267">00444</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#ae722d51a41c8bbfb71262033b5366267">defaultPlusExpr</a>;
<a name="l00445"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#adaebb75807818796d34d2ff776755528">00445</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#adaebb75807818796d34d2ff776755528">defaultMinusExpr</a> ;
<a name="l00446"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a52e766e9bd39c2061de7c46368fd28e0">00446</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a52e766e9bd39c2061de7c46368fd28e0">defaultMultExpr</a> ;
<a name="l00447"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a7ee722984f64a327d4afd1d44915c94c">00447</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a7ee722984f64a327d4afd1d44915c94c">defaultDivideExpr</a>;
<a name="l00448"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ab47f89174cf6213f2379e9df4eef8bec">00448</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#ab47f89174cf6213f2379e9df4eef8bec">defaultPowExpr</a> ;
<a name="l00449"></a>00449
<a name="l00450"></a>00450 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a26d25a02f8647a37593d84c75e23d78c">getHead</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="l00451"></a>00451 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a1de92cf7646580a4c25596cd91a0ece4">getHeadExpr</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="l00452"></a>00452
<a name="l00453"></a>00453
<a name="l00454"></a>00454
<a name="l00455"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a48b9c68f68437b817726cedaf097a531">00455</a> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a48b9c68f68437b817726cedaf097a531">null_cdlist</a>;
<a name="l00456"></a>00456
<a name="l00457"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ab4cd6dafd73a1cdb2ce8d0bfa68975f5">00457</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#ab4cd6dafd73a1cdb2ce8d0bfa68975f5">d_transThm</a>;
<a name="l00458"></a>00458
<a name="l00459"></a>00459 <span class="keyword">inline</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a641298c9d293b81af61f5de825b3324a">pushBackList</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& node, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> ex);
<a name="l00460"></a>00460 <span class="keyword">inline</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a88227f7c82c03ffd8ad44a959cc47554">pushForwList</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& node, <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> ex);
<a name="l00461"></a>00461
<a name="l00462"></a>00462
<a name="l00463"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a0026da40c823471fb89c809d5429213f">00463</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<CDList<std::vector<Expr></a> >* > <a class="code" href="classCVC3_1_1TheoryQuant.html#a0026da40c823471fb89c809d5429213f">d_mtrigs_inst</a>; <span class="comment">//map expr to bindings</span>
<a name="l00464"></a>00464
<a name="l00465"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ab211a218c1b6d7f99ce2310730b27bbb">00465</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<CDList<Expr></a>* > <a class="code" href="classCVC3_1_1TheoryQuant.html#ab211a218c1b6d7f99ce2310730b27bbb">d_same_head_expr</a>; <span class="comment">//map an expr to a list of expres shard the same head</span>
<a name="l00466"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a0a9d848eb97d33e8c555015cb126c39b">00466</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<CDList<Expr></a>* > <a class="code" href="classCVC3_1_1TheoryQuant.html#a0a9d848eb97d33e8c555015cb126c39b">d_eq_list</a>; <span class="comment">//the equalities list</span>
<a name="l00467"></a>00467
<a name="l00468"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#afeebec46ae80ed697b00a5da3e043576">00468</a> <a class="code" href="classCVC3_1_1CDList.html">CDList<Theorem></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#afeebec46ae80ed697b00a5da3e043576">d_eqsUpdate</a>; <span class="comment">//the equalities list collected from update()</span>
<a name="l00469"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a5d4d5c909890619d446f8e1563d86e60">00469</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a5d4d5c909890619d446f8e1563d86e60">d_lastEqsUpdatePos</a>;
<a name="l00470"></a>00470
<a name="l00471"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a66b5c3d369b6e969015c566d86014e46">00471</a> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr ></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a66b5c3d369b6e969015c566d86014e46">d_eqs</a>; <span class="comment">//the equalities list</span>
<a name="l00472"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#aecebd6c0ff45e853d495b3a940a34a65">00472</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t ></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#aecebd6c0ff45e853d495b3a940a34a65">d_eqs_pos</a>; <span class="comment">//the equalities list</span>
<a name="l00473"></a>00473
<a name="l00474"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#acc57bb5cdcafa8c1fbdf85c030e35d00">00474</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<CDO<size_t></a>* > <a class="code" href="classCVC3_1_1TheoryQuant.html#acc57bb5cdcafa8c1fbdf85c030e35d00">d_eq_pos</a>;
<a name="l00475"></a>00475
<a name="l00476"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a33efe13ffba90a746bea195b8892a437">00476</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<CDList<Expr></a>* > <a class="code" href="classCVC3_1_1TheoryQuant.html#a33efe13ffba90a746bea195b8892a437">d_parent_list</a>;
<a name="l00477"></a>00477 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#afd3873e6105a187cba1e1c364c6b06d1">collectChangedTerms</a>(<a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& changed_terms);
<a name="l00478"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ab36ea36a9cc54b697a0d188f725558c1">00478</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<std::vector<Expr></a> > <a class="code" href="classCVC3_1_1TheoryQuant.html#ab36ea36a9cc54b697a0d188f725558c1">d_mtrigs_bvorder</a>;
<a name="l00479"></a>00479
<a name="l00480"></a>00480 <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a40cb1864bfcfedf2f6b20db57ba662ed">loc_gterm</a>(<span class="keyword">const</span> std::vector<Expr>& border,
<a name="l00481"></a>00481 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm,
<a name="l00482"></a>00482 <span class="keywordtype">int</span> pos);
<a name="l00483"></a>00483
<a name="l00484"></a>00484 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a21e6b9a3115caa0b22322bd75d883347">recSearchCover</a>(<span class="keyword">const</span> std::vector<Expr>& border,
<a name="l00485"></a>00485 <span class="keyword">const</span> std::vector<Expr>& mtrigs,
<a name="l00486"></a>00486 <span class="keywordtype">int</span> cur_depth,
<a name="l00487"></a>00487 std::vector<std::vector<Expr> >& instSet,
<a name="l00488"></a>00488 std::vector<Expr>& cur_inst
<a name="l00489"></a>00489 );
<a name="l00490"></a>00490
<a name="l00491"></a>00491 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a681dfda538563ad8b07372fde28947e9">searchCover</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& thm,
<a name="l00492"></a>00492 <span class="keyword">const</span> std::vector<Expr>& border,
<a name="l00493"></a>00493 std::vector<std::vector<Expr> >& instSet
<a name="l00494"></a>00494 );
<a name="l00495"></a>00495
<a name="l00496"></a>00496
<a name="l00497"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a99ff15c8d97f8c5539d744d077679bbd">00497</a> std::map<Type, std::vector<Expr>,<a class="code" href="classCVC3_1_1TheoryQuant_1_1TypeComp.html">TypeComp</a> > <a class="code" href="classCVC3_1_1TheoryQuant.html#a99ff15c8d97f8c5539d744d077679bbd">d_typeExprMap</a>;
<a name="l00498"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#aaab4c2084e0104f66d12fd9d08b9823b">00498</a> std::set<std::string> <a class="code" href="classCVC3_1_1TheoryQuant.html#aaab4c2084e0104f66d12fd9d08b9823b">cacheHead</a>;
<a name="l00499"></a>00499
<a name="l00500"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ad705af0d0dad0e43422b8f2b6c7f6885">00500</a> <a class="code" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#ad705af0d0dad0e43422b8f2b6c7f6885">d_allInstCount</a> ; <span class="comment">//the number instantiations asserted in SAT</span>
<a name="l00501"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ab35f04d2883c028bd5a5abe0d7004e06">00501</a> <a class="code" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#ab35f04d2883c028bd5a5abe0d7004e06">d_allInstCount2</a> ;
<a name="l00502"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a96b6c0364f1b8e2aa6f5156eb7bfe469">00502</a> <a class="code" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a96b6c0364f1b8e2aa6f5156eb7bfe469">d_totalInstCount</a> ;<span class="comment">// the total number of instantiations.</span>
<a name="l00503"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ab3e1ed0e8cc74fac887ded9f56a17f78">00503</a> <a class="code" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#ab3e1ed0e8cc74fac887ded9f56a17f78">d_trueInstCount</a>;<span class="comment">//the number of instantiation simplified to be true.</span>
<a name="l00504"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#aa6905effa7a717856118ed19f818e7f3">00504</a> <a class="code" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#aa6905effa7a717856118ed19f818e7f3">d_abInstCount</a>;
<a name="l00505"></a>00505
<a name="l00506"></a>00506 <span class="comment">// size_t d_totalInstCount;</span>
<a name="l00507"></a>00507 <span class="comment">// size_t d_trueInstCount;</span>
<a name="l00508"></a>00508 <span class="comment">// size_t d_abInstCount;</span>
<a name="l00509"></a>00509
<a name="l00510"></a>00510
<a name="l00511"></a>00511
<a name="l00512"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a4f00e0765ee64e22e984587a4579bde6">00512</a> std::vector<Theorem> <a class="code" href="classCVC3_1_1TheoryQuant.html#a4f00e0765ee64e22e984587a4579bde6">d_cacheTheorem</a>;
<a name="l00513"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a65a292cd648bd4af31f19ff9c7532ea4">00513</a> <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a65a292cd648bd4af31f19ff9c7532ea4">d_cacheThmPos</a>;
<a name="l00514"></a>00514
<a name="l00515"></a>00515 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#ac91bfb78e30e5f81d1d11a25a47f33b1">addNotify</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="l00516"></a>00516
<a name="l00517"></a>00517 <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a66e269df47eb8d5827b10c15937c6432">sendInstNew</a>();
<a name="l00518"></a>00518
<a name="l00519"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#aabd606d2811108af2cd562c63d9cfbdd">00519</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, std::set<std::vector<Expr></a> > > <a class="code" href="classCVC3_1_1TheoryQuant.html#aabd606d2811108af2cd562c63d9cfbdd">d_instHistory</a>;<span class="comment">//the history of instantiations</span>
<a name="l00520"></a>00520 <span class="comment">//map univ to the trig, gterm and result</span>
<a name="l00521"></a>00521
<a name="l00522"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#acb9e190ab07b49b4d1e62c4edbf75ca5">00522</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<int></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#acb9e190ab07b49b4d1e62c4edbf75ca5">d_thmCount</a>;
<a name="l00523"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a3e97f6a9759fca392443aee3d9ef0c0d">00523</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<size_t></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a3e97f6a9759fca392443aee3d9ef0c0d">d_totalThmCount</a>;
<a name="l00524"></a>00524
<a name="l00525"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ad8356f54f8d013951ebfd9480e940867">00525</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<CDMap<Expr, bool></a>* > <a class="code" href="classCVC3_1_1TheoryQuant.html#ad8356f54f8d013951ebfd9480e940867">d_bindHistory</a>; <span class="comment">//the history of instantiations</span>
<a name="l00526"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a7e78eaa04046525a5655c6b012948357">00526</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<std::hash_map<Expr, bool></a>* > <a class="code" href="classCVC3_1_1TheoryQuant.html#a7e78eaa04046525a5655c6b012948357">d_bindGlobalHistory</a>; <span class="comment">//the history of instantiations</span>
<a name="l00527"></a>00527
<a name="l00528"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a7e9807fc95db1efef6f3ac955a034f85">00528</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<std::hash_map<Expr, Theorem></a>* > <a class="code" href="classCVC3_1_1TheoryQuant.html#a7e9807fc95db1efef6f3ac955a034f85">d_bindGlobalThmHistory</a>; <span class="comment">//the history of instantiations</span>
<a name="l00529"></a>00529
<a name="l00530"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a66b101a27d3ee2d8494a6cb268e1ef8c">00530</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<std::set<std::vector<Expr></a> > > <a class="code" href="classCVC3_1_1TheoryQuant.html#a66b101a27d3ee2d8494a6cb268e1ef8c">d_instHistoryGlobal</a>;<span class="comment">//the history of instantiations</span>
<a name="l00531"></a>00531
<a name="l00532"></a>00532
<a name="l00533"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#aa05d5ab159323722c0c86f7bbbd4fa73">00533</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<std::vector<Expr></a> > <a class="code" href="classCVC3_1_1TheoryQuant.html#aa05d5ab159323722c0c86f7bbbd4fa73">d_subTermsMap</a>;
<a name="l00534"></a>00534 <span class="comment">//std::map<Expr, std::vector<Expr> > d_subTermsMap;</span>
<a name="l00535"></a>00535 <span class="keyword">const</span> std::vector<Expr>& <a class="code" href="classCVC3_1_1TheoryQuant.html#aa1e8210488cd01cfc4b36c105b0f8484">getSubTerms</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="l00536"></a>00536
<a name="l00537"></a>00537
<a name="l00538"></a>00538 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a1422df86ad2222a61bfd19e71bb36d37">simplifyExprMap</a>(<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a>& orgExprMap);
<a name="l00539"></a>00539 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a510dde7cfaa1f736d1507efb0f630622">simplifyVectorExprMap</a>(std::vector<<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> >& orgVectorExprMap);
<a name="l00540"></a>00540 std::string <a class="code" href="classCVC3_1_1TheoryQuant.html#a8592168894e51ae87e4c765ba64f5d4c">exprMap2string</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a>& vec);
<a name="l00541"></a>00541 std::string <a class="code" href="classCVC3_1_1TheoryQuant.html#a08ba0747b982df3234846c79e2c184a9">exprMap2stringSimplify</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a>& vec);
<a name="l00542"></a>00542 std::string <a class="code" href="classCVC3_1_1TheoryQuant.html#adf21f465d1b5579bd540535993f0fb3e">exprMap2stringSig</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a>& vec);
<a name="l00543"></a>00543
<a name="l00544"></a>00544 <span class="comment">//ExprMap<int > d_thmTimes; </span>
<a name="l00545"></a>00545 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a9c0b1e3cb9cdd4a69f70cc912c14d438">enqueueInst</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>);
<a name="l00546"></a>00546 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a9c0b1e3cb9cdd4a69f70cc912c14d438">enqueueInst</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& univ, <span class="keyword">const</span> std::vector<Expr>& bind, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm);
<a name="l00547"></a>00547 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a9c0b1e3cb9cdd4a69f70cc912c14d438">enqueueInst</a>(<span class="keywordtype">size_t</span> univ_id , <span class="keyword">const</span> std::vector<Expr>& bind, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm);
<a name="l00548"></a>00548 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a9c0b1e3cb9cdd4a69f70cc912c14d438">enqueueInst</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& univ,
<a name="l00549"></a>00549 <a class="code" href="classCVC3_1_1Trigger.html">Trigger</a>& trig,
<a name="l00550"></a>00550 <span class="keyword">const</span> std::vector<Expr>& binds,
<a name="l00551"></a>00551 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm
<a name="l00552"></a>00552 );
<a name="l00553"></a>00553
<a name="l00554"></a>00554 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a52ca7d3454b8359a1aee518b57f9720a">synCheckSat</a>(<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a><<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a><std::vector<dynTrig>* >* >& , <span class="keywordtype">bool</span>);
<a name="l00555"></a>00555 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a52ca7d3454b8359a1aee518b57f9720a">synCheckSat</a>(<span class="keywordtype">bool</span>);
<a name="l00556"></a>00556 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#afe19c7bd637cb0c5fad7ab0494135010">semCheckSat</a>(<span class="keywordtype">bool</span>);
<a name="l00557"></a>00557 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a8ccfdf955d67688e51dc9bcbb3911a2d">naiveCheckSat</a>(<span class="keywordtype">bool</span>);
<a name="l00558"></a>00558
<a name="l00559"></a>00559 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a02124fe37089a15098eddb145fef3541">insted</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> & univ, <span class="keyword">const</span> std::vector<Expr>& binds);
<a name="l00560"></a>00560 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a1e1906aefb76bb94539706422769ca56">synInst</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> & univ, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allterms, <span class="keywordtype">size_t</span> tBegin);
<a name="l00561"></a>00561
<a name="l00562"></a>00562 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a7db6cfe00994c2a42281569e9adb464a">synFullInst</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> & univ, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allterms, <span class="keywordtype">size_t</span> tBegin);
<a name="l00563"></a>00563
<a name="l00564"></a>00564 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a99d04925b72f6f7219bb759ef05a88e6">arrayHeuristic</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Trigger.html">Trigger</a>& trig, <span class="keywordtype">size_t</span> univid);
<a name="l00565"></a>00565
<a name="l00566"></a>00566 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#ad3380307e5e4a152e9cbd4595931dc3a">simpRAWList</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& org);
<a name="l00567"></a>00567
<a name="l00568"></a>00568 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#ae568ecab36a477db5114c8f7a53e3755">synNewInst</a>(<span class="keywordtype">size_t</span> univ_id, <span class="keyword">const</span> std::vector<Expr>& binds, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Trigger.html">Trigger</a>& trig );
<a name="l00569"></a>00569 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a49dcf36058067da8bb3746c6c675e586">synMultInst</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> & univ, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allterms, <span class="keywordtype">size_t</span> tBegin);
<a name="l00570"></a>00570
<a name="l00571"></a>00571 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a98757263b2fee18abdf1455940ac591a">synPartInst</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> & univ, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allterms, <span class="keywordtype">size_t</span> tBegin);
<a name="l00572"></a>00572
<a name="l00573"></a>00573 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a4d6102e7b0c820e32c1488da4b19e140">semInst</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> & univ, <span class="keywordtype">size_t</span> tBegin);
<a name="l00574"></a>00574
<a name="l00575"></a>00575
<a name="l00576"></a>00576 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a068a9d83c75c80f1cb92104570bb1bac">goodSynMatch</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="l00577"></a>00577 <span class="keyword">const</span> std::vector<Expr> & boundVars,
<a name="l00578"></a>00578 std::vector<std::vector<Expr> >& instBindsTerm,
<a name="l00579"></a>00579 std::vector<Expr>& instGterm,
<a name="l00580"></a>00580 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allterms,
<a name="l00581"></a>00581 <span class="keywordtype">size_t</span> tBegin);
<a name="l00582"></a>00582 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a9efbf461e32e3c55fb05c8828f1ccac7">goodSynMatchNewTrig</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Trigger.html">Trigger</a>& trig,
<a name="l00583"></a>00583 <span class="keyword">const</span> std::vector<Expr> & boundVars,
<a name="l00584"></a>00584 std::vector<std::vector<Expr> >& instBinds,
<a name="l00585"></a>00585 std::vector<Expr>& instGterms,
<a name="l00586"></a>00586 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allterms,
<a name="l00587"></a>00587 <span class="keywordtype">size_t</span> tBegin);
<a name="l00588"></a>00588
<a name="l00589"></a>00589 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a9efbf461e32e3c55fb05c8828f1ccac7">goodSynMatchNewTrig</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Trigger.html">Trigger</a>& trig,
<a name="l00590"></a>00590 <span class="keyword">const</span> std::vector<Expr> & boundVars,
<a name="l00591"></a>00591 std::vector<std::vector<Expr> >& instBinds,
<a name="l00592"></a>00592 std::vector<Expr>& instGterms,
<a name="l00593"></a>00593 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm);
<a name="l00594"></a>00594
<a name="l00595"></a>00595 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a7aa91c8e11e7d0058082d1be9e5cb851">matchListOld</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& list, <span class="keywordtype">size_t</span> gbegin, <span class="keywordtype">size_t</span> gend);
<a name="l00596"></a>00596 <span class="comment">// void matchListOld(const Expr& gterm);</span>
<a name="l00597"></a>00597 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a8631dcdf3e42b922ea500115b2f70629">matchListNew</a>(<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a><<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a><std::vector<dynTrig>*>*>& new_trigs,
<a name="l00598"></a>00598 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& list,
<a name="l00599"></a>00599 <span class="keywordtype">size_t</span> gbegin,
<a name="l00600"></a>00600 <span class="keywordtype">size_t</span> gend);
<a name="l00601"></a>00601
<a name="l00602"></a>00602 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a7cefd1998194a1bfb4025c51202f3a33">delNewTrigs</a>(<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a><<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a><std::vector<dynTrig>*>*>& new_trigs);
<a name="l00603"></a>00603 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a211c3255d97a25eb0041ec8738d78a53">combineOldNewTrigs</a>(<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a><<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a><std::vector<dynTrig>*>*>& new_trigs);
<a name="l00604"></a>00604
<a name="l00605"></a>00605 <span class="keyword">inline</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#af1a7155ec3ea39cc6416e5889a6b06dc">add_parent</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#a1e31c3827dae4bdfeeb6430c5c0f48b4">parent</a>);
<a name="l00606"></a>00606
<a name="l00607"></a>00607 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a9f44d577beb7d01fa993ec72c8e144b9">newTopMatch</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm,
<a name="l00608"></a>00608 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& vterm,
<a name="l00609"></a>00609 std::vector<<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> >& binds,
<a name="l00610"></a>00610 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Trigger.html">Trigger</a>& trig);
<a name="l00611"></a>00611
<a name="l00612"></a>00612 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#abf931ce810d553219994f72b7098a5d0">newTopMatchSig</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm,
<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>& vterm,
<a name="l00614"></a>00614 std::vector<<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> >& binds,
<a name="l00615"></a>00615 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Trigger.html">Trigger</a>& trig);
<a name="l00616"></a>00616
<a name="l00617"></a>00617 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a663ab694805834cbb8af2e3e1c0a07b0">newTopMatchNoSig</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm,
<a name="l00618"></a>00618 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& vterm,
<a name="l00619"></a>00619 std::vector<<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> >& binds,
<a name="l00620"></a>00620 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Trigger.html">Trigger</a>& trig);
<a name="l00621"></a>00621
<a name="l00622"></a>00622
<a name="l00623"></a>00623
<a name="l00624"></a>00624 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#adbebf5bb207253848504a3711ddab1c9">newTopMatchBackupOnly</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm,
<a name="l00625"></a>00625 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& vterm,
<a name="l00626"></a>00626 std::vector<<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> >& binds,
<a name="l00627"></a>00627 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Trigger.html">Trigger</a>& trig);
<a name="l00628"></a>00628
<a name="l00629"></a>00629
<a name="l00630"></a>00630 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#abe90a3995031ac7ab9e020be4bf828a2">synMatchTopPred</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Trigger.html">Trigger</a> trig, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a>& env);
<a name="l00631"></a>00631
<a name="l00632"></a>00632 <span class="comment">// inline bool matchChild(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env);</span>
<a name="l00633"></a>00633 <span class="comment">// inline void matchChild(const Expr& gterm, const Expr& vterm, std::vector<ExprMap<Expr> >& env);</span>
<a name="l00634"></a>00634
<a name="l00635"></a>00635 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a33dfaf67440a78f618a6c379fd884330">recSynMatch</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& vterm, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a>& env);
<a name="l00636"></a>00636
<a name="l00637"></a>00637 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#aede3f8a2e1b235a5cafde5f62a3356cf">recMultMatch</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm,<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& vterm, std::vector<<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> >& binds);
<a name="l00638"></a>00638 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a6105760e18793163cafd935f92214b57">recMultMatchDebug</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm,<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& vterm, std::vector<<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> >& binds);
<a name="l00639"></a>00639 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a017c02318b460823b9e5e63b8b72a14f">recMultMatchNewWay</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm,<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& vterm, std::vector<<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> >& binds);
<a name="l00640"></a>00640 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a22391b53ffa8331b754fb7ad85b58ec0">recMultMatchOldWay</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm,<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& vterm, std::vector<<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> >& binds);
<a name="l00641"></a>00641
<a name="l00642"></a>00642 <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#addac94f519d0c54d739281e72989a669">multMatchChild</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& vterm, std::vector<<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> >& binds, <span class="keywordtype">bool</span> top=<span class="keyword">false</span>);
<a name="l00643"></a>00643 <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a036828f1d240572e4a37e22af4d79d06">multMatchTop</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& vterm, std::vector<<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> >& binds);
<a name="l00644"></a>00644
<a name="l00645"></a>00645
<a name="l00646"></a>00646 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#ad2e8ad874c79cb5300302d30b6475b7b">recSynMatchBackupOnly</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& vterm, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a>& env);
<a name="l00647"></a>00647
<a name="l00648"></a>00648 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a0529a0896f101fc28d0bda6a06a30017">hasGoodSynInstNewTrigOld</a>(<a class="code" href="classCVC3_1_1Trigger.html">Trigger</a>& trig,
<a name="l00649"></a>00649 std::vector<Expr> & boundVars,
<a name="l00650"></a>00650 std::vector<std::vector<Expr> >& instBinds,
<a name="l00651"></a>00651 std::vector<Expr>& instGterms,
<a name="l00652"></a>00652 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allterms,
<a name="l00653"></a>00653 <span class="keywordtype">size_t</span> tBegin);
<a name="l00654"></a>00654
<a name="l00655"></a>00655 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a32914adfab6f1127e54e77789507f7e2">hasGoodSynInstNewTrig</a>(<a class="code" href="classCVC3_1_1Trigger.html">Trigger</a>& trig,
<a name="l00656"></a>00656 <span class="keyword">const</span> std::vector<Expr> & boundVars,
<a name="l00657"></a>00657 std::vector<std::vector<Expr> >& instBinds,
<a name="l00658"></a>00658 std::vector<Expr>& instGterms,
<a name="l00659"></a>00659 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allterms,
<a name="l00660"></a>00660 <span class="keywordtype">size_t</span> tBegin);
<a name="l00661"></a>00661
<a name="l00662"></a>00662
<a name="l00663"></a>00663 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a133000dab6d34bc6686aa55b67a7820a">hasGoodSynMultiInst</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="l00664"></a>00664 std::vector<Expr>& bVars,
<a name="l00665"></a>00665 std::vector<std::vector<Expr> >& instSet,
<a name="l00666"></a>00666 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allterms,
<a name="l00667"></a>00667 <span class="keywordtype">size_t</span> tBegin);
<a name="l00668"></a>00668
<a name="l00669"></a>00669 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a8e4d77afeb2cf976688bc923b3c7b3d4">recGoodSemMatch</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="l00670"></a>00670 <span class="keyword">const</span> std::vector<Expr>& bVars,
<a name="l00671"></a>00671 std::vector<Expr>& newInst,
<a name="l00672"></a>00672 std::set<std::vector<Expr> >& instSet);
<a name="l00673"></a>00673
<a name="l00674"></a>00674 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#acd5769f981e6fbefb01c35459836682f">hasGoodSemInst</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="l00675"></a>00675 std::vector<Expr>& bVars,
<a name="l00676"></a>00676 std::set<std::vector<Expr> >& instSet,
<a name="l00677"></a>00677 <span class="keywordtype">size_t</span> tBegin);
<a name="l00678"></a>00678
<a name="l00679"></a>00679 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a243490ead7aaf5a0a311076661f783d1">isTransLike</a> (<span class="keyword">const</span> std::vector<Expr>& cur_trig);
<a name="l00680"></a>00680 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#aa837ec5c9ce0d4363fbb47eade316008">isTrans2Like</a> (<span class="keyword">const</span> std::vector<Expr>& all_terms, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& tr2);
<a name="l00681"></a>00681
<a name="l00682"></a>00682
<a name="l00683"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#aa7c01b86ccf4a315711e7d09c47c71cd">00683</a> <span class="keyword">static</span> <span class="keyword">const</span> <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#aa7c01b86ccf4a315711e7d09c47c71cd">MAX_TRIG_BVS</a>=15;
<a name="l00684"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#af51bfd58e92b284832770c68c1685ab6">00684</a> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#af51bfd58e92b284832770c68c1685ab6">d_mybvs</a>[<a class="code" href="classCVC3_1_1TheoryQuant.html#aa7c01b86ccf4a315711e7d09c47c71cd">MAX_TRIG_BVS</a>];
<a name="l00685"></a>00685
<a name="l00686"></a>00686 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a6177e4b547322f04e6ff282521120a37">recGeneralTrig</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& trig, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a>& bvs, <span class="keywordtype">size_t</span>& mybvs_count);
<a name="l00687"></a>00687 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a14f9823bc4dbe53b96c895bafa71df1a">generalTrig</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& trig, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a>& bvs);
<a name="l00688"></a>00688
<a name="l00689"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#ac1dc98cab588b291d74859884fc25f5e">00689</a> <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<CDMap<Expr, CDList<dynTrig></a>* >* > <a class="code" href="classCVC3_1_1TheoryQuant.html#ac1dc98cab588b291d74859884fc25f5e">d_allmap_trigs</a>;
<a name="l00690"></a>00690
<a name="l00691"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#a0dd41bdd27bbd7c71fc45749fb80ff96">00691</a> <a class="code" href="classCVC3_1_1CDList.html">CDList<Trigger></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a0dd41bdd27bbd7c71fc45749fb80ff96">d_alltrig_list</a>;
<a name="l00692"></a>00692
<a name="l00693"></a>00693 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#ad7f534d41a6c648eb5fbad4bbc1c92a1">registerTrig</a>(<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a><<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a><std::vector<dynTrig>* >* >& cur_trig_map,
<a name="l00694"></a>00694 <a class="code" href="classCVC3_1_1Trigger.html">Trigger</a> trig,
<a name="l00695"></a>00695 <span class="keyword">const</span> std::vector<Expr> thmBVs,
<a name="l00696"></a>00696 <span class="keywordtype">size_t</span> univ_id);
<a name="l00697"></a>00697
<a name="l00698"></a>00698 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#ad9323b081878d5b80294cd48b68dd8a1">registerTrigReal</a>(<a class="code" href="classCVC3_1_1Trigger.html">Trigger</a> trig, <span class="keyword">const</span> std::vector<Expr>, <span class="keywordtype">size_t</span> univ_id);
<a name="l00699"></a>00699
<a name="l00700"></a>00700 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a8cfa16216ec725f8b63ce5071c311b37">canMatch</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a>& env);
<a name="l00701"></a>00701 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a108c813a9b45447451b2230e9ad26801">setGround</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& trig, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& univ, <span class="keyword">const</span> std::vector<Expr>& subTerms) ;
<a name="l00702"></a>00702
<a name="l00703"></a>00703 <span class="comment">// std::string getHead(const Expr& e) ;</span>
<a name="l00704"></a>00704 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a892fb1c6479c80fe7cab50a156d04b97">setupTriggers</a>(<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a><<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap</a><std::vector<dynTrig>* >*>& trig_maps,
<a name="l00705"></a>00705 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm,
<a name="l00706"></a>00706 <span class="keywordtype">size_t</span> univs_id);
<a name="l00707"></a>00707
<a name="l00708"></a>00708 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a3417f85c140e902187726b52a4628966">saveContext</a>();
<a name="l00709"></a>00709
<a name="l00710"></a>00710 <span class="comment"></span>
<a name="l00711"></a>00711 <span class="comment"> /*! \brief categorizes all the terms contained in an expressions by</span>
<a name="l00712"></a>00712 <span class="comment"> *type.</span>
<a name="l00713"></a>00713 <span class="comment"> *</span>
<a name="l00714"></a>00714 <span class="comment"> * Updates d_contextTerms, d_contextMap, d_contextCache accordingly.</span>
<a name="l00715"></a>00715 <span class="comment"> * returns true if the expression does not contain bound variables, false</span>
<a name="l00716"></a>00716 <span class="comment"> * otherwise.</span>
<a name="l00717"></a>00717 <span class="comment"> */</span>
<a name="l00718"></a>00718
<a name="l00719"></a>00719
<a name="l00720"></a>00720 <span class="keyword">public</span>:
<a name="l00721"></a>00721 <a class="code" href="classCVC3_1_1TheoryQuant.html#aa78a307b46795fba7cd31d7459f5af4e" title="categorizes all the terms contained in an expressions by type.">TheoryQuant</a>(<a class="code" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">TheoryCore</a>* core); <span class="comment">//!< Constructor</span>
<a name="l00722"></a>00722 <span class="comment"></span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a653f0e36db9a5c07024565e77d01abb0" title="Destructor.">~TheoryQuant</a>(); <span class="comment">//! Destructor</span>
<a name="l00723"></a>00723 <span class="comment"></span>
<a name="l00724"></a>00724 <a class="code" href="classCVC3_1_1QuantProofRules.html">QuantProofRules</a>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a493eb80061815c95bab507f41343b260" title="Destructor.">createProofRules</a>();
<a name="l00725"></a>00725
<a name="l00726"></a>00726
<a name="l00727"></a>00727
<a name="l00728"></a><a class="code" href="classCVC3_1_1TheoryQuant.html#aae3f95b1c6505b090105271bbccd7408">00728</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#aae3f95b1c6505b090105271bbccd7408" title="Theory interface.">addSharedTerm</a>(<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="comment">//!< Theory interface</span>
<a name="l00729"></a>00729 <span class="comment"></span> <span class="comment"></span>
<a name="l00730"></a>00730 <span class="comment"> /*! \brief Theory interface function to assert quantified formulas</span>
<a name="l00731"></a>00731 <span class="comment"> *</span>
<a name="l00732"></a>00732 <span class="comment"> * pushes in negations and converts to either universally or existentially </span>
<a name="l00733"></a>00733 <span class="comment"> * quantified theorems. Universals are stored in a database while </span>
<a name="l00734"></a>00734 <span class="comment"> * existentials are enqueued to be handled by the search engine.</span>
<a name="l00735"></a>00735 <span class="comment"> */</span>
<a name="l00736"></a>00736 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a98ceeca1859a3d4b0c01fc85a3f610ea" title="Theory interface function to assert quantified formulas.">assertFact</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e);
<a name="l00737"></a>00737
<a name="l00738"></a>00738
<a name="l00739"></a>00739 <span class="comment">/* \brief Checks the satisfiability of the universal theorems stored in a </span>
<a name="l00740"></a>00740 <span class="comment"> * databse by instantiating them.</span>
<a name="l00741"></a>00741 <span class="comment"> *</span>
<a name="l00742"></a>00742 <span class="comment"> * There are two algorithms that the checkSat function uses to find </span>
<a name="l00743"></a>00743 <span class="comment"> * instnatiations. The first algortihm looks for instanitations in a saved </span>
<a name="l00744"></a>00744 <span class="comment"> * database of previous instantiations that worked in proving an earlier</span>
<a name="l00745"></a>00745 <span class="comment"> * theorem unsatifiable. All of the class variables with the word saved in</span>
<a name="l00746"></a>00746 <span class="comment"> * them are for the use of this algorithm. The other algorithm uses terms </span>
<a name="l00747"></a>00747 <span class="comment"> * found in the assertions that exist in the particular context when </span>
<a name="l00748"></a>00748 <span class="comment"> * checkSat is called. All of the class variables with the word context in</span>
<a name="l00749"></a>00749 <span class="comment"> * them are used for the second algorithm.</span>
<a name="l00750"></a>00750 <span class="comment"> */</span>
<a name="l00751"></a>00751 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#af8346007d3494f2c89687e8b14dc86a3" title="Check for satisfiability in the theory.">checkSat</a>(<span class="keywordtype">bool</span> fullEffort);
<a name="l00752"></a>00752 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a8669c171bcd467dc782f4268093cab11" title="Set up the term e for call-backs when e or its children change.">setup</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="l00753"></a>00753
<a name="l00754"></a>00754 <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#aa3dcc4288e4738de508875ecccbe32eb">help</a>(<span class="keywordtype">int</span> i);
<a name="l00755"></a>00755
<a name="l00756"></a>00756 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a03756dc7d7ff3b399cae1c98140eccb8" title="Notify a theory of a new equality.">update</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& e, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& d);<span class="comment"></span>
<a name="l00757"></a>00757 <span class="comment"> /*!\brief Used to notify the quantifier algorithm of possible </span>
<a name="l00758"></a>00758 <span class="comment"> * instantiations that were used in proving a context inconsistent.</span>
<a name="l00759"></a>00759 <span class="comment"> */</span>
<a name="l00760"></a>00760 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a915c35bc6dedbc7827f8800fa9d2ac44" title="Used to notify the quantifier algorithm of possible instantiations that were used in proving a contex...">debug</a>(<span class="keywordtype">int</span> i);
<a name="l00761"></a>00761 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#acfc01954af4379d6ee3917afbdb73612" title="Used to notify the quantifier algorithm of possible instantiations that were used in proving a contex...">notifyInconsistent</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm); <span class="comment"></span>
<a name="l00762"></a>00762 <span class="comment"> //! computes the type of a quantified term. Always a boolean.</span>
<a name="l00763"></a>00763 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#aa48359564f5cfda755d46d1aed992dc8" title="computes the type of a quantified term. Always a boolean.">computeType</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="l00764"></a>00764 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#ac702ce1fbdd3fee29f4b1c8868579276">computeTCC</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="l00765"></a>00765
<a name="l00766"></a>00766 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a4ddfed955f288872e94794075f019c9f" title="Theory-specific parsing implemented by the DP.">parseExprOp</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="l00767"></a>00767
<a name="l00768"></a>00768 <a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& <a class="code" href="classCVC3_1_1TheoryQuant.html#aa0c1c26775ebf349dbaa34e7a0dfc268" title="Theory-specific pretty-printing.">print</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os, <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="l00769"></a>00769 };
<a name="l00770"></a>00770
<a name="l00771"></a>00771 }
<a name="l00772"></a>00772
<a name="l00773"></a>00773 <span class="preprocessor">#endif</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>
