<!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: Member List</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 class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="hierarchy.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a> </li>
<li class="navelem"><a class="el" href="classCVC3_1_1VCL.html">VCL</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="headertitle">
<div class="title">CVC3::VCL Member List</div> </div>
</div>
<div class="contents">
This is the complete list of members for <a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a>, including all inherited members.<table>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a8e7b1855a671cd3684319b371a28f2f9">addPairToArithOrder</a>(const Expr &smaller, const Expr &bigger)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a6e5209f607aaaaeedbdc69e56afd13b3">andExpr</a>(const Expr &left, const Expr &right)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a8467914594e6a5346398bb46a82bb310">andExpr</a>(const std::vector< Expr > &children)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a1b3d360dba2a71284d04c7b1465ca757">arrayType</a>(const Type &typeIndex, const Type &typeData)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#aea0cd6db38e63d1c40bf79f21251566c">assertFormula</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a36b8bf3bc3abab2decfa04faee15f4fb">bitvecType</a>(int n)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ad344206a7bab732b8b08a86a4cd530dd">boolType</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a52edb765ba784038221c6e4ea9d359af">boundVarExpr</a>(const std::string &name, const std::string &uid, const Type &type)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#af4f8f201c7915eb1f762612375e6ccec">checkContinue</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ae3fdb7172562507072fb05f19561e7ef">checkTCC</a>(const Expr &tcc)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a5f4dea7a2339b50b34ddb6514a028130">checkUnsat</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#aab6dff108d0fe7154e4fe1d6573f7d7e">cmdsFromString</a>(const std::string &s, InputLanguage lang)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a04480c805a21d6a1661b9c113b9f2cdc">computeBVConst</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a574d03796ebbc4d20e668172ac97e581">core</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ValidityChecker.html#a7f8784feff00600cda0508c4050a8976">create</a>(const CLFlags &flags)</td><td><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td><code> [static]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ValidityChecker.html#ae2876962373b8e7cefd5909160e4729d">create</a>()</td><td><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td><code> [static]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ValidityChecker.html#ab2cf736ffff14ff2254c407be3f49334">createFlags</a>()</td><td><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td><code> [static]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ac277dff0e38bab93673461c41898b0cc">createOp</a>(const std::string &name, const Type &type)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a49590168c0338addd56e63641709ebea">createOp</a>(const std::string &name, const Type &type, const Expr &def)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a9f16ab34b0b1f7e5dfe17390dd72c39f">createType</a>(const std::string &typeName)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a6fefe58ed7b305b789f5c8cc45e99a04">createType</a>(const std::string &typeName, const Type &def)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#aa6c54159235f97cb9efc0e759070776a">d_batchedAssertions</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ac8ea2beb5efa17c968e7312db331ef83">d_batchedAssertionsIdx</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a2b40a6191db7398dc35d7294ef7f5cf5">d_cm</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#af81bf916ed823bb6578a35fb555a4a5a">d_dump</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a82e3b0230008233cddbb44489238097f">d_em</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ac56c9b24bf7e95089f59acd4b8795aef">d_flags</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a44bab91924f750908ea96a44feb37a15">d_lastClosure</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ac7b0947fe5b3c9c737828be483ba27de">d_lastQuery</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a1a8b62c258a4104da2ee425761e06d34">d_lastQueryTCC</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a98a4d96994e90f013ce7ddeeaea617e9">d_modelStackPushed</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a453046f429f9d2529b00be9c0e573ac7">d_nextIdx</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ab21d710d786fc113e73da60c2201f237">d_se</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ac5d3b29754d41125c6f0eec7de1f8fd3">d_stackLevel</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a3c7c5a1be001f03b02670ddbc5ff8c5e">d_statistics</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#afa0de50278d9008bb8da2e53d1842810">d_theories</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a7ecdb7ee559f64dad9c090985ac6c64b">d_theoryArith</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a7bef1476e19d2ac7c3e39f108cff1438">d_theoryArray</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a4feddacffa44b4ecffd88dd1c1ef5f5f">d_theoryBitvector</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a83c1ecc49a06d59154fcec151115ee41">d_theoryCore</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ab8fd0353a6ebea5268cb6bf75e43edbb">d_theoryDatatype</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a67512d691a8bbdfcf5a599beb6d881db">d_theoryQuant</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#af0fa33ca11ef9598d27baa79a20b7d06">d_theoryRecords</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a4c9b122ddd801eea777472c9f49aa6dd">d_theorySimulate</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a36a31c39519edb4c051724d0fe684e9f">d_theoryUF</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ae2de028959c8cb591ece07d6a0ad6fd2">d_tm</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a283c9912783c441bba4b59339c5e6f53">d_translator</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a00dfc7df82e450d5eaabce47f33657eb">d_userAssertions</a></td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a0e4c14571fa8b5e85654e8a4c5cdeff3">dataType</a>(const std::string &name, const std::string &constructor, const std::vector< std::string > &selectors, const std::vector< Expr > &types)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#adeb6c1750f63ed133f8da731fcd0a870">dataType</a>(const std::string &name, const std::vector< std::string > &constructors, const std::vector< std::vector< std::string > > &selectors, const std::vector< std::vector< Expr > > &types)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ae65bc001e859cb1bb90093335767a12c">dataType</a>(const std::vector< std::string > &names, const std::vector< std::vector< std::string > > &constructors, const std::vector< std::vector< std::vector< std::string > > > &selectors, const std::vector< std::vector< std::vector< Expr > > > &types, std::vector< Type > &returnTypes)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#aec600c20c4157a459c29e78989ecdfc1">datatypeConsExpr</a>(const std::string &constructor, const std::vector< Expr > &args)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a62f5f50e1c29fd9571cb5c69b0fcc6e5">datatypeSelExpr</a>(const std::string &selector, const Expr &arg)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a6e732eeb679d7bd8023548a1b5e8d1e5">datatypeTestExpr</a>(const std::string &constructor, const Expr &arg)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#abbb03bdcc2bbe1354740884e56de90cc">deriveClosure</a>(const Theorem3 &thm)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a106a8117c3f249e2cc0a3e3a13f9740a">destroy</a>(void)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#adcea906016ca3187ea900f1d756db280">distinctExpr</a>(const std::vector< Expr > &children)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#acabb3affe2525e363aa6c361305de34e">divideExpr</a>(const Expr &left, const Expr &right)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a4f17e52a13206ce3ad8c5d86cd9de037">eqExpr</a>(const Expr &child0, const Expr &child1)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a31a2891fc46ffcc5defeb229e2a12d07">existsExpr</a>(const std::vector< Expr > &vars, const Expr &body)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a15bb1224861f7a92d4ab9fe6b6fff0f0">exprFromString</a>(const std::string &s)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a87be808345d6e2ee8015443c0cdd129a">falseExpr</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#af6092976dbe77be8467d2c7e61bcd1aa">forallExpr</a>(const std::vector< Expr > &vars, const Expr &body)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a59bf75e014217aefa07096d1729e6b2d">forallExpr</a>(const std::vector< Expr > &vars, const Expr &body, const Expr &trigger)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a88bf58cbbfa14bc15c5dbb8cf7ba3ecc">forallExpr</a>(const std::vector< Expr > &vars, const Expr &body, const std::vector< Expr > &triggers)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#aba40de981b8807c20c707c094a96b976">forallExpr</a>(const std::vector< Expr > &vars, const Expr &body, const std::vector< std::vector< Expr > > &triggers)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a1421f580601f509b1e7ff7ca8b2f8e9f">funExpr</a>(const Op &op, const Expr &child)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#abe89cf2af04179a93a2a27485e6c9473">funExpr</a>(const Op &op, const Expr &left, const Expr &right)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ae17dc6e81ba5fc1f854d7e223ecfe820">funExpr</a>(const Op &op, const Expr &child0, const Expr &child1, const Expr &child2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ae99d54ff8ff60083b35678f6943f61c8">funExpr</a>(const Op &op, const std::vector< Expr > &children)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a574fecab80d464a244d391312d2ab898">funType</a>(const Type &typeDom, const Type &typeRan)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#adcc7672eceaadf25f03cf8f74b036724">funType</a>(const std::vector< Type > &typeDom, const Type &typeRan)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#aa04879197ff8c223ef9e95022a3b5003">geExpr</a>(const Expr &left, const Expr &right)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a170bc9df9cdfb20b02256d0779385ecd">getAssignment</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a2ec20cac361d8ffd161fed6fb47bef16">getAssumptions</a>(const Assumptions &a, std::vector< Expr > &assumptions)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a85b907166d3a2400e9ced227a5133d51">getAssumptions</a>(std::vector< Expr > &assumptions)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a09efdca949d7b5d2192e74c33604a340">getAssumptionsRec</a>(const Theorem &thm, std::set< UserAssertion > &assumptions, bool addTCCs)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ad15c979254ddf1bf3d077f299dc85e35">getAssumptionsTCC</a>(std::vector< Expr > &assumptions)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#af4022f5b9fa00e3b497143d3c042547e">getAssumptionsUsed</a>(std::vector< Expr > &assumptions)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#afb33aac5733ec0c5d186388b55d8d1f1">getBaseType</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a523146e4e023cbb4110f9906e96ce861">getBaseType</a>(const Type &e)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#aef495640a259f901152b5dc43d541633">getClosure</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a14239feee2666a95a4b4d514d5ce4cb7">getConcreteModel</a>(ExprMap< Expr > &m)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a78c08c36ccc94ca3222a2ea7ab4fb558">getCounterExample</a>(std::vector< Expr > &assumptions, bool inOrder)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#abb99bb93652210f73799830b5974aaa5">getCurrentContext</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a811f456c7be235f67a45c9359475f770">getEM</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [inline, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a499633a949434b41a8555d0cf6e435f6">getFlags</a>() const </td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [inline, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#af6906b893f5e64392d83664cc977a5cd">getImpliedLiteral</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a6892f923575572e122a09b706a7f21fb">getInternalAssumptions</a>(std::vector< Expr > &assumptions)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a6d3042cf06ef777fca838f600fb009fe">getMemory</a>(int verbosity=0)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ac251e9ad09e9c1846ba6032f29e5428d">getProof</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ac762d30a06609aa527064eade8241590">getProofClosure</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a42476ddbf6bbc848404e7e86c1e9976b">getProofQuery</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a78d06cf8f6910e635224e27d39d1079d">getProofTCC</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a2c6c8bea5a7157b00fffc255feffcd22">getStatistics</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [inline, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a9e603f49fd6223ca2ccb6727b205c617">getTCC</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a59c9d442ef836e4aea70dda513b8a29d">getType</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ae55b1e91aca97e231cf5288c7257998f">getTypePred</a>(const Type &t, const Expr &e)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ace44061f3aa2cb7653f03b3ae7befe61">getUserAssumptions</a>(std::vector< Expr > &assumptions)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#af22ef97200024412e3a6b49c88635390">getValue</a>(Expr e)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a39b6e5d030aa9aaf0bd57332cab4d5fc">gtExpr</a>(const Expr &left, const Expr &right)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a13142479360bbf0154be61ce7620f226">idExpr</a>(const std::string &name)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a67da7d1d56277df0d30c031565a04aa4">iffExpr</a>(const Expr &left, const Expr &right)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a633fc9e011f529f0992d604ea4b66b9b">impliesExpr</a>(const Expr &hyp, const Expr &conc)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a91662cae6c452f3d342face36e9eab77">importExpr</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a827601ba5a9150c94e8ae3c1ac67839b">importType</a>(const Type &t)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#abb721e41cd062c4d629db1dbe7c8b23a">incomplete</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ae4c250b81ad25e02b54d283ed6359c35">incomplete</a>(std::vector< std::string > &reasons)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a0af2aa4f9b6df1bb331eafa9fc4f25a5">inconsistent</a>(std::vector< Expr > &assumptions)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a459dc08bbf0d900d4f368ab1f40a4cf4">inconsistent</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a8e8d0e2a3eed319ecfca2aba48e642eb">init</a>(void)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [private]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#aba7fbeffde84d5f4e789f52aac61fe1d">intType</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a87991a89b4411b323746c8b588d9848f">iteExpr</a>(const Expr &ifpart, const Expr &thenpart, const Expr &elsepart)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a9cdd152a9dc4d6b69a3abb7c48ce9151">lambdaExpr</a>(const std::vector< Expr > &vars, const Expr &body)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a5cf90d2c620b7e4f521cdd2affa85d9f">leExpr</a>(const Expr &left, const Expr &right)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a92cd091e843eafa303aa1fe8cbe0f881">listExpr</a>(const std::vector< Expr > &kids)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a72ddc8e798ad18dc3db168e5029b13e1">listExpr</a>(const Expr &e1)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a930389cb9570297308eb5959f9e8442d">listExpr</a>(const Expr &e1, const Expr &e2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a9c1a8c014d62d307d0ecb68eda14e030">listExpr</a>(const Expr &e1, const Expr &e2, const Expr &e3)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#adee40e9cf75ecf2fd7f6e06f04fb4761">listExpr</a>(const std::string &op, const std::vector< Expr > &kids)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a113b6106484ceb0f0716603f21c906de">listExpr</a>(const std::string &op, const Expr &e1)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a0d491e327498b82725891b5ea9a5928c">listExpr</a>(const std::string &op, const Expr &e1, const Expr &e2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a00eff8291d17fa253566e48325bf3b7c">listExpr</a>(const std::string &op, const Expr &e1, const Expr &e2, const Expr &e3)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a22ebe140bc8edb5a4f2150828d7a63de">loadFile</a>(const std::string &fileName, InputLanguage lang=PRESENTATION_LANG, bool interactive=false, bool calledFromParser=false)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a335f72bbfb065244a109142c79d73eeb">loadFile</a>(std::istream &is, InputLanguage lang=PRESENTATION_LANG, bool interactive=false)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#aa9830a10a07a840c3cde40c86160d0e4">logAnnotation</a>(const Expr &annot)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#abf7359c0359f4e1bbf24c5f8fe93f9f0">lookupOp</a>(const std::string &name, Type *type)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a90fd1c2ef6f64c534916b905e4b4e802">lookupType</a>(const std::string &typeName)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a23460fae006d9ef030f8908ab732b0ef">lookupVar</a>(const std::string &name, Type *type)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#aee9a9ef0742792f7c1357154f1d2a190">ltExpr</a>(const Expr &left, const Expr &right)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a41b81d8fe76fa4bb44a69e16dfed7dc6">minusExpr</a>(const Expr &left, const Expr &right)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ac3d1c85bda8df4d88efb626cb7715244">multExpr</a>(const Expr &left, const Expr &right)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a0fd006b863de61f56d243522d41082ed">newBVAndExpr</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a17593d9ec67a755c50f751dffe8b4629">newBVAndExpr</a>(const std::vector< Expr > &kids)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a6066ea30e01094ecec5da8c3495b3f16">newBVASHR</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a1a1e3f3f38cb6f11681b2dd236ee9f2f">newBVCompExpr</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ad808ce75e7443dec968f150527c7e13f">newBVConstExpr</a>(const std::string &s, int base)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a70b9632e4c948f67117bc1fe56a1aafa">newBVConstExpr</a>(const std::vector< bool > &bits)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ab4a55736ee4768e8857885988e00d77f">newBVConstExpr</a>(const Rational &r, int len)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a4eddf5c30347830b147179e7eb6732bf">newBVExtractExpr</a>(const Expr &e, int hi, int low)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#aafa81880381e35ca26e79d5fb7dbb923">newBVLEExpr</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a3918baa97a08c2d921a071aeae1620ab">newBVLSHR</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#afbcef11e642cd00f7dc4abeca0c67890">newBVLTExpr</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a7435145013feee0f53d6a81fd1942f85">newBVMultExpr</a>(int numbits, const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a7d208c54bf0609c3f0f634f70947ee75">newBVNandExpr</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a15a2cba3773e26da60610ddf3f1f20fb">newBVNegExpr</a>(const Expr &t1)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#aea79ee80d345a7e49f80038db8a5b904">newBVNorExpr</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a850bc85eb4f08da10eaca359f8510b00">newBVOrExpr</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a6bfaea51e4c360ab46d82c964289123c">newBVOrExpr</a>(const std::vector< Expr > &kids)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#aa57e50da2a4941aa09539ca28066b672">newBVPlusExpr</a>(int numbits, const std::vector< Expr > &k)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#aa349bae1e41c1ba6223fa8fbfedf531f">newBVPlusExpr</a>(int numbits, const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a1479e6734fcdf11520f3b653cd1436d1">newBVSDivExpr</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a981627b5d8100269392c1a1daf2776d7">newBVSHL</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a356c133efc5c121fa96e3006f2ef081e">newBVSLEExpr</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a1f9cdb1f89dd900659b46fdf3ab80f16">newBVSLTExpr</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a22457c0b227803396b927b8cae0d0a9c">newBVSModExpr</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a4179f0c70e3530b54a4e94879a76ea42">newBVSRemExpr</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a1632f50800db737db3a0fb757bac79f7">newBVSubExpr</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ac9670fe188638ce265f77904c14db441">newBVUDivExpr</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a4311e3b750558bf8a1b37d42c9874abc">newBVUminusExpr</a>(const Expr &t1)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a743a8cf8a7f08257fd3cb24674fa0304">newBVURemExpr</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ae5969df90d601a8aa881391653839d4e">newBVXnorExpr</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#adb46114412c8b2b967a213b9749642a2">newBVXnorExpr</a>(const std::vector< Expr > &kids)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a22b8c4a8b8e10feac5a0cb2be04b64e7">newBVXorExpr</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a2f95f00a6aad1ea0f7c55cdd896ef6d8">newBVXorExpr</a>(const std::vector< Expr > &kids)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a953786b640a1dedcef7d8e79907073f1">newConcatExpr</a>(const Expr &t1, const Expr &t2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#abf90bf1abdb42ca036171d6c70863165">newConcatExpr</a>(const std::vector< Expr > &kids)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#acf0785a00fa5a359f9313556a4da5529">newFixedConstWidthLeftShiftExpr</a>(const Expr &t1, int r)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a7ed70646c308375d2909680c34b959b2">newFixedLeftShiftExpr</a>(const Expr &t1, int r)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a2b35f788365e50336e4b6c0a462c23de">newFixedRightShiftExpr</a>(const Expr &t1, int r)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ad865f8a255fa67367cb1260598b68c3c">newSXExpr</a>(const Expr &t1, int len)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a0e605dfe1b15e52663073f05c44a2fd6">notExpr</a>(const Expr &child)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a000ff901b570233b669fb61786f81827">orExpr</a>(const Expr &left, const Expr &right)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ad3ac4c516a060c3fa03a4cd52506e4b3">orExpr</a>(const std::vector< Expr > &children)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a52fb774eea4d48077d8c95f4e1d124d1">parseExpr</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ae56f7fe27f179fbaa01299e3c91a74cf">parseType</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#adad9006fd502d1d9ff190a8a4a343905">plusExpr</a>(const Expr &left, const Expr &right)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#adb4461aac312f9681f4b410dcf5396e9">plusExpr</a>(const std::vector< Expr > &children)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a4ce3054f8f8cc88c5a4933408776d1a6">pop</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ad44c144ec31ebd2bb327070395d0d7fe">popScope</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a330c7d817571648e016de1cfa8f15dea">popto</a>(int stackLevel)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a72d3528e64b5695df57c7d9b4fd671b2">poptoScope</a>(int scopeLevel)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a686b064b5030c7d3bcf8aea018ed556f">powExpr</a>(const Expr &x, const Expr &n)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a12f292f435d36c466292267e9f6425e5">printExpr</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ab02f9ebeef419f59aa94fc19842f26e0">printExpr</a>(const Expr &e, std::ostream &os)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a29fe4941b5cbb201d7918afeac0dc3cb">printStatistics</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [inline, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a551314970fbd6bae877a9e634da5e0e8">push</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a2a1a1c5fc74e90b471a6d0fbd7407e21">pushScope</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#aebafad6eace10f8aa2687cc6c600c53e">query</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#acfc983096f1d7aa9799d360a9cef8d3b">ratExpr</a>(int n, int d)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a0bb82227b049be1571cd1ac76c6fd713">ratExpr</a>(const std::string &n, const std::string &d, int base)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a08c469b8571beb3d14ec94c43383c491">ratExpr</a>(const std::string &n, int base)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a84a759c7fa5b4ec5ddb84c883bdf75a5">readExpr</a>(const Expr &array, const Expr &index)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#aea5eb2afa1a4917c1251340f22a7f54b">realType</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#afe7f6ce6960db261e58d996e00164d64">recordExpr</a>(const std::string &field, const Expr &expr)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a9259afee51e2d525bc6ae192f534b686">recordExpr</a>(const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#aa6a023a06bfaec39f2c2dbf5b4e1e8dc">recordExpr</a>(const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1, const std::string &field2, const Expr &expr2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#af456da30bbb52b31fdc77971b71d47bf">recordExpr</a>(const std::vector< std::string > &fields, const std::vector< Expr > &exprs)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a5402e161e9f0c8158f3ffc99ffee7585">recordType</a>(const std::string &field, const Type &type)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a446a3a15b247192930dccfc6d9c1939e">recordType</a>(const std::string &field0, const Type &type0, const std::string &field1, const Type &type1)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ac56448d9022fd70d82949cc679b206f1">recordType</a>(const std::string &field0, const Type &type0, const std::string &field1, const Type &type1, const std::string &field2, const Type &type2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ad1bec7c4c41438b50c0c287852fa3312">recordType</a>(const std::vector< std::string > &fields, const std::vector< Type > &types)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#abdf0c8d98e38c5b824e2ea7473eb3e55">recSelectExpr</a>(const Expr &record, const std::string &field)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a38d7fbf8d93c20be9924f26fe437ade6">recUpdateExpr</a>(const Expr &record, const std::string &field, const Expr &newValue)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a54c9ceeaa6e94edd5af791d4fec621f5">registerAtom</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a83197a54652f37925771d6de682a54a9">reprocessFlags</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ab21a08026f0fbc5e58619874952a7745">reset</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#afd3d88e7e58e6098c9f570fc7e812547">restart</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#af2cf35f9a462d155002d5684c817052f">returnFromCheck</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#aad6deac1e5b9eca3637a1e774cd082dc">scopeLevel</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a38721614a497ca377725ae2e4651afce">setMultiTrigger</a>(const Expr &e, const std::vector< Expr > &multiTrigger)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a1564c391386056f59b20973e3436c9ae">setResourceLimit</a>(unsigned limit)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a88cf6568b5efb0707a44db0436572ead">setTimeLimit</a>(unsigned limit)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a89f6413e4777f866048cfe8922d28c74">setTrigger</a>(const Expr &e, const Expr &trigger)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a1c4ae115cdfbc91f2655b2a7d14a4179">setTriggers</a>(const Expr &e, const std::vector< std::vector< Expr > > &triggers)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#abed8eb2bc5db4894605aa32c9f3a36ef">setTriggers</a>(const Expr &e, const std::vector< Expr > &triggers)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a21bd43458adee37cf07946df6801c06f">simplify</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a0d31184262b06af8779994646ce18eaf">simplifyThm</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a9ab50d02ab11cfd598cdc9b6684b7758">simulateExpr</a>(const Expr &f, const Expr &s0, const std::vector< Expr > &inputs, const Expr &n)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ac43f348af95c325526a514e5c65d5871">stackLevel</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a2598c55b4d6b4cac912ff4e2f46239dc">stringExpr</a>(const std::string &str)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a79a94f22666ae19579e55ae2cc6318a4">subrangeType</a>(const Expr &l, const Expr &r)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a31aecd4893d74a75daeef186e3b8f81e">subtypeType</a>(const Expr &pred, const Expr &witness)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a71d76efee21313adcdf56240c27745ab">transClosure</a>(const Op &op)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a779d3811f66b5cf54b679e8a708bc292">trueExpr</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a39611be62fadaaeadcd97f84cbc7e162">tryModelGeneration</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a1a6f8cc80b6041ab02e6213a39862af4">tupleExpr</a>(const std::vector< Expr > &exprs)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a7c0e2b25a828d0e637cdc4f89fe9378c">tupleSelectExpr</a>(const Expr &tuple, int index)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ac2e6baf2eeb267e1b8f12392070ad787">tupleType</a>(const Type &type0, const Type &type1)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a9ebfe8a0227e0dae6800e9ba31fb262f">tupleType</a>(const Type &type0, const Type &type1, const Type &type2)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a1be510191730f07d749f283e91c212a0">tupleType</a>(const std::vector< Type > &types)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ac2ab260c25eaff6d52378d66563a2ddd">tupleUpdateExpr</a>(const Expr &tuple, int index, const Expr &newValue)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ab62447c6c1a4f71eeeb6d8aa665bbdc2">uminusExpr</a>(const Expr &child)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ValidityChecker.html#a15399f370b5af3e31e1ee2add14470bf">ValidityChecker</a>()</td><td><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td><code> [inline]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#aae01a35fe02e9097aba1277b428c94fc">value</a>(const Expr &e)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#a434b487f2d0aaf3a2bfcd86716cfa566">varExpr</a>(const std::string &name, const Type &type)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ae3dc0d1d7ab4c060d79f90ce683f6613">varExpr</a>(const std::string &name, const Type &type, const Expr &def)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ab10a1284f50157d26caca145f8335cd1">VCL</a>(const CLFlags &flags)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ab7da4a56f788600a62c928917d74c540">writeExpr</a>(const Expr &array, const Expr &index, const Expr &newValue)</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td><code> [virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1ValidityChecker.html#a4ba951ee63a5a1ffb804f282980a1a68">~ValidityChecker</a>()</td><td><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td><code> [inline, virtual]</code></td></tr>
<tr class="memlist"><td><a class="el" href="classCVC3_1_1VCL.html#ac65059211da91a793d0df775763c7f68">~VCL</a>()</td><td><a class="el" href="classCVC3_1_1VCL.html">CVC3::VCL</a></td><td></td></tr>
</table></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>
