<!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 class="current"><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><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_r"></a>- r -</h3><ul>
<li>rafineInequalityToInteger()
: <a class="el" href="classCVC3_1_1TheoryArithOld.html#aea59b6a8576bd484d6bcede8363e4076">CVC3::TheoryArithOld</a>
</li>
<li>rafineIntegerConstraints()
: <a class="el" href="classCVC3_1_1TheoryArithNew.html#a68884e312bf69a858ed5a45979571d1a">CVC3::TheoryArithNew</a>
</li>
<li>rafineStrictInteger()
: <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a4b28aa17702ca3f9703e61ca012ca236">CVC3::ArithTheoremProducer</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a7638b18d73c05e7bedad7c4cdfeca809">CVC3::ArithTheoremProducer3</a>
, <a class="el" href="classCVC3_1_1ArithProofRules.html#a4b61e3ea9d5ac911806de95241cf35de">CVC3::ArithProofRules</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#af6182f9b295bde40a9047b1651d979a5">CVC3::ArithTheoremProducerOld</a>
</li>
<li>rat()
: <a class="el" href="classCVC3_1_1TheoryBitvector.html#ac88ba0954e217df731ebb362135ea107">CVC3::TheoryBitvector</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ae0d46b17ef012eabbbe62cac026bfab9">CVC3::ArithTheoremProducer</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a4440979f29e7ec3519212ff1e23d758f">CVC3::ArithTheoremProducer3</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a8e7bf5bdb1872df7f21920c64a37c612">CVC3::ArithTheoremProducerOld</a>
, <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#ae03f092d2050783885e338b5880b2645">CVC3::BitvectorTheoremProducer</a>
, <a class="el" href="classCVC3_1_1TheoryArith.html#a11b44bafcad3c0875372d6c90a041e2d">CVC3::TheoryArith</a>
</li>
<li>ratExpr()
: <a class="el" href="classCVC3_1_1VCL.html#acfc983096f1d7aa9799d360a9cef8d3b">CVC3::VCL</a>
, <a class="el" href="classCVC3_1_1ValidityChecker.html#aec8119cdf4ae54522453bcc7bd38ee7c">CVC3::ValidityChecker</a>
</li>
<li>Rational()
: <a class="el" href="classCVC3_1_1Rational.html#a9ad06945464ca21b2171a27d7b47c29e">CVC3::Rational</a>
</li>
<li>readArrayLiteral()
: <a class="el" href="classCVC3_1_1ArrayProofRules.html#aa5e52ae0cc9df232b4304421d0ed5e3c">CVC3::ArrayProofRules</a>
, <a class="el" href="classCVC3_1_1ArrayTheoremProducer.html#a8c0cbeb8e41da7e06528641cdf3be3fb">CVC3::ArrayTheoremProducer</a>
</li>
<li>readExpr()
: <a class="el" href="classCVC3_1_1ValidityChecker.html#aa57f5268209bff87129ef39c711be6a4">CVC3::ValidityChecker</a>
, <a class="el" href="classCVC3_1_1VCL.html#a84a759c7fa5b4ec5ddb84c883bdf75a5">CVC3::VCL</a>
</li>
<li>real_solve()
: <a class="el" href="classCSolver.html#af5c60a4d643467e199c00415fedc7e1d">CSolver</a>
</li>
<li>realShadow()
: <a class="el" href="classCVC3_1_1ArithProofRules.html#a203c7079289189cd4bf4f604c10645e5">CVC3::ArithProofRules</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a8092c96a87d952fc1e572bb9237ff994">CVC3::ArithTheoremProducer</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a6f08ce700f85f9ba2967ecee42e7a550">CVC3::ArithTheoremProducer3</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a8f7858787d55442d57e5924dd232f842">CVC3::ArithTheoremProducerOld</a>
</li>
<li>realShadowEq()
: <a class="el" href="classCVC3_1_1ArithProofRules.html#a08dfccc28787af2a4141ed0f5a66bc9d">CVC3::ArithProofRules</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a6e14251c516153e14539a34598daca04">CVC3::ArithTheoremProducer</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a955e74558aee9ebc9de4c084819e93ac">CVC3::ArithTheoremProducer3</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a5033cb7a4be3d2e9bc1cd60582482c5f">CVC3::ArithTheoremProducerOld</a>
</li>
<li>realType()
: <a class="el" href="classCVC3_1_1TheoryArith.html#a03fa81194322b92c488033695bec7204">CVC3::TheoryArith</a>
, <a class="el" href="classCVC3_1_1ValidityChecker.html#af80938787dc3dc10d794cabcde2eedd9">CVC3::ValidityChecker</a>
, <a class="el" href="classCVC3_1_1VCL.html#aea5eb2afa1a4917c1251340f22a7f54b">CVC3::VCL</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a4606a94098ae94cdae1b924dc7f7b4ae">CVC3::ArithTheoremProducer</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ad010c33575ebd1dc229c2a1526c229c5">CVC3::ArithTheoremProducer3</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#ab22e2bf40e2473ab9dc34097c28a46a3">CVC3::ArithTheoremProducerOld</a>
</li>
<li>rebuild()
: <a class="el" href="group__ExprPkg.html#ga3df149427d124797567614e07080519d">CVC3::Expr</a>
, <a class="el" href="group__EM__Priv.html#gacaab5ccf5cf81d11185979051d301d5e">CVC3::ExprManager</a>
, <a class="el" href="classCVC3_1_1ExprValue.html#a2a5a87b2cdf0318ac9555ed82bd781c5">CVC3::ExprValue</a>
</li>
<li>rebuildRec()
: <a class="el" href="group__EM__Priv.html#gaa86d7ed7800549f1621d2d5ce64ce643">CVC3::ExprManager</a>
</li>
<li>recCompleteInster()
: <a class="el" href="classrecCompleteInster.html#aa1a041cf953f51866aa0b53480f927bb">recCompleteInster</a>
</li>
<li>recFindBoundVars()
: <a class="el" href="classCVC3_1_1QuantTheoremProducer.html#a8ab1be71db5a5816f69eb45aa8c2009f">CVC3::QuantTheoremProducer</a>
</li>
<li>recGeneralTrig()
: <a class="el" href="classCVC3_1_1TheoryQuant.html#a6177e4b547322f04e6ff282521120a37">CVC3::TheoryQuant</a>
</li>
<li>recGoodSemMatch()
: <a class="el" href="classCVC3_1_1TheoryQuant.html#a8e4d77afeb2cf976688bc923b3c7b3d4">CVC3::TheoryQuant</a>
</li>
<li>recInstantiate()
: <a class="el" href="classCVC3_1_1TheoryQuant.html#a9e3bb4497a71d84322a8f97a86d2b11c">CVC3::TheoryQuant</a>
</li>
<li>recInstMacros()
: <a class="el" href="classCVC3_1_1CompleteInstPreProcessor.html#a91a6a2cc72569859fe20fbe3f1f7b69a">CVC3::CompleteInstPreProcessor</a>
</li>
<li>recMultMatch()
: <a class="el" href="classCVC3_1_1TheoryQuant.html#aede3f8a2e1b235a5cafde5f62a3356cf">CVC3::TheoryQuant</a>
</li>
<li>recMultMatchDebug()
: <a class="el" href="classCVC3_1_1TheoryQuant.html#a6105760e18793163cafd935f92214b57">CVC3::TheoryQuant</a>
</li>
<li>recMultMatchNewWay()
: <a class="el" href="classCVC3_1_1TheoryQuant.html#a017c02318b460823b9e5e63b8b72a14f">CVC3::TheoryQuant</a>
</li>
<li>recMultMatchOldWay()
: <a class="el" href="classCVC3_1_1TheoryQuant.html#a22391b53ffa8331b754fb7ad85b58ec0">CVC3::TheoryQuant</a>
</li>
<li>recordExpr()
: <a class="el" href="classCVC3_1_1ValidityChecker.html#ad855a87b02f19efb297d45778a7ca52f">CVC3::ValidityChecker</a>
, <a class="el" href="classCVC3_1_1VCL.html#afe7f6ce6960db261e58d996e00164d64">CVC3::VCL</a>
, <a class="el" href="classCVC3_1_1RecordsTheoremProducer.html#a3ab7c99b6e0525c7cbc0d3793819b2ff">CVC3::RecordsTheoremProducer</a>
, <a class="el" href="classCVC3_1_1TheoryRecords.html#aa5a9cbcd30ed23792c030d70181483d3">CVC3::TheoryRecords</a>
</li>
<li>recordFact()
: <a class="el" href="group__SE__Fast.html#ga2ec0e19a01ac0926b690c50a3206c5a3">CVC3::SearchEngineFast</a>
</li>
<li>recordNewRootLit()
: <a class="el" href="classCVC3_1_1SearchSat.html#a0f3b2311296e520c22aea55c68c4b477">CVC3::SearchSat</a>
</li>
<li>recordSelect()
: <a class="el" href="classCVC3_1_1TheoryRecords.html#a6123e229d2eac24364f4cf1b30927f0c">CVC3::TheoryRecords</a>
, <a class="el" href="classCVC3_1_1RecordsTheoremProducer.html#aed507ebecfef1025611db992ab56f742">CVC3::RecordsTheoremProducer</a>
</li>
<li>RecordsTheoremProducer()
: <a class="el" href="classCVC3_1_1RecordsTheoremProducer.html#ae3c59db05725732c5cd94761d9e58862">CVC3::RecordsTheoremProducer</a>
</li>
<li>recordType()
: <a class="el" href="classCVC3_1_1TheoryRecords.html#a4b298f0e7a25449c945480544996d105">CVC3::TheoryRecords</a>
, <a class="el" href="classCVC3_1_1ValidityChecker.html#ad9a6df13065bfc62ea5ece1513716835">CVC3::ValidityChecker</a>
, <a class="el" href="classCVC3_1_1VCL.html#a5402e161e9f0c8158f3ffc99ffee7585">CVC3::VCL</a>
, <a class="el" href="classCVC3_1_1RecordsTheoremProducer.html#abb8b17796882d077d7e5f7c948092c99">CVC3::RecordsTheoremProducer</a>
</li>
<li>recordUpdate()
: <a class="el" href="classCVC3_1_1TheoryRecords.html#ad6d5734bb5b21cada7e7958c6840e2c4">CVC3::TheoryRecords</a>
, <a class="el" href="classCVC3_1_1RecordsTheoremProducer.html#af3aa58710dd1e1adda7e9d44034a1c59">CVC3::RecordsTheoremProducer</a>
</li>
<li>recQuantLevel()
: <a class="el" href="classCVC3_1_1TheoremValue.html#aa437b081740be2d064d8d71e1db90d04">CVC3::TheoremValue</a>
</li>
<li>recRewriteNot()
: <a class="el" href="classCVC3_1_1CompleteInstPreProcessor.html#ae7bef3316e99205836a6c490ce97d0e5">CVC3::CompleteInstPreProcessor</a>
</li>
<li>recSearchCover()
: <a class="el" href="classCVC3_1_1TheoryQuant.html#a21e6b9a3115caa0b22322bd75d883347">CVC3::TheoryQuant</a>
</li>
<li>recSelectExpr()
: <a class="el" href="classCVC3_1_1ValidityChecker.html#ae9fea52582c06a904679b4a844299313">CVC3::ValidityChecker</a>
, <a class="el" href="classCVC3_1_1VCL.html#abdf0c8d98e38c5b824e2ea7473eb3e55">CVC3::VCL</a>
</li>
<li>recSkolemize()
: <a class="el" href="classCVC3_1_1CompleteInstPreProcessor.html#a26a13f237507dfff8de68bbba747246a">CVC3::CompleteInstPreProcessor</a>
</li>
<li>recSynMatch()
: <a class="el" href="classCVC3_1_1TheoryQuant.html#a33dfaf67440a78f618a6c379fd884330">CVC3::TheoryQuant</a>
</li>
<li>recSynMatchBackupOnly()
: <a class="el" href="classCVC3_1_1TheoryQuant.html#ad2e8ad874c79cb5300302d30b6475b7b">CVC3::TheoryQuant</a>
</li>
<li>recUpdateExpr()
: <a class="el" href="classCVC3_1_1ValidityChecker.html#a0a3ff4cc5a24717e6ab7f17ca9ea19c3">CVC3::ValidityChecker</a>
, <a class="el" href="classCVC3_1_1VCL.html#a38d7fbf8d93c20be9924f26fe437ade6">CVC3::VCL</a>
</li>
<li>recursiveCanonSimpCheck()
: <a class="el" href="classCVC3_1_1TheoryArith.html#adea0b08bcb123d6dca2b4742326b87c1">CVC3::TheoryArith</a>
</li>
<li>recursiveMap()
: <a class="el" href="classCVC3_1_1TheoryQuant.html#a184ff0daa00e9777c766aec5e1fc3015">CVC3::TheoryQuant</a>
</li>
<li>recursivePrint()
: <a class="el" href="classCVC3_1_1Theorem.html#a472f420688e07c506969a4ed6b9a110e">CVC3::Theorem</a>
</li>
<li>recursiveQuantSubst()
: <a class="el" href="group__ExprPkg.html#ga644bfdf1ae59727d6626c764208483e8">CVC3::Expr</a>
</li>
<li>recursiveSubst()
: <a class="el" href="group__ExprPkg.html#ga7ee0a2ffca952496e3f1d8c9c9d66aab">CVC3::Expr</a>
</li>
<li>reduceDB()
: <a class="el" href="classMiniSat_1_1Solver.html#a62eea2c00917497fbfb843bf9ca4482e">MiniSat::Solver</a>
</li>
<li>Ref()
: <a class="el" href="classObj.html#affea650ea97fb6b188313b857e60aa8b">Obj</a>
</li>
<li>RefCDO()
: <a class="el" href="classCVC3_1_1SmartCDO_1_1RefCDO.html#a5f1602d72a9f1c1bc98ec9886d2ed145">CVC3::SmartCDO< T >::RefCDO< U ></a>
</li>
<li>refineCounterExample()
: <a class="el" href="group__Theory__API.html#gab23238889b7f68caa0715e6ab5d31775">CVC3::Theory</a>
, <a class="el" href="classCVC3_1_1TheoryArith.html#aa438bb4c5ceaeca9b2bb692d725d6ce8">CVC3::TheoryArith</a>
, <a class="el" href="classCVC3_1_1TheoryArith3.html#ae44a95809991c134c6ed6a8c795a06bc">CVC3::TheoryArith3</a>
, <a class="el" href="classCVC3_1_1TheoryArithNew.html#a3dafcfa8f6451023a83ce69c53fac641">CVC3::TheoryArithNew</a>
, <a class="el" href="classCVC3_1_1TheoryArithOld.html#aa4dc2c586e3bf401a1940a2057508d9f">CVC3::TheoryArithOld</a>
, <a class="el" href="classCVC3_1_1TheoryCore.html#a6822c229c357d1afcda22bc073d45142">CVC3::TheoryCore</a>
</li>
<li>reflexivityRule()
: <a class="el" href="classCVC3_1_1CommonProofRules.html#a61c1fe56b4ed9744006883a7784ddb71">CVC3::CommonProofRules</a>
, <a class="el" href="classCVC3_1_1Theory.html#af860f5d5e01423628c97c399606916ff">CVC3::Theory</a>
, <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a306058f7ced3d7220b2d1a40892faae7">CVC3::CommonTheoremProducer</a>
</li>
<li>RefNotifyObj()
: <a class="el" href="classCVC3_1_1SmartCDO_1_1RefCDO_1_1RefNotifyObj.html#aecfde4144e9f871a76a28fa1f0498825">CVC3::SmartCDO< T >::RefCDO< U >::RefNotifyObj</a>
</li>
<li>RefPtr()
: <a class="el" href="classRefPtr.html#a2cd09e15a519391964175834ab653f85">RefPtr< T ></a>
</li>
<li>refutes()
: <a class="el" href="classCVC3_1_1Theorem.html#a657f0037f907743988443bffdf2e505c">CVC3::Theorem</a>
</li>
<li>RegisterAssignmentHook()
: <a class="el" href="classSatSolver.html#a658bb40c580f149024c59509e9e3acd0">SatSolver</a>
, <a class="el" href="classXchaff.html#a0a98f9f270df69b9f86d15258b915afb">Xchaff</a>
, <a class="el" href="classCSolver.html#afcbec396917ed73948a67db3732054ae">CSolver</a>
</li>
<li>registerAtom()
: <a class="el" href="classSAT_1_1CNF__Manager_1_1CNFCallback.html#a5bfb2992c14e9a7a1c824f1df49aa8b3">SAT::CNF_Manager::CNFCallback</a>
, <a class="el" href="classSAT_1_1CNF__Manager.html#aad4c1fe260c5c15d94a4010d82569e74">SAT::CNF_Manager</a>
, <a class="el" href="group__SE.html#ga0f7c2870341319738e7d8c6662e6d7cc">CVC3::SearchEngine</a>
, <a class="el" href="group__SE.html#gac4e5351fec1964bf7571d67e90a1538d">CVC3::SearchImplBase</a>
, <a class="el" href="classCVC3_1_1SearchSat.html#a2ca4a66d1bf7d0227e646edd3c9b9964">CVC3::SearchSat</a>
, <a class="el" href="group__Theory__API.html#gafb1431aa8258f6663ad948ebb08e5330">CVC3::Theory</a>
, <a class="el" href="classCVC3_1_1TheoryArithNew.html#acf71ca1da6261f1fb8f14522613de497">CVC3::TheoryArithNew</a>
, <a class="el" href="classCVC3_1_1TheoryArithOld.html#ad4d5973db0c0b0d26e358450b0c0a4a1">CVC3::TheoryArithOld</a>
, <a class="el" href="classCVC3_1_1TheoryCore.html#ade1177fbf32e95b9433eb608c82857d7">CVC3::TheoryCore</a>
, <a class="el" href="classCVC3_1_1ValidityChecker.html#aa1cc8c465b3d30a3db3b1e9f86917606">CVC3::ValidityChecker</a>
, <a class="el" href="classCVC3_1_1VCL.html#a54c9ceeaa6e94edd5af791d4fec621f5">CVC3::VCL</a>
, <a class="el" href="classCVC3_1_1SearchSatCNFCallback.html#aedf8407f7bd6e3b1eceba553acd5bbf9">CVC3::SearchSatCNFCallback</a>
</li>
<li>registerClause()
: <a class="el" href="classMiniSat_1_1Derivation.html#a86b49978f3ea0aa72cd4815e241ff7ad">MiniSat::Derivation</a>
</li>
<li>registerCNFCallback()
: <a class="el" href="classSAT_1_1CNF__Manager.html#a0d2b7a6369e9e7ad4ae6aca1398e404d">SAT::CNF_Manager</a>
</li>
<li>registerCoreSatAPI()
: <a class="el" href="classCVC3_1_1TheoryCore.html#afb6629080bceb44023f1bb3a44f9136f">CVC3::TheoryCore</a>
</li>
<li>RegisterDecisionHook()
: <a class="el" href="classSatSolver.html#a76cc15252a711e8a9a21e49a30d7e920">SatSolver</a>
, <a class="el" href="classXchaff.html#a029881b7aad15145d313fae454637a6a">Xchaff</a>
, <a class="el" href="classCSolver.html#aac7bf85fb8516ff4b3478598306fcb2e">CSolver</a>
</li>
<li>RegisterDeductionHook()
: <a class="el" href="classSatSolver.html#a856cf7839d83dcc04ee421d2595fc671">SatSolver</a>
, <a class="el" href="classXchaff.html#a2ffce1f21eb64712d4e26e1dbc4b0e36">Xchaff</a>
, <a class="el" href="classCSolver.html#a5aeafd67c7a77683ae040c11fbf033b1">CSolver</a>
</li>
<li>RegisterDLevelHook()
: <a class="el" href="classSatSolver.html#a2f5308d9fdff97f882186073f05d8874">SatSolver</a>
, <a class="el" href="classXchaff.html#a9826417dcd2303591eaeb3259ac154f9">Xchaff</a>
, <a class="el" href="classCSolver.html#aa0f5bd7cea8ed3bc7254e29d744566fb">CSolver</a>
</li>
<li>registerInference()
: <a class="el" href="classMiniSat_1_1Derivation.html#a7c0cfa1103212b370236814a4923dec5">MiniSat::Derivation</a>
</li>
<li>registerInputClause()
: <a class="el" href="classMiniSat_1_1Derivation.html#a8f1063fe441a90d388e56ca4002a87e1">MiniSat::Derivation</a>
</li>
<li>registerKinds()
: <a class="el" href="classCVC3_1_1Theory.html#a41499be2b31d82e7bec5efc880126510">CVC3::Theory</a>
</li>
<li>registerLeaf()
: <a class="el" href="classSAT_1_1SatProof.html#a36554406554d1f6ea793c98b104bd071">SAT::SatProof</a>
</li>
<li>registerNode()
: <a class="el" href="classSAT_1_1SatProof.html#a95ddb594997f8a50a62b277f1db6c1aa">SAT::SatProof</a>
</li>
<li>registerPrettyPrinter()
: <a class="el" href="group__EM__Priv.html#gacd01e4de3a171218d0192a9450fb7605">CVC3::ExprManager</a>
</li>
<li>registerSubclass()
: <a class="el" href="group__EM__Priv.html#ga10284641fda307d52345f73e8ad5def0">CVC3::ExprManager</a>
</li>
<li>registerTheory()
: <a class="el" href="classCVC3_1_1Theory.html#a97a6f8e09f71513da969fa7847346c6f">CVC3::Theory</a>
</li>
<li>registerTrig()
: <a class="el" href="classCVC3_1_1TheoryQuant.html#ad7f534d41a6c648eb5fbad4bbc1c92a1">CVC3::TheoryQuant</a>
</li>
<li>registerTrigReal()
: <a class="el" href="classCVC3_1_1TheoryQuant.html#ad9323b081878d5b80294cd48b68dd8a1">CVC3::TheoryQuant</a>
</li>
<li>registerTypeComputer()
: <a class="el" href="group__EM__Priv.html#ga39c8449d567e83ccd711cb2ff1a91dbf">CVC3::ExprManager</a>
</li>
<li>registerUnit()
: <a class="el" href="classSAT_1_1CNF__Formula.html#a3b0eb426b9713bbc92041f046dd83ab5">SAT::CNF_Formula</a>
, <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#ab72a764586f913bc1aa45e0334a75140">SAT::CNF_Formula_Impl</a>
, <a class="el" href="classSAT_1_1CD__CNF__Formula.html#a41c4e53bdf4c9d98afbdbea4a735fce9">SAT::CD_CNF_Formula</a>
</li>
<li>registerVar()
: <a class="el" href="classMiniSat_1_1Solver.html#a7a11f6c3676dd169d093a4e7c5af5299">MiniSat::Solver</a>
</li>
<li>RegTheoremValue()
: <a class="el" href="classCVC3_1_1RegTheoremValue.html#a50beadc804ee4d42e7b55195f97b865b">CVC3::RegTheoremValue</a>
</li>
<li>release()
: <a class="el" href="classMiniSat_1_1vec.html#af4a503f0e38f91fa5d236c29b833c104">MiniSat::vec< T ></a>
</li>
<li>relToClosure()
: <a class="el" href="classCVC3_1_1UFProofRules.html#a3a6ee8bd1e49a0a5ce39a7d4c8506d28">CVC3::UFProofRules</a>
, <a class="el" href="classCVC3_1_1UFTheoremProducer.html#a3eb24835ec0a434ea5d787fb3c2d91e6">CVC3::UFTheoremProducer</a>
</li>
<li>relTrans()
: <a class="el" href="classCVC3_1_1UFProofRules.html#ab66928a2bf8ea96c965023cbe5e021e4">CVC3::UFProofRules</a>
, <a class="el" href="classCVC3_1_1UFTheoremProducer.html#ac11af95d2d197203d7cb2213e68282b8">CVC3::UFTheoremProducer</a>
</li>
<li>remove()
: <a class="el" href="classMiniSat_1_1Solver.html#a241e960f84c150b1421bf4e3b3a6b073">MiniSat::Solver</a>
</li>
<li>removedClause()
: <a class="el" href="classMiniSat_1_1Derivation.html#a98bcad6982734612b1afd68e38dea7b8">MiniSat::Derivation</a>
</li>
<li>RemoveFunctionApps()
: <a class="el" href="classCVC3_1_1ExprTransform.html#a42100ea2839cf15346eab2c8ca29b744">CVC3::ExprTransform</a>
</li>
<li>removeWatch()
: <a class="el" href="classMiniSat_1_1Solver.html#a94c3f4932f4c9d17b4a6dc1839c813f5">MiniSat::Solver</a>
</li>
<li>renameExpr()
: <a class="el" href="classCVC3_1_1Theory.html#a07c2391015494b5f71def510c1fb6e26">CVC3::Theory</a>
</li>
<li>repeatRule()
: <a class="el" href="classCVC3_1_1BitvectorProofRules.html#aed9f65e2eed1299d80b6ec63274568a4">CVC3::BitvectorProofRules</a>
, <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a9b9a128c7c863d01c804bfec956ffb6c">CVC3::BitvectorTheoremProducer</a>
</li>
<li>replaceITE()
: <a class="el" href="group__SE.html#ga687e32d21d7fe7e4b26873ae86a47ae5">CVC3::SearchImplBase</a>
</li>
<li>replaceITErec()
: <a class="el" href="classSAT_1_1CNF__Manager.html#a9c44bb0556800d1f05eca51d68a73e67">SAT::CNF_Manager</a>
</li>
<li>reportResult()
: <a class="el" href="classCVC3_1_1VCCmd.html#ad61f2528e834203b51ff974f5212a26b">CVC3::VCCmd</a>
</li>
<li>reprocessFlags()
: <a class="el" href="classCVC3_1_1ValidityChecker.html#a0acc9330bfe47d579f1fa105d2603e85">CVC3::ValidityChecker</a>
, <a class="el" href="classCVC3_1_1VCL.html#a83197a54652f37925771d6de682a54a9">CVC3::VCL</a>
</li>
<li>requestPop()
: <a class="el" href="classMiniSat_1_1Solver.html#a8be8edbecd5a07bd39990ee7ba0918e3">MiniSat::Solver</a>
</li>
<li>reset()
: <a class="el" href="classSAT_1_1Var.html#a625819a54d89e98b26ae423b7a9fe1c8">SAT::Var</a>
, <a class="el" href="classSAT_1_1Lit.html#a3bb64db99db01facd58c54e48b3f7800">SAT::Lit</a>
, <a class="el" href="classSAT_1_1CNF__Formula__Impl.html#a6bc99606944e873ded2b37c954b18170">SAT::CNF_Formula_Impl</a>
, <a class="el" href="classCVC3_1_1Parser.html#a84d22e302246021152e5dbc950e67758">CVC3::Parser</a>
, <a class="el" href="classCVC3_1_1ValidityChecker.html#accfa11d7cb5f45e4f73c01c09507f6b0">CVC3::ValidityChecker</a>
, <a class="el" href="classCVC3_1_1VCL.html#ab21a08026f0fbc5e58619874952a7745">CVC3::VCL</a>
</li>
<li>Reset()
: <a class="el" href="unionSatSolver_1_1Var.html#a0749bf538158732dcaaaa37a53130246">SatSolver::Var</a>
, <a class="el" href="unionSatSolver_1_1Lit.html#a920ad716dbc5a6695f234c80fa686c3f">SatSolver::Lit</a>
, <a class="el" href="unionSatSolver_1_1Clause.html#a0301c94286fe257cbaa640aa77049dc1">SatSolver::Clause</a>
, <a class="el" href="classSatSolver.html#ac64e81107b4b94fd1f6fb76b219a0517">SatSolver</a>
, <a class="el" href="classXchaff.html#ae8d8fe530dede206922f26f52f1cafcf">Xchaff</a>
</li>
<li>resetDag()
: <a class="el" href="classCVC3_1_1ExprStream.html#a004714bd282bfa11595d21bce94e72ec">CVC3::ExprStream</a>
</li>
<li>ResetException()
: <a class="el" href="classCVC3_1_1ResetException.html#a2d49a36a490100c6e235c172b9d19f51">CVC3::ResetException</a>
</li>
<li>resetIndent()
: <a class="el" href="classCVC3_1_1ExprStream.html#a946110c3457868fe38ce8c1d4cdde916">CVC3::ExprStream</a>
</li>
<li>resize()
: <a class="el" href="classHash_1_1hash__table.html#a47532315fb2a36897f1e866d72e64dab">Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey ></a>
</li>
<li>resolveID()
: <a class="el" href="classCVC3_1_1Theory.html#a07b326cd94b2bb8bafa39faf07caaec5">CVC3::Theory</a>
</li>
<li>resolveTheoryImplication()
: <a class="el" href="classMiniSat_1_1Solver.html#a22b59f22e9df28fcb892e5873d998c75">MiniSat::Solver</a>
</li>
<li>Restart()
: <a class="el" href="classSatSolver.html#aa05fce07f5c3363e2362a3b1de7795db">SatSolver</a>
, <a class="el" href="classXchaff.html#a53ce24894150638b3285f7b12ebf23ba">Xchaff</a>
</li>
<li>restart()
: <a class="el" href="group__SE.html#ga715936653b5bef3e3d9fd2a8a873bafd">CVC3::SearchEngine</a>
, <a class="el" href="group__SE.html#gad4a8edbe5a6520fc9f564ec1c65d4729">CVC3::SearchImplBase</a>
, <a class="el" href="classCVC3_1_1SearchSat.html#ae7bf52f7780c6f2e085cf23c507fc3e1">CVC3::SearchSat</a>
, <a class="el" href="classCVC3_1_1ValidityChecker.html#aefdc8ccae46e254d26b574d5d3ad6fc1">CVC3::ValidityChecker</a>
, <a class="el" href="classCVC3_1_1VCL.html#afd3d88e7e58e6098c9f570fc7e812547">CVC3::VCL</a>
, <a class="el" href="classCSolver.html#a5b9ce0b016266150cad691e4bb475668">CSolver</a>
</li>
<li>restartInternal()
: <a class="el" href="group__SE__Fast.html#ga99dd1f1c52ecae319bd0b5a3b689a31d">CVC3::SearchEngineFast</a>
, <a class="el" href="group__SE.html#gaf89e6b914a2099b366258953fccb6277">CVC3::SearchImplBase</a>
, <a class="el" href="group__SE__Simple.html#ga29f819e266d4821ae874f69da080247c">CVC3::SearchSimple</a>
</li>
<li>restore()
: <a class="el" href="classCVC3_1_1ContextObjChain.html#a83e5207b9d496337691b30f072c117c7">CVC3::ContextObjChain</a>
, <a class="el" href="group__Context.html#ga1b0a5ef8d8aef498218f0dfddea851a7">CVC3::Scope</a>
, <a class="el" href="classCVC3_1_1SearchSat.html#a41d79aff18a635a5cdc2c789bb784a0a">CVC3::SearchSat</a>
</li>
<li>restoreData()
: <a class="el" href="classCVC3_1_1CDOmap.html#a6bb9afb0c43a91a329fee43b2f8560fe">CVC3::CDOmap< Key, Data, HashFcn ></a>
, <a class="el" href="classCVC3_1_1CDFlags.html#acf55a63e2265061bbc48a1d6c5ce0026">CVC3::CDFlags</a>
, <a class="el" href="classCVC3_1_1CDList.html#ae8dd8c4621883f2f9e39a9961ae677a4">CVC3::CDList< T ></a>
, <a class="el" href="classCVC3_1_1CDMapData.html#ad0d096840f77467d25f872b561fb92b6">CVC3::CDMapData</a>
, <a class="el" href="classCVC3_1_1CDMap.html#a3dd8677771f90789863f269a9aa5a8d1">CVC3::CDMap< Key, Data, HashFcn ></a>
, <a class="el" href="classCVC3_1_1CDOmapOrdered.html#a2cea38d82ffa72b4acaec4393f25bb8d">CVC3::CDOmapOrdered< Key, Data ></a>
, <a class="el" href="classCVC3_1_1CDMapOrderedData.html#a90205615c92b3ff1b981f7e7fb08b049">CVC3::CDMapOrderedData</a>
, <a class="el" href="classCVC3_1_1CDMapOrdered.html#a9e7a27a2fa9f7f1e38a9d766ab63f17a">CVC3::CDMapOrdered< Key, Data ></a>
, <a class="el" href="classCVC3_1_1CDO.html#ab8396db3f236e6e5417b474d3a8f2b97">CVC3::CDO< T ></a>
, <a class="el" href="classCVC3_1_1ContextObj.html#a37109b576b9dbaeee06f37cdc78f1a2e">CVC3::ContextObj</a>
</li>
<li>restoreIndent()
: <a class="el" href="group__EM__Priv.html#ga3fe43b71bb148045c114e054934f5304">CVC3::ExprManager</a>
</li>
<li>restorePre()
: <a class="el" href="classCVC3_1_1SearchSat.html#aff33fe25d0761167062aa871e1992ded">CVC3::SearchSat</a>
</li>
<li>Restorer()
: <a class="el" href="classCVC3_1_1SearchSat_1_1Restorer.html#a60db1d8baa0ef8723379d512481d51d9">CVC3::SearchSat::Restorer</a>
</li>
<li>resumeGC()
: <a class="el" href="classCVC3_1_1VariableManager.html#ad7d360514fcfd910668eabd097dbe81c">CVC3::VariableManager</a>
, <a class="el" href="group__EM__Priv.html#gafd44d7be33c1111722aa7bb9f3b8b2e9">CVC3::ExprManager</a>
</li>
<li>returnFromCheck()
: <a class="el" href="classCVC3_1_1ValidityChecker.html#a021eced066a375b644402863e3435919">CVC3::ValidityChecker</a>
, <a class="el" href="group__SE.html#gad552593fb43fd5751f12942f3a29a90e">CVC3::SearchEngine</a>
, <a class="el" href="group__SE.html#ga7d62893d0d19ed50cc1f616a92d536c0">CVC3::SearchImplBase</a>
, <a class="el" href="classCVC3_1_1SearchSat.html#a43a09dbf7232bfdb6f10aee4df1add94">CVC3::SearchSat</a>
, <a class="el" href="classCVC3_1_1VCL.html#af2cf35f9a462d155002d5684c817052f">CVC3::VCL</a>
</li>
<li>rewrite()
: <a class="el" href="classCVC3_1_1TheoryRecords.html#a56d1048536807a3bb9d746c833b75c47">CVC3::TheoryRecords</a>
, <a class="el" href="classCVC3_1_1TheoryBitvector.html#a82d63a41524830f12abe05b948eab4ca">CVC3::TheoryBitvector</a>
, <a class="el" href="group__Theory__API.html#gaa6475baeb444915fa3b2f5c58dc5148a">CVC3::Theory</a>
, <a class="el" href="classCVC3_1_1TheoryArith.html#aaa06e89f76f2313953a35d867c33942f">CVC3::TheoryArith</a>
, <a class="el" href="classCVC3_1_1TheoryArith3.html#a372ca4601f982473511cd0fc55c83374">CVC3::TheoryArith3</a>
, <a class="el" href="classCVC3_1_1TheoryArithNew.html#adf76a677d3133da1fb3e8cf33ba26cc9">CVC3::TheoryArithNew</a>
, <a class="el" href="classCVC3_1_1TheoryArithOld.html#a17c6d2694c44f77da17d5b32620b0761">CVC3::TheoryArithOld</a>
, <a class="el" href="classCVC3_1_1TheoryArray.html#ad26e3958bc32f28030d57c9b8415d69f">CVC3::TheoryArray</a>
, <a class="el" href="classCVC3_1_1TheoryCore.html#a54bce613a6b49a9a8a1a888ec36346d8">CVC3::TheoryCore</a>
, <a class="el" href="classCVC3_1_1TheoryDatatype.html#a5fea4f3ab06825c2df409082095f7d96">CVC3::TheoryDatatype</a>
, <a class="el" href="classCVC3_1_1TheoryQuant.html#aaed061533566d5aa74f4195a6eece020">CVC3::TheoryQuant</a>
, <a class="el" href="classCVC3_1_1TheorySimulate.html#a7ffc512dc7ea5a3178445b904c7071e2">CVC3::TheorySimulate</a>
, <a class="el" href="classCVC3_1_1TheoryUF.html#a128eb911fae9a65232037d6cf0c4f0e5">CVC3::TheoryUF</a>
</li>
<li>rewriteAnd()
: <a class="el" href="classCVC3_1_1Theory.html#aba1822f2d985b50f6405c290c3814c1a">CVC3::Theory</a>
, <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ad74cb42b63d2f92b55c79281e84816c1">CVC3::CommonTheoremProducer</a>
, <a class="el" href="classCVC3_1_1CommonProofRules.html#a1d546d9530a3c15cd627a141137a8616">CVC3::CommonProofRules</a>
</li>
<li>rewriteAndSubterms()
: <a class="el" href="classCVC3_1_1CoreProofRules.html#a07d66271324bda72a66505bb427df156">CVC3::CoreProofRules</a>
, <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a8c67942a0f72ee11abe27c992e0833c1">CVC3::CoreTheoremProducer</a>
</li>
<li>rewriteAtomic()
: <a class="el" href="group__Theory__API.html#gaacb9782eae3d1121c415cd4b7650025c">CVC3::Theory</a>
, <a class="el" href="classCVC3_1_1TheoryBitvector.html#a55e7711ed3e5be41dd7aca955a9ecc7a">CVC3::TheoryBitvector</a>
</li>
<li>rewriteAux()
: <a class="el" href="classCVC3_1_1TheoryRecords.html#a89f926d66c9b7b414160bb12f42f4485">CVC3::TheoryRecords</a>
</li>
<li>rewriteBoolean()
: <a class="el" href="classCVC3_1_1TheoryBitvector.html#ac2ed14005bb197aaad28ead0cb537a72">CVC3::TheoryBitvector</a>
</li>
<li>rewriteBV()
: <a class="el" href="classCVC3_1_1TheoryBitvector.html#a214442814e895d26ac43c42663741fbd">CVC3::TheoryBitvector</a>
</li>
<li>rewriteBVCOMP()
: <a class="el" href="classCVC3_1_1BitvectorProofRules.html#acccc78337e0a0143b9635e1cd49ac657">CVC3::BitvectorProofRules</a>
, <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#ab314017086d977ee1f4facb23208864c">CVC3::BitvectorTheoremProducer</a>
</li>
<li>rewriteBVSub()
: <a class="el" href="classCVC3_1_1BitvectorProofRules.html#a693f8801e36967bf64a0fef0290cad5a">CVC3::BitvectorProofRules</a>
, <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a1a040de059cc4fedf5cdd00cec37fc9c">CVC3::BitvectorTheoremProducer</a>
</li>
<li>rewriteCC()
: <a class="el" href="classCVC3_1_1Theory.html#a2d91d71489b0c0a9822cef765326bc89">CVC3::Theory</a>
</li>
<li>rewriteCore()
: <a class="el" href="classCVC3_1_1TheoryCore.html#a84a6096579ca77dda6b673da7f1fce7c">CVC3::TheoryCore</a>
</li>
<li>rewriteDistinct()
: <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a17536e7c7ffa8d9a34981458a20f21ff">CVC3::CoreTheoremProducer</a>
, <a class="el" href="classCVC3_1_1CoreProofRules.html#ae429bb5ede0ce74b02cb85f8d0a372dd">CVC3::CoreProofRules</a>
</li>
<li>rewriteIff()
: <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ab2233ef28defaf0af1b6a8cc4b887708">CVC3::CommonTheoremProducer</a>
, <a class="el" href="classCVC3_1_1CommonProofRules.html#a5c50bf251b95dfc47ccfc6e8b51426c1">CVC3::CommonProofRules</a>
</li>
<li>rewriteImplies()
: <a class="el" href="classCVC3_1_1CoreProofRules.html#a3389cd795acc4cee4b591c1488293963">CVC3::CoreProofRules</a>
, <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#ac88efa4d7c591f187d3212c7162ef9a5">CVC3::CoreTheoremProducer</a>
</li>
<li>rewriteIte()
: <a class="el" href="classCVC3_1_1Theory.html#a0f2e0c6647ff6282ee2f65116a82e13b">CVC3::Theory</a>
</li>
<li>rewriteIteBool()
: <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#ac888377c574a056b251446902c010352">CVC3::CoreTheoremProducer</a>
, <a class="el" href="classCVC3_1_1CoreProofRules.html#aa66c668de7d5a026297a6bc901a1f7c3">CVC3::CoreProofRules</a>
</li>
<li>rewriteIteCond()
: <a class="el" href="classCVC3_1_1CoreProofRules.html#a03f8a74b8b1b6d90ff23a0a6150c49d6">CVC3::CoreProofRules</a>
, <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#acc27c290c53fdaab6977d43d765b10e3">CVC3::CoreTheoremProducer</a>
</li>
<li>rewriteIteElse()
: <a class="el" href="classCVC3_1_1CoreProofRules.html#a7912f66f5be7e05b0c85f15596747be4">CVC3::CoreProofRules</a>
, <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#ae1092dc92aef4300caf926b48ac2ec65">CVC3::CoreTheoremProducer</a>
</li>
<li>rewriteIteFalse()
: <a class="el" href="classCVC3_1_1CommonProofRules.html#a95af3ce5ccd4212b15bac9b249004c48">CVC3::CommonProofRules</a>
, <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a1711198c758a0475449b1889815f1371">CVC3::CommonTheoremProducer</a>
</li>
<li>rewriteIteSame()
: <a class="el" href="classCVC3_1_1CommonProofRules.html#a6cb02a9489ef5ed4e548f49bbd07439f">CVC3::CommonProofRules</a>
, <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#aad60929c1c8c79287a16bc995cd9c51c">CVC3::CommonTheoremProducer</a>
</li>
<li>rewriteIteThen()
: <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a490808acd89e0732678d570599c93165">CVC3::CoreTheoremProducer</a>
, <a class="el" href="classCVC3_1_1CoreProofRules.html#a8117a95eed02c35936f988d1c9c2bdab">CVC3::CoreProofRules</a>
</li>
<li>rewriteIteToAnd()
: <a class="el" href="classCVC3_1_1CoreProofRules.html#a3eb08bdf90ac80d5c372e4791120d894">CVC3::CoreProofRules</a>
, <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#ae681f89828ece60f9725c5696204cd72">CVC3::CoreTheoremProducer</a>
</li>
<li>rewriteIteToIff()
: <a class="el" href="classCVC3_1_1CoreProofRules.html#a8a98457f410ab11e4b66adad150e1b67">CVC3::CoreProofRules</a>
, <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#abba61fa631a3e3fd6ae8761754f01c72">CVC3::CoreTheoremProducer</a>
</li>
<li>rewriteIteToImp()
: <a class="el" href="classCVC3_1_1CoreProofRules.html#a1d30881c6f1a902575da033dbbeb2aa9">CVC3::CoreProofRules</a>
, <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#af0468c432ee5bfc5f82675f4b50e2002">CVC3::CoreTheoremProducer</a>
</li>
<li>rewriteIteToNot()
: <a class="el" href="classCVC3_1_1CoreProofRules.html#a71c2aa506efd447f6c411159f44d5af0">CVC3::CoreProofRules</a>
, <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a27d39117a5ede71d9c460b0232bdd469">CVC3::CoreTheoremProducer</a>
</li>
<li>rewriteIteToOr()
: <a class="el" href="classCVC3_1_1CoreProofRules.html#ab23828c9cc70a3805a0be7632e03163b">CVC3::CoreProofRules</a>
, <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a2db95a382b0141d9a5098e9ca9ddd0f7">CVC3::CoreTheoremProducer</a>
</li>
<li>rewriteIteTrue()
: <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a2459a321ea5cdab974dc2cf029934a71">CVC3::CommonTheoremProducer</a>
, <a class="el" href="classCVC3_1_1CommonProofRules.html#a0e770e47e947275a69b4c9f225f8beb6">CVC3::CommonProofRules</a>
</li>
<li>rewriteLeavesConst()
: <a class="el" href="classCVC3_1_1ArithProofRules.html#a81d9ea1e5c2d42c2b60a893c879145bd">CVC3::ArithProofRules</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a120563be6dbb828da3e9b6a9d4d35e32">CVC3::ArithTheoremProducerOld</a>
</li>
<li>rewriteLetDecl()
: <a class="el" href="classCVC3_1_1CoreProofRules.html#acad687c3e6faa5709961210637c260da">CVC3::CoreProofRules</a>
, <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a222db72dc6f637e582dfb9b8dd4e362c">CVC3::CoreTheoremProducer</a>
</li>
<li>rewriteLitCore()
: <a class="el" href="classCVC3_1_1TheoryCore.html#a8ba8c93d75329369b8d91f37a463ef09">CVC3::TheoryCore</a>
</li>
<li>rewriteLiteral()
: <a class="el" href="classCVC3_1_1TheoryCore.html#a586e77e855946fd0b5f541ec06f7decd">CVC3::TheoryCore</a>
</li>
<li>rewriteLitSelect()
: <a class="el" href="classCVC3_1_1RecordsTheoremProducer.html#a6daf5a4886315133bf830d52c6fb010d">CVC3::RecordsTheoremProducer</a>
, <a class="el" href="classCVC3_1_1RecordsProofRules.html#a3e3add607e89398f2cc6cc38ea99d1ff">CVC3::RecordsProofRules</a>
</li>
<li>rewriteLitUpdate()
: <a class="el" href="classCVC3_1_1RecordsProofRules.html#a123d754579587119040963036a57b20c">CVC3::RecordsProofRules</a>
, <a class="el" href="classCVC3_1_1RecordsTheoremProducer.html#ae794bafd39256699bda95e85e01ffd39">CVC3::RecordsTheoremProducer</a>
</li>
<li>rewriteNAND()
: <a class="el" href="classCVC3_1_1BitvectorProofRules.html#a53c8279d20f7d229437790ce6c0da2da">CVC3::BitvectorProofRules</a>
, <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a2d49a06be7aae5f5675977fdc1b6457e">CVC3::BitvectorTheoremProducer</a>
</li>
<li>rewriteNOR()
: <a class="el" href="classCVC3_1_1BitvectorProofRules.html#a8e2d34a4c387bd5eace8b7e6237bd936">CVC3::BitvectorProofRules</a>
, <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a372c699b42bb9ab8b64e2a836bedcffd">CVC3::BitvectorTheoremProducer</a>
</li>
<li>rewriteNot()
: <a class="el" href="classCVC3_1_1CompleteInstPreProcessor.html#a0d86f8e44226c42e5c9f35ec866a7459">CVC3::CompleteInstPreProcessor</a>
</li>
<li>rewriteNotAnd()
: <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a66f5d185eca0ccf417b4bf5ed4448f72">CVC3::CoreTheoremProducer</a>
, <a class="el" href="classCVC3_1_1CoreProofRules.html#ade3007866410b6565ee0ea1ff4c49a99">CVC3::CoreProofRules</a>
</li>
<li>rewriteNotExists()
: <a class="el" href="classCVC3_1_1QuantTheoremProducer.html#a658fde1235cb9668d454cbe9144b1da9">CVC3::QuantTheoremProducer</a>
, <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a2535d1565f3f7b830063ad9ae3e1c4e7">CVC3::CommonTheoremProducer</a>
, <a class="el" href="classCVC3_1_1CommonProofRules.html#a12d8ca9f5547fb3a3239d7dc6f53987c">CVC3::CommonProofRules</a>
, <a class="el" href="classCVC3_1_1QuantProofRules.html#a4c8b8bfac3db9139fbdf4d8c22e61c79">CVC3::QuantProofRules</a>
</li>
<li>rewriteNotFalse()
: <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#aace9193e3ff294ef6065178a55610e88">CVC3::CommonTheoremProducer</a>
, <a class="el" href="classCVC3_1_1CommonProofRules.html#a30fa79637f4308e8e733015624293775">CVC3::CommonProofRules</a>
</li>
<li>rewriteNotForall()
: <a class="el" href="classCVC3_1_1CommonProofRules.html#ad14f0ceb0d486ba3d78c2c3c6e47382a">CVC3::CommonProofRules</a>
, <a class="el" href="classCVC3_1_1QuantTheoremProducer.html#af59e47a4b45f624d2d8e088d5668f596">CVC3::QuantTheoremProducer</a>
, <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a6241bfc091691a667ed41a9d36d4cab6">CVC3::CommonTheoremProducer</a>
, <a class="el" href="classCVC3_1_1QuantProofRules.html#a5e3e699c8e55b7f9bd8878cb7ed28ef0">CVC3::QuantProofRules</a>
</li>
<li>rewriteNotIff()
: <a class="el" href="classCVC3_1_1CoreProofRules.html#ae480ca62cb7a8656f01ea3f938fb97d8">CVC3::CoreProofRules</a>
, <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a7da16f5874fbc0870f57a9deeeec80b8">CVC3::CoreTheoremProducer</a>
</li>
<li>rewriteNotIte()
: <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#accd799779aa02c5d84352cc48e975b3d">CVC3::CoreTheoremProducer</a>
, <a class="el" href="classCVC3_1_1CoreProofRules.html#ac68942cf0c21011f9429042e279b4a54">CVC3::CoreProofRules</a>
</li>
<li>rewriteNotNot()
: <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a84b83e300ddf9e67e427b2815ecff1e7">CVC3::CommonTheoremProducer</a>
, <a class="el" href="classCVC3_1_1CommonProofRules.html#a8a04ff29591a019d4d4cf073c0987316">CVC3::CommonProofRules</a>
</li>
<li>rewriteNotOr()
: <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#a5ce6abeb6a346d20f5d5860a30a33e28">CVC3::CoreTheoremProducer</a>
, <a class="el" href="classCVC3_1_1CoreProofRules.html#aea875ee7355ae6aab01b84c176dbccf6">CVC3::CoreProofRules</a>
</li>
<li>rewriteNotTrue()
: <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a49ce394a818d2ab83b2f97d44cd66f1b">CVC3::CommonTheoremProducer</a>
, <a class="el" href="classCVC3_1_1CommonProofRules.html#ad55b11590196fbd73d24daa1d0d6eeb1">CVC3::CommonProofRules</a>
</li>
<li>rewriteOpDef()
: <a class="el" href="classCVC3_1_1UFTheoremProducer.html#a236af9209026d20f514c7ceba28c3f76">CVC3::UFTheoremProducer</a>
, <a class="el" href="classCVC3_1_1UFProofRules.html#a0bb7ab17e898f5dbb49e9767c3c1072d">CVC3::UFProofRules</a>
</li>
<li>rewriteOr()
: <a class="el" href="classCVC3_1_1Theory.html#ad58c336212c2669f3cf32c0915ee3788">CVC3::Theory</a>
, <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#aa0d6b0fbe3838ae22b4a90d92d1530e2">CVC3::CommonTheoremProducer</a>
, <a class="el" href="classCVC3_1_1CommonProofRules.html#a44474beaa5761147eb816db48c795c4b">CVC3::CommonProofRules</a>
, <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a9f135d57462754cd9903190d4fe4aec8">CVC3::CommonTheoremProducer</a>
</li>
<li>rewriteOrSubterms()
: <a class="el" href="classCVC3_1_1CoreTheoremProducer.html#ae6b1fd56b11dbe24218cd2f5c74518c9">CVC3::CoreTheoremProducer</a>
, <a class="el" href="classCVC3_1_1CoreProofRules.html#a0d589028239025d0e43c92c04b5d586a">CVC3::CoreProofRules</a>
</li>
<li>rewriteReadWrite()
: <a class="el" href="classCVC3_1_1ArrayTheoremProducer.html#a508cb6e565c59ad0e91ee380774ea379">CVC3::ArrayTheoremProducer</a>
, <a class="el" href="classCVC3_1_1ArrayProofRules.html#a7cc5971eef4c841bd3b5c2dce8029b53">CVC3::ArrayProofRules</a>
</li>
<li>rewriteReadWrite2()
: <a class="el" href="classCVC3_1_1ArrayTheoremProducer.html#a5b6d56f4f0f05cb3671b3c01b293d3bc">CVC3::ArrayTheoremProducer</a>
, <a class="el" href="classCVC3_1_1ArrayProofRules.html#ae493f58a14d1ab904de9e24fab6f7c10">CVC3::ArrayProofRules</a>
</li>
<li>rewriteRedundantWrite1()
: <a class="el" href="classCVC3_1_1ArrayProofRules.html#ad6a2685b58c198964d3e62b0cd9b7536">CVC3::ArrayProofRules</a>
, <a class="el" href="classCVC3_1_1ArrayTheoremProducer.html#a1b4dd97c680555f98834c0c2eb63beca">CVC3::ArrayTheoremProducer</a>
</li>
<li>rewriteRedundantWrite2()
: <a class="el" href="classCVC3_1_1ArrayTheoremProducer.html#a4eb3fa026164aa36735dde9de93067e6">CVC3::ArrayTheoremProducer</a>
, <a class="el" href="classCVC3_1_1ArrayProofRules.html#a528af9ac1b1f4d43bbf14cad57f0cad7">CVC3::ArrayProofRules</a>
</li>
<li>rewriteReflexivity()
: <a class="el" href="classCVC3_1_1CommonProofRules.html#ad078b5d25129b200fe04b20c5962aa34">CVC3::CommonProofRules</a>
, <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#a26b00cb395f45971ace24a4529189e1b">CVC3::CommonTheoremProducer</a>
</li>
<li>rewriteSameStore()
: <a class="el" href="classCVC3_1_1ArrayTheoremProducer.html#a0ab9aba97b1937710a9eba916ae02c05">CVC3::ArrayTheoremProducer</a>
, <a class="el" href="classCVC3_1_1ArrayProofRules.html#a972bcffba3fec45e0407b21eb337cc36">CVC3::ArrayProofRules</a>
</li>
<li>rewriteSelCons()
: <a class="el" href="classCVC3_1_1DatatypeProofRules.html#a8ecc9e0e858ab2da52632df61ee8a44e">CVC3::DatatypeProofRules</a>
, <a class="el" href="classCVC3_1_1DatatypeTheoremProducer.html#af9bedcb0fceb3b92975fef0e052d5029">CVC3::DatatypeTheoremProducer</a>
</li>
<li>rewriteTestCons()
: <a class="el" href="classCVC3_1_1DatatypeProofRules.html#ad6df2a8a8c661ed1a1be34ce66910a36">CVC3::DatatypeProofRules</a>
, <a class="el" href="classCVC3_1_1DatatypeTheoremProducer.html#a789906697a69645f117c5d4cab0242de">CVC3::DatatypeTheoremProducer</a>
</li>
<li>rewriteToDiff()
: <a class="el" href="classCVC3_1_1TheoryArith.html#a5fcd4d9b9075f8d00096eea469b81abc">CVC3::TheoryArith</a>
</li>
<li>rewriteUpdateSelect()
: <a class="el" href="classCVC3_1_1RecordsProofRules.html#aa89519b074a161d4709cc57c72be9877">CVC3::RecordsProofRules</a>
, <a class="el" href="classCVC3_1_1RecordsTheoremProducer.html#aa5d335a5684178e3553a9ce69a265046">CVC3::RecordsTheoremProducer</a>
</li>
<li>rewriteUsingSymmetry()
: <a class="el" href="classCVC3_1_1CommonProofRules.html#a338cafc978d9b6a447e8d58af42d7e5b">CVC3::CommonProofRules</a>
, <a class="el" href="classCVC3_1_1CommonTheoremProducer.html#ac0813c68583ad6f0661d4c1affe3c6d8">CVC3::CommonTheoremProducer</a>
</li>
<li>rewriteWriteWrite()
: <a class="el" href="classCVC3_1_1ArrayProofRules.html#a7bd90a2d883b5a0e9de8de61ae495be2">CVC3::ArrayProofRules</a>
, <a class="el" href="classCVC3_1_1ArrayTheoremProducer.html#a45d175085355a9ff4215371c08fae566">CVC3::ArrayTheoremProducer</a>
</li>
<li>rewriteXNOR()
: <a class="el" href="classCVC3_1_1BitvectorProofRules.html#af126175b4dbb92231ec44c14f32d8b21">CVC3::BitvectorProofRules</a>
, <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a70ad43279f8061f7be4e35c49205ab69">CVC3::BitvectorTheoremProducer</a>
</li>
<li>rightMinusLeft()
: <a class="el" href="classCVC3_1_1ArithProofRules.html#acde77bf4aa73ff6b9a079b372ed7cc51">CVC3::ArithProofRules</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aca76a2dbee73d7ad9e2529ac8ce142a4">CVC3::ArithTheoremProducer3</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a3eb1309c184247837239c098d9c9100a">CVC3::ArithTheoremProducer</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a088b20af694e737e1c7ff12d2ff74d7c">CVC3::ArithTheoremProducerOld</a>
</li>
<li>rightShiftToConcat()
: <a class="el" href="classCVC3_1_1BitvectorProofRules.html#ab2d4f1d9f2f71845d0e2efb2e9ab0f02">CVC3::BitvectorProofRules</a>
, <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a7d91d285e929d00572f3da4da772f505">CVC3::BitvectorTheoremProducer</a>
</li>
<li>rotlRule()
: <a class="el" href="classCVC3_1_1BitvectorProofRules.html#a9a9c214170ee9595f2eb0b0552b6130f">CVC3::BitvectorProofRules</a>
, <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#afdc5b05255d1d217c26d5e3660957fde">CVC3::BitvectorTheoremProducer</a>
</li>
<li>rotrRule()
: <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a6495867fe7ef34a838e83315dd8b02e4">CVC3::BitvectorTheoremProducer</a>
, <a class="el" href="classCVC3_1_1BitvectorProofRules.html#aca310d258dd22e4e50b19274047c6528">CVC3::BitvectorProofRules</a>
</li>
<li>run_periodic_functions()
: <a class="el" href="classCSolver.html#a0ffdf7d6d085ca70b50391598bf4c543">CSolver</a>
</li>
<li>RWTheoremValue()
: <a class="el" href="classCVC3_1_1RWTheoremValue.html#a0609a1142e41b1d43d43d5f60f8f701c">CVC3::RWTheoremValue</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>
