<!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="namespaceMiniSat.html">MiniSat</a></li><li class="navelem"><a class="el" href="classMiniSat_1_1Solver.html">Solver</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">MiniSat::Solver Member List</div> </div>
</div><!--header-->
<div class="contents">
<p>This is the complete list of members for <a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a>, including all inherited members.</p>
<table class="directory">
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a36711ef6cb28057fa6f00235f58c03ff">addClause</a>(std::vector< Lit > &literals, CVC3::Theorem theorem, int clauseID)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#af3e9229206719e24e2a951be84c33a42">addClause</a>(Lit p, CVC3::Theorem theorem)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a03e24ae79c2068ab70b8c9633829777c">addClause</a>(const Clause &clause, bool keepClauseID)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a27b79e9b52cd9850e3e21cd2e2af9a04">addClause</a>(const SAT::Clause &clause, bool isTheoryClause)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ab7ceeed839df517256ce77c126f28e00">addFormula</a>(const SAT::CNF_Formula &cnf, bool isTheoryClause)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#af3891961fe824bc91b47b59ee1e4a90b">addWatch</a>(Lit literal, Clause *clause)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a4d58130f36a501e919bb82f5f1438e32">allClausesSatisfied</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ab4bacf381f8980c23eb2184c712b882d">analyze</a>(int &out_btlevel)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#affb21521fe39f5d003e61180dc3f5f3c">analyze_minimize</a>(std::vector< Lit > &out_learnt, Inference *inference, int &pushID)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ab91573c3ebb667e9e94f30f889598434">analyze_removable</a>(Lit p, unsigned int min_level, int pushID)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a48e255f2f05f6d56518c8e8925b30639">assume</a>(Lit p)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a49421463a8047553ffbd5fc9d04c0ad8">backtrack</a>(int level, Clause *clause)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ad4c405a5b6aac64b41c190aaa68004aa">checkClause</a>(const Clause &clause) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a9e152e0ed1d83a51f7886df8cd5fe681">checkClauses</a>() const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a9457fd91045b9496ef5bdcd1a93fcae5">checkTrail</a>() const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a09e6b3c658982dbaeec9a18d440dbe7a">checkWatched</a>(const Clause &clause) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a6b4bb1db7b767e1368884b178f523dcf">checkWatched</a>() const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a4154a7c87f54bcbf48e8e1689dae68a9">claBumpActivity</a>(Clause *c)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a3e6ce9dc49e278926bfcc32289a343c1">claDecayActivity</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a3cdc4675e024f72e82d718596159456d">claRescaleActivity</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a7fce9c6a705405959f91d559a6e06ee4">createFrom</a>(const Solver *solver)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">static</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#aac50fbefa27ff761747fe0873722f927">curAssigns</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#afb1410338334a3220d95ec28e5a68f71">curClauses</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#abbb1190222cc3ad99638caf6e86ee698">cvcToMiniSat</a>(const SAT::Clause &clause, int id)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a0765ad8a98718bb5523e487e32d66ae1">d_activity</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a81ed0225fec06bae415c6d86c86781f1">d_analyze_redundant</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ae2fd56e35cc318aed56d10fc7e5af484">d_analyze_seen</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#aede680f26ad5344891484b6f821de222">d_analyze_stack</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a8fd906b3d57929f47f9a6eb6740e35e9">d_assigns</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a3b0e8d36281ddcfefb54812accad5a55">d_cla_decay</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a5b10958ebb6b146f8cfb2d6ec08ab667">d_cla_inc</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ad6e3d6a97a4ae9dda9ac7b9bed97bed8">d_clauseIDCounter</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ae4d0195d229b334f9d9c2f3122e41bd1">d_clauses</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a431f60a202eee24b3928ca6c6195baa5">d_conflict</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a18b5a09a43e43ae4bde40537e652e987">d_decider</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#aece892bd1701b50038331c77b70d0949">d_default_params</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ad2d7fa92335dfd68f8598a5a41d17e93">d_derivation</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a4ecef2c87d4be7bf5a0ba8b4e800e09c">d_expensive_ccmin</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a53dec8ba9fc22afeeef701f1a329a669">d_inSearch</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a0c9270be1c0980e631de98b3408a8031">d_learnts</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a34c9afcb69ae37cebbf43a61505009b3">d_level</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a813826a370752a20165602e79b18f7c6">d_ok</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#aab79cd4bf5792f72c191d8149e77bc93">d_order</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#adbae4eb042f37351c6cac493e6743813">d_pendingClauses</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a99b8d67e03c83f148906ff00e8e88851">d_popLemmas</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#acb6671d85d64f00c04ea17b3b6e144f6">d_popRequests</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a6f9c67d77e57b99fef5de801623245a4">d_pushes</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ab0b2d4e87d57046e30c2cb3554925e2b">d_pushIDs</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a22427732a96158ab53c2ffc61714fca4">d_qhead</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a4405fbaba3ed712f704d5c85a390b558">d_reason</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#afc17e3fc6c5eb525504acbe000d9c5ca">d_registeredVars</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a160ccfc80ff29cd6947b0d009400e434">d_rootLevel</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span><span class="mlabel">static</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ac114e23a9bd1329c9002eb758c1595b7">d_simpDB_assigns</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a4f2b0a42acb3d470ca9500b2f4fd8077">d_simpDB_props</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ac380f5046f3dddbb0bdebf4107d8d506">d_simpRD_learnts</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ac2c0d8b62a85616add0930b4947c8f96">d_stats</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ad9d115b0ec2a84ce5ab3f1de19683f06">d_thead</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a8336c93fe51668a8cd322f9a059d5137">d_theoryAPI</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a587104e3c6bb31d2bc7942bc1fde8b1e">d_theoryExplanations</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#af092e4552ff6a34e5fcb5f67de96c845">d_trail</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#abf42fb28430f7b099c65c4e9b28ffb09">d_trail_lim</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a31a1d57eabc2169a4a9fc1cf4c87a2a7">d_trail_pos</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a354cacc000d52901cb2a60d1fe659d26">d_var_decay</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#aa9cba0f1df8f31b5ae94f2ce0ccb290f">d_var_inc</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a6a3e831d47c15ac42fe7a7002c276c0e">d_watches</a></td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a18c18c858ec2b635eede59e396f3b102">decisionLevel</a>() const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a8cc5207e3580ab0f09c6e9c225eaebff">doPops</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a7884b17f0f740781df424864717efac2">enqueue</a>(Lit fact, int decisionLevel, Clause *reason)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a70a7ffd14675ce9d3f1d445a79505278">getClauses</a>() const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a0d0c1aef5c834bc7ba7682ac3fe5b59c">getConflictLevel</a>(const Clause &clause) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a82e89493435ed86eb83f6af47fc78379">getDerivation</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a4d5144ec81209e86f7374972b8a78aa0">getImplicationLevel</a>(const Clause &clause) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#aadbf5bfce16879745ac1fc7e5226957c">getLemmas</a>() const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a68a7d96223af2e9b67d8b25d047284e4">getLevel</a>(Var var) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a70b4f991bd7a679be32a89aa1d22eb8d">getLevel</a>(Lit lit) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ac051d3f7a6f6e93269769f2ff8eb9878">getProof</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a4f5805d21238ad316845059fb378a05f">getPushID</a>(Var var) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#aa095aa10adf85a246b525e0bc717e942">getPushID</a>(Lit lit) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a8660c6ceafa236f5533e432bb859aeba">getReason</a>(Var var) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a031fbfd0b0f291ad294dc9e49a8e7ec7">getReason</a>(Lit literal, bool resolveTheoryImplication=true)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ac386ec8bbd27857254bae149db775412">getStats</a>() const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a16a71aec47f38eed46547c52ca9b152b">getTrail</a>() const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#adc9d01899ff6c1eefea8749a1a97309b">getValue</a>(Var x) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a2c6d2ce4210d3bfbc3d659dd724d02f0">getValue</a>(Lit p) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ac8d866ffb2253fdc01fe310558871da3">getWatches</a>(Lit literal)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a8987b0395fc1f850ee7b748e9685560a">getWatches</a>(Lit literal) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a1bcf27269a8286f82b3235d982e4724e">inPush</a>() const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ae28b9db22e418c5907fb82dbe49a6832">inSearch</a>() const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#aa0d36a2c07c88350dd9d54e62b3cef7b">insertClause</a>(Clause *clause)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a2ba80609ff72dbd93ae116a25923808d">insertLemma</a>(const Clause *lemma, int clauseID, int pushID)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a41ac244ff15b83ca4a863ee85cf27814">isConflicting</a>() const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a7eb95fc222427a795a3b5ae48e94518e">isConsistent</a>() const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a871c1c054262f9673518c46f7efc8450">isImpliedAt</a>(Lit lit, int clausePushID) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ad64d6215811b4c4ca6c5ac86da4c787d">isPermSatisfied</a>(Clause *c) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a344d9206f065425f276b408e86b7e1d3">isReason</a>(const Clause *c) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a31a0f344abc3fd65ee540f954b014f62">isRegistered</a>(Var var)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#af2bc4c7b90705664cf10982944640b3f">nAssigns</a>() const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#af57851d84d9e00837b1b09106bf5db27">nClauses</a>() const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a7323aff4aaa93c01e6008e8e033d2b8f">nextClauseID</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a2beb4ee59904cb55b5b3e69886a0701c">nLearnts</a>() const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a679fa13af0d75beca98981dc40f3f2a2">nVars</a>() const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#aa8b5dfa883cace427d4b8b89769ca6df">orderClause</a>(std::vector< Lit > &literals) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a2f75013fed205f5b38cd23b9d87dcd1a">pop</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a6662641d5c0dea8d89041f5cf9dbc4af">popClauses</a>(const PushEntry &pushEntry, std::vector< Clause * > &clauses)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a80f70ef105eabcf61758427d041281d6">popTheories</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ac3d7b1cc4327878d22b91d105ea32409">printDIMACS</a>() const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#af8254dba6facc2d13c85202d9d09b3f9">printState</a>() const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#aace9125740233af99f0de4e0288b075e">propagate</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a5ff984eddca26831d3057733f3848fdf">propLookahead</a>(const SearchParams &params)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a776adc363c0056e2077fbe659ae6f709">protocolPropagation</a>() const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#aec12c38c0c17d7067e12da239353ebc8">push</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a62eea2c00917497fbfb843bf9ca4482e">reduceDB</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a7a11f6c3676dd169d093a4e7c5af5299">registerVar</a>(Var var)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a241e960f84c150b1421bf4e3b3a6b073">remove</a>(Clause *c, bool just_dealloc=false)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a94c3f4932f4c9d17b4a6dc1839c813f5">removeWatch</a>(std::vector< Clause * > &ws, Clause *elem)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a8be8edbecd5a07bd39990ee7ba0918e3">requestPop</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a22b59f22e9df28fcb892e5873d998c75">resolveTheoryImplication</a>(Lit literal)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#af43d31ac67426e7b3b699491b02d62c1">search</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#adf6fbd3cddfa511acae41f180b187454">setLevel</a>(Var var, int level)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#aae4dc01729a30c592f939d7d922f5774">setLevel</a>(Lit lit, int level)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a07e86f7cb7f6a34c4e28df990cbf43d1">setPushID</a>(Var var, Clause *from)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#abe63b049c7c54b810266baffb315c89b">simplifyClause</a>(std::vector< Lit > &literals, int clausePushID) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a4e6b8a057747d66f650e6e785f8fc334">simplifyDB</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ae192cadcb9b0cace709e816612b42f02">Solver</a>(SAT::DPLLT::TheoryAPI *theoryAPI, SAT::DPLLT::Decider *decider, bool logDerivation)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ac4949ee43735e3de2869ff606ccc197c">toString</a>(Lit literal, bool showAssignment) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a1fb9f09c66fb11ee96a0761ee2869511">toString</a>(const std::vector< Lit > &clause, bool showAssignment) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ad18f5b06217e20ca14269eb41264be1f">toString</a>(const Clause &clause, bool showAssignment) const </td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#abe256fba9eac8bb202c8c58c87b1bb82">updateConflict</a>(Clause *clause)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#ab4af8739e981ec3caaa5a20ef1eb2f0f">varBumpActivity</a>(Lit p)</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a91d54211b76e271e6838b57fca9ecfad">varDecayActivity</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">protected</span></td></tr>
<tr class="even"><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#a711410b67cec21e4fc1480ea6490f4f2">varRescaleActivity</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"><span class="mlabel">protected</span></td></tr>
<tr><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html#aba52d3c92fafceb6fe39f937f2d73db3">~Solver</a>()</td><td class="entry"><a class="el" href="classMiniSat_1_1Solver.html">MiniSat::Solver</a></td><td class="entry"></td></tr>
</table></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:20 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>
