<!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"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: theory_quant.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<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 id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="dir_68267d1309a1af8e8297ef4c3efbcdba.html">src</a></li><li class="navelem"><a class="el" href="dir_b0856f6b0d80ccb263b2f415c91f9e17.html">include</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">theory_quant.h</div> </div>
</div><!--header-->
<div class="contents">
<a href="theory__quant_8h.html">Go to the documentation of this file.</a><div class="fragment"><div class="line"><a name="l00001"></a><span class="lineno"> 1</span> <span class="comment">/*****************************************************************************/</span><span class="comment"></span></div>
<div class="line"><a name="l00002"></a><span class="lineno"> 2</span> <span class="comment">/*!</span></div>
<div class="line"><a name="l00003"></a><span class="lineno"> 3</span> <span class="comment"> * \file theory_quant.h</span></div>
<div class="line"><a name="l00004"></a><span class="lineno"> 4</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00005"></a><span class="lineno"> 5</span> <span class="comment"> * Author: Sergey Berezin, Yeting Ge</span></div>
<div class="line"><a name="l00006"></a><span class="lineno"> 6</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00007"></a><span class="lineno"> 7</span> <span class="comment"> * Created: Jun 24 21:13:59 GMT 2003</span></div>
<div class="line"><a name="l00008"></a><span class="lineno"> 8</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00009"></a><span class="lineno"> 9</span> <span class="comment"> * <hr></span></div>
<div class="line"><a name="l00010"></a><span class="lineno"> 10</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00011"></a><span class="lineno"> 11</span> <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span></div>
<div class="line"><a name="l00012"></a><span class="lineno"> 12</span> <span class="comment"> * and its documentation for any purpose is hereby granted without</span></div>
<div class="line"><a name="l00013"></a><span class="lineno"> 13</span> <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span></div>
<div class="line"><a name="l00014"></a><span class="lineno"> 14</span> <span class="comment"> * LICENSE file provided with this distribution.</span></div>
<div class="line"><a name="l00015"></a><span class="lineno"> 15</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00016"></a><span class="lineno"> 16</span> <span class="comment"> * <hr></span></div>
<div class="line"><a name="l00017"></a><span class="lineno"> 17</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00018"></a><span class="lineno"> 18</span> <span class="comment"> * ! Author: Daniel Wichs</span></div>
<div class="line"><a name="l00019"></a><span class="lineno"> 19</span> <span class="comment"> * ! Created: Wednesday July 2, 2003</span></div>
<div class="line"><a name="l00020"></a><span class="lineno"> 20</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00021"></a><span class="lineno"> 21</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00022"></a><span class="lineno"> 22</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00023"></a><span class="lineno"> 23</span> <span class="comment">/*****************************************************************************/</span></div>
<div class="line"><a name="l00024"></a><span class="lineno"> 24</span> <span class="preprocessor">#ifndef _cvc3__include__theory_quant_h_</span></div>
<div class="line"><a name="l00025"></a><span class="lineno"> 25</span> <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__theory_quant_h_</span></div>
<div class="line"><a name="l00026"></a><span class="lineno"> 26</span> <span class="preprocessor"></span></div>
<div class="line"><a name="l00027"></a><span class="lineno"> 27</span> <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></div>
<div class="line"><a name="l00028"></a><span class="lineno"> 28</span> <span class="preprocessor">#include "<a class="code" href="cdmap_8h.html">cdmap.h</a>"</span></div>
<div class="line"><a name="l00029"></a><span class="lineno"> 29</span> <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></div>
<div class="line"><a name="l00030"></a><span class="lineno"> 30</span> <span class="preprocessor">#include<queue></span></div>
<div class="line"><a name="l00031"></a><span class="lineno"> 31</span> </div>
<div class="line"><a name="l00032"></a><span class="lineno"> 32</span> <span class="keyword">namespace </span>CVC3 {</div>
<div class="line"><a name="l00033"></a><span class="lineno"> 33</span> </div>
<div class="line"><a name="l00034"></a><span class="lineno"> 34</span> <span class="keyword">class </span>QuantProofRules;</div>
<div class="line"><a name="l00035"></a><span class="lineno"> 35</span> </div>
<div class="line"><a name="l00036"></a><span class="lineno"> 36</span> <span class="comment">/*****************************************************************************/</span><span class="comment"></span></div>
<div class="line"><a name="l00037"></a><span class="lineno"> 37</span> <span class="comment">/*!</span></div>
<div class="line"><a name="l00038"></a><span class="lineno"> 38</span> <span class="comment"> *\class TheoryQuant</span></div>
<div class="line"><a name="l00039"></a><span class="lineno"> 39</span> <span class="comment"> *\ingroup Theories</span></div>
<div class="line"><a name="l00040"></a><span class="lineno"> 40</span> <span class="comment"> *\brief This theory handles quantifiers.</span></div>
<div class="line"><a name="l00041"></a><span class="lineno"> 41</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00042"></a><span class="lineno"> 42</span> <span class="comment"> * Author: Daniel Wichs</span></div>
<div class="line"><a name="l00043"></a><span class="lineno"> 43</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00044"></a><span class="lineno"> 44</span> <span class="comment"> * Created: Wednesday July 2, 2003</span></div>
<div class="line"><a name="l00045"></a><span class="lineno"> 45</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00046"></a><span class="lineno"> 46</span> <span class="comment">/*****************************************************************************/</span></div>
<div class="line"><a name="l00047"></a><span class="lineno"> 47</span> </div>
<div class="line"><a name="l00048"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#aa6262a73c1109f35a6c533421f5dd393aa36f330d6c384df84029d036339d875e"> 48</a></span>  <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>;</div>
<div class="line"><a name="l00049"></a><span class="lineno"> 49</span> </div>
<div class="line"><a name="l00050"></a><span class="lineno"><a class="code" href="classCVC3_1_1Trigger.html"> 50</a></span>  <span class="keyword">class </span><a class="code" href="classCVC3_1_1Trigger.html">Trigger</a> {</div>
<div class="line"><a name="l00051"></a><span class="lineno"> 51</span>  <span class="keyword">public</span>: </div>
<div class="line"><a name="l00052"></a><span class="lineno"><a class="code" href="classCVC3_1_1Trigger.html#a4e021ea47393a20e2a5ed518547b6cc5"> 52</a></span>  <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>;</div>
<div class="line"><a name="l00053"></a><span class="lineno"><a class="code" href="classCVC3_1_1Trigger.html#a072357cd5b19a3c255274a10c2e65ae1"> 53</a></span>  <a class="code" href="namespaceCVC3.html#aa6262a73c1109f35a6c533421f5dd393">Polarity</a> <a class="code" href="classCVC3_1_1Trigger.html#a072357cd5b19a3c255274a10c2e65ae1">polarity</a>;</div>
<div class="line"><a name="l00054"></a><span class="lineno"> 54</span>  </div>
<div class="line"><a name="l00055"></a><span class="lineno"><a class="code" href="classCVC3_1_1Trigger.html#a0316ac0451c9906e1ffa14269bca4822"> 55</a></span>  std::vector<Expr> <a class="code" href="classCVC3_1_1Trigger.html#a0316ac0451c9906e1ffa14269bca4822">bvs</a>;</div>
<div class="line"><a name="l00056"></a><span class="lineno"><a class="code" href="classCVC3_1_1Trigger.html#a872b399bef4cb0181eef18c043dcf7c0"> 56</a></span>  <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>;</div>
<div class="line"><a name="l00057"></a><span class="lineno"><a class="code" href="classCVC3_1_1Trigger.html#a1b9f95a061179c63bb5c4a6572525149"> 57</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#a1b9f95a061179c63bb5c4a6572525149">hasRWOp</a>;</div>
<div class="line"><a name="l00058"></a><span class="lineno"><a class="code" href="classCVC3_1_1Trigger.html#ad27afc7a2fc903e53a03ab91a91ab2bb"> 58</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#ad27afc7a2fc903e53a03ab91a91ab2bb">hasTrans</a>;</div>
<div class="line"><a name="l00059"></a><span class="lineno"><a class="code" href="classCVC3_1_1Trigger.html#a164f72606a374f8bf9b1a86394df8e5a"> 59</a></span>  <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></div>
<div class="line"><a name="l00060"></a><span class="lineno"><a class="code" href="classCVC3_1_1Trigger.html#a91aa68f794175b4a3d587bc735d90db1"> 60</a></span>  <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></div>
<div class="line"><a name="l00061"></a><span class="lineno"><a class="code" href="classCVC3_1_1Trigger.html#a1da964c1eddeeca162f2ad07084a519a"> 61</a></span>  <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></div>
<div class="line"><a name="l00062"></a><span class="lineno"><a class="code" href="classCVC3_1_1Trigger.html#a263a81925c4e496b2db59a5c46c716da"> 62</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#a263a81925c4e496b2db59a5c46c716da">isMulti</a>;</div>
<div class="line"><a name="l00063"></a><span class="lineno"><a class="code" href="classCVC3_1_1Trigger.html#a7030f34d847ed61e24838c23b12e33f1"> 63</a></span>  <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1Trigger.html#a7030f34d847ed61e24838c23b12e33f1">multiIndex</a>; </div>
<div class="line"><a name="l00064"></a><span class="lineno"><a class="code" href="classCVC3_1_1Trigger.html#aca45e27343e0e829d3515bb5e5614811"> 64</a></span>  <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1Trigger.html#aca45e27343e0e829d3515bb5e5614811">multiId</a>;</div>
<div class="line"><a name="l00065"></a><span class="lineno"> 65</span> </div>
<div class="line"><a name="l00066"></a><span class="lineno"> 66</span>  <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>);</div>
<div class="line"><a name="l00067"></a><span class="lineno"> 67</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#aa5a20c74a358c4c9a83cf9f92f6e32da">isPos</a>();</div>
<div class="line"><a name="l00068"></a><span class="lineno"> 68</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#ab6de8624e192483eca4c6af43ccdf0ae">isNeg</a>();</div>
<div class="line"><a name="l00069"></a><span class="lineno"> 69</span>  <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>();</div>
<div class="line"><a name="l00070"></a><span class="lineno"> 70</span>  std::vector<Expr> <a class="code" href="classCVC3_1_1Trigger.html#af93f5d8aab866ffa559363feedcd50e3">getBVs</a>(); </div>
<div class="line"><a name="l00071"></a><span class="lineno"> 71</span>  <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);</div>
<div class="line"><a name="l00072"></a><span class="lineno"> 72</span>  <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>();</div>
<div class="line"><a name="l00073"></a><span class="lineno"> 73</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Trigger.html#a8dc23a790de84038e254b3b1677405f1">setRWOp</a>(<span class="keywordtype">bool</span> b);</div>
<div class="line"><a name="l00074"></a><span class="lineno"> 74</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#aba631f56bfe8dac2b9833e4e692e6333">hasRW</a>(); </div>
<div class="line"><a name="l00075"></a><span class="lineno"> 75</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Trigger.html#ab28f10324850f03d8dd2d711d2084d42">setTrans</a>(<span class="keywordtype">bool</span> b);</div>
<div class="line"><a name="l00076"></a><span class="lineno"> 76</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#a0302d9d47d4c5ca8f19796e4848f458d">hasTr</a>(); </div>
<div class="line"><a name="l00077"></a><span class="lineno"> 77</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Trigger.html#a677feb42871ff81f92c5070b455f4692">setTrans2</a>(<span class="keywordtype">bool</span> b);</div>
<div class="line"><a name="l00078"></a><span class="lineno"> 78</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#aefbd02bbe97a369587ef7dcb07521adb">hasTr2</a>(); </div>
<div class="line"><a name="l00079"></a><span class="lineno"> 79</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Trigger.html#a3340abe4247b968ae8c2d6d76dbdad7a">setSimp</a>();</div>
<div class="line"><a name="l00080"></a><span class="lineno"> 80</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#a7fd4df8cdf6f965b6560a7859d3e3cfb">isSimp</a>(); </div>
<div class="line"><a name="l00081"></a><span class="lineno"> 81</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Trigger.html#ac49043dc15a503a32759cf4538809e6e">setSuperSimp</a>();</div>
<div class="line"><a name="l00082"></a><span class="lineno"> 82</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#a010f25f800a4abf9bbf242886f7d790b">isSuperSimp</a>(); </div>
<div class="line"><a name="l00083"></a><span class="lineno"> 83</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Trigger.html#ab86a9c01de2cf98869b3952d823603aa">setMultiTrig</a>();</div>
<div class="line"><a name="l00084"></a><span class="lineno"> 84</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Trigger.html#a5fcf09b60025ebbfe31d5b659312681d">isMultiTrig</a>(); </div>
<div class="line"><a name="l00085"></a><span class="lineno"> 85</span> </div>
<div class="line"><a name="l00086"></a><span class="lineno"> 86</span>  </div>
<div class="line"><a name="l00087"></a><span class="lineno"> 87</span>  };</div>
<div class="line"><a name="l00088"></a><span class="lineno"> 88</span> </div>
<div class="line"><a name="l00089"></a><span class="lineno"><a class="code" href="structCVC3_1_1dynTrig.html"> 89</a></span>  <span class="keyword">typedef</span> <span class="keyword">struct </span><a class="code" href="structCVC3_1_1dynTrig.html">dynTrig</a>{</div>
<div class="line"><a name="l00090"></a><span class="lineno"><a class="code" href="structCVC3_1_1dynTrig.html#ab9c6198f3d1bbe415ff1a92ccb1c760c"> 90</a></span>  <a class="code" href="classCVC3_1_1Trigger.html">Trigger</a> <a class="code" href="structCVC3_1_1dynTrig.html#ab9c6198f3d1bbe415ff1a92ccb1c760c">trig</a>;</div>
<div class="line"><a name="l00091"></a><span class="lineno"><a class="code" href="structCVC3_1_1dynTrig.html#ab8473d4aa20bfbcb9120043818cd319f"> 91</a></span>  <span class="keywordtype">size_t</span> <a class="code" href="structCVC3_1_1dynTrig.html#ab8473d4aa20bfbcb9120043818cd319f">univ_id</a>;</div>
<div class="line"><a name="l00092"></a><span class="lineno"><a class="code" href="structCVC3_1_1dynTrig.html#a724a541dbe2ffe257a30b5931c786d4a"> 92</a></span>  <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> <a class="code" href="structCVC3_1_1dynTrig.html#a724a541dbe2ffe257a30b5931c786d4a">binds</a>;</div>
<div class="line"><a name="l00093"></a><span class="lineno"> 93</span>  <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>);</div>
<div class="line"><a name="l00094"></a><span class="lineno"> 94</span>  } <a class="code" href="namespaceCVC3.html#adbf44ec4d7f9e553da5d876964266546">dynTrig</a>;</div>
<div class="line"><a name="l00095"></a><span class="lineno"> 95</span>  </div>
<div class="line"><a name="l00096"></a><span class="lineno"> 96</span> </div>
<div class="line"><a name="l00097"></a><span class="lineno"><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html"> 97</a></span>  <span class="keyword">class </span><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html">CompleteInstPreProcessor</a> {</div>
<div class="line"><a name="l00098"></a><span class="lineno"> 98</span>  </div>
<div class="line"><a name="l00099"></a><span class="lineno"><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#ad41c79afe0059463b226d9a60cd9d39d"> 99</a></span>  <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></div>
<div class="line"><a name="l00100"></a><span class="lineno"><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a135b1e372b6f3a33941c6fa2ecc93d3e"> 100</a></span>  <a class="code" href="classCVC3_1_1QuantProofRules.html">QuantProofRules</a>* <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a135b1e372b6f3a33941c6fa2ecc93d3e">d_quant_rules</a>;</div>
<div class="line"><a name="l00101"></a><span class="lineno"> 101</span> </div>
<div class="line"><a name="l00102"></a><span class="lineno"><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a3837998b3df09387a2a162258ef6b2db"> 102</a></span>  std::set<Expr> <a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a3837998b3df09387a2a162258ef6b2db">d_allIndex</a>; <span class="comment">//a set contains all index</span></div>
<div class="line"><a name="l00103"></a><span class="lineno"> 103</span> </div>
<div class="line"><a name="l00104"></a><span class="lineno"><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#af4ab970a26f5f10316e10b88cd88f5ed"> 104</a></span>  <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></div>
<div class="line"><a name="l00105"></a><span class="lineno"> 105</span> </div>
<div class="line"><a name="l00106"></a><span class="lineno"><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a8c3444e4e7e06812e1823c4b0d323034"> 106</a></span>  <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></div>
<div class="line"><a name="l00107"></a><span class="lineno"> 107</span> </div>
<div class="line"><a name="l00108"></a><span class="lineno"><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#ae0b4227a71a7d717dd55cc141a638eb1"> 108</a></span>  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></div>
<div class="line"><a name="l00109"></a><span class="lineno"> 109</span>  </div>
<div class="line"><a name="l00110"></a><span class="lineno"><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a40a454874f53c168f0e05cffe5d3d853"> 110</a></span>  <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></div>
<div class="line"><a name="l00111"></a><span class="lineno"> 111</span> </div>
<div class="line"><a name="l00112"></a><span class="lineno"><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a7a68974e437e44e62cc3020f51f881cc"> 112</a></span>  <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></div>
<div class="line"><a name="l00113"></a><span class="lineno"> 113</span> </div>
<div class="line"><a name="l00114"></a><span class="lineno"><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a316d10c5eb6ecb1b11fb212d4835a735"> 114</a></span>  <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></div>
<div class="line"><a name="l00115"></a><span class="lineno"> 115</span> </div>
<div class="line"><a name="l00116"></a><span class="lineno"><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#ad488e4d5e4340e0401a201a7afcb45f5"> 116</a></span>  <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></div>
<div class="line"><a name="l00117"></a><span class="lineno"> 117</span>  <span class="comment"></span></div>
<div class="line"><a name="l00118"></a><span class="lineno"> 118</span> <span class="comment"> //! if all formulas checked so far are good</span></div>
<div class="line"><a name="l00119"></a><span class="lineno"><a class="code" href="classCVC3_1_1CompleteInstPreProcessor.html#a99f6e270ce292ce04b1dea58cf5b95c3"> 119</a></span> <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> ;</div>
<div class="line"><a name="l00120"></a><span class="lineno"> 120</span> <span class="comment"></span></div>
<div class="line"><a name="l00121"></a><span class="lineno"> 121</span> <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></div>
<div class="line"><a name="l00122"></a><span class="lineno"> 122</span> <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);</div>
<div class="line"><a name="l00123"></a><span class="lineno"> 123</span> </div>
<div class="line"><a name="l00124"></a><span class="lineno"> 124</span>  <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);</div>
<div class="line"><a name="l00125"></a><span class="lineno"> 125</span> <span class="comment"></span></div>
<div class="line"><a name="l00126"></a><span class="lineno"> 126</span> <span class="comment"> //! insert an index</span></div>
<div class="line"><a name="l00127"></a><span class="lineno"> 127</span> <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);</div>
<div class="line"><a name="l00128"></a><span class="lineno"> 128</span>  </div>
<div class="line"><a name="l00129"></a><span class="lineno"> 129</span>  <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);</div>
<div class="line"><a name="l00130"></a><span class="lineno"> 130</span> </div>
<div class="line"><a name="l00131"></a><span class="lineno"> 131</span>  <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);</div>
<div class="line"><a name="l00132"></a><span class="lineno"> 132</span> <span class="comment"></span></div>
<div class="line"><a name="l00133"></a><span class="lineno"> 133</span> <span class="comment"> //! if e is a quant in the array property fragmenet</span></div>
<div class="line"><a name="l00134"></a><span class="lineno"> 134</span> <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);</div>
<div class="line"><a name="l00135"></a><span class="lineno"> 135</span> <span class="comment"></span></div>
<div class="line"><a name="l00136"></a><span class="lineno"> 136</span> <span class="comment"> //! return e+1</span></div>
<div class="line"><a name="l00137"></a><span class="lineno"> 137</span> <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);</div>
<div class="line"><a name="l00138"></a><span class="lineno"> 138</span> <span class="comment"></span></div>
<div class="line"><a name="l00139"></a><span class="lineno"> 139</span> <span class="comment"> //! return e-1</span></div>
<div class="line"><a name="l00140"></a><span class="lineno"> 140</span> <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);</div>
<div class="line"><a name="l00141"></a><span class="lineno"> 141</span> </div>
<div class="line"><a name="l00142"></a><span class="lineno"> 142</span>  <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);</div>
<div class="line"><a name="l00143"></a><span class="lineno"> 143</span>  <span class="comment"></span></div>
<div class="line"><a name="l00144"></a><span class="lineno"> 144</span> <span class="comment"> //! if assert is a macro definition</span></div>
<div class="line"><a name="l00145"></a><span class="lineno"> 145</span> <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);</div>
<div class="line"><a name="l00146"></a><span class="lineno"> 146</span> </div>
<div class="line"><a name="l00147"></a><span class="lineno"> 147</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#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);</div>
<div class="line"><a name="l00148"></a><span class="lineno"> 148</span> </div>
<div class="line"><a name="l00149"></a><span class="lineno"> 149</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#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>&);</div>
<div class="line"><a name="l00150"></a><span class="lineno"> 150</span> </div>
<div class="line"><a name="l00151"></a><span class="lineno"> 151</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#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>&);</div>
<div class="line"><a name="l00152"></a><span class="lineno"> 152</span> <span class="comment"></span></div>
<div class="line"><a name="l00153"></a><span class="lineno"> 153</span> <span class="comment"> //! rewrite neg polarity forall / exists to pos polarity</span></div>
<div class="line"><a name="l00154"></a><span class="lineno"> 154</span> <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> &);</div>
<div class="line"><a name="l00155"></a><span class="lineno"> 155</span>  </div>
<div class="line"><a name="l00156"></a><span class="lineno"> 156</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#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>&);</div>
<div class="line"><a name="l00157"></a><span class="lineno"> 157</span> </div>
<div class="line"><a name="l00158"></a><span class="lineno"> 158</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#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>&);</div>
<div class="line"><a name="l00159"></a><span class="lineno"> 159</span> </div>
<div class="line"><a name="l00160"></a><span class="lineno"> 160</span>  <span class="keyword">public</span> :</div>
<div class="line"><a name="l00161"></a><span class="lineno"> 161</span> </div>
<div class="line"><a name="l00162"></a><span class="lineno"> 162</span>  <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>*);</div>
<div class="line"><a name="l00163"></a><span class="lineno"> 163</span> <span class="comment"></span></div>
<div class="line"><a name="l00164"></a><span class="lineno"> 164</span> <span class="comment"> //! if e is a formula in the array property fragment </span></div>
<div class="line"><a name="l00165"></a><span class="lineno"> 165</span> <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);</div>
<div class="line"><a name="l00166"></a><span class="lineno"> 166</span> <span class="comment"></span></div>
<div class="line"><a name="l00167"></a><span class="lineno"> 167</span> <span class="comment"> //! collect index for instantiation</span></div>
<div class="line"><a name="l00168"></a><span class="lineno"> 168</span> <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);</div>
<div class="line"><a name="l00169"></a><span class="lineno"> 169</span> <span class="comment"></span></div>
<div class="line"><a name="l00170"></a><span class="lineno"> 170</span> <span class="comment"> //! inst forall quant using index from collectIndex</span></div>
<div class="line"><a name="l00171"></a><span class="lineno"> 171</span> <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);</div>
<div class="line"><a name="l00172"></a><span class="lineno"> 172</span> <span class="comment"></span></div>
<div class="line"><a name="l00173"></a><span class="lineno"> 173</span> <span class="comment"> //! if there are macros</span></div>
<div class="line"><a name="l00174"></a><span class="lineno"> 174</span> <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);</div>
<div class="line"><a name="l00175"></a><span class="lineno"> 175</span> <span class="comment"></span></div>
<div class="line"><a name="l00176"></a><span class="lineno"> 176</span> <span class="comment"> //! substitute a macro in assert</span></div>
<div class="line"><a name="l00177"></a><span class="lineno"> 177</span> <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> );</div>
<div class="line"><a name="l00178"></a><span class="lineno"> 178</span> <span class="comment"></span></div>
<div class="line"><a name="l00179"></a><span class="lineno"> 179</span> <span class="comment"> //! simplify a=a to True</span></div>
<div class="line"><a name="l00180"></a><span class="lineno"> 180</span> <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> &);</div>
<div class="line"><a name="l00181"></a><span class="lineno"> 181</span>  <span class="comment"></span></div>
<div class="line"><a name="l00182"></a><span class="lineno"> 182</span> <span class="comment"> //! put all quants in postive form and then skolemize all exists </span></div>
<div class="line"><a name="l00183"></a><span class="lineno"> 183</span> <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> &);</div>
<div class="line"><a name="l00184"></a><span class="lineno"> 184</span>  };</div>
<div class="line"><a name="l00185"></a><span class="lineno"> 185</span>  </div>
<div class="line"><a name="l00186"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html"> 186</a></span>  <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> {</div>
<div class="line"><a name="l00187"></a><span class="lineno"> 187</span>  </div>
<div class="line"><a name="l00188"></a><span class="lineno"> 188</span>  <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);</div>
<div class="line"><a name="l00189"></a><span class="lineno"> 189</span> </div>
<div class="line"><a name="l00190"></a><span class="lineno"> 190</span>  <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);</div>
<div class="line"><a name="l00191"></a><span class="lineno"> 191</span> </div>
<div class="line"><a name="l00192"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant_1_1TypeComp.html"> 192</a></span>  <span class="keyword">class </span><a class="code" href="classCVC3_1_1TheoryQuant_1_1TypeComp.html">TypeComp</a> { <span class="comment">//!< needed for typeMap</span></div>
<div class="line"><a name="l00193"></a><span class="lineno"> 193</span> <span class="comment"></span> <span class="keyword">public</span>:</div>
<div class="line"><a name="l00194"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant_1_1TypeComp.html#adeafb5c7ebe3a272107f25d0fd695940"> 194</a></span>  <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></div>
<div class="line"><a name="l00195"></a><span class="lineno"> 195</span> <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>()); }</div>
<div class="line"><a name="l00196"></a><span class="lineno"> 196</span>  };</div>
<div class="line"><a name="l00197"></a><span class="lineno"> 197</span> <span class="comment"></span></div>
<div class="line"><a name="l00198"></a><span class="lineno"> 198</span> <span class="comment"> //! used to facilitate instantiation of universal quantifiers</span></div>
<div class="line"><a name="l00199"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a9530e1a16572ad8b35d7c3bd08c9803a"> 199</a></span> <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>; </div>
<div class="line"><a name="l00200"></a><span class="lineno"> 200</span> <span class="comment"></span></div>
<div class="line"><a name="l00201"></a><span class="lineno"> 201</span> <span class="comment"> //! database of universally quantified theorems</span></div>
<div class="line"><a name="l00202"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a8c837bb9045c09ceb44d135e13f1788a"> 202</a></span> <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>; </div>
<div class="line"><a name="l00203"></a><span class="lineno"> 203</span> </div>
<div class="line"><a name="l00204"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a98562e5cbaac2c2abec9a0814726e990"> 204</a></span>  <a class="code" href="classCVC3_1_1CDList.html">CDList<Theorem></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a98562e5cbaac2c2abec9a0814726e990">d_rawUnivs</a>; </div>
<div class="line"><a name="l00205"></a><span class="lineno"> 205</span> </div>
<div class="line"><a name="l00206"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a6ed4dff6a76e12a20c1b11cf2080106f"> 206</a></span>  <a class="code" href="classCVC3_1_1CDList.html">CDList<dynTrig></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a6ed4dff6a76e12a20c1b11cf2080106f">d_arrayTrigs</a>; </div>
<div class="line"><a name="l00207"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a8182fa76e03957abb77e540861c4db40"> 207</a></span>  <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a8182fa76e03957abb77e540861c4db40">d_lastArrayPos</a>;</div>
<div class="line"><a name="l00208"></a><span class="lineno"> 208</span> <span class="comment"></span></div>
<div class="line"><a name="l00209"></a><span class="lineno"> 209</span> <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></div>
<div class="line"><a name="l00210"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a216345a29be8f6c9e135b656e16fd4ca"> 210</a></span> <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>;</div>
<div class="line"><a name="l00211"></a><span class="lineno"> 211</span> </div>
<div class="line"><a name="l00212"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a20237cf6afe027d65533f121fa9baa8d"> 212</a></span>  std::queue<Theorem> <a class="code" href="classCVC3_1_1TheoryQuant.html#a20237cf6afe027d65533f121fa9baa8d">d_simplifiedThmQueue</a>;</div>
<div class="line"><a name="l00213"></a><span class="lineno"> 213</span> </div>
<div class="line"><a name="l00214"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#adced7c9130c7f24e53f2553eae73246c"> 214</a></span>  std::queue<Theorem> <a class="code" href="classCVC3_1_1TheoryQuant.html#adced7c9130c7f24e53f2553eae73246c">d_gUnivQueue</a>;</div>
<div class="line"><a name="l00215"></a><span class="lineno"> 215</span>  </div>
<div class="line"><a name="l00216"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a7f68f552fa0794f221bbceeb7918c167"> 216</a></span>  std::queue<Expr> <a class="code" href="classCVC3_1_1TheoryQuant.html#a7f68f552fa0794f221bbceeb7918c167">d_gBindQueue</a>;</div>
<div class="line"><a name="l00217"></a><span class="lineno"> 217</span> </div>
<div class="line"><a name="l00218"></a><span class="lineno"> 218</span> </div>
<div class="line"><a name="l00219"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#afa26420c222cf2a7f47c09842b164307"> 219</a></span>  <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>;</div>
<div class="line"><a name="l00220"></a><span class="lineno"> 220</span> <span class="comment"></span></div>
<div class="line"><a name="l00221"></a><span class="lineno"> 221</span> <span class="comment"> //!tracks the possition of preds </span></div>
<div class="line"><a name="l00222"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ad1c890b18078d4c9ce5ef49517f539c4"> 222</a></span> <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></div>
<div class="line"><a name="l00223"></a><span class="lineno"> 223</span> <span class="comment"> //!tracks the possition of terms </span></div>
<div class="line"><a name="l00224"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ada0a9362e554f531636059ba0f128ac9"> 224</a></span> <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>;</div>
<div class="line"><a name="l00225"></a><span class="lineno"> 225</span> <span class="comment"></span></div>
<div class="line"><a name="l00226"></a><span class="lineno"> 226</span> <span class="comment"> //!tracks the positions of preds for partial instantiation</span></div>
<div class="line"><a name="l00227"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ac84aea59c42a90500d10f8604e7eb822"> 227</a></span> <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></div>
<div class="line"><a name="l00228"></a><span class="lineno"> 228</span> <span class="comment"> //!tracks the possition of terms for partial instantiation</span></div>
<div class="line"><a name="l00229"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a9141a0d67cecc9180e1838b1e03f2062"> 229</a></span> <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></div>
<div class="line"><a name="l00230"></a><span class="lineno"> 230</span> <span class="comment"> //!tracks a possition in the database of universals for partial instantiation</span></div>
<div class="line"><a name="l00231"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a49b552d6d70733a9c6dd60eee5a2a646"> 231</a></span> <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>;</div>
<div class="line"><a name="l00232"></a><span class="lineno"> 232</span>  <span class="comment"></span></div>
<div class="line"><a name="l00233"></a><span class="lineno"> 233</span> <span class="comment"> //! the last decision level on which partial instantion is called</span></div>
<div class="line"><a name="l00234"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#adb2db1fc47d328213e2f8bef1de71b88"> 234</a></span> <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>;</div>
<div class="line"><a name="l00235"></a><span class="lineno"> 235</span> </div>
<div class="line"><a name="l00236"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a777ab16b886b05ea63180e44bd62fe43"> 236</a></span>  <a class="code" href="classCVC3_1_1CDO.html">CDO<bool></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a777ab16b886b05ea63180e44bd62fe43">d_partCalled</a>;</div>
<div class="line"><a name="l00237"></a><span class="lineno"> 237</span>  <span class="comment"></span></div>
<div class="line"><a name="l00238"></a><span class="lineno"> 238</span> <span class="comment"> //! the max instantiation level reached</span></div>
<div class="line"><a name="l00239"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a5c321d21dbbf2e23a772dec478dd6ade"> 239</a></span> <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>;</div>
<div class="line"><a name="l00240"></a><span class="lineno"> 240</span> </div>
<div class="line"><a name="l00241"></a><span class="lineno"> 241</span> </div>
<div class="line"><a name="l00242"></a><span class="lineno"> 242</span>  <span class="comment"></span></div>
<div class="line"><a name="l00243"></a><span class="lineno"> 243</span> <span class="comment"> //!useful gterms for matching</span></div>
<div class="line"><a name="l00244"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ae2aa24cf865298deb21463f1c64cefed"> 244</a></span> <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>; </div>
<div class="line"><a name="l00245"></a><span class="lineno"> 245</span> <span class="comment"></span></div>
<div class="line"><a name="l00246"></a><span class="lineno"> 246</span> <span class="comment"> //!tracks the position in d_usefulGterms</span></div>
<div class="line"><a name="l00247"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a949092aaf1aba7329ab512031f8399cc"> 247</a></span> <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>;</div>
<div class="line"><a name="l00248"></a><span class="lineno"> 248</span>  <span class="comment"></span></div>
<div class="line"><a name="l00249"></a><span class="lineno"> 249</span> <span class="comment"> //!tracks a possition in the savedTerms map</span></div>
<div class="line"><a name="l00250"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a12325d3d4d8cd79170c4cf3ec61a511f"> 250</a></span> <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></div>
<div class="line"><a name="l00251"></a><span class="lineno"> 251</span> <span class="comment"> //!tracks a possition in the database of universals</span></div>
<div class="line"><a name="l00252"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a78e66cea83a0bd258f7c7064bac4808c"> 252</a></span> <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>;</div>
<div class="line"><a name="l00253"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a54e9b1c666a443f2fd4b8abf48077f5b"> 253</a></span>  <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></div>
<div class="line"><a name="l00254"></a><span class="lineno"> 254</span> <span class="comment"> //!tracks a possition in the database of universals</span></div>
<div class="line"><a name="l00255"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a8b5e246c61121a22421d550d4376d3f0"> 255</a></span> <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></div>
<div class="line"><a name="l00256"></a><span class="lineno"> 256</span> <span class="comment"> //!tracks a possition in the database of universals if fulleffort mode, the d_univsSavedPos now uesed when fulleffort=0 only.</span></div>
<div class="line"><a name="l00257"></a><span class="lineno"> 257</span> <span class="comment"></span></div>
<div class="line"><a name="l00258"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a0388d31f826f4786e14d252726c8c26a"> 258</a></span>  <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>;</div>
<div class="line"><a name="l00259"></a><span class="lineno"> 259</span>  </div>
<div class="line"><a name="l00260"></a><span class="lineno"> 260</span>  </div>
<div class="line"><a name="l00261"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a9bc78df3616eacf20e564a08c8a9896f"> 261</a></span>  <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></div>
<div class="line"><a name="l00262"></a><span class="lineno"> 262</span> <span class="comment"></span><span class="comment"></span></div>
<div class="line"><a name="l00263"></a><span class="lineno"> 263</span> <span class="comment"> //! set if the fullEffort = 1</span></div>
<div class="line"><a name="l00264"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a97c18d8746ce2afdd83a9e12c84cdd24"> 264</a></span> <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>; </div>
<div class="line"><a name="l00265"></a><span class="lineno"> 265</span> </div>
<div class="line"><a name="l00266"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a6c0bfa341c282227a4a94e27d997bf01"> 266</a></span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a6c0bfa341c282227a4a94e27d997bf01">d_allout</a>; </div>
<div class="line"><a name="l00267"></a><span class="lineno"> 267</span> <span class="comment"></span></div>
<div class="line"><a name="l00268"></a><span class="lineno"> 268</span> <span class="comment"> //! a map of types to posisitions in the d_contextTerms list</span></div>
<div class="line"><a name="l00269"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a9f6efeac1026260673ddbf7f083504da"> 269</a></span> <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></div>
<div class="line"><a name="l00270"></a><span class="lineno"> 270</span> <span class="comment"> //! a list of all the terms appearing in the current context</span></div>
<div class="line"><a name="l00271"></a><span class="lineno"> 271</span> <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></div>
<div class="line"><a name="l00272"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#aa859e8e5d08c4c4a64c110f956209b72"> 272</a></span> <span class="comment"> //!< chache of expressions</span></div>
<div class="line"><a name="l00273"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ab4a7ed7a25824178d2a60fb9d2645632"> 273</a></span> <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>;</div>
<div class="line"><a name="l00274"></a><span class="lineno"> 274</span>  <span class="comment"></span></div>
<div class="line"><a name="l00275"></a><span class="lineno"> 275</span> <span class="comment"> //! a map of types to positions in the d_savedTerms vector</span></div>
<div class="line"><a name="l00276"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a151130d7ab3011be448ea16b0eb96156"> 276</a></span> <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>;</div>
<div class="line"><a name="l00277"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a2090a926ff4120c1f417693974afd49e"> 277</a></span>  <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></div>
<div class="line"><a name="l00278"></a><span class="lineno"> 278</span> <span class="comment"></span><span class="comment"> //! a vector of all of the terms that have produced conflicts.</span></div>
<div class="line"><a name="l00279"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ab8eafb65bdcded93b43a311e65d80051"> 279</a></span> <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>; </div>
<div class="line"><a name="l00280"></a><span class="lineno"> 280</span> <span class="comment"></span></div>
<div class="line"><a name="l00281"></a><span class="lineno"> 281</span> <span class="comment"> //! a map of instantiated universals to a vector of their instantiations</span></div>
<div class="line"><a name="l00282"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#afbc66a1d0e321ce140c1db73d22d2551"> 282</a></span> <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>;</div>
<div class="line"><a name="l00283"></a><span class="lineno"> 283</span> <span class="comment"></span></div>
<div class="line"><a name="l00284"></a><span class="lineno"> 284</span> <span class="comment"> //! quantifier theorem production rules</span></div>
<div class="line"><a name="l00285"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a402f8b86c479687a21ff3e71581e9cd4"> 285</a></span> <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>;</div>
<div class="line"><a name="l00286"></a><span class="lineno"> 286</span>  </div>
<div class="line"><a name="l00287"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#aad0370d3aabc256eb298dfcc27229e72"> 287</a></span>  <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></div>
<div class="line"><a name="l00288"></a><span class="lineno"> 288</span> <span class="comment"></span><span class="comment"></span></div>
<div class="line"><a name="l00289"></a><span class="lineno"> 289</span> <span class="comment"> /*! \brief categorizes all the terms contained in an expressions by</span></div>
<div class="line"><a name="l00290"></a><span class="lineno"> 290</span> <span class="comment"> *type.</span></div>
<div class="line"><a name="l00291"></a><span class="lineno"> 291</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00292"></a><span class="lineno"> 292</span> <span class="comment"> * Updates d_contextTerms, d_contextMap, d_contextCache accordingly.</span></div>
<div class="line"><a name="l00293"></a><span class="lineno"> 293</span> <span class="comment"> * returns true if the expression does not contain bound variables, false</span></div>
<div class="line"><a name="l00294"></a><span class="lineno"> 294</span> <span class="comment"> * otherwise.</span></div>
<div class="line"><a name="l00295"></a><span class="lineno"> 295</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00296"></a><span class="lineno"> 296</span>  <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);</div>
<div class="line"><a name="l00297"></a><span class="lineno"> 297</span> <span class="comment"></span></div>
<div class="line"><a name="l00298"></a><span class="lineno"> 298</span> <span class="comment"> /*! \brief categorizes all the terms contained in a vector of expressions by</span></div>
<div class="line"><a name="l00299"></a><span class="lineno"> 299</span> <span class="comment"> * type.</span></div>
<div class="line"><a name="l00300"></a><span class="lineno"> 300</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00301"></a><span class="lineno"> 301</span> <span class="comment"> * Updates d_contextTerms, d_contextMap, d_contextCache accordingly.</span></div>
<div class="line"><a name="l00302"></a><span class="lineno"> 302</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00303"></a><span class="lineno"> 303</span>  <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);</div>
<div class="line"><a name="l00304"></a><span class="lineno"> 304</span>  <span class="comment"></span></div>
<div class="line"><a name="l00305"></a><span class="lineno"> 305</span> <span class="comment"> /*! \brief Queues up all possible instantiations of bound</span></div>
<div class="line"><a name="l00306"></a><span class="lineno"> 306</span> <span class="comment"> * variables.</span></div>
<div class="line"><a name="l00307"></a><span class="lineno"> 307</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00308"></a><span class="lineno"> 308</span> <span class="comment"> * The savedMap boolean indicates whether to use savedMap or</span></div>
<div class="line"><a name="l00309"></a><span class="lineno"> 309</span> <span class="comment"> * d_contextMap the all boolean indicates weather to use all</span></div>
<div class="line"><a name="l00310"></a><span class="lineno"> 310</span> <span class="comment"> * instantiation or only new ones and newIndex is the index where</span></div>
<div class="line"><a name="l00311"></a><span class="lineno"> 311</span> <span class="comment"> * new instantiations begin.</span></div>
<div class="line"><a name="l00312"></a><span class="lineno"> 312</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00313"></a><span class="lineno"> 313</span>  <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, </div>
<div class="line"><a name="l00314"></a><span class="lineno"> 314</span>  <span class="keywordtype">size_t</span> newIndex);<span class="comment"></span></div>
<div class="line"><a name="l00315"></a><span class="lineno"> 315</span> <span class="comment"> //! does most of the work of the instantiate function.</span></div>
<div class="line"><a name="l00316"></a><span class="lineno"> 316</span> <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, </div>
<div class="line"><a name="l00317"></a><span class="lineno"> 317</span>  std::vector<Expr>& varReplacements);</div>
<div class="line"><a name="l00318"></a><span class="lineno"> 318</span> <span class="comment"></span></div>
<div class="line"><a name="l00319"></a><span class="lineno"> 319</span> <span class="comment"> /*! \brief A recursive function used to find instantiated universals</span></div>
<div class="line"><a name="l00320"></a><span class="lineno"> 320</span> <span class="comment"> * in the hierarchy of assumptions.</span></div>
<div class="line"><a name="l00321"></a><span class="lineno"> 321</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00322"></a><span class="lineno"> 322</span>  <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);</div>
<div class="line"><a name="l00323"></a><span class="lineno"> 323</span> </div>
<div class="line"><a name="l00324"></a><span class="lineno"> 324</span>  <span class="comment">// CDO<bool> usedup;</span></div>
<div class="line"><a name="l00325"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a941345e490bc23ed9454bc98513fafb2"> 325</a></span>  <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></div>
<div class="line"><a name="l00326"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a71f7265b98a79dff4f924fa84c6720d5"> 326</a></span> <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></div>
<div class="line"><a name="l00327"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a6849ba1ee187928b1c254722525f8c5e"> 327</a></span> <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></div>
<div class="line"><a name="l00328"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a307d487df3c5ba9770f4f2c99a1ce912"> 328</a></span> <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></div>
<div class="line"><a name="l00329"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#affe271f96919ed4bb74e331159573d03"> 329</a></span> <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></div>
<div class="line"><a name="l00330"></a><span class="lineno"> 330</span> <span class="comment"></span></div>
<div class="line"><a name="l00331"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#aa6c894d36bb697a93713950312593e53"> 331</a></span>  <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></div>
<div class="line"><a name="l00332"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ad0bf093cc6fe61456b2d186333fa1476"> 332</a></span> <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></div>
<div class="line"><a name="l00333"></a><span class="lineno"> 333</span>  <span class="comment">// const bool* d_useInstEnd;</span></div>
<div class="line"><a name="l00334"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ae18bcd5e6dd77c740c08a37a90face8d"> 334</a></span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#ae18bcd5e6dd77c740c08a37a90face8d">d_useInstLCache</a>;</div>
<div class="line"><a name="l00335"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#aed3aa4f475cb2d920dcc137009aa208c"> 335</a></span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#aed3aa4f475cb2d920dcc137009aa208c">d_useInstGCache</a>;</div>
<div class="line"><a name="l00336"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a0cb98a0e60550b47b6cf62d58ef7526c"> 336</a></span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a0cb98a0e60550b47b6cf62d58ef7526c">d_useInstThmCache</a>;</div>
<div class="line"><a name="l00337"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a26af226b922851112e91577ca7e3b452"> 337</a></span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a26af226b922851112e91577ca7e3b452">d_useInstTrue</a>;</div>
<div class="line"><a name="l00338"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a40f07b217c6934bba4480207f798eea2"> 338</a></span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a40f07b217c6934bba4480207f798eea2">d_usePullVar</a>;</div>
<div class="line"><a name="l00339"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a8f7f76c25794e58a8bbd35bbb37e3aed"> 339</a></span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a8f7f76c25794e58a8bbd35bbb37e3aed">d_useExprScore</a>;</div>
<div class="line"><a name="l00340"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a1f1f4c18fe0c68dfb7eea0d3bd0220db"> 340</a></span>  <span class="keyword">const</span> <span class="keywordtype">int</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a1f1f4c18fe0c68dfb7eea0d3bd0220db">d_useTrigLoop</a>;</div>
<div class="line"><a name="l00341"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a5f3ae02fd56df2f401da18b10ffc068b"> 341</a></span>  <span class="keyword">const</span> <span class="keywordtype">int</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a5f3ae02fd56df2f401da18b10ffc068b">d_maxInst</a>;</div>
<div class="line"><a name="l00342"></a><span class="lineno"> 342</span>  <span class="comment">// const int* d_maxUserScore;</span></div>
<div class="line"><a name="l00343"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#aa223ccaf4a6297fbe9243905f2fa1cd3"> 343</a></span>  <span class="keyword">const</span> <span class="keywordtype">int</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#aa223ccaf4a6297fbe9243905f2fa1cd3">d_maxIL</a>;</div>
<div class="line"><a name="l00344"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a6bde73c972d4bfc46683279e6c18b7df"> 344</a></span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a6bde73c972d4bfc46683279e6c18b7df">d_useTrans</a>;</div>
<div class="line"><a name="l00345"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a596216803168d232d335c3a2e7b35a02"> 345</a></span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a596216803168d232d335c3a2e7b35a02">d_useTrans2</a>;</div>
<div class="line"><a name="l00346"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a2a8534b65e4c74e2c28c98f297b931e0"> 346</a></span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a2a8534b65e4c74e2c28c98f297b931e0">d_useManTrig</a>;</div>
<div class="line"><a name="l00347"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a2dc4c4cd98dd966b17a705399db80bd4"> 347</a></span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a2dc4c4cd98dd966b17a705399db80bd4">d_useGFact</a>;</div>
<div class="line"><a name="l00348"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a343bd1867fbb824c16f2bc376d031234"> 348</a></span>  <span class="keyword">const</span> <span class="keywordtype">int</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a343bd1867fbb824c16f2bc376d031234">d_gfactLimit</a>;</div>
<div class="line"><a name="l00349"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a1caf0d9c2c9ff8ac77123921158e781c"> 349</a></span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a1caf0d9c2c9ff8ac77123921158e781c">d_useInstAll</a>;</div>
<div class="line"><a name="l00350"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a7285a10b61c56f1abd386d15da664341"> 350</a></span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a7285a10b61c56f1abd386d15da664341">d_usePolarity</a>;</div>
<div class="line"><a name="l00351"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ab6987761a0573b5a1f96be74f5be6594"> 351</a></span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#ab6987761a0573b5a1f96be74f5be6594">d_useEqu</a>;</div>
<div class="line"><a name="l00352"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ad7cb228fd0c997d6d0cb92ebdf36f0d4"> 352</a></span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#ad7cb228fd0c997d6d0cb92ebdf36f0d4">d_useNewEqu</a>;</div>
<div class="line"><a name="l00353"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ac5ecfdb795d8741da3942e7e4ec19928"> 353</a></span>  <span class="keyword">const</span> <span class="keywordtype">int</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#ac5ecfdb795d8741da3942e7e4ec19928">d_maxNaiveCall</a>;</div>
<div class="line"><a name="l00354"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ae3655c358b7c2b206c7a467eb7cc4880"> 354</a></span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>* <a class="code" href="classCVC3_1_1TheoryQuant.html#ae3655c358b7c2b206c7a467eb7cc4880">d_useNaiveInst</a>;</div>
<div class="line"><a name="l00355"></a><span class="lineno"> 355</span> </div>
<div class="line"><a name="l00356"></a><span class="lineno"> 356</span> </div>
<div class="line"><a name="l00357"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a0353fa5170be84ed1feffc0adaea61b6"> 357</a></span>  <a class="code" href="classCVC3_1_1CDO.html">CDO<int></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a0353fa5170be84ed1feffc0adaea61b6">d_curMaxExprScore</a>;</div>
<div class="line"><a name="l00358"></a><span class="lineno"> 358</span> </div>
<div class="line"><a name="l00359"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ae765160d5df0404da2d869a19ce3392d"> 359</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#ae765160d5df0404da2d869a19ce3392d">d_useFullTrig</a>;</div>
<div class="line"><a name="l00360"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a43d925d46b17106af6676a693bb3e81c"> 360</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a43d925d46b17106af6676a693bb3e81c">d_usePartTrig</a>;</div>
<div class="line"><a name="l00361"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a94cdc6b5d40ea0d468176829f3b7cc7f"> 361</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a94cdc6b5d40ea0d468176829f3b7cc7f">d_useMultTrig</a>;</div>
<div class="line"><a name="l00362"></a><span class="lineno"> 362</span> </div>
<div class="line"><a name="l00363"></a><span class="lineno"> 363</span>  <span class="comment">//ExprMap<std::vector<Expr> > d_arrayIndic; //map array name to a list of indics</span></div>
<div class="line"><a name="l00364"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a42bf4d8a8865547e765374f47c89a42d"> 364</a></span>  <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></div>
<div class="line"><a name="l00365"></a><span class="lineno"> 365</span>  <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);</div>
<div class="line"><a name="l00366"></a><span class="lineno"> 366</span> </div>
<div class="line"><a name="l00367"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a257fa05e1227011338ff18b07bbd8ea7"> 367</a></span>  std::vector<Expr> <a class="code" href="classCVC3_1_1TheoryQuant.html#a257fa05e1227011338ff18b07bbd8ea7">d_allInsts</a>; <span class="comment">//! all instantiations</span></div>
<div class="line"><a name="l00368"></a><span class="lineno"> 368</span> <span class="comment"></span></div>
<div class="line"><a name="l00369"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a7e5a0fbbbe03ac62ae2fe52ea6768988"> 369</a></span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a7e5a0fbbbe03ac62ae2fe52ea6768988" title="all instantiations">d_initMaxScore</a>;</div>
<div class="line"><a name="l00370"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#adb5ce0ce6808f4d60284a2658256a772"> 370</a></span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#adb5ce0ce6808f4d60284a2658256a772">d_offset_multi_trig</a> ;</div>
<div class="line"><a name="l00371"></a><span class="lineno"> 371</span>  </div>
<div class="line"><a name="l00372"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a42b268e32a020cedcca5c58efd84c114"> 372</a></span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a42b268e32a020cedcca5c58efd84c114">d_instThisRound</a>;</div>
<div class="line"><a name="l00373"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a0615dcf3f868ddbd02984a29e482427e"> 373</a></span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a0615dcf3f868ddbd02984a29e482427e">d_callThisRound</a>;</div>
<div class="line"><a name="l00374"></a><span class="lineno"> 374</span> </div>
<div class="line"><a name="l00375"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#aa60a22e8795e5046cd17d016d40705b2"> 375</a></span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#aa60a22e8795e5046cd17d016d40705b2">partial_called</a>;</div>
<div class="line"><a name="l00376"></a><span class="lineno"> 376</span> </div>
<div class="line"><a name="l00377"></a><span class="lineno"> 377</span>  <span class="comment">// ExprMap<std::vector<Expr> > d_fullTriggers;</span></div>
<div class="line"><a name="l00378"></a><span class="lineno"> 378</span>  <span class="comment">//for multi-triggers, now we only have one set of multi-triggers.</span></div>
<div class="line"><a name="l00379"></a><span class="lineno"> 379</span> </div>
<div class="line"><a name="l00380"></a><span class="lineno"> 380</span> </div>
<div class="line"><a name="l00381"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ac1f7a57f263b0bbc3d2bd87e7a931598"> 381</a></span>  <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>;</div>
<div class="line"><a name="l00382"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ab00d303da385069d53e20c8fe52248b0"> 382</a></span>  <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>;</div>
<div class="line"><a name="l00383"></a><span class="lineno"> 383</span> </div>
<div class="line"><a name="l00384"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a590efa99276b0b530def7c750931f0e0"> 384</a></span>  <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>;</div>
<div class="line"><a name="l00385"></a><span class="lineno"> 385</span>  <span class="comment">//for multi-triggers, now we only have one set of multi-triggers.</span></div>
<div class="line"><a name="l00386"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ab3d76fe9a84814d0493dc47928450be1"> 386</a></span>  <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>;</div>
<div class="line"><a name="l00387"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a9b64987d5098fd227f10b45e0365da63"> 387</a></span>  <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>;</div>
<div class="line"><a name="l00388"></a><span class="lineno"> 388</span> </div>
<div class="line"><a name="l00389"></a><span class="lineno"> 389</span>  </div>
<div class="line"><a name="l00390"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ad9e2ac11111d8068cd47101e914400ec"> 390</a></span>  <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></div>
<div class="line"><a name="l00391"></a><span class="lineno"> 391</span> </div>
<div class="line"><a name="l00392"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a8acfdb59fc63cde21b7d9ec22796756d"> 392</a></span>  std::map<ExprIndex, int> <a class="code" href="classCVC3_1_1TheoryQuant.html#a8acfdb59fc63cde21b7d9ec22796756d">d_indexScore</a>;</div>
<div class="line"><a name="l00393"></a><span class="lineno"> 393</span> </div>
<div class="line"><a name="l00394"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a712b1f8b6128c2f5290b02b16285fac4"> 394</a></span>  std::map<ExprIndex, Expr> <a class="code" href="classCVC3_1_1TheoryQuant.html#a712b1f8b6128c2f5290b02b16285fac4">d_indexExpr</a>;</div>
<div class="line"><a name="l00395"></a><span class="lineno"> 395</span> </div>
<div class="line"><a name="l00396"></a><span class="lineno"> 396</span>  <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);</div>
<div class="line"><a name="l00397"></a><span class="lineno"> 397</span> <span class="comment"></span></div>
<div class="line"><a name="l00398"></a><span class="lineno"> 398</span> <span class="comment"> //!the score for a full trigger</span></div>
<div class="line"><a name="l00399"></a><span class="lineno"> 399</span> <span class="comment"></span> </div>
<div class="line"><a name="l00400"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#aa0f0f35f81aad33349edb9a4ae1f50c2"> 400</a></span>  <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>;</div>
<div class="line"><a name="l00401"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a149311d8fb4973ba78aaef0b49fcdeb3"> 401</a></span>  <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<bool></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a149311d8fb4973ba78aaef0b49fcdeb3">d_hasMoreBVs</a>;</div>
<div class="line"><a name="l00402"></a><span class="lineno"> 402</span> </div>
<div class="line"><a name="l00403"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a32a16dc1f3abd4bb2923512863dad2e3"> 403</a></span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a32a16dc1f3abd4bb2923512863dad2e3">d_trans_num</a>;</div>
<div class="line"><a name="l00404"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a21177e07fa85adab68a40245f7b56dc7"> 404</a></span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a21177e07fa85adab68a40245f7b56dc7">d_trans2_num</a>;</div>
<div class="line"><a name="l00405"></a><span class="lineno"> 405</span> </div>
<div class="line"><a name="l00406"></a><span class="lineno"><a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html"> 406</a></span>  <span class="keyword">typedef</span> <span class="keyword">struct</span>{</div>
<div class="line"><a name="l00407"></a><span class="lineno"><a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#a30585771f9ea7ba104b9b0e96aae8f58"> 407</a></span>  std::vector<std::vector<size_t> > <a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#a30585771f9ea7ba104b9b0e96aae8f58">common_pos</a>;</div>
<div class="line"><a name="l00408"></a><span class="lineno"><a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#aa9a7e0ca5f85e46d2a87574d31340882"> 408</a></span>  std::vector<std::vector<size_t> > <a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#aa9a7e0ca5f85e46d2a87574d31340882">var_pos</a>; </div>
<div class="line"><a name="l00409"></a><span class="lineno"> 409</span>  </div>
<div class="line"><a name="l00410"></a><span class="lineno"><a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#ae8069d3960f8fca170b24437747be5be"> 410</a></span>  std::vector<CDMap<Expr, bool>* > <a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#ae8069d3960f8fca170b24437747be5be">var_binds_found</a>;</div>
<div class="line"><a name="l00411"></a><span class="lineno"> 411</span> </div>
<div class="line"><a name="l00412"></a><span class="lineno"><a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#adb3cde79421ada753728f06749d81a26"> 412</a></span>  std::vector<ExprMap<CDList<Expr>* >* > <a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#adb3cde79421ada753728f06749d81a26">uncomm_list</a>; <span class="comment">//</span></div>
<div class="line"><a name="l00413"></a><span class="lineno"><a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#a1bb00c7646f04ef7a7b1effe16afbf47"> 413</a></span>  <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></div>
<div class="line"><a name="l00414"></a><span class="lineno"><a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#a96287846947610728257c05150e830a0"> 414</a></span>  <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></div>
<div class="line"><a name="l00415"></a><span class="lineno"> 415</span>  } <a class="code" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html">multTrigsInfo</a> ;</div>
<div class="line"><a name="l00416"></a><span class="lineno"> 416</span>  </div>
<div class="line"><a name="l00417"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#abe536d22495efd45fcb3c35cadc3f417"> 417</a></span>  <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<multTrigsInfo></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#abe536d22495efd45fcb3c35cadc3f417">d_multitrigs_maps</a>;</div>
<div class="line"><a name="l00418"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a5ba728c791a6e156c1e1252698656154"> 418</a></span>  std::vector<multTrigsInfo> <a class="code" href="classCVC3_1_1TheoryQuant.html#a5ba728c791a6e156c1e1252698656154">d_all_multTrigsInfo</a>;</div>
<div class="line"><a name="l00419"></a><span class="lineno"> 419</span>  </div>
<div class="line"><a name="l00420"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a5988b551d392a2675afe20061c374387"> 420</a></span>  <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>;</div>
<div class="line"><a name="l00421"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a09130b8c278fc53d6b978144fc060b88"> 421</a></span>  <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>;</div>
<div class="line"><a name="l00422"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a40d9d2a6ac497d8925d85b1534f927fe"> 422</a></span>  <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>;</div>
<div class="line"><a name="l00423"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a1c1cea4c4d5aa9cd0e85233daf082a14"> 423</a></span>  <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>;</div>
<div class="line"><a name="l00424"></a><span class="lineno"> 424</span> </div>
<div class="line"><a name="l00425"></a><span class="lineno"> 425</span> </div>
<div class="line"><a name="l00426"></a><span class="lineno"> 426</span>  <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);</div>
<div class="line"><a name="l00427"></a><span class="lineno"> 427</span>  </div>
<div class="line"><a name="l00428"></a><span class="lineno"> 428</span>  <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);</div>
<div class="line"><a name="l00429"></a><span class="lineno"> 429</span> </div>
<div class="line"><a name="l00430"></a><span class="lineno"> 430</span>  <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);</div>
<div class="line"><a name="l00431"></a><span class="lineno"> 431</span> </div>
<div class="line"><a name="l00432"></a><span class="lineno"> 432</span>  <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);</div>
<div class="line"><a name="l00433"></a><span class="lineno"> 433</span> </div>
<div class="line"><a name="l00434"></a><span class="lineno"> 434</span>  </div>
<div class="line"><a name="l00435"></a><span class="lineno"> 435</span>  <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);</div>
<div class="line"><a name="l00436"></a><span class="lineno"> 436</span>  </div>
<div class="line"><a name="l00437"></a><span class="lineno"> 437</span>  <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);</div>
<div class="line"><a name="l00438"></a><span class="lineno"> 438</span> </div>
<div class="line"><a name="l00439"></a><span class="lineno"> 439</span>  <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);</div>
<div class="line"><a name="l00440"></a><span class="lineno"> 440</span>  <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);</div>
<div class="line"><a name="l00441"></a><span class="lineno"> 441</span> </div>
<div class="line"><a name="l00442"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a8c198e6cf92b67913a4c2eeba3049591"> 442</a></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#a8c198e6cf92b67913a4c2eeba3049591">defaultWriteExpr</a>;</div>
<div class="line"><a name="l00443"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ac3c6c90503e2a63b01cb71aec8e67959"> 443</a></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#ac3c6c90503e2a63b01cb71aec8e67959">defaultReadExpr</a>;</div>
<div class="line"><a name="l00444"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ae722d51a41c8bbfb71262033b5366267"> 444</a></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#ae722d51a41c8bbfb71262033b5366267">defaultPlusExpr</a>;</div>
<div class="line"><a name="l00445"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#adaebb75807818796d34d2ff776755528"> 445</a></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#adaebb75807818796d34d2ff776755528">defaultMinusExpr</a> ;</div>
<div class="line"><a name="l00446"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a52e766e9bd39c2061de7c46368fd28e0"> 446</a></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#a52e766e9bd39c2061de7c46368fd28e0">defaultMultExpr</a> ;</div>
<div class="line"><a name="l00447"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a7ee722984f64a327d4afd1d44915c94c"> 447</a></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#a7ee722984f64a327d4afd1d44915c94c">defaultDivideExpr</a>;</div>
<div class="line"><a name="l00448"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ab47f89174cf6213f2379e9df4eef8bec"> 448</a></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#ab47f89174cf6213f2379e9df4eef8bec">defaultPowExpr</a> ;</div>
<div class="line"><a name="l00449"></a><span class="lineno"> 449</span> </div>
<div class="line"><a name="l00450"></a><span class="lineno"> 450</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#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) ;</div>
<div class="line"><a name="l00451"></a><span class="lineno"> 451</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#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) ;</div>
<div class="line"><a name="l00452"></a><span class="lineno"> 452</span> </div>
<div class="line"><a name="l00453"></a><span class="lineno"> 453</span> </div>
<div class="line"><a name="l00454"></a><span class="lineno"> 454</span> </div>
<div class="line"><a name="l00455"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a48b9c68f68437b817726cedaf097a531"> 455</a></span>  <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a48b9c68f68437b817726cedaf097a531">null_cdlist</a>;</div>
<div class="line"><a name="l00456"></a><span class="lineno"> 456</span> </div>
<div class="line"><a name="l00457"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ab4cd6dafd73a1cdb2ce8d0bfa68975f5"> 457</a></span>  <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#ab4cd6dafd73a1cdb2ce8d0bfa68975f5">d_transThm</a>;</div>
<div class="line"><a name="l00458"></a><span class="lineno"> 458</span> </div>
<div class="line"><a name="l00459"></a><span class="lineno"> 459</span>  <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);</div>
<div class="line"><a name="l00460"></a><span class="lineno"> 460</span>  <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);</div>
<div class="line"><a name="l00461"></a><span class="lineno"> 461</span>  </div>
<div class="line"><a name="l00462"></a><span class="lineno"> 462</span>  </div>
<div class="line"><a name="l00463"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a0026da40c823471fb89c809d5429213f"> 463</a></span>  <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></div>
<div class="line"><a name="l00464"></a><span class="lineno"> 464</span>  </div>
<div class="line"><a name="l00465"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ab211a218c1b6d7f99ce2310730b27bbb"> 465</a></span>  <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></div>
<div class="line"><a name="l00466"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a0a9d848eb97d33e8c555015cb126c39b"> 466</a></span>  <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></div>
<div class="line"><a name="l00467"></a><span class="lineno"> 467</span> </div>
<div class="line"><a name="l00468"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#afeebec46ae80ed697b00a5da3e043576"> 468</a></span>  <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></div>
<div class="line"><a name="l00469"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a5d4d5c909890619d446f8e1563d86e60"> 469</a></span>  <a class="code" href="classCVC3_1_1CDO.html">CDO<size_t></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a5d4d5c909890619d446f8e1563d86e60">d_lastEqsUpdatePos</a>;</div>
<div class="line"><a name="l00470"></a><span class="lineno"> 470</span> </div>
<div class="line"><a name="l00471"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a66b5c3d369b6e969015c566d86014e46"> 471</a></span>  <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></div>
<div class="line"><a name="l00472"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#aecebd6c0ff45e853d495b3a940a34a65"> 472</a></span>  <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></div>
<div class="line"><a name="l00473"></a><span class="lineno"> 473</span> </div>
<div class="line"><a name="l00474"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#acc57bb5cdcafa8c1fbdf85c030e35d00"> 474</a></span>  <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>;</div>
<div class="line"><a name="l00475"></a><span class="lineno"> 475</span> </div>
<div class="line"><a name="l00476"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a33efe13ffba90a746bea195b8892a437"> 476</a></span>  <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>; </div>
<div class="line"><a name="l00477"></a><span class="lineno"> 477</span>  <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);</div>
<div class="line"><a name="l00478"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ab36ea36a9cc54b697a0d188f725558c1"> 478</a></span>  <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>;</div>
<div class="line"><a name="l00479"></a><span class="lineno"> 479</span> </div>
<div class="line"><a name="l00480"></a><span class="lineno"> 480</span>  <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,</div>
<div class="line"><a name="l00481"></a><span class="lineno"> 481</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm, </div>
<div class="line"><a name="l00482"></a><span class="lineno"> 482</span>  <span class="keywordtype">int</span> pos);</div>
<div class="line"><a name="l00483"></a><span class="lineno"> 483</span> </div>
<div class="line"><a name="l00484"></a><span class="lineno"> 484</span>  <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,</div>
<div class="line"><a name="l00485"></a><span class="lineno"> 485</span>  <span class="keyword">const</span> std::vector<Expr>& mtrigs, </div>
<div class="line"><a name="l00486"></a><span class="lineno"> 486</span>  <span class="keywordtype">int</span> cur_depth, </div>
<div class="line"><a name="l00487"></a><span class="lineno"> 487</span>  std::vector<std::vector<Expr> >& instSet,</div>
<div class="line"><a name="l00488"></a><span class="lineno"> 488</span>  std::vector<Expr>& cur_inst</div>
<div class="line"><a name="l00489"></a><span class="lineno"> 489</span>  );</div>
<div class="line"><a name="l00490"></a><span class="lineno"> 490</span> </div>
<div class="line"><a name="l00491"></a><span class="lineno"> 491</span>  <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, </div>
<div class="line"><a name="l00492"></a><span class="lineno"> 492</span>  <span class="keyword">const</span> std::vector<Expr>& border,</div>
<div class="line"><a name="l00493"></a><span class="lineno"> 493</span>  std::vector<std::vector<Expr> >& instSet</div>
<div class="line"><a name="l00494"></a><span class="lineno"> 494</span>  );</div>
<div class="line"><a name="l00495"></a><span class="lineno"> 495</span> </div>
<div class="line"><a name="l00496"></a><span class="lineno"> 496</span> </div>
<div class="line"><a name="l00497"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a99ff15c8d97f8c5539d744d077679bbd"> 497</a></span>  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>;</div>
<div class="line"><a name="l00498"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#aaab4c2084e0104f66d12fd9d08b9823b"> 498</a></span>  std::set<std::string> <a class="code" href="classCVC3_1_1TheoryQuant.html#aaab4c2084e0104f66d12fd9d08b9823b">cacheHead</a>;</div>
<div class="line"><a name="l00499"></a><span class="lineno"> 499</span> </div>
<div class="line"><a name="l00500"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ad705af0d0dad0e43422b8f2b6c7f6885"> 500</a></span>  <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></div>
<div class="line"><a name="l00501"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ab35f04d2883c028bd5a5abe0d7004e06"> 501</a></span>  <a class="code" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#ab35f04d2883c028bd5a5abe0d7004e06">d_allInstCount2</a> ; </div>
<div class="line"><a name="l00502"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a96b6c0364f1b8e2aa6f5156eb7bfe469"> 502</a></span>  <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></div>
<div class="line"><a name="l00503"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ab3e1ed0e8cc74fac887ded9f56a17f78"> 503</a></span>  <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></div>
<div class="line"><a name="l00504"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#aa6905effa7a717856118ed19f818e7f3"> 504</a></span>  <a class="code" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="code" href="classCVC3_1_1TheoryQuant.html#aa6905effa7a717856118ed19f818e7f3">d_abInstCount</a>;</div>
<div class="line"><a name="l00505"></a><span class="lineno"> 505</span> </div>
<div class="line"><a name="l00506"></a><span class="lineno"> 506</span>  <span class="comment">// size_t d_totalInstCount;</span></div>
<div class="line"><a name="l00507"></a><span class="lineno"> 507</span>  <span class="comment">// size_t d_trueInstCount;</span></div>
<div class="line"><a name="l00508"></a><span class="lineno"> 508</span>  <span class="comment">// size_t d_abInstCount;</span></div>
<div class="line"><a name="l00509"></a><span class="lineno"> 509</span>  </div>
<div class="line"><a name="l00510"></a><span class="lineno"> 510</span> </div>
<div class="line"><a name="l00511"></a><span class="lineno"> 511</span> </div>
<div class="line"><a name="l00512"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a4f00e0765ee64e22e984587a4579bde6"> 512</a></span>  std::vector<Theorem> <a class="code" href="classCVC3_1_1TheoryQuant.html#a4f00e0765ee64e22e984587a4579bde6">d_cacheTheorem</a>;</div>
<div class="line"><a name="l00513"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a65a292cd648bd4af31f19ff9c7532ea4"> 513</a></span>  <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a65a292cd648bd4af31f19ff9c7532ea4">d_cacheThmPos</a>;</div>
<div class="line"><a name="l00514"></a><span class="lineno"> 514</span> </div>
<div class="line"><a name="l00515"></a><span class="lineno"> 515</span>  <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);</div>
<div class="line"><a name="l00516"></a><span class="lineno"> 516</span> </div>
<div class="line"><a name="l00517"></a><span class="lineno"> 517</span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a66e269df47eb8d5827b10c15937c6432">sendInstNew</a>();</div>
<div class="line"><a name="l00518"></a><span class="lineno"> 518</span> </div>
<div class="line"><a name="l00519"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#aabd606d2811108af2cd562c63d9cfbdd"> 519</a></span>  <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></div>
<div class="line"><a name="l00520"></a><span class="lineno"> 520</span>  <span class="comment">//map univ to the trig, gterm and result</span></div>
<div class="line"><a name="l00521"></a><span class="lineno"> 521</span> </div>
<div class="line"><a name="l00522"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#acb9e190ab07b49b4d1e62c4edbf75ca5"> 522</a></span>  <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<int></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#acb9e190ab07b49b4d1e62c4edbf75ca5">d_thmCount</a>; </div>
<div class="line"><a name="l00523"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a3e97f6a9759fca392443aee3d9ef0c0d"> 523</a></span>  <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<size_t></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a3e97f6a9759fca392443aee3d9ef0c0d">d_totalThmCount</a>; </div>
<div class="line"><a name="l00524"></a><span class="lineno"> 524</span> </div>
<div class="line"><a name="l00525"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ad8356f54f8d013951ebfd9480e940867"> 525</a></span>  <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></div>
<div class="line"><a name="l00526"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a7e78eaa04046525a5655c6b012948357"> 526</a></span>  <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></div>
<div class="line"><a name="l00527"></a><span class="lineno"> 527</span> </div>
<div class="line"><a name="l00528"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a7e9807fc95db1efef6f3ac955a034f85"> 528</a></span>  <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></div>
<div class="line"><a name="l00529"></a><span class="lineno"> 529</span> </div>
<div class="line"><a name="l00530"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a66b101a27d3ee2d8494a6cb268e1ef8c"> 530</a></span>  <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></div>
<div class="line"><a name="l00531"></a><span class="lineno"> 531</span> </div>
<div class="line"><a name="l00532"></a><span class="lineno"> 532</span>  </div>
<div class="line"><a name="l00533"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#aa05d5ab159323722c0c86f7bbbd4fa73"> 533</a></span>  <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>;</div>
<div class="line"><a name="l00534"></a><span class="lineno"> 534</span>  <span class="comment">//std::map<Expr, std::vector<Expr> > d_subTermsMap;</span></div>
<div class="line"><a name="l00535"></a><span class="lineno"> 535</span>  <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);</div>
<div class="line"><a name="l00536"></a><span class="lineno"> 536</span> </div>
<div class="line"><a name="l00537"></a><span class="lineno"> 537</span> </div>
<div class="line"><a name="l00538"></a><span class="lineno"> 538</span>  <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);</div>
<div class="line"><a name="l00539"></a><span class="lineno"> 539</span>  <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);</div>
<div class="line"><a name="l00540"></a><span class="lineno"> 540</span>  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);</div>
<div class="line"><a name="l00541"></a><span class="lineno"> 541</span>  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);</div>
<div class="line"><a name="l00542"></a><span class="lineno"> 542</span>  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);</div>
<div class="line"><a name="l00543"></a><span class="lineno"> 543</span> </div>
<div class="line"><a name="l00544"></a><span class="lineno"> 544</span>  <span class="comment">//ExprMap<int > d_thmTimes; </span></div>
<div class="line"><a name="l00545"></a><span class="lineno"> 545</span>  <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>); </div>
<div class="line"><a name="l00546"></a><span class="lineno"> 546</span>  <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);</div>
<div class="line"><a name="l00547"></a><span class="lineno"> 547</span>  <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);</div>
<div class="line"><a name="l00548"></a><span class="lineno"> 548</span>  <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, </div>
<div class="line"><a name="l00549"></a><span class="lineno"> 549</span>  <a class="code" href="classCVC3_1_1Trigger.html">Trigger</a>& trig,</div>
<div class="line"><a name="l00550"></a><span class="lineno"> 550</span>  <span class="keyword">const</span> std::vector<Expr>& binds, </div>
<div class="line"><a name="l00551"></a><span class="lineno"> 551</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm</div>
<div class="line"><a name="l00552"></a><span class="lineno"> 552</span>  );</div>
<div class="line"><a name="l00553"></a><span class="lineno"> 553</span>  </div>
<div class="line"><a name="l00554"></a><span class="lineno"> 554</span>  <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>);</div>
<div class="line"><a name="l00555"></a><span class="lineno"> 555</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a52ca7d3454b8359a1aee518b57f9720a">synCheckSat</a>(<span class="keywordtype">bool</span>);</div>
<div class="line"><a name="l00556"></a><span class="lineno"> 556</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#afe19c7bd637cb0c5fad7ab0494135010">semCheckSat</a>(<span class="keywordtype">bool</span>);</div>
<div class="line"><a name="l00557"></a><span class="lineno"> 557</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a8ccfdf955d67688e51dc9bcbb3911a2d">naiveCheckSat</a>(<span class="keywordtype">bool</span>);</div>
<div class="line"><a name="l00558"></a><span class="lineno"> 558</span> </div>
<div class="line"><a name="l00559"></a><span class="lineno"> 559</span>  <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);</div>
<div class="line"><a name="l00560"></a><span class="lineno"> 560</span>  <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);</div>
<div class="line"><a name="l00561"></a><span class="lineno"> 561</span> </div>
<div class="line"><a name="l00562"></a><span class="lineno"> 562</span>  <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);</div>
<div class="line"><a name="l00563"></a><span class="lineno"> 563</span> </div>
<div class="line"><a name="l00564"></a><span class="lineno"> 564</span>  <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);</div>
<div class="line"><a name="l00565"></a><span class="lineno"> 565</span>  </div>
<div class="line"><a name="l00566"></a><span class="lineno"> 566</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#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);</div>
<div class="line"><a name="l00567"></a><span class="lineno"> 567</span> </div>
<div class="line"><a name="l00568"></a><span class="lineno"> 568</span>  <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 );</div>
<div class="line"><a name="l00569"></a><span class="lineno"> 569</span>  <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);</div>
<div class="line"><a name="l00570"></a><span class="lineno"> 570</span> </div>
<div class="line"><a name="l00571"></a><span class="lineno"> 571</span>  <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);</div>
<div class="line"><a name="l00572"></a><span class="lineno"> 572</span> </div>
<div class="line"><a name="l00573"></a><span class="lineno"> 573</span>  <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);</div>
<div class="line"><a name="l00574"></a><span class="lineno"> 574</span> </div>
<div class="line"><a name="l00575"></a><span class="lineno"> 575</span> </div>
<div class="line"><a name="l00576"></a><span class="lineno"> 576</span>  <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,</div>
<div class="line"><a name="l00577"></a><span class="lineno"> 577</span>  <span class="keyword">const</span> std::vector<Expr> & boundVars,</div>
<div class="line"><a name="l00578"></a><span class="lineno"> 578</span>  std::vector<std::vector<Expr> >& instBindsTerm,</div>
<div class="line"><a name="l00579"></a><span class="lineno"> 579</span>  std::vector<Expr>& instGterm,</div>
<div class="line"><a name="l00580"></a><span class="lineno"> 580</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allterms, </div>
<div class="line"><a name="l00581"></a><span class="lineno"> 581</span>  <span class="keywordtype">size_t</span> tBegin);</div>
<div class="line"><a name="l00582"></a><span class="lineno"> 582</span>  <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,</div>
<div class="line"><a name="l00583"></a><span class="lineno"> 583</span>  <span class="keyword">const</span> std::vector<Expr> & boundVars,</div>
<div class="line"><a name="l00584"></a><span class="lineno"> 584</span>  std::vector<std::vector<Expr> >& instBinds,</div>
<div class="line"><a name="l00585"></a><span class="lineno"> 585</span>  std::vector<Expr>& instGterms,</div>
<div class="line"><a name="l00586"></a><span class="lineno"> 586</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allterms, </div>
<div class="line"><a name="l00587"></a><span class="lineno"> 587</span>  <span class="keywordtype">size_t</span> tBegin);</div>
<div class="line"><a name="l00588"></a><span class="lineno"> 588</span> </div>
<div class="line"><a name="l00589"></a><span class="lineno"> 589</span>  <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,</div>
<div class="line"><a name="l00590"></a><span class="lineno"> 590</span>  <span class="keyword">const</span> std::vector<Expr> & boundVars,</div>
<div class="line"><a name="l00591"></a><span class="lineno"> 591</span>  std::vector<std::vector<Expr> >& instBinds,</div>
<div class="line"><a name="l00592"></a><span class="lineno"> 592</span>  std::vector<Expr>& instGterms,</div>
<div class="line"><a name="l00593"></a><span class="lineno"> 593</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& gterm);</div>
<div class="line"><a name="l00594"></a><span class="lineno"> 594</span> </div>
<div class="line"><a name="l00595"></a><span class="lineno"> 595</span>  <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);</div>
<div class="line"><a name="l00596"></a><span class="lineno"> 596</span>  <span class="comment">// void matchListOld(const Expr& gterm);</span></div>
<div class="line"><a name="l00597"></a><span class="lineno"> 597</span>  <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,</div>
<div class="line"><a name="l00598"></a><span class="lineno"> 598</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& list,</div>
<div class="line"><a name="l00599"></a><span class="lineno"> 599</span>  <span class="keywordtype">size_t</span> gbegin,</div>
<div class="line"><a name="l00600"></a><span class="lineno"> 600</span>  <span class="keywordtype">size_t</span> gend);</div>
<div class="line"><a name="l00601"></a><span class="lineno"> 601</span>  </div>
<div class="line"><a name="l00602"></a><span class="lineno"> 602</span>  <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);</div>
<div class="line"><a name="l00603"></a><span class="lineno"> 603</span>  <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);</div>
<div class="line"><a name="l00604"></a><span class="lineno"> 604</span> </div>
<div class="line"><a name="l00605"></a><span class="lineno"> 605</span>  <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>);</div>
<div class="line"><a name="l00606"></a><span class="lineno"> 606</span> </div>
<div class="line"><a name="l00607"></a><span class="lineno"> 607</span>  <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, </div>
<div class="line"><a name="l00608"></a><span class="lineno"> 608</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& vterm, </div>
<div class="line"><a name="l00609"></a><span class="lineno"> 609</span>  std::vector<<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> >& binds, </div>
<div class="line"><a name="l00610"></a><span class="lineno"> 610</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Trigger.html">Trigger</a>& trig);</div>
<div class="line"><a name="l00611"></a><span class="lineno"> 611</span> </div>
<div class="line"><a name="l00612"></a><span class="lineno"> 612</span>  <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, </div>
<div class="line"><a name="l00613"></a><span class="lineno"> 613</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& vterm, </div>
<div class="line"><a name="l00614"></a><span class="lineno"> 614</span>  std::vector<<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> >& binds, </div>
<div class="line"><a name="l00615"></a><span class="lineno"> 615</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Trigger.html">Trigger</a>& trig);</div>
<div class="line"><a name="l00616"></a><span class="lineno"> 616</span>  </div>
<div class="line"><a name="l00617"></a><span class="lineno"> 617</span>  <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, </div>
<div class="line"><a name="l00618"></a><span class="lineno"> 618</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& vterm, </div>
<div class="line"><a name="l00619"></a><span class="lineno"> 619</span>  std::vector<<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> >& binds, </div>
<div class="line"><a name="l00620"></a><span class="lineno"> 620</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Trigger.html">Trigger</a>& trig);</div>
<div class="line"><a name="l00621"></a><span class="lineno"> 621</span> </div>
<div class="line"><a name="l00622"></a><span class="lineno"> 622</span> </div>
<div class="line"><a name="l00623"></a><span class="lineno"> 623</span> </div>
<div class="line"><a name="l00624"></a><span class="lineno"> 624</span>  <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, </div>
<div class="line"><a name="l00625"></a><span class="lineno"> 625</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& vterm, </div>
<div class="line"><a name="l00626"></a><span class="lineno"> 626</span>  std::vector<<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> >& binds, </div>
<div class="line"><a name="l00627"></a><span class="lineno"> 627</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Trigger.html">Trigger</a>& trig);</div>
<div class="line"><a name="l00628"></a><span class="lineno"> 628</span> </div>
<div class="line"><a name="l00629"></a><span class="lineno"> 629</span> </div>
<div class="line"><a name="l00630"></a><span class="lineno"> 630</span>  <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);</div>
<div class="line"><a name="l00631"></a><span class="lineno"> 631</span> </div>
<div class="line"><a name="l00632"></a><span class="lineno"> 632</span>  <span class="comment">// inline bool matchChild(const Expr& gterm, const Expr& vterm, ExprMap<Expr>& env);</span></div>
<div class="line"><a name="l00633"></a><span class="lineno"> 633</span>  <span class="comment">// inline void matchChild(const Expr& gterm, const Expr& vterm, std::vector<ExprMap<Expr> >& env);</span></div>
<div class="line"><a name="l00634"></a><span class="lineno"> 634</span>  </div>
<div class="line"><a name="l00635"></a><span class="lineno"> 635</span>  <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);</div>
<div class="line"><a name="l00636"></a><span class="lineno"> 636</span> </div>
<div class="line"><a name="l00637"></a><span class="lineno"> 637</span>  <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);</div>
<div class="line"><a name="l00638"></a><span class="lineno"> 638</span>  <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);</div>
<div class="line"><a name="l00639"></a><span class="lineno"> 639</span>  <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);</div>
<div class="line"><a name="l00640"></a><span class="lineno"> 640</span>  <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);</div>
<div class="line"><a name="l00641"></a><span class="lineno"> 641</span> </div>
<div class="line"><a name="l00642"></a><span class="lineno"> 642</span>  <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>);</div>
<div class="line"><a name="l00643"></a><span class="lineno"> 643</span>  <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);</div>
<div class="line"><a name="l00644"></a><span class="lineno"> 644</span> </div>
<div class="line"><a name="l00645"></a><span class="lineno"> 645</span> </div>
<div class="line"><a name="l00646"></a><span class="lineno"> 646</span>  <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);</div>
<div class="line"><a name="l00647"></a><span class="lineno"> 647</span> </div>
<div class="line"><a name="l00648"></a><span class="lineno"> 648</span>  <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, </div>
<div class="line"><a name="l00649"></a><span class="lineno"> 649</span>  std::vector<Expr> & boundVars, </div>
<div class="line"><a name="l00650"></a><span class="lineno"> 650</span>  std::vector<std::vector<Expr> >& instBinds, </div>
<div class="line"><a name="l00651"></a><span class="lineno"> 651</span>  std::vector<Expr>& instGterms, </div>
<div class="line"><a name="l00652"></a><span class="lineno"> 652</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allterms, </div>
<div class="line"><a name="l00653"></a><span class="lineno"> 653</span>  <span class="keywordtype">size_t</span> tBegin); </div>
<div class="line"><a name="l00654"></a><span class="lineno"> 654</span>  </div>
<div class="line"><a name="l00655"></a><span class="lineno"> 655</span>  <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, </div>
<div class="line"><a name="l00656"></a><span class="lineno"> 656</span>  <span class="keyword">const</span> std::vector<Expr> & boundVars, </div>
<div class="line"><a name="l00657"></a><span class="lineno"> 657</span>  std::vector<std::vector<Expr> >& instBinds, </div>
<div class="line"><a name="l00658"></a><span class="lineno"> 658</span>  std::vector<Expr>& instGterms, </div>
<div class="line"><a name="l00659"></a><span class="lineno"> 659</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allterms, </div>
<div class="line"><a name="l00660"></a><span class="lineno"> 660</span>  <span class="keywordtype">size_t</span> tBegin); </div>
<div class="line"><a name="l00661"></a><span class="lineno"> 661</span> </div>
<div class="line"><a name="l00662"></a><span class="lineno"> 662</span> </div>
<div class="line"><a name="l00663"></a><span class="lineno"> 663</span>  <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,</div>
<div class="line"><a name="l00664"></a><span class="lineno"> 664</span>  std::vector<Expr>& bVars,</div>
<div class="line"><a name="l00665"></a><span class="lineno"> 665</span>  std::vector<std::vector<Expr> >& instSet,</div>
<div class="line"><a name="l00666"></a><span class="lineno"> 666</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>& allterms, </div>
<div class="line"><a name="l00667"></a><span class="lineno"> 667</span>  <span class="keywordtype">size_t</span> tBegin);</div>
<div class="line"><a name="l00668"></a><span class="lineno"> 668</span>  </div>
<div class="line"><a name="l00669"></a><span class="lineno"> 669</span>  <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,</div>
<div class="line"><a name="l00670"></a><span class="lineno"> 670</span>  <span class="keyword">const</span> std::vector<Expr>& bVars,</div>
<div class="line"><a name="l00671"></a><span class="lineno"> 671</span>  std::vector<Expr>& newInst,</div>
<div class="line"><a name="l00672"></a><span class="lineno"> 672</span>  std::set<std::vector<Expr> >& instSet);</div>
<div class="line"><a name="l00673"></a><span class="lineno"> 673</span>  </div>
<div class="line"><a name="l00674"></a><span class="lineno"> 674</span>  <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,</div>
<div class="line"><a name="l00675"></a><span class="lineno"> 675</span>  std::vector<Expr>& bVars,</div>
<div class="line"><a name="l00676"></a><span class="lineno"> 676</span>  std::set<std::vector<Expr> >& instSet,</div>
<div class="line"><a name="l00677"></a><span class="lineno"> 677</span>  <span class="keywordtype">size_t</span> tBegin);</div>
<div class="line"><a name="l00678"></a><span class="lineno"> 678</span> </div>
<div class="line"><a name="l00679"></a><span class="lineno"> 679</span>  <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);</div>
<div class="line"><a name="l00680"></a><span class="lineno"> 680</span>  <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);</div>
<div class="line"><a name="l00681"></a><span class="lineno"> 681</span>  </div>
<div class="line"><a name="l00682"></a><span class="lineno"> 682</span> </div>
<div class="line"><a name="l00683"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#aa7c01b86ccf4a315711e7d09c47c71cd"> 683</a></span>  <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;</div>
<div class="line"><a name="l00684"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#af51bfd58e92b284832770c68c1685ab6"> 684</a></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#af51bfd58e92b284832770c68c1685ab6">d_mybvs</a>[<a class="code" href="classCVC3_1_1TheoryQuant.html#aa7c01b86ccf4a315711e7d09c47c71cd">MAX_TRIG_BVS</a>];</div>
<div class="line"><a name="l00685"></a><span class="lineno"> 685</span>  </div>
<div class="line"><a name="l00686"></a><span class="lineno"> 686</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#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);</div>
<div class="line"><a name="l00687"></a><span class="lineno"> 687</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#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);</div>
<div class="line"><a name="l00688"></a><span class="lineno"> 688</span> </div>
<div class="line"><a name="l00689"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#ac1dc98cab588b291d74859884fc25f5e"> 689</a></span>  <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>;</div>
<div class="line"><a name="l00690"></a><span class="lineno"> 690</span>  </div>
<div class="line"><a name="l00691"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#a0dd41bdd27bbd7c71fc45749fb80ff96"> 691</a></span>  <a class="code" href="classCVC3_1_1CDList.html">CDList<Trigger></a> <a class="code" href="classCVC3_1_1TheoryQuant.html#a0dd41bdd27bbd7c71fc45749fb80ff96">d_alltrig_list</a>;</div>
<div class="line"><a name="l00692"></a><span class="lineno"> 692</span> </div>
<div class="line"><a name="l00693"></a><span class="lineno"> 693</span>  <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,</div>
<div class="line"><a name="l00694"></a><span class="lineno"> 694</span>  <a class="code" href="classCVC3_1_1Trigger.html">Trigger</a> trig, </div>
<div class="line"><a name="l00695"></a><span class="lineno"> 695</span>  <span class="keyword">const</span> std::vector<Expr> thmBVs, </div>
<div class="line"><a name="l00696"></a><span class="lineno"> 696</span>  <span class="keywordtype">size_t</span> univ_id);</div>
<div class="line"><a name="l00697"></a><span class="lineno"> 697</span>  </div>
<div class="line"><a name="l00698"></a><span class="lineno"> 698</span>  <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);</div>
<div class="line"><a name="l00699"></a><span class="lineno"> 699</span> </div>
<div class="line"><a name="l00700"></a><span class="lineno"> 700</span>  <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);</div>
<div class="line"><a name="l00701"></a><span class="lineno"> 701</span>  <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) ; </div>
<div class="line"><a name="l00702"></a><span class="lineno"> 702</span> </div>
<div class="line"><a name="l00703"></a><span class="lineno"> 703</span>  <span class="comment">// std::string getHead(const Expr& e) ;</span></div>
<div class="line"><a name="l00704"></a><span class="lineno"> 704</span>  <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,</div>
<div class="line"><a name="l00705"></a><span class="lineno"> 705</span>  <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm, </div>
<div class="line"><a name="l00706"></a><span class="lineno"> 706</span>  <span class="keywordtype">size_t</span> univs_id);</div>
<div class="line"><a name="l00707"></a><span class="lineno"> 707</span> </div>
<div class="line"><a name="l00708"></a><span class="lineno"> 708</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a3417f85c140e902187726b52a4628966">saveContext</a>();</div>
<div class="line"><a name="l00709"></a><span class="lineno"> 709</span> </div>
<div class="line"><a name="l00710"></a><span class="lineno"> 710</span> <span class="comment"></span></div>
<div class="line"><a name="l00711"></a><span class="lineno"> 711</span> <span class="comment"> /*! \brief categorizes all the terms contained in an expressions by</span></div>
<div class="line"><a name="l00712"></a><span class="lineno"> 712</span> <span class="comment"> *type.</span></div>
<div class="line"><a name="l00713"></a><span class="lineno"> 713</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00714"></a><span class="lineno"> 714</span> <span class="comment"> * Updates d_contextTerms, d_contextMap, d_contextCache accordingly.</span></div>
<div class="line"><a name="l00715"></a><span class="lineno"> 715</span> <span class="comment"> * returns true if the expression does not contain bound variables, false</span></div>
<div class="line"><a name="l00716"></a><span class="lineno"> 716</span> <span class="comment"> * otherwise.</span></div>
<div class="line"><a name="l00717"></a><span class="lineno"> 717</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00718"></a><span class="lineno"> 718</span> </div>
<div class="line"><a name="l00719"></a><span class="lineno"> 719</span>  </div>
<div class="line"><a name="l00720"></a><span class="lineno"> 720</span>  <span class="keyword">public</span>:</div>
<div class="line"><a name="l00721"></a><span class="lineno"> 721</span>  <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></div>
<div class="line"><a name="l00722"></a><span class="lineno"> 722</span> <span class="comment"></span> <a class="code" href="classCVC3_1_1TheoryQuant.html#a653f0e36db9a5c07024565e77d01abb0" title="Destructor.">~TheoryQuant</a>(); <span class="comment">//! Destructor</span></div>
<div class="line"><a name="l00723"></a><span class="lineno"> 723</span> <span class="comment"></span></div>
<div class="line"><a name="l00724"></a><span class="lineno"> 724</span>  <a class="code" href="classCVC3_1_1QuantProofRules.html">QuantProofRules</a>* <a class="code" href="classCVC3_1_1TheoryQuant.html#a493eb80061815c95bab507f41343b260" title="Destructor.">createProofRules</a>();</div>
<div class="line"><a name="l00725"></a><span class="lineno"> 725</span>  </div>
<div class="line"><a name="l00726"></a><span class="lineno"> 726</span> </div>
<div class="line"><a name="l00727"></a><span class="lineno"> 727</span>  </div>
<div class="line"><a name="l00728"></a><span class="lineno"><a class="code" href="classCVC3_1_1TheoryQuant.html#aae3f95b1c6505b090105271bbccd7408"> 728</a></span>  <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></div>
<div class="line"><a name="l00729"></a><span class="lineno"> 729</span> <span class="comment"></span> <span class="comment"></span></div>
<div class="line"><a name="l00730"></a><span class="lineno"> 730</span> <span class="comment"> /*! \brief Theory interface function to assert quantified formulas</span></div>
<div class="line"><a name="l00731"></a><span class="lineno"> 731</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00732"></a><span class="lineno"> 732</span> <span class="comment"> * pushes in negations and converts to either universally or existentially </span></div>
<div class="line"><a name="l00733"></a><span class="lineno"> 733</span> <span class="comment"> * quantified theorems. Universals are stored in a database while </span></div>
<div class="line"><a name="l00734"></a><span class="lineno"> 734</span> <span class="comment"> * existentials are enqueued to be handled by the search engine.</span></div>
<div class="line"><a name="l00735"></a><span class="lineno"> 735</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00736"></a><span class="lineno"> 736</span>  <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); </div>
<div class="line"><a name="l00737"></a><span class="lineno"> 737</span>  </div>
<div class="line"><a name="l00738"></a><span class="lineno"> 738</span> </div>
<div class="line"><a name="l00739"></a><span class="lineno"> 739</span>  <span class="comment">/* \brief Checks the satisfiability of the universal theorems stored in a </span></div>
<div class="line"><a name="l00740"></a><span class="lineno"> 740</span> <span class="comment"> * databse by instantiating them.</span></div>
<div class="line"><a name="l00741"></a><span class="lineno"> 741</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00742"></a><span class="lineno"> 742</span> <span class="comment"> * There are two algorithms that the checkSat function uses to find </span></div>
<div class="line"><a name="l00743"></a><span class="lineno"> 743</span> <span class="comment"> * instnatiations. The first algortihm looks for instanitations in a saved </span></div>
<div class="line"><a name="l00744"></a><span class="lineno"> 744</span> <span class="comment"> * database of previous instantiations that worked in proving an earlier</span></div>
<div class="line"><a name="l00745"></a><span class="lineno"> 745</span> <span class="comment"> * theorem unsatifiable. All of the class variables with the word saved in</span></div>
<div class="line"><a name="l00746"></a><span class="lineno"> 746</span> <span class="comment"> * them are for the use of this algorithm. The other algorithm uses terms </span></div>
<div class="line"><a name="l00747"></a><span class="lineno"> 747</span> <span class="comment"> * found in the assertions that exist in the particular context when </span></div>
<div class="line"><a name="l00748"></a><span class="lineno"> 748</span> <span class="comment"> * checkSat is called. All of the class variables with the word context in</span></div>
<div class="line"><a name="l00749"></a><span class="lineno"> 749</span> <span class="comment"> * them are used for the second algorithm.</span></div>
<div class="line"><a name="l00750"></a><span class="lineno"> 750</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00751"></a><span class="lineno"> 751</span>  <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);</div>
<div class="line"><a name="l00752"></a><span class="lineno"> 752</span>  <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); </div>
<div class="line"><a name="l00753"></a><span class="lineno"> 753</span>  </div>
<div class="line"><a name="l00754"></a><span class="lineno"> 754</span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1TheoryQuant.html#aa3dcc4288e4738de508875ecccbe32eb">help</a>(<span class="keywordtype">int</span> i);</div>
<div class="line"><a name="l00755"></a><span class="lineno"> 755</span>  </div>
<div class="line"><a name="l00756"></a><span class="lineno"> 756</span>  <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></div>
<div class="line"><a name="l00757"></a><span class="lineno"> 757</span> <span class="comment"> /*!\brief Used to notify the quantifier algorithm of possible </span></div>
<div class="line"><a name="l00758"></a><span class="lineno"> 758</span> <span class="comment"> * instantiations that were used in proving a context inconsistent.</span></div>
<div class="line"><a name="l00759"></a><span class="lineno"> 759</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00760"></a><span class="lineno"> 760</span>  <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);</div>
<div class="line"><a name="l00761"></a><span class="lineno"> 761</span>  <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></div>
<div class="line"><a name="l00762"></a><span class="lineno"> 762</span> <span class="comment"> //! computes the type of a quantified term. Always a boolean.</span></div>
<div class="line"><a name="l00763"></a><span class="lineno"> 763</span> <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); </div>
<div class="line"><a name="l00764"></a><span class="lineno"> 764</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#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);</div>
<div class="line"><a name="l00765"></a><span class="lineno"> 765</span>  </div>
<div class="line"><a name="l00766"></a><span class="lineno"> 766</span>  <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);</div>
<div class="line"><a name="l00767"></a><span class="lineno"> 767</span> </div>
<div class="line"><a name="l00768"></a><span class="lineno"> 768</span>  <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);</div>
<div class="line"><a name="l00769"></a><span class="lineno"> 769</span>  };</div>
<div class="line"><a name="l00770"></a><span class="lineno"> 770</span>  </div>
<div class="line"><a name="l00771"></a><span class="lineno"> 771</span> }</div>
<div class="line"><a name="l00772"></a><span class="lineno"> 772</span> </div>
<div class="line"><a name="l00773"></a><span class="lineno"> 773</span> <span class="preprocessor">#endif</span></div>
</div><!-- fragment --></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:15 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
