<!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 class="current"><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><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_m"></a>- m -</h3><ul>
<li>Make()
: <a class="el" href="classLFSCBoolRes.html#a721ac95de042a1be9fcfe6d7b6e5df71">LFSCBoolRes</a>
, <a class="el" href="classLFSCClausify.html#a976ffe7504641550090b29a9b5cf5732">LFSCClausify</a>
, <a class="el" href="classLFSCLraAxiom.html#ae8250c8db4183085e62a5b0c5966127a">LFSCLraAxiom</a>
, <a class="el" href="classLFSCPfLambda.html#abcb32823122bdb0558104cceeed81490">LFSCPfLambda</a>
, <a class="el" href="classLFSCProofGeneric.html#a1bf5343c88454d1ffb552a3e2f59ddc8">LFSCProofGeneric</a>
, <a class="el" href="classLFSCLraMulC.html#ab2262ccc40a6212bbc9182700a2b0e73">LFSCLraMulC</a>
, <a class="el" href="classLFSCProofGeneric.html#a9f28fa214447cdab3c480e45d0073e7f">LFSCProofGeneric</a>
, <a class="el" href="classLFSCClausify.html#abaec88f39f6f56cc6f21887c35b61beb">LFSCClausify</a>
, <a class="el" href="classLFSCLraSub.html#a66b3327a7dadc49a0e072b6d1f6f6289">LFSCLraSub</a>
, <a class="el" href="classLFSCPfLet.html#a8a9295947ba6381d158f39b570fcebaf">LFSCPfLet</a>
, <a class="el" href="classLFSCLraPoly.html#ac525239ecb136141bfa7e2b2f2b0391d">LFSCLraPoly</a>
, <a class="el" href="classLFSCLem.html#abb9541ac21517f3bd70abb11a97a7715">LFSCLem</a>
, <a class="el" href="classLFSCAssume.html#a1936e5119fa84aec4acc5d8ba83bc30b">LFSCAssume</a>
, <a class="el" href="classLFSCLraPoly.html#ae2ca7c3166c207c584a5c8888d5d2ad8">LFSCLraPoly</a>
, <a class="el" href="classLFSCLraContra.html#aa561c53b9672b46c4490329b65b1f5fd">LFSCLraContra</a>
, <a class="el" href="classLFSCLraAdd.html#aa1d14054914f4333c90cf53a0d23de76">LFSCLraAdd</a>
, <a class="el" href="classLFSCProofExpr.html#a5889c9d07ff4346fe7cd9533a236839a">LFSCProofExpr</a>
, <a class="el" href="classLFSCPfVar.html#ac7b68737c0763fbc46619c54bd1df148">LFSCPfVar</a>
</li>
<li>Make_and_elim()
: <a class="el" href="classLFSCProof.html#a547ec01104eb074ab2eb4f25ea9435e0">LFSCProof</a>
</li>
<li>Make_CNF()
: <a class="el" href="classLFSCProof.html#ab1b22c672f110e3f9abe22b2bf377fb3">LFSCProof</a>
</li>
<li>Make_i()
: <a class="el" href="classLFSCClausify.html#af22d08150cb2f47d017ed68e3c31093a">LFSCClausify</a>
</li>
<li>make_lambda()
: <a class="el" href="classLFSCProof.html#a396c41fc6012caf4dde358af52d25905">LFSCProof</a>
</li>
<li>make_let_map()
: <a class="el" href="classLFSCPrinter.html#a411ca081d553c254903811d65e56b6d2">LFSCPrinter</a>
</li>
<li>make_let_proof()
: <a class="el" href="classLFSCConvert.html#a4632b62661448d6fde086cbe7d260398">LFSCConvert</a>
</li>
<li>Make_mimic()
: <a class="el" href="classLFSCProof.html#a979135fb775da82a9bf06befd9def730">LFSCProof</a>
</li>
<li>Make_not_not_elim()
: <a class="el" href="classLFSCProof.html#a95e3c7629c196ed189ad0525304e48cb">LFSCProof</a>
</li>
<li>make_trusted()
: <a class="el" href="classLFSCConvert.html#a973be3db649311c32e126e0c15c8e51e">LFSCConvert</a>
</li>
<li>MakeC()
: <a class="el" href="classLFSCBoolRes.html#a6313b796f9dbbf3352cdb113eb83d42d">LFSCBoolRes</a>
</li>
<li>makeCopy()
: <a class="el" href="classCVC3_1_1CDList.html#a73cc9e67876b310570f199849c4b4c34">CVC3::CDList< T ></a>
, <a class="el" href="classCVC3_1_1CDOmap.html#a6386a73023acf410a8df5b7bb0d08e49">CVC3::CDOmap< Key, Data, HashFcn ></a>
, <a class="el" href="classCVC3_1_1CDMapData.html#a8b7d38c1c2ed1bfc0d9d3f198609fb04">CVC3::CDMapData</a>
, <a class="el" href="classCVC3_1_1CDMap.html#aa4ff8e99983ef020ad28d075a26f8ac9">CVC3::CDMap< Key, Data, HashFcn ></a>
, <a class="el" href="classCVC3_1_1CDOmapOrdered.html#a0045f7e37636e889e0cd197068c643f3">CVC3::CDOmapOrdered< Key, Data ></a>
, <a class="el" href="classCVC3_1_1CDMapOrderedData.html#adaf47bcee164f95b2a5e6aad676ea53c">CVC3::CDMapOrderedData</a>
, <a class="el" href="classCVC3_1_1CDMapOrdered.html#a48ad3cbe534e9c42ec5def51cfd007c5">CVC3::CDMapOrdered< Key, Data ></a>
, <a class="el" href="classCVC3_1_1CDO.html#a07f3f963911d58ec1e09fa879c934609">CVC3::CDO< T ></a>
, <a class="el" href="classCVC3_1_1ContextObj.html#a11da9a588638bb9c3fdbd5218dfdf9c6">CVC3::ContextObj</a>
, <a class="el" href="classCVC3_1_1CDFlags.html#a33acad825f9e9bd5953483a948da241d">CVC3::CDFlags</a>
</li>
<li>makeCurrent()
: <a class="el" href="classCVC3_1_1ContextObj.html#a780166170b1df8eb7a7632eae66c3511">CVC3::ContextObj</a>
</li>
<li>makeDecision()
: <a class="el" href="classSAT_1_1DPLLT_1_1Decider.html#a9a15df2a6d6fdd38d9719f5681c068f2">SAT::DPLLT::Decider</a>
, <a class="el" href="classCVC3_1_1SearchSat.html#afa9bdddd9bef64500f6a958d90682c37">CVC3::SearchSat</a>
, <a class="el" href="classCVC3_1_1SearchSatDecider.html#ad58d3667503de13c9921d751f8663e00">CVC3::SearchSatDecider</a>
</li>
<li>MakeEq()
: <a class="el" href="classLFSCLraAxiom.html#aa66e0ed64485094885554d14f6129112">LFSCLraAxiom</a>
</li>
<li>MakeLit()
: <a class="el" href="classSatSolver.html#a66bbef74a05f145e477adf37a1e1d116">SatSolver</a>
, <a class="el" href="classXchaff.html#a9e916fd4048dfdcfdec013481e970303">Xchaff</a>
</li>
<li>MakeStr()
: <a class="el" href="classLFSCProofGeneric.html#abf29b3cdedf8439a6ee65ebc137340f5">LFSCProofGeneric</a>
</li>
<li>MakeUnk()
: <a class="el" href="classLFSCProofGeneric.html#a49ff2fcc1122bbecf8fff0559ddeccad">LFSCProofGeneric</a>
</li>
<li>MakeV()
: <a class="el" href="classLFSCPfVar.html#a0d9785d85b1d55610f43d6f0ba3de955">LFSCPfVar</a>
</li>
<li>mapTermsByType()
: <a class="el" href="classCVC3_1_1TheoryQuant.html#a151e98ce89abebbe306580f7fcd06704">CVC3::TheoryQuant</a>
</li>
<li>mark_clause_deleted()
: <a class="el" href="classCDatabase.html#a6529c55a489afcd88e37370d6a61ae96">CDatabase</a>
</li>
<li>mark_var_in_new_cl()
: <a class="el" href="classCDatabase.html#a8fa67bd6b830c6853b01ed51b5fd183c">CDatabase</a>
</li>
<li>mark_vars_at_level()
: <a class="el" href="classCSolver.html#a525a84f821d273c9883a407c585b8b0d">CSolver</a>
</li>
<li>markDeleted()
: <a class="el" href="classCVC3_1_1Clause.html#a47d7c887d12dce3ad803bd7e9fbdefe8">CVC3::Clause</a>
</li>
<li>MarkNonSolvableEq()
: <a class="el" href="classCVC3_1_1BitvectorProofRules.html#a02032b49999aa3913265a22cac129045">CVC3::BitvectorProofRules</a>
, <a class="el" href="classCVC3_1_1BitvectorTheoremProducer.html#a0f02e48875ccb661cae7cc7a2489dce1">CVC3::BitvectorTheoremProducer</a>
</li>
<li>markSat()
: <a class="el" href="classCVC3_1_1Clause.html#ae266a9c156142d2f9f53ec741d7304df">CVC3::Clause</a>
</li>
<li>matches()
: <a class="el" href="classCVC3_1_1Theorem.html#a1d50e47a6c0a1dc6ac9328c5b8e63d1c">CVC3::Theorem</a>
</li>
<li>matchListNew()
: <a class="el" href="classCVC3_1_1TheoryQuant.html#a8631dcdf3e42b922ea500115b2f70629">CVC3::TheoryQuant</a>
</li>
<li>matchListOld()
: <a class="el" href="classCVC3_1_1TheoryQuant.html#a7aa91c8e11e7d0058082d1be9e5cb851">CVC3::TheoryQuant</a>
</li>
<li>max_dlevel()
: <a class="el" href="classCSolver.html#a881e379b28047fde2157720bf4ee9fd0">CSolver</a>
</li>
<li>mem_usage()
: <a class="el" href="classCSolver.html#af5b9bcac3d3bf0530bc36285ce8cc7f6">CSolver</a>
, <a class="el" href="classCDatabase.html#a1758bead04486434d17201a4bc9e6e40">CDatabase</a>
</li>
<li>MemoryManagerChunks()
: <a class="el" href="classCVC3_1_1MemoryManagerChunks.html#a5efded8dddcac26ffaa5d63b8706aa4f">CVC3::MemoryManagerChunks</a>
</li>
<li>MemoryManagerMalloc()
: <a class="el" href="classCVC3_1_1MemoryManagerMalloc.html#a14bec98b0e53f1062e1ec32b05e5e6db">CVC3::MemoryManagerMalloc</a>
</li>
<li>mergeLabels()
: <a class="el" href="classCVC3_1_1TheoryDatatype.html#a942fa3974b5c4bc2f44e202a6adc80c8">CVC3::TheoryDatatype</a>
, <a class="el" href="classCVC3_1_1TheoryDatatypeLazy.html#a59df564de13b5482c49581880e816c8f">CVC3::TheoryDatatypeLazy</a>
</li>
<li>min()
: <a class="el" href="classCVC3_1_1TheoryBitvector.html#ab4f87aca710aa31e6d438e91301beffc">CVC3::TheoryBitvector</a>
</li>
<li>minusExpr()
: <a class="el" href="classCVC3_1_1ValidityChecker.html#a980a35d1a660890e16a66a7c1bfd6ba0">CVC3::ValidityChecker</a>
, <a class="el" href="classCVC3_1_1VCL.html#a41b81d8fe76fa4bb44a69e16dfed7dc6">CVC3::VCL</a>
</li>
<li>minusOne()
: <a class="el" href="classCVC3_1_1CompleteInstPreProcessor.html#a8229594b976a7bee92940c1a8ebec1bf">CVC3::CompleteInstPreProcessor</a>
</li>
<li>minusToPlus()
: <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ab369e518fc2ee411503253fa0b1515d6">CVC3::ArithTheoremProducer</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ab0d610d377cc20e3ce16823713d25403">CVC3::ArithTheoremProducer3</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#ae3458f7b381a95e124e3204ed66904ef">CVC3::ArithTheoremProducerOld</a>
, <a class="el" href="classCVC3_1_1ArithProofRules.html#a4319c532082c0f43794b34a2fb9df73f">CVC3::ArithProofRules</a>
</li>
<li>mkClause()
: <a class="el" href="classXchaff.html#a68161914638f53d93a26ff242e437472">Xchaff</a>
</li>
<li>mkLit()
: <a class="el" href="classSAT_1_1Lit.html#a4ce14efe342a740556003ec1c0d2e006">SAT::Lit</a>
, <a class="el" href="classXchaff.html#a216cb72b0a5a4568ef9a0eb430b2d933">Xchaff</a>
</li>
<li>mkOp()
: <a class="el" href="group__ExprPkg.html#ga3aefe2fb15c2d8e3a51dd92dbcc5cdc5">CVC3::Expr</a>
</li>
<li>mkVar()
: <a class="el" href="classXchaff.html#a7ffa41a1a67d90266b131230adebda68">Xchaff</a>
</li>
<li>modEq()
: <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#ada3b48ce9720177b4a427237efe0453f">CVC3::ArithTheoremProducer3</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a3cb8580c7627250ffe999de9a1b2c8c3">CVC3::ArithTheoremProducer</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a0f531ca3d0d71a1872e1519aeafa7700">CVC3::ArithTheoremProducerOld</a>
</li>
<li>modified()
: <a class="el" href="classCVC3_1_1CLFlag.html#a75bcd631f1de487481c0a06c6f5db984">CVC3::CLFlag</a>
</li>
<li>monomialModM()
: <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a9551aaeb071bd9c2b5703f69c2243e14">CVC3::ArithTheoremProducerOld</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a69adf7d70a6a71e5c0e3489535a18108">CVC3::ArithTheoremProducer</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a5245a34c6f9e903db87e17df1d33c09d">CVC3::ArithTheoremProducer3</a>
</li>
<li>monomialMulF()
: <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aea07da55e987ccd27d0f57e08558af01">CVC3::ArithTheoremProducer3</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a2e2582c11f6547ed6faefaec6c9142f9">CVC3::ArithTheoremProducerOld</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a41da83b4624daa43a84bc049b5b7d836">CVC3::ArithTheoremProducer</a>
</li>
<li>moveSumConstantRight()
: <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#a2b44fabb65bb6748259aee8959be465e">CVC3::ArithTheoremProducerOld</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#aad289f36b55fe8be7f7af0f62aedaae8">CVC3::ArithTheoremProducer3</a>
, <a class="el" href="classCVC3_1_1ArithProofRules.html#a18e5970bc4f670a63ca5775750f099ab">CVC3::ArithProofRules</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a77b99e94956d407e5cd20701e6771120">CVC3::ArithTheoremProducer</a>
</li>
<li>moveTo()
: <a class="el" href="classMiniSat_1_1vec.html#a8eb1dc3699eefcdf0dda42c35613b0ca">MiniSat::vec< T ></a>
</li>
<li>mult_rational()
: <a class="el" href="classTReturn.html#ac7a0e50d750845a8cfd72bc9faf4949d">TReturn</a>
</li>
<li>multEqn()
: <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#afd7a6da45999fb3237cdbbbf9c5f19e8">CVC3::ArithTheoremProducer3</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#ae66ddbc1457e3c032ea9059625059992">CVC3::ArithTheoremProducer</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#aeb54d03f4672718b7de6160a88bf33cb">CVC3::ArithTheoremProducerOld</a>
, <a class="el" href="classCVC3_1_1ArithProofRules.html#ad62d795eb10e67c655c608774881bde3">CVC3::ArithProofRules</a>
</li>
<li>multEqZero()
: <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a57eafe7c2a127ca4b4706437b777d610">CVC3::ArithTheoremProducer3</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a0040d5d848f7040df940b92d95a75930">CVC3::ArithTheoremProducer</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#ad73622cdec4a472af97d68de6716fe0a">CVC3::ArithTheoremProducerOld</a>
, <a class="el" href="classCVC3_1_1ArithProofRules.html#af8f4f59bd12fdd8f93d1fd49ae41279e">CVC3::ArithProofRules</a>
</li>
<li>multExpr()
: <a class="el" href="classCVC3_1_1ValidityChecker.html#ab1b58d4021a8e31263908cd5bee33e32">CVC3::ValidityChecker</a>
, <a class="el" href="classCVC3_1_1VCL.html#ac3d1c85bda8df4d88efb626cb7715244">CVC3::VCL</a>
</li>
<li>multIneqn()
: <a class="el" href="classCVC3_1_1ArithTheoremProducer3.html#a8af6455fe4a8889cfb7b0b8c865b847c">CVC3::ArithTheoremProducer3</a>
, <a class="el" href="classCVC3_1_1ArithProofRules.html#a70e83cfbc207a5d15fedd4adde7e9e76">CVC3::ArithProofRules</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducer.html#a3d245f36a2e42684ec2fd9356d89111f">CVC3::ArithTheoremProducer</a>
, <a class="el" href="classCVC3_1_1ArithTheoremProducerOld.html#aa425318a5846e14a94b2a3a34bb99b6d">CVC3::ArithTheoremProducerOld</a>
</li>
<li>multiplicative_inverse()
: <a class="el" href="classCVC3_1_1TheoryBitvector.html#a425367b8c2d69e637c93742ab1ed2134">CVC3::TheoryBitvector</a>
</li>
<li>multiply_coeff()
: <a class="el" href="classCVC3_1_1TheoryBitvector.html#a265761c739bb7084fa9016e527499da5">CVC3::TheoryBitvector</a>
</li>
<li>multMatchChild()
: <a class="el" href="classCVC3_1_1TheoryQuant.html#addac94f519d0c54d739281e72989a669">CVC3::TheoryQuant</a>
</li>
<li>multMatchTop()
: <a class="el" href="classCVC3_1_1TheoryQuant.html#a036828f1d240572e4a37e22af4d79d06">CVC3::TheoryQuant</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>
