<!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: Member List</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 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="inherits.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_1ValidityChecker.html">ValidityChecker</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">CVC3::ValidityChecker Member List</div> </div>
</div><!--header-->
<div class="contents">
<p>This is the complete list of members for <a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a>, including all inherited members.</p>
<table class="directory">
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a56eb352f856ddbad57c5d59386c6b707">addPairToArithOrder</a>(const Expr &smaller, const Expr &bigger)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#af8222f001fe69abe9c4a856e2e9a935a">andExpr</a>(const Expr &left, const Expr &right)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a782499c21bc5c36f7de7e9cc8a1a2997">andExpr</a>(const std::vector< Expr > &children)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aae1f7ef4714ecdadb4d0b63a0145a442">arrayType</a>(const Type &typeIndex, const Type &typeData)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ad57f0a783141d3c7b0424102ea8724ac">assertFormula</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a3258e23feb3ab38beeff3e72121ac6f0">bitvecType</a>(int n)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aa86f4ae2faff53326d76f0d7bbc45198">boolType</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a1b5cf16e412204959d3bc2e5f4ba9d73">boundVarExpr</a>(const std::string &name, const std::string &uid, const Type &type)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a7be9a77c0c8cbce185d02f5e5f40d21a">checkContinue</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a66b10d795e7ecfa0fa8ce8b69eb07c10">checkUnsat</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a62a2ba9f59ad2cad1ff64a60d4f8b0db">cmdsFromString</a>(const std::string &s, InputLanguage lang=PRESENTATION_LANG)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a330c358aff5ee5e0b73e12699448e5cf">computeBVConst</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a7f8784feff00600cda0508c4050a8976">create</a>(const CLFlags &flags)</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">static</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ae2876962373b8e7cefd5909160e4729d">create</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">static</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ab2cf736ffff14ff2254c407be3f49334">createFlags</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">static</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#af4c4ae47ec16622d9e2a9d9df8142b4f">createOp</a>(const std::string &name, const Type &type)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#abde9fa1109c88f65e2034ec6d1a30d46">createOp</a>(const std::string &name, const Type &type, const Expr &def)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aaaef06da81d945fb5fd75cc134f80ca5">createType</a>(const std::string &typeName)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a35edea60cb51fde8ab8025d7956ecc25">createType</a>(const std::string &typeName, const Type &def)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a6cc46f1745f4296f9479479a58d3db6d">dataType</a>(const std::string &name, const std::string &constructor, const std::vector< std::string > &selectors, const std::vector< Expr > &types)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a02598f355a0454ac3e154695b3419661">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)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a3b3cc340170bbab622f36f36c3cb63e9">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)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a199639435bcf617344a134ee69ea34aa">datatypeConsExpr</a>(const std::string &constructor, const std::vector< Expr > &args)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a891eae13d340b39b32b3fc92850d2ce0">datatypeSelExpr</a>(const std::string &selector, const Expr &arg)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a31cd218b72bbf503568e894d9d5f0d06">datatypeTestExpr</a>(const std::string &constructor, const Expr &arg)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a87e95d316f668b4c7c4e12f5cb4fcbef">distinctExpr</a>(const std::vector< Expr > &children)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#af61a10ae50d4d513c09f76dddd11223e">divideExpr</a>(const Expr &numerator, const Expr &denominator)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a9f38181a6d1dcb0540301e68f444f45a">eqExpr</a>(const Expr &child0, const Expr &child1)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ad61bd94dda8f8f4352825ea546f82ed7">existsExpr</a>(const std::vector< Expr > &vars, const Expr &body)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ae6916c7ceb64dca00922dfccd5882aa6">exprFromString</a>(const std::string &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a9050dd9dbfb463a488d6f9fe98ef968a">falseExpr</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ac206ae42778d68f60f96d5b086cdf664">forallExpr</a>(const std::vector< Expr > &vars, const Expr &body)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a26c6a6fe5b7c71bdcea6777d9da65b22">forallExpr</a>(const std::vector< Expr > &vars, const Expr &body, const Expr &trigger)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ae0acc6220fdf5384faff502fabb37725">forallExpr</a>(const std::vector< Expr > &vars, const Expr &body, const std::vector< Expr > &triggers)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a6c0a38d28c5971d191b5dd47ca5bd640">forallExpr</a>(const std::vector< Expr > &vars, const Expr &body, const std::vector< std::vector< Expr > > &triggers)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a5c19fd5e1a8e43a8883eca58ad797ed5">funExpr</a>(const Op &op, const Expr &child)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a8673ac26f4037bee851cf5f656961c4b">funExpr</a>(const Op &op, const Expr &left, const Expr &right)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a37857ca31df69f5feda44ab7d83b9744">funExpr</a>(const Op &op, const Expr &child0, const Expr &child1, const Expr &child2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#af65af33c8863feca3060c1a81b0e3529">funExpr</a>(const Op &op, const std::vector< Expr > &children)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a2186221f05f3990b9eded526d24211be">funType</a>(const Type &typeDom, const Type &typeRan)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aa0648db7219413e066d9aa24b932af44">funType</a>(const std::vector< Type > &typeDom, const Type &typeRan)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a74b157ad937af0cac261946a38ea332d">geExpr</a>(const Expr &left, const Expr &right)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ad9650915ed1bd526642a9c8d059e7e37">getAssignment</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a3a38ef396cf06f30bb5bceb5249716e1">getAssumptions</a>(std::vector< Expr > &assumptions)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a48cceb9c7004dc5887e4f5067b8bc77a">getAssumptionsTCC</a>(std::vector< Expr > &assumptions)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a9cde84236d816aebd6c0a6c78c0c597e">getAssumptionsUsed</a>(std::vector< Expr > &assumptions)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a8422058e2d91a225252aca7e4234666b">getBaseType</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a5719a951194add8706db1ae0668f91ab">getBaseType</a>(const Type &t)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a31e9c1b41d4887a377af5af9c43586da">getClosure</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a40c96301728846e2e3cc913ca716f897">getConcreteModel</a>(ExprMap< Expr > &m)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a4e3b0f9d1129f476f116ad766105ddad">getCounterExample</a>(std::vector< Expr > &assumptions, bool inOrder=true)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aebd7d6618f53f20bb08d091f624277cf">getCurrentContext</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a448e0df25ec6d756861e7d1d217f1063">getEM</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a9a09f71dc5a3dd47f0240abceab2fad3">getFlags</a>() const =0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ad8983a33e3540b26cbdc37d3017caa89">getImpliedLiteral</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a406c7204afd077131364090d7049f07c">getInternalAssumptions</a>(std::vector< Expr > &assumptions)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ae82f9d7b8b0584323baa04d7d99a1ba4">getProof</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a28fcabfa37fb118b722525255f0d3b98">getProofClosure</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a93e30f775885bd6ebe8d8fab162139ef">getProofQuery</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a92b98914e5abc57e902e2afc431615ed">getProofTCC</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ae2b134cb3f8caf1d2bac8a257bc95819">getStatistics</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a7a46eaebfca225ea519648db19d6c904">getTCC</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ac400a59525f16fe303e052cbff3d1dae">getType</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#add33b9e05f224922b1a2e4563af8d115">getTypePred</a>(const Type &t, const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a1e21fa2a9b7176bda081fe4516295bbd">getUserAssumptions</a>(std::vector< Expr > &assumptions)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ab946acc8d84a44eb7bfec63d42bb0b91">getValue</a>(Expr e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a51bb953c045384b30acbca69eca53b2f">gtExpr</a>(const Expr &left, const Expr &right)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a6f312184c35aef5dd85e0c6c190380a1">idExpr</a>(const std::string &name)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a511f5b02036944b06b3d93b1f65f489f">iffExpr</a>(const Expr &left, const Expr &right)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ab4b31fcadd98a16e3f63e2daec6a6799">impliesExpr</a>(const Expr &hyp, const Expr &conc)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ab1ca7951861c04f7b639732b933d1861">importExpr</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a280e966c77bb0ea5dc6848b1174c46b1">importType</a>(const Type &t)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a20580108288f5df03a54076a9bd8fed5">incomplete</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a92c7ba802985d0722843c4b9678bf8f8">incomplete</a>(std::vector< std::string > &reasons)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aef6a6eb5eb79e61a2e754ddbb65504a8">inconsistent</a>(std::vector< Expr > &assumptions)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aaf2a1447b7618070f993e8d0aafc6044">inconsistent</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ad93120c84052c413953cf7fcd3c95048">intType</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a786cae5bef71cdbe8cab9f773a35f4a7">iteExpr</a>(const Expr &ifpart, const Expr &thenpart, const Expr &elsepart)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a4530620e9da6098c859b97563ed98037">lambdaExpr</a>(const std::vector< Expr > &vars, const Expr &body)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a9dc437cff8d309fa99cbd90b3ad55341">leExpr</a>(const Expr &left, const Expr &right)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a9e157d46874e099d9330437aa0c72921">listExpr</a>(const std::vector< Expr > &kids)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a69b6549c4b8c5b0359a178a702092ca1">listExpr</a>(const Expr &e1)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a0a1c99ce1610410633f64f15b072cbac">listExpr</a>(const Expr &e1, const Expr &e2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a33bcc63389cbaa2b4ed57dc27ced550c">listExpr</a>(const Expr &e1, const Expr &e2, const Expr &e3)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aaa1477d189f7a4d371db6c64e34425fe">listExpr</a>(const std::string &op, const std::vector< Expr > &kids)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a91ba6ab255bd8c21b213d86c8c278cff">listExpr</a>(const std::string &op, const Expr &e1)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a5539561d6b46cb09e28d9fb9f5625378">listExpr</a>(const std::string &op, const Expr &e1, const Expr &e2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a8bf6c06961a950b75896d5541a29a5e0">listExpr</a>(const std::string &op, const Expr &e1, const Expr &e2, const Expr &e3)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a68a96b7331b5a81b67c600cec05bbf8e">loadFile</a>(const std::string &fileName, InputLanguage lang=PRESENTATION_LANG, bool interactive=false, bool calledFromParser=false)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a73171527f6a3385c99e2376f8e4f9f18">loadFile</a>(std::istream &is, InputLanguage lang=PRESENTATION_LANG, bool interactive=false)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a6f81650a2585c2698d30225c37754acf">logAnnotation</a>(const Expr &annot)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a96eb85aad0bdafe47b24f3d8666851b8">lookupOp</a>(const std::string &name, Type *type)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aee7ad74875ca4ac07a4cdf9e5089584b">lookupType</a>(const std::string &typeName)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ac6f1a71f35354ac7d1e28073e47b889f">lookupVar</a>(const std::string &name, Type *type)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a7cef5cc2b578e99e8939ad76711e495c">ltExpr</a>(const Expr &left, const Expr &right)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a980a35d1a660890e16a66a7c1bfd6ba0">minusExpr</a>(const Expr &left, const Expr &right)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ab1b58d4021a8e31263908cd5bee33e32">multExpr</a>(const Expr &left, const Expr &right)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a7e50b3d60b806d79d5d97af6eba19728">newBVAndExpr</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aa296310ead028a1818684badd1b626a3">newBVAndExpr</a>(const std::vector< Expr > &kids)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a10500cd28b37adb1506da26936b866b1">newBVASHR</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ad47dc2aa5cb69948ca184b76d0b8bac3">newBVCompExpr</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a8d7cfd2bc38e6608e8fabccf396182f6">newBVConstExpr</a>(const std::string &s, int base=2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a28499d277d7ca254bb6f27231e5ea7ad">newBVConstExpr</a>(const std::vector< bool > &bits)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a55feceb97242f35f5e6e0beba486a9e2">newBVConstExpr</a>(const Rational &r, int len=0)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a551eb1485d629c284e29cb8eeb776ed8">newBVExtractExpr</a>(const Expr &e, int hi, int low)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ae1ea9da1883a75470f13bfca8f2614df">newBVLEExpr</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ae73dae1021a603627147fffb53765ee5">newBVLSHR</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a198d8a4d7933db5372b99671e0b27771">newBVLTExpr</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a7d2751f32319f1758e53d41d14b2d469">newBVMultExpr</a>(int numbits, const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#afc90e5d6df401f5649b861e46c952dfb">newBVNandExpr</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ad57809ddb17768c8fd447627f9b6b90a">newBVNegExpr</a>(const Expr &t1)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#af28f37f86585ba30ba867e88355cf422">newBVNorExpr</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a98141c19a7abc59774f527b4f98bc1aa">newBVOrExpr</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ab0613b10344029d78ce4159850c0cc49">newBVOrExpr</a>(const std::vector< Expr > &kids)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a23c5240a0e31c7a7e2347bdf17520526">newBVPlusExpr</a>(int numbits, const std::vector< Expr > &k)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a6ffaf04bb5e8b0cdabcb332714b954ed">newBVPlusExpr</a>(int numbits, const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ac141bc76b56a69a7f42d8a9185b76282">newBVSDivExpr</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aef98247579fe6a8d82e57ef39b3e5e59">newBVSHL</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#acc2e768b37eda39b33ace039431b2aff">newBVSLEExpr</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a61e842ef10b0d0cfa3f754f1f341db8a">newBVSLTExpr</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a2ae931f1eb92ae772d08cd0dd92c9028">newBVSModExpr</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ada8d6b6601f3483501b2991d0fb5ba05">newBVSRemExpr</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#abd84a40922bde06c6cb06128e89f5536">newBVSubExpr</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ad10093c8e25797c4ae394d8b592b9b0f">newBVUDivExpr</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a1153da8c9d561e38913edff9aa36c226">newBVUminusExpr</a>(const Expr &t1)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a8a5823232eb256efcb711b94900be93a">newBVURemExpr</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a4ae3ef20079db52d6c84de84364eb8af">newBVXnorExpr</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a3777362ed37835d5e1b2868cf2f57d73">newBVXnorExpr</a>(const std::vector< Expr > &kids)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ae1a6e8a5e57111a42db87e9d11e6b150">newBVXorExpr</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ae9a8fde34d2c8665b61b5148de63351b">newBVXorExpr</a>(const std::vector< Expr > &kids)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a194e5e6621de9203ff1b184a22c32b48">newConcatExpr</a>(const Expr &t1, const Expr &t2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#af0881961c56ba9e1cd5b4032eb0646aa">newConcatExpr</a>(const std::vector< Expr > &kids)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a2b425aabd7b4a7f0635d72834618f3dd">newFixedConstWidthLeftShiftExpr</a>(const Expr &t1, int r)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#acbe544873a0659f8a864d9ce3f463a50">newFixedLeftShiftExpr</a>(const Expr &t1, int r)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a182b0b4867a96e83bf725b1e566e98a0">newFixedRightShiftExpr</a>(const Expr &t1, int r)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a37a4a71934720db828f801c44da32240">newSXExpr</a>(const Expr &t1, int len)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a0f4ac83f5387e0d4033844fb0755cd2d">notExpr</a>(const Expr &child)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a57b5029fb74ce92d7978bf3d6b2d03a2">orExpr</a>(const Expr &left, const Expr &right)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a58e51a14fdad8ad5d8f846f0a824ca5a">orExpr</a>(const std::vector< Expr > &children)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ad1f1ac87cd8a210686d04eb82a6133c5">parseExpr</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aa20afe1496d2987a83ada2292c175af4">parseType</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a6046359a3839172691301d9757a3eeb1">plusExpr</a>(const Expr &left, const Expr &right)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a2b17a5ea1b6f80692257f44096c2ab00">plusExpr</a>(const std::vector< Expr > &children)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a3cee14a9c3b852b501a0594dd951f60c">pop</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aa619f5732634c9274efaf7a61d5de646">popScope</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a7448ad88871ee774e6de9eae725867ab">popto</a>(int stackLevel)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a4ce4e72785c769c641466c0477a50c24">poptoScope</a>(int scopeLevel)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a24381e7d9d7f45f7ef13c149d8b153cb">powExpr</a>(const Expr &x, const Expr &n)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a6f6909a3f7da22df2bf97b21319883eb">printExpr</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a2101d9c595f2d31f44ee5d5c1d8dc877">printExpr</a>(const Expr &e, std::ostream &os)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#adbbcda1a243c746f667bcba597482cd6">printStatistics</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a93cbbe8c21c2404b03ccaa43636d5f59">push</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aa6abf3f929951daba04f5e7874aa471c">pushScope</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a93b515a079fc8fdae5826dfcc343909e">query</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aec8119cdf4ae54522453bcc7bd38ee7c">ratExpr</a>(int n, int d=1)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a851711fb4ec7ad24d15cc19eb95269ff">ratExpr</a>(const std::string &n, const std::string &d, int base)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#abce3bbb3799ea401847be8855c8312b4">ratExpr</a>(const std::string &n, int base=10)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aa57f5268209bff87129ef39c711be6a4">readExpr</a>(const Expr &array, const Expr &index)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#af80938787dc3dc10d794cabcde2eedd9">realType</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ad855a87b02f19efb297d45778a7ca52f">recordExpr</a>(const std::string &field, const Expr &expr)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a486502a65e20eb2a842023fc13afbd0a">recordExpr</a>(const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a4f76dcae4a0b14df794453aade69e6d0">recordExpr</a>(const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1, const std::string &field2, const Expr &expr2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a762d5440e18fad5794d0969de0400edd">recordExpr</a>(const std::vector< std::string > &fields, const std::vector< Expr > &exprs)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ad9a6df13065bfc62ea5ece1513716835">recordType</a>(const std::string &field, const Type &type)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a33e7b277c1dda7aa16531561bc4d3997">recordType</a>(const std::string &field0, const Type &type0, const std::string &field1, const Type &type1)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a3c8d0b2262555d33ef81ffc462a97f45">recordType</a>(const std::string &field0, const Type &type0, const std::string &field1, const Type &type1, const std::string &field2, const Type &type2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#af0e24a3aa4ef5cc072a57e988e045f17">recordType</a>(const std::vector< std::string > &fields, const std::vector< Type > &types)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ae9fea52582c06a904679b4a844299313">recSelectExpr</a>(const Expr &record, const std::string &field)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a0a3ff4cc5a24717e6ab7f17ca9ea19c3">recUpdateExpr</a>(const Expr &record, const std::string &field, const Expr &newValue)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aa1cc8c465b3d30a3db3b1e9f86917606">registerAtom</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a0acc9330bfe47d579f1fa105d2603e85">reprocessFlags</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#accfa11d7cb5f45e4f73c01c09507f6b0">reset</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aefdc8ccae46e254d26b574d5d3ad6fc1">restart</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a021eced066a375b644402863e3435919">returnFromCheck</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a8e60da88d484801579c15960f41a3f72">scopeLevel</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a120871553bce7c74daaa544688a8e260">setMultiTrigger</a>(const Expr &e, const std::vector< Expr > &multiTrigger)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aae0d652a72139c5cf856a7eeb68874cd">setResourceLimit</a>(unsigned limit)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ae3a672c7d533a463b2cc0c850a67fda8">setTimeLimit</a>(unsigned limit)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a830a327a8bd9b90bb67a6189c18959c8">setTrigger</a>(const Expr &e, const Expr &trigger)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a9deb04632dc242cab8bc609a60d5c273">setTriggers</a>(const Expr &e, const std::vector< std::vector< Expr > > &triggers)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a32aef3bed0c68b9a279b977ab65b97db">setTriggers</a>(const Expr &e, const std::vector< Expr > &triggers)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a088a718e4f0041caea02312077a586c9">simplify</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a95230659969525d8bba737defd237736">simulateExpr</a>(const Expr &f, const Expr &s0, const std::vector< Expr > &inputs, const Expr &n)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ac1a5a5a29d08461ec42bc904524aa550">stackLevel</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ad40a03e7a5bc4b308ec2ca52b17845b0">stringExpr</a>(const std::string &str)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a5cc434a4b1279e19eda6f2a9fdb7ada3">subrangeType</a>(const Expr &l, const Expr &r)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aad96bcbbf85248e8444dfe61a8195b76">subtypeType</a>(const Expr &pred, const Expr &witness)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#aa2ffae23f96fba3e94b0eb2102bd515c">transClosure</a>(const Op &op)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a4e9d64bd0f01ce88b9e8494861ab527d">trueExpr</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a2c9bb81c75da36453ffb16a804a24605">tryModelGeneration</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a3cb64e29675d0e83c5627bf5fc0d3379">tupleExpr</a>(const std::vector< Expr > &exprs)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#ab65fb702c2a05091991c64c6296f7166">tupleSelectExpr</a>(const Expr &tuple, int index)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a4b2fa25ca712dabced8f9601150f64d5">tupleType</a>(const Type &type0, const Type &type1)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a4331cfc2d225141128ea420cf67ea0ec">tupleType</a>(const Type &type0, const Type &type1, const Type &type2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a2073f3aaa4d4b24eeb1ab953c7b45277">tupleType</a>(const std::vector< Type > &types)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#afa0dc38eaf0f6784b05bde26fb553220">tupleUpdateExpr</a>(const Expr &tuple, int index, const Expr &newValue)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a12f382fd07555fd752a1fdd73c229024">uminusExpr</a>(const Expr &child)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a15399f370b5af3e31e1ee2add14470bf">ValidityChecker</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a65c5205beaa041a5d390a5803e401bd3">value</a>(const Expr &e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a4dc02c11317b0f12606e5ec264dd9ca9">varExpr</a>(const std::string &name, const Type &type)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a06148508523578e0dbfa8c8cc6f5fdef">varExpr</a>(const std::string &name, const Type &type, const Expr &def)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a82d1cd4a539ba065a4d2aa7967af5000">writeExpr</a>(const Expr &array, const Expr &index, const Expr &newValue)=0</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html#a4ba951ee63a5a1ffb804f282980a1a68">~ValidityChecker</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1ValidityChecker.html">CVC3::ValidityChecker</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
</table></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:19 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>
