<!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: Class Members - Functions</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 class="current"><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="navrow3" class="tabs2">
<ul class="tablist">
<li><a href="functions.html"><span>All</span></a></li>
<li class="current"><a href="functions_func.html"><span>Functions</span></a></li>
<li><a href="functions_vars.html"><span>Variables</span></a></li>
<li><a href="functions_type.html"><span>Typedefs</span></a></li>
<li><a href="functions_enum.html"><span>Enumerations</span></a></li>
<li><a href="functions_eval.html"><span>Enumerator</span></a></li>
<li><a href="functions_rela.html"><span>Related Functions</span></a></li>
</ul>
</div>
<div id="navrow4" class="tabs3">
<ul class="tablist">
<li><a href="functions_func.html#index_a"><span>a</span></a></li>
<li><a href="functions_func_0x62.html#index_b"><span>b</span></a></li>
<li><a href="functions_func_0x63.html#index_c"><span>c</span></a></li>
<li><a href="functions_func_0x64.html#index_d"><span>d</span></a></li>
<li><a href="functions_func_0x65.html#index_e"><span>e</span></a></li>
<li><a href="functions_func_0x66.html#index_f"><span>f</span></a></li>
<li><a href="functions_func_0x67.html#index_g"><span>g</span></a></li>
<li><a href="functions_func_0x68.html#index_h"><span>h</span></a></li>
<li><a href="functions_func_0x69.html#index_i"><span>i</span></a></li>
<li><a href="functions_func_0x6b.html#index_k"><span>k</span></a></li>
<li><a href="functions_func_0x6c.html#index_l"><span>l</span></a></li>
<li><a href="functions_func_0x6d.html#index_m"><span>m</span></a></li>
<li><a href="functions_func_0x6e.html#index_n"><span>n</span></a></li>
<li><a href="functions_func_0x6f.html#index_o"><span>o</span></a></li>
<li><a href="functions_func_0x70.html#index_p"><span>p</span></a></li>
<li><a href="functions_func_0x71.html#index_q"><span>q</span></a></li>
<li><a href="functions_func_0x72.html#index_r"><span>r</span></a></li>
<li><a href="functions_func_0x73.html#index_s"><span>s</span></a></li>
<li><a href="functions_func_0x74.html#index_t"><span>t</span></a></li>
<li><a href="functions_func_0x75.html#index_u"><span>u</span></a></li>
<li class="current"><a href="functions_func_0x76.html#index_v"><span>v</span></a></li>
<li><a href="functions_func_0x77.html#index_w"><span>w</span></a></li>
<li><a href="functions_func_0x78.html#index_x"><span>x</span></a></li>
<li><a href="functions_func_0x7a.html#index_z"><span>z</span></a></li>
<li><a href="functions_func_0x7e.html#index_0x7e"><span>~</span></a></li>
</ul>
</div>
</div><!-- top -->
<div class="contents">
 
