<!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</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 class="current"><a href="functions.html"><span>All</span></a></li>
<li><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.html#index_0x3a"><span>:</span></a></li>
<li><a href="functions_0x5f.html#index__"><span>_</span></a></li>
<li><a href="functions_0x61.html#index_a"><span>a</span></a></li>
<li><a href="functions_0x62.html#index_b"><span>b</span></a></li>
<li><a href="functions_0x63.html#index_c"><span>c</span></a></li>
<li><a href="functions_0x64.html#index_d"><span>d</span></a></li>
<li><a href="functions_0x65.html#index_e"><span>e</span></a></li>
<li><a href="functions_0x66.html#index_f"><span>f</span></a></li>
<li><a href="functions_0x67.html#index_g"><span>g</span></a></li>
<li><a href="functions_0x68.html#index_h"><span>h</span></a></li>
<li><a href="functions_0x69.html#index_i"><span>i</span></a></li>
<li><a href="functions_0x6b.html#index_k"><span>k</span></a></li>
<li><a href="functions_0x6c.html#index_l"><span>l</span></a></li>
<li><a href="functions_0x6d.html#index_m"><span>m</span></a></li>
<li><a href="functions_0x6e.html#index_n"><span>n</span></a></li>
<li><a href="functions_0x6f.html#index_o"><span>o</span></a></li>
<li><a href="functions_0x70.html#index_p"><span>p</span></a></li>
<li><a href="functions_0x71.html#index_q"><span>q</span></a></li>
<li><a href="functions_0x72.html#index_r"><span>r</span></a></li>
<li><a href="functions_0x73.html#index_s"><span>s</span></a></li>
<li><a href="functions_0x74.html#index_t"><span>t</span></a></li>
<li class="current"><a href="functions_0x75.html#index_u"><span>u</span></a></li>
<li><a href="functions_0x76.html#index_v"><span>v</span></a></li>
<li><a href="functions_0x77.html#index_w"><span>w</span></a></li>
<li><a href="functions_0x78.html#index_x"><span>x</span></a></li>
<li><a href="functions_0x79.html#index_y"><span>y</span></a></li>
<li><a href="functions_0x7a.html#index_z"><span>z</span></a></li>
<li><a href="functions_0x7e.html#index_0x7e"><span>~</span></a></li>
</ul>
</div>
</div><!-- top -->
<div class="contents">
<div class="textblock">Here is a list of all class members with links to the classes they belong to:</div>
<h3><a class="anchor" id="index_u"></a>- u -</h3><ul>
<li>UFTheoremProducer()
: <a class="el" href="classCVC3_1_1UFTheoremProducer.html#ab0ae60ea5456fc19630e4fbc8a117652">CVC3::UFTheoremProducer</a>
</li>
<li>uminusExpr()
: <a class="el" href="classCVC3_1_1ValidityChecker.html#a12f382fd07555fd752a1fdd73c229024">CVC3::ValidityChecker</a>
, <a class="el" href="classCVC3_1_1VCL.html#ab62447c6c1a4f71eeeb6d8aa665bbdc2">CVC3::VCL</a>
</li>
<li>uMinusToMult()
: <a class="el" href="classCVC3_1_1ArithProofRules.html#aa95faca93e7b4a1cf21667ff88d390e4">CVC3::ArithProofRules</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#aaafdbe9dcc49728cc2bf16b43045c193">CVC3::ArithTheoremProducer</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a878e091ad5cfd2877ddce73d6f664e16">CVC3::ArithTheoremProducer3</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a8165eb2a8fea70e0d1d2c8ebb1358855">CVC3::ArithTheoremProducerOld</a>
</li>
<li>uncomm_list
: <a class="el" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#adb3cde79421ada753728f06749d81a26">CVC3::TheoryQuant::multTrigsInfo</a>
</li>
<li>underflow()
: <a class="el" href="classstd_1_1fdinbuf.html#a0ec8bd416990c0f15ed57b4bb970290a">std::fdinbuf</a>
</li>
<li>undo()
: <a class="el" href="classMiniSat_1_1VarOrder.html#a9a5913c635dc1c57cd1127a8af30eefb">MiniSat::VarOrder</a>
</li>
<li>uniqueID()
: <a class="el" href="classCVC3_1_1ParserTemp.html#ac58b842291d5311156374fcdcbc1e400">CVC3::ParserTemp</a>
</li>
<li>unitProp()
: <a class="el" href="group__SE__Rules.html#gae7221bb8b77313a9b53a4beca9cc0aa0">CVC3::SearchEngineRules</a>
, <a class="el" href="classCVC3_1_1SearchEngineTheoremProducer.html#af764cf6eae285f0dbd3d430b76c5e19d">CVC3::SearchEngineTheoremProducer</a>
</li>
<li>unitPropagation()
: <a class="el" href="group__SE__Fast.html#ga88d524fb175ae8156696cc73cb182ffd">CVC3::SearchEngineFast</a>
</li>
<li>univ_id
: <a class="el" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#a96287846947610728257c05150e830a0">CVC3::TheoryQuant::multTrigsInfo</a>
, <a class="el" href="structCVC3_1_1dynTrig.html#ab8473d4aa20bfbcb9120043818cd319f">CVC3::dynTrig</a>
</li>
<li>universalInst()
: <a class="el" href="classCVC3_1_1QuantProofRules.html#acd29cce770506d20b67609642e7d489f">CVC3::QuantProofRules</a>
, <a class="el" href="classCVC3_1_1QuantTheoremProducer.html#a3cb05ffcc0b75525969c925fea988235">CVC3::QuantTheoremProducer</a>
</li>
<li>univThm
: <a class="el" href="structCVC3_1_1TheoryQuant_1_1multTrigsInfo.html#a1bb00c7646f04ef7a7b1effe16afbf47">CVC3::TheoryQuant::multTrigsInfo</a>
</li>
<li>UNKNOWN
: <a class="el" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5aea98bec3ab0d44524d1ea379c9209b9b1a">SAT::Var</a>
, <a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53a77f70e9dedb02009ba4ab7e6fbea1de3">SatSolver</a>
</li>
<li>unnegate()
: <a class="el" href="group__ExprPkg.html#ga39070a3fb12c398dc5bb7526d6aeb7f3">CVC3::Expr</a>
</li>
<li>unodeCount
: <a class="el" href="classLFSCConvert.html#a30a3b3353b977cc9b3e359f3aa8e2876">LFSCConvert</a>
</li>
<li>unodeCountTh
: <a class="el" href="classLFSCConvert.html#afc452237398520ff33c13c05d95d3083">LFSCConvert</a>
</li>
<li>Unref()
: <a class="el" href="classObj.html#a12a1e309d16b982d06f8cad8b7a7863f">Obj</a>
</li>
<li>unregisterKinds()
: <a class="el" href="classCVC3_1_1Theory.html#aafdee81857fde584632759c78ed821f5">CVC3::Theory</a>
</li>
<li>unregisterPrettyPrinter()
: <a class="el" href="group__EM__Priv.html#ga4662ac518622beab3379f6da23380a75">CVC3::ExprManager</a>
</li>
<li>unregisterTheory()
: <a class="el" href="classCVC3_1_1Theory.html#a6bdcdfdf6d658b1b1b7c548ea4782e6e">CVC3::Theory</a>
</li>
<li>unsat_theorem
: <a class="el" href="classCVC3_1_1TheoryArithOld_1_1DifferenceLogicGraph.html#a627796132ea73d35fbcf828d68425a3b">CVC3::TheoryArithOld::DifferenceLogicGraph</a>
</li>
<li>unsatAsString()
: <a class="el" href="classCVC3_1_1TheoryArithNew.html#afbbf8a22ba662eaea65afbbcb135ff83">CVC3::TheoryArithNew</a>
</li>
<li>unsatBasicVariables
: <a class="el" href="classCVC3_1_1TheoryArithNew.html#a3accb9cf21e2168036e7b365649820fa">CVC3::TheoryArithNew</a>
</li>
<li>UNSATISFIABLE
: <a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53ad154fc26948177f01812d287e6340734">SatSolver</a>
</li>
<li>unset_ht()
: <a class="el" href="classCLitPoolElement.html#af96c5ff47035816003a5c33b6d2591d7">CLitPoolElement</a>
</li>
<li>unset_var_value()
: <a class="el" href="classCSolver.html#a78ae7136f91966fdc7a55af71060875c">CSolver</a>
</li>
<li>unsign()
: <a class="el" href="classMiniSat_1_1Lit.html#aefb3402fa70808367aea2c399e35664b">MiniSat::Lit</a>
</li>
<li>Unsigned
: <a class="el" href="classCVC3_1_1Rational.html#a1be03a40a6c2eca44dad1e7d2af079b8">CVC3::Rational</a>
, <a class="el" href="classCVC3_1_1Unsigned.html#a1df4a745a91568850aa8ad667ccda270">CVC3::Unsigned</a>
</li>
<li>update()
: <a class="el" href="classCVC3_1_1TheoryArithOld.html#a314a1422f7fb05eb90d94cd88625fd0c">CVC3::TheoryArithOld</a>
, <a class="el" href="classMiniSat_1_1VarOrder.html#a75869a564989c014a16d43f4422f0316">MiniSat::VarOrder</a>
, <a class="el" href="classCVC3_1_1TheoryDatatype.html#a4d1da766acf310b425f564027c70b8b9">CVC3::TheoryDatatype</a>
, <a class="el" href="classCVC3_1_1CDFlags.html#abb050623665ab804a001e2167d72f2e0">CVC3::CDFlags</a>
, <a class="el" href="classCVC3_1_1ContextObj.html#a90584d2833b9fe6451dcb1379170f285">CVC3::ContextObj</a>
, <a class="el" href="group__Theory__API.html#gac41af6a90290fe83b2ee6c53cbfc4a62">CVC3::Theory</a>
, <a class="el" href="classCVC3_1_1TheoryArith.html#a065b02fa3e5ea7bf335b94ae42102cad">CVC3::TheoryArith</a>
, <a class="el" href="classCVC3_1_1TheoryArith3.html#a91d859d6893c57f28679590a23a32f15">CVC3::TheoryArith3</a>
, <a class="el" href="classCVC3_1_1TheoryArithNew.html#a3790410296752fded1074ce1b808598b">CVC3::TheoryArithNew</a>
, <a class="el" href="classCVC3_1_1TheoryUF.html#ace17a32e291a61b858e0892b21083f5d">CVC3::TheoryUF</a>
, <a class="el" href="classCVC3_1_1TheoryArray.html#a98649fa8384e42c564d2bbae90e45454">CVC3::TheoryArray</a>
, <a class="el" href="classCVC3_1_1TheoryBitvector.html#a57edac7a7e4ffd04e778f3858a000457">CVC3::TheoryBitvector</a>
, <a class="el" href="classCVC3_1_1TheoryCore.html#a435e2305420c1ed5b2ff1e4758a50dc5">CVC3::TheoryCore</a>
, <a class="el" href="classCVC3_1_1TheoryDatatypeLazy.html#a1f5719671fd527eb010fbb2a2f14e79d">CVC3::TheoryDatatypeLazy</a>
, <a class="el" href="classCVC3_1_1TheoryQuant.html#a03756dc7d7ff3b399cae1c98140eccb8">CVC3::TheoryQuant</a>
, <a class="el" href="classCVC3_1_1TheoryRecords.html#a070b5644bc6e362999305ee8bb3774ff">CVC3::TheoryRecords</a>
</li>
<li>update_var_stats()
: <a class="el" href="classCSolver.html#acc181946a5845c647818631415c22c22">CSolver</a>
</li>
<li>updateCC()
: <a class="el" href="classCVC3_1_1Theory.html#a0b9e5a75b0e23a334563392f075df9e2">CVC3::Theory</a>
</li>
<li>updateConflict()
: <a class="el" href="classMiniSat_1_1Solver.html#abe256fba9eac8bb202c8c58c87b1bb82">MiniSat::Solver</a>
</li>
<li>updateConstrained()
: <a class="el" href="classCVC3_1_1TheoryArithOld.html#abc26aaf78f6b9a25b3c5f3923719ddb7">CVC3::TheoryArithOld</a>
</li>
<li>updateDependencies()
: <a class="el" href="classCVC3_1_1TheoryArithNew.html#a85da313a2d543ca7343191a4cc20fa0d">CVC3::TheoryArithNew</a>
</li>
<li>updateDependenciesAdd()
: <a class="el" href="classCVC3_1_1TheoryArithNew.html#a59752d5aa73e48dd1a6c133a41a3c5d4">CVC3::TheoryArithNew</a>
</li>
<li>updateDependenciesRemove()
: <a class="el" href="classCVC3_1_1TheoryArithNew.html#aa21dc626bcc3110d6f90cddfa66e7729">CVC3::TheoryArithNew</a>
</li>
<li>updateFreshVariables()
: <a class="el" href="classCVC3_1_1TheoryArithNew.html#a16a43c368ec23e06c847ae9684a98381">CVC3::TheoryArithNew</a>
</li>
<li>updateHelper()
: <a class="el" href="classCVC3_1_1Theory.html#ad6cb45844df7f1b08a53e41e40a362e3">CVC3::Theory</a>
</li>
<li>updateLitCounts()
: <a class="el" href="group__SE__Fast.html#ga775b06e155128cc8817f254bc293c6c6">CVC3::SearchEngineFast</a>
</li>
<li>updateLitScores()
: <a class="el" href="group__SE__Fast.html#ga7311848b70f91fad18ca95b7347749cb">CVC3::SearchEngineFast</a>
</li>
<li>updateQueue()
: <a class="el" href="classCVC3_1_1ExprTransform.html#ad12aee56d7dd01276af2d993ce4676c9">CVC3::ExprTransform</a>
</li>
<li>updateStats()
: <a class="el" href="classCVC3_1_1TheoryArithNew.html#af80703576d25418c16a5a187e8bcd0ef">CVC3::TheoryArithNew</a>
, <a class="el" href="classCVC3_1_1TheoryArith3.html#a6dffd309689d82e967c9bbe05d2ba982">CVC3::TheoryArith3</a>
, <a class="el" href="classCVC3_1_1TheoryArithOld.html#aeda9acb0bae07ff39ce79f8b0e2e83f7">CVC3::TheoryArithOld</a>
, <a class="el" href="classCVC3_1_1TheoryArithNew.html#a8105c616e2a7410133e6f4c908d35def">CVC3::TheoryArithNew</a>
, <a class="el" href="classCVC3_1_1TheoryArith3.html#a4a5c3ac4853b75db75d61b5a00b1c9d2">CVC3::TheoryArith3</a>
</li>
<li>updateSubsumptionDB()
: <a class="el" href="classCVC3_1_1TheoryArithOld.html#a1a20be9ae34b5301092b70364d8b4bb1">CVC3::TheoryArithOld</a>
, <a class="el" href="classCVC3_1_1TheoryArith3.html#ae4e1a30b7247216751f1eaea91362cc0">CVC3::TheoryArith3</a>
</li>
<li>updateSubterms()
: <a class="el" href="classCVC3_1_1TheoryBitvector.html#aa12fe04ae2312b60f15f5fc594d533f4">CVC3::TheoryBitvector</a>
</li>
<li>updateValue()
: <a class="el" href="classCVC3_1_1TheoryArithNew.html#ad22fa5522add29991c72dab60da2e922">CVC3::TheoryArithNew</a>
</li>
<li>upperBound
: <a class="el" href="classCVC3_1_1TheoryArithNew.html#a485637b86fce6c4a8d53d54e286d2eb8">CVC3::TheoryArithNew</a>
</li>
<li>UserAssertion()
: <a class="el" href="classCVC3_1_1VCL_1_1UserAssertion.html#a46d21bf4dced20a940cd8ce7a97bf4d6">CVC3::VCL::UserAssertion</a>
</li>
<li>USES_CC
: <a class="el" href="group__ExprPkg.html#gga5285f004f382cfb7a002f8dea3b3316cad414c75c14f9cc186e6e7df225396627">CVC3::Expr</a>
</li>
<li>usesCC()
: <a class="el" href="group__ExprPkg.html#ga0f1f1ce3472f18a4b6575805e0347bce">CVC3::Expr</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>
