<!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.cpp File Reference</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_9e7e03df595ffb1777a4cf881e60662b.html">theory_quant</a></li> </ul>
</div>
</div><!-- top -->
<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><!--header-->
<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>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="nested-classes"></a>
Classes</h2></td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">class  </td><td class="memItemRight" valign="bottom"><a class="el" href="classrecCompleteInster.html">recCompleteInster</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="func-members"></a>
Functions</h2></td></tr>
<tr class="memitem:ac540b3d9d2b6b96fb7e8ca2df7ccb678"><td class="memItemLeft" align="right" valign="top">std::string </td><td class="memItemRight" valign="bottom"><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)</td></tr>
<tr class="separator:ac540b3d9d2b6b96fb7e8ca2df7ccb678"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae2ef120eda296c8008688042714b2fc9"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="theory__quant_8cpp.html#ae2ef120eda296c8008688042714b2fc9">isSysPred</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:ae2ef120eda296c8008688042714b2fc9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad02abacd5bb6a0e7dc5fe4f2d9300dfe"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="theory__quant_8cpp.html#ad02abacd5bb6a0e7dc5fe4f2d9300dfe">canGetHead</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:ad02abacd5bb6a0e7dc5fe4f2d9300dfe"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:abfd229253e2b4548aec82a3c604175a8"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="theory__quant_8cpp.html#abfd229253e2b4548aec82a3c604175a8">isSimpleTrig</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &t)</td></tr>
<tr class="separator:abfd229253e2b4548aec82a3c604175a8"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a96efdadd956037ab4b1ca55b5d54faea"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="theory__quant_8cpp.html#a96efdadd956037ab4b1ca55b5d54faea">isSuperSimpleTrig</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &t)</td></tr>
<tr class="separator:a96efdadd956037ab4b1ca55b5d54faea"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a45fb04ec0356578e698622eb7ac59d04"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="theory__quant_8cpp.html#a45fb04ec0356578e698622eb7ac59d04">usefulInMatch</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:a45fb04ec0356578e698622eb7ac59d04"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac5b507b0c113276077e5a7ff29fc7604"><td class="memItemLeft" align="right" valign="top">static void </td><td class="memItemRight" valign="bottom"><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)</td></tr>
<tr class="separator:ac5b507b0c113276077e5a7ff29fc7604"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a284771b2ec3f2c7410dce560633123a6"><td class="memItemLeft" align="right" valign="top">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > </td><td class="memItemRight" valign="bottom"><a class="el" href="theory__quant_8cpp.html#a284771b2ec3f2c7410dce560633123a6">getSubTrig</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:a284771b2ec3f2c7410dce560633123a6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a28d6afee25aa51bcd4f5d41179cefc2b"><td class="memItemLeft" align="right" valign="top">static void </td><td class="memItemRight" valign="bottom"><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)</td></tr>
<tr class="separator:a28d6afee25aa51bcd4f5d41179cefc2b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:adccadd475af73b2fb9c61f33735977a0"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="theory__quant_8cpp.html#adccadd475af73b2fb9c61f33735977a0">recursiveExprScore</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:adccadd475af73b2fb9c61f33735977a0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa0227fe4666655a02e5e43c9650b5f7d"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="theory__quant_8cpp.html#aa0227fe4666655a02e5e43c9650b5f7d">exprScore</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:aa0227fe4666655a02e5e43c9650b5f7d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a779ed57bff05a3a131337d749e91db15"><td class="memItemLeft" align="right" valign="top">static bool </td><td class="memItemRight" valign="bottom"><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)</td></tr>
<tr class="memdesc:a779ed57bff05a3a131337d749e91db15"><td class="mdescLeft"> </td><td class="mdescRight">get the bound vars in term e, <a href="#a779ed57bff05a3a131337d749e91db15"></a><br/></td></tr>
<tr class="separator:a779ed57bff05a3a131337d749e91db15"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab0c1ea5ae3c53ec0bbf2e04b1f33e757"><td class="memItemLeft" align="right" valign="top">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > </td><td class="memItemRight" valign="bottom"><a class="el" href="theory__quant_8cpp.html#ab0c1ea5ae3c53ec0bbf2e04b1f33e757">getBoundVars</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:ab0c1ea5ae3c53ec0bbf2e04b1f33e757"><td class="mdescLeft"> </td><td class="mdescRight">get bound vars in term e, <a href="#ab0c1ea5ae3c53ec0bbf2e04b1f33e757"></a><br/></td></tr>
<tr class="separator:ab0c1ea5ae3c53ec0bbf2e04b1f33e757"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae79a351634c32cc5b514d37efb810677"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><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)</td></tr>
<tr class="separator:ae79a351634c32cc5b514d37efb810677"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4a97be803d167c43000680f2008abf21"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="theory__quant_8cpp.html#a4a97be803d167c43000680f2008abf21">isUniterpFunc</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:a4a97be803d167c43000680f2008abf21"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a57148644393433bb1267393b8a18e785"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="theory__quant_8cpp.html#a57148644393433bb1267393b8a18e785">isGround</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:a57148644393433bb1267393b8a18e785"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab2eabe9580c3d9a962173108df445a51"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><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)</td></tr>
<tr class="separator:ab2eabe9580c3d9a962173108df445a51"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a964c839e8f67da1a35acc097463b5f7e"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><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)</td></tr>
<tr class="separator:a964c839e8f67da1a35acc097463b5f7e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a28f516e79b8ffb0e4e998eac196bd9cc"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="theory__quant_8cpp.html#a28f516e79b8ffb0e4e998eac196bd9cc">isGoodSysPredTrigger</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:a28f516e79b8ffb0e4e998eac196bd9cc"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa98360024a0b2da76e6a57210efea027"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><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)</td></tr>
<tr class="separator:aa98360024a0b2da76e6a57210efea027"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae4d6f79b2b5eb00c102cd9cd325ecf77"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><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)</td></tr>
<tr class="separator:ae4d6f79b2b5eb00c102cd9cd325ecf77"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:acb48e181095d3c2c86486677a1b9937d"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><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)</td></tr>
<tr class="separator:acb48e181095d3c2c86486677a1b9937d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad577dba7e2b661fa6caa2355ca90f0d6"><td class="memItemLeft" align="right" valign="top">static bool </td><td class="memItemRight" valign="bottom"><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)</td></tr>
<tr class="separator:ad577dba7e2b661fa6caa2355ca90f0d6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:acaa6717f00a26724ea7e9f5bfd1fa656"><td class="memItemLeft" align="right" valign="top">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > </td><td class="memItemRight" valign="bottom"><a class="el" href="theory__quant_8cpp.html#acaa6717f00a26724ea7e9f5bfd1fa656">getPartTriggers</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:acaa6717f00a26724ea7e9f5bfd1fa656"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae0833342972b17d872e2d6f4f45b3812"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="theory__quant_8cpp.html#ae0833342972b17d872e2d6f4f45b3812">trigInitScore</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:ae0833342972b17d872e2d6f4f45b3812"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8822f0191c9cafc521b190dbc29ce8bd"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><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)</td></tr>
<tr class="separator:a8822f0191c9cafc521b190dbc29ce8bd"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a68eed73f49f190f0b990027b28688f7f"><td class="memItemLeft" align="right" valign="top">size_t </td><td class="memItemRight" valign="bottom"><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)</td></tr>
<tr class="separator:a68eed73f49f190f0b990027b28688f7f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a8ba2c2ab53110996e9faf4d432a3af7d"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="theory__quant_8cpp.html#a8ba2c2ab53110996e9faf4d432a3af7d">hasMoreBVs</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &thm)</td></tr>
<tr class="memdesc:a8ba2c2ab53110996e9faf4d432a3af7d"><td class="mdescLeft"> </td><td class="mdescRight">test if a sub-term contains more bounded vars than quantified by out-most quantifier. <a href="#a8ba2c2ab53110996e9faf4d432a3af7d"></a><br/></td></tr>
<tr class="separator:a8ba2c2ab53110996e9faf4d432a3af7d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac9940420b1f3427ebe821902adbb578d"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><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)</td></tr>
<tr class="separator:ac9940420b1f3427ebe821902adbb578d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a4564697c1b2ea1e3a70ef36383ca1c41"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="theory__quant_8cpp.html#a4564697c1b2ea1e3a70ef36383ca1c41">getLeft</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:a4564697c1b2ea1e3a70ef36383ca1c41"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9162c5e3cbe41ca756947718e983180b"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="theory__quant_8cpp.html#a9162c5e3cbe41ca756947718e983180b">getRight</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:a9162c5e3cbe41ca756947718e983180b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a438706926ba67238b44f3186b511b49f"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><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)</td></tr>
<tr class="separator:a438706926ba67238b44f3186b511b49f"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="var-members"></a>
Variables</h2></td></tr>
<tr class="memitem:a6ab61b1ab2bcdf0a5384bb93d3fb7ac2"><td class="memItemLeft" align="right" valign="top">static const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="theory__quant_8cpp.html#a6ab61b1ab2bcdf0a5384bb93d3fb7ac2">null_expr</a></td></tr>
<tr class="separator:a6ab61b1ab2bcdf0a5384bb93d3fb7ac2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a7f1fce06f1566f5c97e3f306c86d5bfc"><td class="memItemLeft" align="right" valign="top">const int </td><td class="memItemRight" valign="bottom"><a class="el" href="theory__quant_8cpp.html#a7f1fce06f1566f5c97e3f306c86d5bfc">FOUND_FALSE</a> = 1</td></tr>
<tr class="separator:a7f1fce06f1566f5c97e3f306c86d5bfc"><td class="memSeparator" colspan="2"> </td></tr>
</table>
<h2 class="groupheader">Function Documentation</h2>
<a class="anchor" id="ac540b3d9d2b6b96fb7e8ca2df7ccb678"></a>
<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>
<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>
<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>
<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>
<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>
<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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">static</span></span> </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>
<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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">static</span></span> </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>
<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>
<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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">static</span></span> </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>
<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>
<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>
<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>
<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>
<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>
<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>
<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>
<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>
<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>
<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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">static</span></span> </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>
<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>
<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>
<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>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<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></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </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>
<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>
<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__arith3_8cpp_source.html#l01449">CVC3::TheoryArith3::normalizeProjectIneqs()</a>, <a class="el" href="theory__arith__old_8cpp_source.html#l01822">CVC3::TheoryArithOld::normalizeProjectIneqs()</a>, <a class="el" href="theory__arith__new_8cpp_source.html#l00507">CVC3::TheoryArithNew::processSimpleIntEq()</a>, <a class="el" href="theory__arith3_8cpp_source.html#l00759">CVC3::TheoryArith3::processSimpleIntEq()</a>, and <a class="el" href="theory__arith__old_8cpp_source.html#l00739">CVC3::TheoryArithOld::processSimpleIntEq()</a>.</p>
</div>
</div>
<a class="anchor" id="a4564697c1b2ea1e3a70ef36383ca1c41"></a>
<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>
<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>
<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>
<h2 class="groupheader">Variable Documentation</h2>
<a class="anchor" id="a6ab61b1ab2bcdf0a5384bb93d3fb7ac2"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> null_expr</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">static</span></span> </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>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const int FOUND_FALSE = 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><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:16 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>