<h3><a class="anchor" id="index_v"></a>- v -</h3><ul>
<li>val()
: <a class="el" href="classCLitPoolElement.html#a253daa80c6f47528feb0b69e1a5c4623">CLitPoolElement</a>
</li>
<li>validIsAtomicFlag()
: <a class="el" href="group__ExprPkg.html#ga501126e42edf75538f510b7b87df96f1">CVC3::Expr</a>
</li>
<li>ValidityChecker()
: <a class="el" href="classCVC3_1_1ValidityChecker.html#a15399f370b5af3e31e1ee2add14470bf">CVC3::ValidityChecker</a>
</li>
<li>validSimpCache()
: <a class="el" href="group__ExprPkg.html#ga99348741c5062f8c8e62962b787a73fd">CVC3::Expr</a>
</li>
<li>validTerminalsConstFlag()
: <a class="el" href="group__ExprPkg.html#ga0016a263d60de73f5924072848515699">CVC3::Expr</a>
</li>
<li>value()
: <a class="el" href="classCVariable.html#a7319394585df665256e74df1282f992f">CVariable</a>
, <a class="el" href="classCVC3_1_1ValidityChecker.html#a65c5205beaa041a5d390a5803e401bd3">CVC3::ValidityChecker</a>
, <a class="el" href="classCVC3_1_1VCL.html#aae01a35fe02e9097aba1277b428c94fc">CVC3::VCL</a>
</li>
<li>Var()
: <a class="el" href="classSAT_1_1Var.html#a9f8ea526dd81b86484d019619070b2d3">SAT::Var</a>
, <a class="el" href="unionSatSolver_1_1Var.html#af6c9795e8f5f2e87e7d7a24660c7ccb4">SatSolver::Var</a>
</li>
<li>var()
: <a class="el" href="classMiniSat_1_1Lit.html#a952944c0a85fca7f8db8b532a72b3fda">MiniSat::Lit</a>
</li>
<li>var_index()
: <a class="el" href="classCLitPoolElement.html#a98d4a07830b749d83c74943efdf9669b">CLitPoolElement</a>
</li>
<li>var_score_pos()
: <a class="el" href="classCVariable.html#a5d0f657e55242e1324c345bb8f6c9877">CVariable</a>
</li>
<li>var_sign()
: <a class="el" href="classCLitPoolElement.html#add6c6301567da71e72923b3c372081cd">CLitPoolElement</a>
</li>
<li>varBumpActivity()
: <a class="el" href="classMiniSat_1_1Solver.html#ab4af8739e981ec3caaa5a20ef1eb2f0f">MiniSat::Solver</a>
</li>
<li>varDecayActivity()
: <a class="el" href="classMiniSat_1_1Solver.html#a91d54211b76e271e6838b57fca9ecfad">MiniSat::Solver</a>
</li>
<li>varExpr()
: <a class="el" href="classCVC3_1_1ValidityChecker.html#a4dc02c11317b0f12606e5ec264dd9ca9">CVC3::ValidityChecker</a>
, <a class="el" href="classCVC3_1_1VCL.html#a434b487f2d0aaf3a2bfcd86716cfa566">CVC3::VCL</a>
</li>
<li>Variable()
: <a class="el" href="classCVC3_1_1Variable.html#a7659f63344c25dbc8209c4c531b2f0be">CVC3::Variable</a>
</li>
<li>variable()
: <a class="el" href="classCDatabase.html#af421024d0ade14743332069684aba162">CDatabase</a>
</li>
<li>VariableManager()
: <a class="el" href="classCVC3_1_1VariableManager.html#a7faa284a5e5a72a87426de1f5cbf1bc9">CVC3::VariableManager</a>
</li>
<li>VariableManagerNotifyObj()
: <a class="el" href="classCVC3_1_1VariableManagerNotifyObj.html#a21ace78bece400d43aa42506d9256d68">CVC3::VariableManagerNotifyObj</a>
</li>
<li>variables()
: <a class="el" href="classCDatabase.html#af4388cf12d2984898332c519b220d67b">CDatabase</a>
</li>
<li>VariableValue()
: <a class="el" href="classCVC3_1_1VariableValue.html#a97912bc131f38a4d5f93bb1456118a0b">CVC3::VariableValue</a>
</li>
<li>varIntroRule()
: <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ac003e84b85d4f51746628fd0f738b7e3">CVC3::CommonTheoremProducer</a>
, <a class="el" href="classCVC3_1_1CommonProofRules.html#aab746efc9d013643bccc065affa82992">CVC3::CommonProofRules</a>
</li>
<li>varIntroSkolem()
: <a class="el" href="classCVC3_1_1CommonProofRules.html#a10fa187373ec24079c10874d8e804ecb">CVC3::CommonProofRules</a>
, <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a84f7da63e9d820ad781efa7e963733aa">CVC3::CommonTheoremProducer</a>
</li>
<li>varOnLHS()
: <a class="el" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a3f5d837020af57b45fbaa704727a7e11">CVC3::TheoryArith3::Ineq</a>
, <a class="el" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#a987945938565d6d6f00d1ca3ebbd125a">CVC3::TheoryArithNew::Ineq</a>
, <a class="el" href="classCVC3_1_1TheoryArithOld_1_1Ineq.html#a720977dd198a7418089d42a9e4dcd149">CVC3::TheoryArithOld::Ineq</a>
</li>
<li>varOnRHS()
: <a class="el" href="classCVC3_1_1TheoryArith3_1_1Ineq.html#a7f588540905cfdd00b515ea59c8c0482">CVC3::TheoryArith3::Ineq</a>
, <a class="el" href="classCVC3_1_1TheoryArithNew_1_1Ineq.html#abfbee8f90a20d877971571b814bccfc1">CVC3::TheoryArithNew::Ineq</a>
, <a class="el" href="classCVC3_1_1TheoryArithOld_1_1Ineq.html#a356ba30a472260912f9bc6f9273929e0">CVC3::TheoryArithOld::Ineq</a>
</li>
<li>VarOrder()
: <a class="el" href="classMiniSat_1_1VarOrder.html#a1c3e0f59f6ab6c69f4e64a85fb7aa250">MiniSat::VarOrder</a>
</li>
<li>VarOrder_lt()
: <a class="el" href="structMiniSat_1_1VarOrder__lt.html#a93e4347a40a0a094ac815624c1094d27">MiniSat::VarOrder_lt</a>
</li>
<li>varRescaleActivity()
: <a class="el" href="classMiniSat_1_1Solver.html#a711410b67cec21e4fc1480ea6490f4f2">MiniSat::Solver</a>
</li>
<li>varToMult()
: <a class="el" href="classCVC3_1_1ArithProofRules.html#a8b8db5ad0a8d4968f429e98964db93c1">CVC3::ArithProofRules</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a7568925b6c26f1c7ba882893f596d214">CVC3::ArithTheoremProducer</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a23340f90880cb869fdcfe6e69a7a2631">CVC3::ArithTheoremProducer3</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#aebcc9153d9e9bfff3678c271674a6053">CVC3::ArithTheoremProducerOld</a>
</li>
<li>VCCmd()
: <a class="el" href="classCVC3_1_1VCCmd.html#a889460a65419467468f7c5596e24171e">CVC3::VCCmd</a>
</li>
<li>VCL()
: <a class="el" href="classCVC3_1_1VCL.html#a65489dde6c6b2042fe62709da13ecab8">CVC3::VCL</a>
</li>
<li>vec()
: <a class="el" href="classMiniSat_1_1vec.html#a6b37f5acb315c411ba81ae82704d3bc5">MiniSat::vec< T ></a>
</li>
<li>verify_integrity()
: <a class="el" href="classCSolver.html#ac14b7728d00ff497795bcedfd3f24faa">CSolver</a>
</li>
<li>verify_solution()
: <a class="el" href="classSAT_1_1DPLLTBasic.html#a1340aa7926370e1bc90d1da906eb8e79">SAT::DPLLTBasic</a>
</li>
<li>verifyConflict()
: <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#acaa4dd5cb5be1e9844e03c82feea84b6">CVC3::SearchEngineTheoremProducer</a>
</li>
<li>version()
: <a class="el" href="classCSolver.html#a1153002750347545ac8b25d08ea96e39">CSolver</a>
</li>
</ul>
</div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:26:24 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>
