<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: theory_quant.cpp File Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><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>
<div class="header">
<div class="summary">
<a href="#nested-classes">Classes</a> |
<a href="#func-members">Functions</a> |
<a href="#var-members">Variables</a> </div>
<div class="headertitle">
<div class="title">theory_quant.cpp File Reference</div> </div>
</div>
<div class="contents">
<div class="textblock"><code>#include "<a class="el" href="theory__quant_8h_source.html">theory_quant.h</a>"</code><br/>
<code>#include "<a class="el" href="theory__arith_8h_source.html">theory_arith.h</a>"</code><br/>
<code>#include "<a class="el" href="theory__array_8h_source.html">theory_array.h</a>"</code><br/>
<code>#include "<a class="el" href="typecheck__exception_8h_source.html">typecheck_exception.h</a>"</code><br/>
<code>#include "<a class="el" href="parser__exception_8h_source.html">parser_exception.h</a>"</code><br/>
<code>#include "<a class="el" href="smtlib__exception_8h_source.html">smtlib_exception.h</a>"</code><br/>
<code>#include "<a class="el" href="quant__proof__rules_8h_source.html">quant_proof_rules.h</a>"</code><br/>
<code>#include "<a class="el" href="theory__core_8h_source.html">theory_core.h</a>"</code><br/>
<code>#include "<a class="el" href="command__line__flags_8h_source.html">command_line_flags.h</a>"</code><br/>
<code>#include "<a class="el" href="vcl_8h_source.html">vcl.h</a>"</code><br/>
<code>#include <string></code><br/>
<code>#include <string.h></code><br/>
<code>#include <algorithm></code><br/>
<code>#include "<a class="el" href="assumptions_8h_source.html">assumptions.h</a>"</code><br/>
</div>
<p><a href="theory__quant_8cpp_source.html">Go to the source code of this file.</a></p>
<h2><a name="nested-classes"></a>
Classes</h2>
<ul>
<li>class <a class="el" href="classrecCompleteInster.html">recCompleteInster</a>
</ul>
<h2><a name="func-members"></a>
Functions</h2>
<ul>
<li>std::string <a class="el" href="theory__quant_8cpp.html#ac540b3d9d2b6b96fb7e8ca2df7ccb678">vectorExpr2string</a> (const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &vec)
<li>bool <a class="el" href="theory__quant_8cpp.html#ae2ef120eda296c8008688042714b2fc9">isSysPred</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li>bool <a class="el" href="theory__quant_8cpp.html#ad02abacd5bb6a0e7dc5fe4f2d9300dfe">canGetHead</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li>bool <a class="el" href="theory__quant_8cpp.html#abfd229253e2b4548aec82a3c604175a8">isSimpleTrig</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &t)
<li>bool <a class="el" href="theory__quant_8cpp.html#a96efdadd956037ab4b1ca55b5d54faea">isSuperSimpleTrig</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &t)
<li>bool <a class="el" href="theory__quant_8cpp.html#a45fb04ec0356578e698622eb7ac59d04">usefulInMatch</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li>static void <a class="el" href="theory__quant_8cpp.html#ac5b507b0c113276077e5a7ff29fc7604">recursiveGetSubTrig</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &res)
<li>std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > <a class="el" href="theory__quant_8cpp.html#a284771b2ec3f2c7410dce560633123a6">getSubTrig</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li>static void <a class="el" href="theory__quant_8cpp.html#a28d6afee25aa51bcd4f5d41179cefc2b">recGetSubTerms</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &res)
<li>int <a class="el" href="theory__quant_8cpp.html#adccadd475af73b2fb9c61f33735977a0">recursiveExprScore</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li>int <a class="el" href="theory__quant_8cpp.html#aa0227fe4666655a02e5e43c9650b5f7d">exprScore</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li>static bool <a class="el" href="theory__quant_8cpp.html#a779ed57bff05a3a131337d749e91db15">recursiveGetBoundVars</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &result)
<dl class="el"><dd class="mdescRight">get the bound vars in term e, <a href="#a779ed57bff05a3a131337d749e91db15"></a><br/></dl><li>std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > <a class="el" href="theory__quant_8cpp.html#ab0c1ea5ae3c53ec0bbf2e04b1f33e757">getBoundVars</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">get bound vars in term e, <a href="#ab0c1ea5ae3c53ec0bbf2e04b1f33e757"></a><br/></dl><li>void <a class="el" href="theory__quant_8cpp.html#ae79a351634c32cc5b514d37efb810677">findPolarity</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< <a class="el" href="namespaceCVC3.html#aa6262a73c1109f35a6c533421f5dd393">Polarity</a> > &res, <a class="el" href="namespaceCVC3.html#aa6262a73c1109f35a6c533421f5dd393">Polarity</a> pol)
<li>bool <a class="el" href="theory__quant_8cpp.html#a4a97be803d167c43000680f2008abf21">isUniterpFunc</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li>bool <a class="el" href="theory__quant_8cpp.html#a57148644393433bb1267393b8a18e785">isGround</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li>void <a class="el" href="theory__quant_8cpp.html#ab2eabe9580c3d9a962173108df445a51">findPolarityAtomic</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< <a class="el" href="namespaceCVC3.html#aa6262a73c1109f35a6c533421f5dd393">Polarity</a> > &res, <a class="el" href="namespaceCVC3.html#aa6262a73c1109f35a6c533421f5dd393">Polarity</a> pol)
<li>void <a class="el" href="theory__quant_8cpp.html#a964c839e8f67da1a35acc097463b5f7e">flatAnds</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &ands, vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &results)
<li>bool <a class="el" href="theory__quant_8cpp.html#a28f516e79b8ffb0e4e998eac196bd9cc">isGoodSysPredTrigger</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li>bool <a class="el" href="theory__quant_8cpp.html#aa98360024a0b2da76e6a57210efea027">isGoodFullTrigger</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &bVarsThm)
<li>bool <a class="el" href="theory__quant_8cpp.html#ae4d6f79b2b5eb00c102cd9cd325ecf77">isGoodMultiTrigger</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &bVarsThm, int offset)
<li>bool <a class="el" href="theory__quant_8cpp.html#acb48e181095d3c2c86486677a1b9937d">isGoodPartTrigger</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &bVarsThm)
<li>static bool <a class="el" href="theory__quant_8cpp.html#ad577dba7e2b661fa6caa2355ca90f0d6">recursiveGetPartTriggers</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &res)
<li>std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > <a class="el" href="theory__quant_8cpp.html#acaa6717f00a26724ea7e9f5bfd1fa656">getPartTriggers</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li>int <a class="el" href="theory__quant_8cpp.html#ae0833342972b17d872e2d6f4f45b3812">trigInitScore</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li>bool <a class="el" href="theory__quant_8cpp.html#a8822f0191c9cafc521b190dbc29ce8bd">goodMultiTriggers</a> (const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &exprs, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > bVars)
<li>size_t <a class="el" href="theory__quant_8cpp.html#a68eed73f49f190f0b990027b28688f7f">locVar</a> (const vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &bvsThm, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &bv)
<li>int <a class="el" href="theory__quant_8cpp.html#a8ba2c2ab53110996e9faf4d432a3af7d">hasMoreBVs</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &thm)
<dl class="el"><dd class="mdescRight">test if a sub-term contains more bounded vars than quantified by out-most quantifier. <a href="#a8ba2c2ab53110996e9faf4d432a3af7d"></a><br/></dl><li>bool <a class="el" href="theory__quant_8cpp.html#ac9940420b1f3427ebe821902adbb578d">isIntx</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const <a class="el" href="classCVC3_1_1Rational.html">Rational</a> &x)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="theory__quant_8cpp.html#a4564697c1b2ea1e3a70ef36383ca1c41">getLeft</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="theory__quant_8cpp.html#a9162c5e3cbe41ca756947718e983180b">getRight</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li>bool <a class="el" href="theory__quant_8cpp.html#a438706926ba67238b44f3186b511b49f">cmpExpr</a> (<a class="el" href="classCVC3_1_1Expr.html">Expr</a> e1, <a class="el" href="classCVC3_1_1Expr.html">Expr</a> e2)
</ul>
<h2><a name="var-members"></a>
Variables</h2>
<ul>
<li>static const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="theory__quant_8cpp.html#a6ab61b1ab2bcdf0a5384bb93d3fb7ac2">null_expr</a>
<li>const int <a class="el" href="theory__quant_8cpp.html#a7f1fce06f1566f5c97e3f306c86d5bfc">FOUND_FALSE</a> = 1
</ul>
<hr/><h2>Function Documentation</h2>
<a class="anchor" id="ac540b3d9d2b6b96fb7e8ca2df7ccb678"></a><!-- doxytag: member="theory_quant.cpp::vectorExpr2string" ref="ac540b3d9d2b6b96fb7e8ca2df7ccb678" args="(const std::vector< Expr > &vec)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string vectorExpr2string </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>vec</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l00244">244</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l00633">CVC3::TheoryQuant::enqueueInst()</a>.</p>
</div>
</div>
<a class="anchor" id="ae2ef120eda296c8008688042714b2fc9"></a><!-- doxytag: member="theory_quant.cpp::isSysPred" ref="ae2ef120eda296c8008688042714b2fc9" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool isSysPred </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l00278">278</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00419">CVC3::Expr::isEq()</a>, <a class="el" href="theory__arith_8h_source.html#l00189">CVC3::isGE()</a>, <a class="el" href="theory__arith_8h_source.html#l00188">CVC3::isGT()</a>, <a class="el" href="theory__arith_8h_source.html#l00187">CVC3::isLE()</a>, and <a class="el" href="theory__arith_8h_source.html#l00186">CVC3::isLT()</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l02481">isGoodMultiTrigger()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02516">isGoodPartTrigger()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02456">isGoodSysPredTrigger()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04377">CVC3::TheoryQuant::newTopMatchNoSig()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04671">CVC3::TheoryQuant::newTopMatchSig()</a>, <a class="el" href="theory__quant_8cpp_source.html#l05587">CVC3::TheoryQuant::recMultMatch()</a>, <a class="el" href="theory__quant_8cpp_source.html#l05310">CVC3::TheoryQuant::recMultMatchDebug()</a>, <a class="el" href="theory__quant_8cpp_source.html#l05478">CVC3::TheoryQuant::recMultMatchOldWay()</a>, <a class="el" href="theory__quant_8cpp_source.html#l00563">recursiveGetSubTrig()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02917">CVC3::TheoryQuant::setupTriggers()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02607">trigInitScore()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l00323">usefulInMatch()</a>.</p>
</div>
</div>
<a class="anchor" id="ad02abacd5bb6a0e7dc5fe4f2d9300dfe"></a><!-- doxytag: member="theory_quant.cpp::canGetHead" ref="ad02abacd5bb6a0e7dc5fe4f2d9300dfe" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool canGetHead </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l00282">282</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00090">APPLY</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="theory__arith_8h_source.html#l00184">CVC3::isDivide()</a>, <a class="el" href="theory__arith_8h_source.html#l00182">CVC3::isMinus()</a>, <a class="el" href="theory__arith_8h_source.html#l00183">CVC3::isMult()</a>, <a class="el" href="theory__arith_8h_source.html#l00181">CVC3::isPlus()</a>, <a class="el" href="theory__arith_8h_source.html#l00185">CVC3::isPow()</a>, <a class="el" href="theory__array_8h_source.html#l00032">CVC3::READ</a>, and <a class="el" href="theory__array_8h_source.html#l00033">CVC3::WRITE</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l02798">CVC3::TheoryQuant::canMatch()</a>, <a class="el" href="theory__quant_8cpp_source.html#l07647">CVC3::TheoryQuant::checkSat()</a>, <a class="el" href="theory__quant_8cpp_source.html#l00295">isSimpleTrig()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02823">CVC3::TheoryQuant::isTransLike()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04075">CVC3::TheoryQuant::matchListOld()</a>, <a class="el" href="theory__quant_8cpp_source.html#l05587">CVC3::TheoryQuant::recMultMatch()</a>, <a class="el" href="theory__quant_8cpp_source.html#l05310">CVC3::TheoryQuant::recMultMatchDebug()</a>, <a class="el" href="theory__quant_8cpp_source.html#l05478">CVC3::TheoryQuant::recMultMatchOldWay()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02917">CVC3::TheoryQuant::setupTriggers()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l00323">usefulInMatch()</a>.</p>
</div>
</div>
<a class="anchor" id="abfd229253e2b4548aec82a3c604175a8"></a><!-- doxytag: member="theory_quant.cpp::isSimpleTrig" ref="abfd229253e2b4548aec82a3c604175a8" args="(const Expr &t)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool isSimpleTrig </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>t</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l00295">295</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="kinds_8h_source.html#l00164">BOUND_VAR</a>, <a class="el" href="theory__quant_8cpp_source.html#l00282">canGetHead()</a>, and <a class="el" href="expr_8h_source.html#l01338">CVC3::Expr::containsBoundVar()</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l00308">isSuperSimpleTrig()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l02917">CVC3::TheoryQuant::setupTriggers()</a>.</p>
</div>
</div>
<a class="anchor" id="a96efdadd956037ab4b1ca55b5d54faea"></a><!-- doxytag: member="theory_quant.cpp::isSuperSimpleTrig" ref="a96efdadd956037ab4b1ca55b5d54faea" args="(const Expr &t)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool isSuperSimpleTrig </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>t</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l00308">308</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="kinds_8h_source.html#l00164">BOUND_VAR</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="theory__quant_8cpp_source.html#l00295">isSimpleTrig()</a>, <a class="el" href="theory__array_8h_source.html#l00032">CVC3::READ</a>, and <a class="el" href="theory__array_8h_source.html#l00033">CVC3::WRITE</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l02917">CVC3::TheoryQuant::setupTriggers()</a>.</p>
</div>
</div>
<a class="anchor" id="a45fb04ec0356578e698622eb7ac59d04"></a><!-- doxytag: member="theory_quant.cpp::usefulInMatch" ref="a45fb04ec0356578e698622eb7ac59d04" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool usefulInMatch </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l00323">323</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theory__quant_8cpp_source.html#l00282">canGetHead()</a>, <a class="el" href="expr_8h_source.html#l00419">CVC3::Expr::isEq()</a>, <a class="el" href="expr_8h_source.html#l00431">CVC3::Expr::isRational()</a>, <a class="el" href="theory__quant_8cpp_source.html#l00278">isSysPred()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l02462">isGoodFullTrigger()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02481">isGoodMultiTrigger()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02516">isGoodPartTrigger()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02456">isGoodSysPredTrigger()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l08119">CVC3::TheoryQuant::synCheckSat()</a>.</p>
</div>
</div>
<a class="anchor" id="ac5b507b0c113276077e5a7ff29fc7604"></a><!-- doxytag: member="theory_quant.cpp::recursiveGetSubTrig" ref="ac5b507b0c113276077e5a7ff29fc7604" args="(const Expr &e, std::vector< Expr > &res)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">static void recursiveGetSubTrig </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>res</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l00563">563</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr_8h_source.html#l01069">CVC3::Expr::getBody()</a>, <a class="el" href="expr_8h_source.html#l01390">CVC3::Expr::getFlag()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, <a class="el" href="expr_8h_source.html#l01007">CVC3::Expr::isClosure()</a>, <a class="el" href="theory__quant_8cpp_source.html#l00278">isSysPred()</a>, <a class="el" href="expr_8h_source.html#l01021">CVC3::Expr::isTerm()</a>, <a class="el" href="expr_8h_source.html#l01005">CVC3::Expr::isVar()</a>, <a class="el" href="kinds_8h_source.html#l00037">RATIONAL_EXPR</a>, and <a class="el" href="expr_8h_source.html#l01395">CVC3::Expr::setFlag()</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l00586">getSubTrig()</a>.</p>
</div>
</div>
<a class="anchor" id="a284771b2ec3f2c7410dce560633123a6"></a><!-- doxytag: member="theory_quant.cpp::getSubTrig" ref="a284771b2ec3f2c7410dce560633123a6" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classCVC3_1_1Expr.html">Expr</a>> getSubTrig </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l00586">586</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01400">CVC3::Expr::clearFlags()</a>, <a class="el" href="theory__quant_8cpp_source.html#l00563">recursiveGetSubTrig()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l02917">CVC3::TheoryQuant::setupTriggers()</a>.</p>
</div>
</div>
<a class="anchor" id="a28d6afee25aa51bcd4f5d41179cefc2b"></a><!-- doxytag: member="theory_quant.cpp::recGetSubTerms" ref="a28d6afee25aa51bcd4f5d41179cefc2b" args="(const Expr &e, std::vector< Expr > &res)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">static void recGetSubTerms </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>res</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l00596">596</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr_8h_source.html#l01069">CVC3::Expr::getBody()</a>, <a class="el" href="expr_8h_source.html#l01390">CVC3::Expr::getFlag()</a>, <a class="el" href="expr_8h_source.html#l01007">CVC3::Expr::isClosure()</a>, and <a class="el" href="expr_8h_source.html#l01395">CVC3::Expr::setFlag()</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l00613">CVC3::TheoryQuant::getSubTerms()</a>.</p>
</div>
</div>
<a class="anchor" id="adccadd475af73b2fb9c61f33735977a0"></a><!-- doxytag: member="theory_quant.cpp::recursiveExprScore" ref="adccadd475af73b2fb9c61f33735977a0" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int recursiveExprScore </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l01042">1042</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, and <a class="el" href="expr_8h_source.html#l01007">CVC3::Expr::isClosure()</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l01059">exprScore()</a>.</p>
</div>
</div>
<a class="anchor" id="aa0227fe4666655a02e5e43c9650b5f7d"></a><!-- doxytag: member="theory_quant.cpp::exprScore" ref="aa0227fe4666655a02e5e43c9650b5f7d" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int exprScore </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l01059">1059</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="theory__quant_8cpp_source.html#l01042">recursiveExprScore()</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l02917">CVC3::TheoryQuant::setupTriggers()</a>.</p>
</div>
</div>
<a class="anchor" id="a779ed57bff05a3a131337d749e91db15"></a><!-- doxytag: member="theory_quant.cpp::recursiveGetBoundVars" ref="a779ed57bff05a3a131337d749e91db15" args="(const Expr &e, std::set< Expr > &result)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">static bool recursiveGetBoundVars </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>result</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>get the bound vars in term e, </p>
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l01111">1111</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="kinds_8h_source.html#l00164">BOUND_VAR</a>, <a class="el" href="expr_8h_source.html#l01338">CVC3::Expr::containsBoundVar()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr_8h_source.html#l01069">CVC3::Expr::getBody()</a>, <a class="el" href="expr_8h_source.html#l01390">CVC3::Expr::getFlag()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01007">CVC3::Expr::isClosure()</a>, <a class="el" href="expr_8h_source.html#l01478">CVC3::Expr::setContainsBoundVar()</a>, and <a class="el" href="expr_8h_source.html#l01395">CVC3::Expr::setFlag()</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l01144">getBoundVars()</a>.</p>
</div>
</div>
<a class="anchor" id="ab0c1ea5ae3c53ec0bbf2e04b1f33e757"></a><!-- doxytag: member="theory_quant.cpp::getBoundVars" ref="ab0c1ea5ae3c53ec0bbf2e04b1f33e757" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::set<<a class="el" href="classCVC3_1_1Expr.html">Expr</a>> getBoundVars </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>get bound vars in term e, </p>
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l01144">1144</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01400">CVC3::Expr::clearFlags()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l01111">recursiveGetBoundVars()</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l02617">CVC3::TheoryQuant::arrayIndexName()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02882">goodMultiTriggers()</a>, <a class="el" href="theory__quant_8cpp_source.html#l03483">hasMoreBVs()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02022">CVC3::CompleteInstPreProcessor::isGood()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02462">isGoodFullTrigger()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02481">isGoodMultiTrigger()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02516">isGoodPartTrigger()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02823">CVC3::TheoryQuant::isTransLike()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01756">CVC3::CompleteInstPreProcessor::rewriteNot()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02917">CVC3::TheoryQuant::setupTriggers()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l02343">CVC3::TheoryQuant::theoryPreprocess()</a>.</p>
</div>
</div>
<a class="anchor" id="ae79a351634c32cc5b514d37efb810677"></a><!-- doxytag: member="theory_quant.cpp::findPolarity" ref="ae79a351634c32cc5b514d37efb810677" args="(const Expr &e, ExprMap< Polarity > &res, Polarity pol)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void findPolarity </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< <a class="el" href="namespaceCVC3.html#aa6262a73c1109f35a6c533421f5dd393">Polarity</a> > & </td>
<td class="paramname"><em>res</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="namespaceCVC3.html#aa6262a73c1109f35a6c533421f5dd393">Polarity</a> </td>
<td class="paramname"><em>pol</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l01166">1166</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr__map_8h_source.html#l00173">CVC3::ExprMap< Data >::count()</a>, <a class="el" href="expr_8h_source.html#l01069">CVC3::Expr::getBody()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="expr_8h_source.html#l00421">CVC3::Expr::isAnd()</a>, <a class="el" href="expr_8cpp_source.html#l00571">CVC3::Expr::isAtomicFormula()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr_8h_source.html#l01007">CVC3::Expr::isClosure()</a>, <a class="el" href="expr_8h_source.html#l00424">CVC3::Expr::isIff()</a>, <a class="el" href="expr_8h_source.html#l00425">CVC3::Expr::isImpl()</a>, <a class="el" href="expr_8h_source.html#l00423">CVC3::Expr::isITE()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="expr_8h_source.html#l00422">CVC3::Expr::isOr()</a>, <a class="el" href="expr_8h_source.html#l00426">CVC3::Expr::isXor()</a>, <a class="el" href="theory__quant_8h_source.html#l00048">CVC3::Neg</a>, <a class="el" href="theory__quant_8h_source.html#l00048">CVC3::Pos</a>, <a class="el" href="theory__quant_8h_source.html#l00048">CVC3::PosNeg</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, and <a class="el" href="theory__quant_8h_source.html#l00048">CVC3::Ukn</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l01861">CVC3::CompleteInstPreProcessor::collect_forall_index()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02103">CVC3::CompleteInstPreProcessor::isGoodQuant()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01756">CVC3::CompleteInstPreProcessor::rewriteNot()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02917">CVC3::TheoryQuant::setupTriggers()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l01731">CVC3::CompleteInstPreProcessor::simplifyQuant()</a>.</p>
</div>
</div>
<a class="anchor" id="a4a97be803d167c43000680f2008abf21"></a><!-- doxytag: member="theory_quant.cpp::isUniterpFunc" ref="a4a97be803d167c43000680f2008abf21" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool isUniterpFunc </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l01231">1231</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, and <a class="el" href="kinds_8h_source.html#l00088">UFUNC</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l01832">CVC3::CompleteInstPreProcessor::collect_shield_index()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01350">CVC3::CompleteInstPreProcessor::collectHeads()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01554">CVC3::CompleteInstPreProcessor::hasShieldVar()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01373">CVC3::CompleteInstPreProcessor::isMacro()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01577">CVC3::CompleteInstPreProcessor::isShield()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l01499">CVC3::CompleteInstPreProcessor::recInstMacros()</a>.</p>
</div>
</div>
<a class="anchor" id="a57148644393433bb1267393b8a18e785"></a><!-- doxytag: member="theory_quant.cpp::isGround" ref="a57148644393433bb1267393b8a18e785" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool isGround </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l01243">1243</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01338">CVC3::Expr::containsBoundVar()</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l01861">CVC3::CompleteInstPreProcessor::collect_forall_index()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01832">CVC3::CompleteInstPreProcessor::collect_shield_index()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01972">CVC3::CompleteInstPreProcessor::collectIndex()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02229">CVC3::CompleteInstPreProcessor::inst()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01577">CVC3::CompleteInstPreProcessor::isShield()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l01763">CVC3::CompleteInstPreProcessor::recRewriteNot()</a>.</p>
</div>
</div>
<a class="anchor" id="ab2eabe9580c3d9a962173108df445a51"></a><!-- doxytag: member="theory_quant.cpp::findPolarityAtomic" ref="ab2eabe9580c3d9a962173108df445a51" args="(const Expr &e, ExprMap< Polarity > &res, Polarity pol)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void findPolarityAtomic </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< <a class="el" href="namespaceCVC3.html#aa6262a73c1109f35a6c533421f5dd393">Polarity</a> > & </td>
<td class="paramname"><em>res</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="namespaceCVC3.html#aa6262a73c1109f35a6c533421f5dd393">Polarity</a> </td>
<td class="paramname"><em>pol</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l01626">1626</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr__map_8h_source.html#l00173">CVC3::ExprMap< Data >::count()</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="expr_8h_source.html#l00421">CVC3::Expr::isAnd()</a>, <a class="el" href="expr_8cpp_source.html#l00571">CVC3::Expr::isAtomicFormula()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr_8h_source.html#l01007">CVC3::Expr::isClosure()</a>, <a class="el" href="expr_8h_source.html#l00424">CVC3::Expr::isIff()</a>, <a class="el" href="expr_8h_source.html#l00425">CVC3::Expr::isImpl()</a>, <a class="el" href="expr_8h_source.html#l00423">CVC3::Expr::isITE()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="expr_8h_source.html#l00422">CVC3::Expr::isOr()</a>, <a class="el" href="expr_8h_source.html#l00426">CVC3::Expr::isXor()</a>, <a class="el" href="theory__quant_8h_source.html#l00048">CVC3::Neg</a>, <a class="el" href="theory__quant_8h_source.html#l00048">CVC3::Pos</a>, <a class="el" href="theory__quant_8h_source.html#l00048">CVC3::PosNeg</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theory__quant_8h_source.html#l00048">CVC3::Ukn</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l01972">CVC3::CompleteInstPreProcessor::collectIndex()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l02022">CVC3::CompleteInstPreProcessor::isGood()</a>.</p>
</div>
</div>
<a class="anchor" id="a964c839e8f67da1a35acc097463b5f7e"></a><!-- doxytag: member="theory_quant.cpp::flatAnds" ref="a964c839e8f67da1a35acc097463b5f7e" args="(const Expr &ands, vector< Expr > &results)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void flatAnds </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>ands</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>results</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l02322">2322</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr_8h_source.html#l00421">CVC3::Expr::isAnd()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, and <a class="el" href="expr_8h_source.html#l00422">CVC3::Expr::isOr()</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l02343">CVC3::TheoryQuant::theoryPreprocess()</a>.</p>
</div>
</div>
<a class="anchor" id="a28f516e79b8ffb0e4e998eac196bd9cc"></a><!-- doxytag: member="theory_quant.cpp::isGoodSysPredTrigger" ref="a28f516e79b8ffb0e4e998eac196bd9cc" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool isGoodSysPredTrigger </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l02456">2456</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="theory__quant_8cpp_source.html#l00278">isSysPred()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l00323">usefulInMatch()</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l02481">isGoodMultiTrigger()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02516">isGoodPartTrigger()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l02607">trigInitScore()</a>.</p>
</div>
</div>
<a class="anchor" id="aa98360024a0b2da76e6a57210efea027"></a><!-- doxytag: member="theory_quant.cpp::isGoodFullTrigger" ref="aa98360024a0b2da76e6a57210efea027" args="(const Expr &e, const std::vector< Expr > &bVarsThm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool isGoodFullTrigger </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>bVarsThm</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l02462">2462</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="theory__quant_8cpp_source.html#l01144">getBoundVars()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l00323">usefulInMatch()</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l02917">CVC3::TheoryQuant::setupTriggers()</a>.</p>
</div>
</div>
<a class="anchor" id="ae4d6f79b2b5eb00c102cd9cd325ecf77"></a><!-- doxytag: member="theory_quant.cpp::isGoodMultiTrigger" ref="ae4d6f79b2b5eb00c102cd9cd325ecf77" args="(const Expr &e, const std::vector< Expr > &bVarsThm, int offset)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool isGoodMultiTrigger </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>bVarsThm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>offset</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l02481">2481</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="theory__quant_8cpp_source.html#l01144">getBoundVars()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02456">isGoodSysPredTrigger()</a>, <a class="el" href="theory__quant_8cpp_source.html#l00278">isSysPred()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l00323">usefulInMatch()</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l02917">CVC3::TheoryQuant::setupTriggers()</a>.</p>
</div>
</div>
<a class="anchor" id="acb48e181095d3c2c86486677a1b9937d"></a><!-- doxytag: member="theory_quant.cpp::isGoodPartTrigger" ref="acb48e181095d3c2c86486677a1b9937d" args="(const Expr &e, const std::vector< Expr > &bVarsThm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool isGoodPartTrigger </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>bVarsThm</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l02516">2516</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="theory__quant_8cpp_source.html#l01144">getBoundVars()</a>, <a class="el" href="theory__quant_8cpp_source.html#l02456">isGoodSysPredTrigger()</a>, <a class="el" href="theory__quant_8cpp_source.html#l00278">isSysPred()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l00323">usefulInMatch()</a>.</p>
</div>
</div>
<a class="anchor" id="ad577dba7e2b661fa6caa2355ca90f0d6"></a><!-- doxytag: member="theory_quant.cpp::recursiveGetPartTriggers" ref="ad577dba7e2b661fa6caa2355ca90f0d6" args="(const Expr &e, std::vector< Expr > &res)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">static bool recursiveGetPartTriggers </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>res</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l02554">2554</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="kinds_8h_source.html#l00164">BOUND_VAR</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr_8h_source.html#l01069">CVC3::Expr::getBody()</a>, <a class="el" href="expr_8h_source.html#l01390">CVC3::Expr::getFlag()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01007">CVC3::Expr::isClosure()</a>, and <a class="el" href="expr_8h_source.html#l01395">CVC3::Expr::setFlag()</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l02599">getPartTriggers()</a>.</p>
</div>
</div>
<a class="anchor" id="acaa6717f00a26724ea7e9f5bfd1fa656"></a><!-- doxytag: member="theory_quant.cpp::getPartTriggers" ref="acaa6717f00a26724ea7e9f5bfd1fa656" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classCVC3_1_1Expr.html">Expr</a>> getPartTriggers </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l02599">2599</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01400">CVC3::Expr::clearFlags()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l02554">recursiveGetPartTriggers()</a>.</p>
</div>
</div>
<a class="anchor" id="ae0833342972b17d872e2d6f4f45b3812"></a><!-- doxytag: member="theory_quant.cpp::trigInitScore" ref="ae0833342972b17d872e2d6f4f45b3812" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int trigInitScore </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l02607">2607</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="theory__quant_8cpp_source.html#l02456">isGoodSysPredTrigger()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l00278">isSysPred()</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l02917">CVC3::TheoryQuant::setupTriggers()</a>.</p>
</div>
</div>
<a class="anchor" id="a8822f0191c9cafc521b190dbc29ce8bd"></a><!-- doxytag: member="theory_quant.cpp::goodMultiTriggers" ref="a8822f0191c9cafc521b190dbc29ce8bd" args="(const std::vector< Expr > &exprs, const std::vector< Expr > bVars)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool goodMultiTriggers </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>exprs</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > </td>
<td class="paramname"><em>bVars</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l02882">2882</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr__map_8h_source.html#l00194">CVC3::ExprMap< Data >::find()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l01144">getBoundVars()</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l02917">CVC3::TheoryQuant::setupTriggers()</a>.</p>
</div>
</div>
<a class="anchor" id="a68eed73f49f190f0b990027b28688f7f"></a><!-- doxytag: member="theory_quant.cpp::locVar" ref="a68eed73f49f190f0b990027b28688f7f" args="(const vector< Expr > &bvsThm, const Expr &bv)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">size_t locVar </td>
<td>(</td>
<td class="paramtype">const vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>bvsThm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>bv</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l02907">2907</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l02917">CVC3::TheoryQuant::setupTriggers()</a>.</p>
</div>
</div>
<a class="anchor" id="a8ba2c2ab53110996e9faf4d432a3af7d"></a><!-- doxytag: member="theory_quant.cpp::hasMoreBVs" ref="a8ba2c2ab53110996e9faf4d432a3af7d" args="(const Expr &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int hasMoreBVs </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>test if a sub-term contains more bounded vars than quantified by out-most quantifier. </p>
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l03483">3483</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theory__quant_8cpp_source.html#l01144">getBoundVars()</a>, <a class="el" href="expr_8h_source.html#l01062">CVC3::Expr::getVars()</a>, and <a class="el" href="expr_8h_source.html#l00428">CVC3::Expr::isForall()</a>.</p>
</div>
</div>
<a class="anchor" id="ac9940420b1f3427ebe821902adbb578d"></a><!-- doxytag: member="theory_quant.cpp::isIntx" ref="ac9940420b1f3427ebe821902adbb578d" args="(const Expr &e, const Rational &x)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool isIntx </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Rational.html">Rational</a> & </td>
<td class="paramname"><em>x</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l03731">3731</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01135">CVC3::Expr::getRational()</a>, and <a class="el" href="expr_8h_source.html#l00431">CVC3::Expr::isRational()</a>.</p>
<p>Referenced by <a class="el" href="theory__arith3_8cpp_source.html#l00432">CVC3::TheoryArith3::doSolve()</a>, <a class="el" href="theory__quant_8cpp_source.html#l03738">getLeft()</a>, <a class="el" href="theory__quant_8cpp_source.html#l03771">getRight()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04377">CVC3::TheoryQuant::newTopMatchNoSig()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04671">CVC3::TheoryQuant::newTopMatchSig()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l01822">CVC3::TheoryArithOld::normalizeProjectIneqs()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l01449">CVC3::TheoryArith3::normalizeProjectIneqs()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l00739">CVC3::TheoryArithOld::processSimpleIntEq()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00507">CVC3::TheoryArithNew::processSimpleIntEq()</a>, and <a class="el" href="theory__arith3_8cpp_source.html#l00759">CVC3::TheoryArith3::processSimpleIntEq()</a>.</p>
</div>
</div>
<a class="anchor" id="a4564697c1b2ea1e3a70ef36383ca1c41"></a><!-- doxytag: member="theory_quant.cpp::getLeft" ref="a4564697c1b2ea1e3a70ef36383ca1c41" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> getLeft </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l03738">3738</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="theory__quant_8cpp_source.html#l03731">isIntx()</a>, <a class="el" href="theory__arith_8h_source.html#l00177">CVC3::isRational()</a>, <a class="el" href="theory__arith_8h_source.html#l00044">CVC3::MULT</a>, <a class="el" href="theory__quant_8cpp_source.html#l00042">null_expr</a>, and <a class="el" href="theory__arith_8h_source.html#l00042">CVC3::PLUS</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l04377">CVC3::TheoryQuant::newTopMatchNoSig()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l04671">CVC3::TheoryQuant::newTopMatchSig()</a>.</p>
</div>
</div>
<a class="anchor" id="a9162c5e3cbe41ca756947718e983180b"></a><!-- doxytag: member="theory_quant.cpp::getRight" ref="a9162c5e3cbe41ca756947718e983180b" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> getRight </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l03771">3771</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="theory__quant_8cpp_source.html#l03731">isIntx()</a>, <a class="el" href="theory__arith_8h_source.html#l00177">CVC3::isRational()</a>, <a class="el" href="theory__arith_8h_source.html#l00044">CVC3::MULT</a>, <a class="el" href="theory__quant_8cpp_source.html#l00042">null_expr</a>, and <a class="el" href="theory__arith_8h_source.html#l00042">CVC3::PLUS</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l04377">CVC3::TheoryQuant::newTopMatchNoSig()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l04671">CVC3::TheoryQuant::newTopMatchSig()</a>.</p>
</div>
</div>
<a class="anchor" id="a438706926ba67238b44f3186b511b49f"></a><!-- doxytag: member="theory_quant.cpp::cmpExpr" ref="a438706926ba67238b44f3186b511b49f" args="(Expr e1, Expr e2)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool cmpExpr </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td>
<td class="paramname"><em>e1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td>
<td class="paramname"><em>e2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l05293">5293</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01173">CVC3::Expr::getIndex()</a>, and <a class="el" href="expr_8h_source.html#l01223">CVC3::Expr::isNull()</a>.</p>
</div>
</div>
<hr/><h2>Variable Documentation</h2>
<a class="anchor" id="a6ab61b1ab2bcdf0a5384bb93d3fb7ac2"></a><!-- doxytag: member="theory_quant.cpp::null_expr" ref="a6ab61b1ab2bcdf0a5384bb93d3fb7ac2" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="theory__quant_8cpp.html#a6ab61b1ab2bcdf0a5384bb93d3fb7ac2">null_expr</a><code> [static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l00042">42</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l00633">CVC3::TheoryQuant::enqueueInst()</a>, <a class="el" href="theory__quant_8cpp_source.html#l01063">CVC3::TheoryQuant::getHeadExpr()</a>, <a class="el" href="theory__quant_8cpp_source.html#l03738">getLeft()</a>, <a class="el" href="theory__quant_8cpp_source.html#l03771">getRight()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04271">CVC3::TheoryQuant::matchListNew()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04075">CVC3::TheoryQuant::matchListOld()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04377">CVC3::TheoryQuant::newTopMatchNoSig()</a>, <a class="el" href="theory__quant_8cpp_source.html#l04671">CVC3::TheoryQuant::newTopMatchSig()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08466">CVC3::TheoryQuant::recInstantiate()</a>, <a class="el" href="theory__quant_8cpp_source.html#l07248">CVC3::TheoryQuant::simpRAWList()</a>, <a class="el" href="theory__quant_8cpp_source.html#l07258">CVC3::TheoryQuant::synNewInst()</a>, <a class="el" href="theory__quant_8cpp_source.html#l00140">CVC3::TheoryQuant::TheoryQuant()</a>, and <a class="el" href="theory__quant_8cpp_source.html#l00045">CVC3::Trigger::Trigger()</a>.</p>
</div>
</div>
<a class="anchor" id="a7f1fce06f1566f5c97e3f306c86d5bfc"></a><!-- doxytag: member="theory_quant.cpp::FOUND_FALSE" ref="a7f1fce06f1566f5c97e3f306c86d5bfc" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const int <a class="el" href="theory__quant_8cpp.html#a7f1fce06f1566f5c97e3f306c86d5bfc">FOUND_FALSE</a> = 1</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__quant_8cpp_source.html#l00043">43</a> of file <a class="el" href="theory__quant_8cpp_source.html">theory_quant.cpp</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l00633">CVC3::TheoryQuant::enqueueInst()</a>.</p>
</div>
</div>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
