<!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"/>
<title>CVC3: MiniSat::Solver Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<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="hierarchy.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>
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pub-static-methods">Static Public Member Functions</a> |
<a href="#pro-methods">Protected Member Functions</a> |
<a href="#pro-attribs">Protected Attributes</a> |
<a href="#pro-static-attribs">Static Protected Attributes</a> </div>
<div class="headertitle">
<div class="title">MiniSat::Solver Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="MiniSat::Solver" -->
<p><code>#include <<a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>></code></p>
<p><a href="classMiniSat_1_1Solver-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="classMiniSat_1_1Solver.html#ae192cadcb9b0cace709e816612b42f02">Solver</a> (<a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html">SAT::DPLLT::TheoryAPI</a> *theoryAPI, <a class="el" href="classSAT_1_1DPLLT_1_1Decider.html">SAT::DPLLT::Decider</a> *decider, bool logDerivation)
<dl class="el"><dd class="mdescRight">Initialization. <a href="#ae192cadcb9b0cace709e816612b42f02"></a><br/></dl><li><a class="el" href="classMiniSat_1_1Solver.html#aba52d3c92fafceb6fe39f937f2d73db3">~Solver</a> ()
<li><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * <a class="el" href="classMiniSat_1_1Solver.html#abbb1190222cc3ad99638caf6e86ee698">cvcToMiniSat</a> (const <a class="el" href="classSAT_1_1Clause.html">SAT::Clause</a> &clause, int id)
<dl class="el"><dd class="mdescRight">problem specification <a href="#abbb1190222cc3ad99638caf6e86ee698"></a><br/></dl><li>void <a class="el" href="classMiniSat_1_1Solver.html#af3e9229206719e24e2a951be84c33a42">addClause</a> (<a class="el" href="classMiniSat_1_1Lit.html">Lit</a> p, <a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> theorem)
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a03e24ae79c2068ab70b8c9633829777c">addClause</a> (const <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> &clause, bool keepClauseID)
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a27b79e9b52cd9850e3e21cd2e2af9a04">addClause</a> (const <a class="el" href="classSAT_1_1Clause.html">SAT::Clause</a> &clause, bool isTheoryClause)
<li>void <a class="el" href="classMiniSat_1_1Solver.html#ab7ceeed839df517256ce77c126f28e00">addFormula</a> (const <a class="el" href="classSAT_1_1CNF__Formula.html">SAT::CNF_Formula</a> &cnf, bool isTheoryClause)
<li>int <a class="el" href="classMiniSat_1_1Solver.html#a7323aff4aaa93c01e6008e8e033d2b8f">nextClauseID</a> ()
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a4e6b8a057747d66f650e6e785f8fc334">simplifyDB</a> ()
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a62eea2c00917497fbfb843bf9ca4482e">reduceDB</a> ()
<li><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">CVC3::QueryResult</a> <a class="el" href="classMiniSat_1_1Solver.html#af43d31ac67426e7b3b699491b02d62c1">search</a> ()
<dl class="el"><dd class="mdescRight">search <a href="#af43d31ac67426e7b3b699491b02d62c1"></a><br/></dl><li><a class="el" href="classMiniSat_1_1Derivation.html">Derivation</a> * <a class="el" href="classMiniSat_1_1Solver.html#ac051d3f7a6f6e93269769f2ff8eb9878">getProof</a> ()
<li>bool <a class="el" href="classMiniSat_1_1Solver.html#ae28b9db22e418c5907fb82dbe49a6832">inSearch</a> () const
<li>bool <a class="el" href="classMiniSat_1_1Solver.html#a7eb95fc222427a795a3b5ae48e94518e">isConsistent</a> () const
<li>void <a class="el" href="classMiniSat_1_1Solver.html#aec12c38c0c17d7067e12da239353ebc8">push</a> ()
<dl class="el"><dd class="mdescRight">Push / Pop. <a href="#aec12c38c0c17d7067e12da239353ebc8"></a><br/></dl><li>void <a class="el" href="classMiniSat_1_1Solver.html#a80f70ef105eabcf61758427d041281d6">popTheories</a> ()
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a8be8edbecd5a07bd39990ee7ba0918e3">requestPop</a> ()
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a8cc5207e3580ab0f09c6e9c225eaebff">doPops</a> ()
<li>bool <a class="el" href="classMiniSat_1_1Solver.html#a1bcf27269a8286f82b3235d982e4724e">inPush</a> () const
<li><a class="el" href="classMiniSat_1_1lbool.html">lbool</a> <a class="el" href="classMiniSat_1_1Solver.html#adc9d01899ff6c1eefea8749a1a97309b">getValue</a> (<a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> x) const
<dl class="el"><dd class="mdescRight">clauses / assignment <a href="#adc9d01899ff6c1eefea8749a1a97309b"></a><br/></dl><li><a class="el" href="classMiniSat_1_1lbool.html">lbool</a> <a class="el" href="classMiniSat_1_1Solver.html#a2c6d2ce4210d3bfbc3d659dd724d02f0">getValue</a> (<a class="el" href="classMiniSat_1_1Lit.html">Lit</a> p) const
<li>int <a class="el" href="classMiniSat_1_1Solver.html#a68a7d96223af2e9b67d8b25d047284e4">getLevel</a> (<a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> var) const
<li>int <a class="el" href="classMiniSat_1_1Solver.html#a70b4f991bd7a679be32a89aa1d22eb8d">getLevel</a> (<a class="el" href="classMiniSat_1_1Lit.html">Lit</a> lit) const
<li>void <a class="el" href="classMiniSat_1_1Solver.html#adf6fbd3cddfa511acae41f180b187454">setLevel</a> (<a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> var, int level)
<li>void <a class="el" href="classMiniSat_1_1Solver.html#aae4dc01729a30c592f939d7d922f5774">setLevel</a> (<a class="el" href="classMiniSat_1_1Lit.html">Lit</a> lit, int level)
<li>bool <a class="el" href="classMiniSat_1_1Solver.html#a344d9206f065425f276b408e86b7e1d3">isReason</a> (const <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> *c) const
<li><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * <a class="el" href="classMiniSat_1_1Solver.html#a8660c6ceafa236f5533e432bb859aeba">getReason</a> (<a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> var) const
<li><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * <a class="el" href="classMiniSat_1_1Solver.html#a031fbfd0b0f291ad294dc9e49a8e7ec7">getReason</a> (<a class="el" href="classMiniSat_1_1Lit.html">Lit</a> literal, bool resolveTheoryImplication=true)
<li>const std::vector< <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * > & <a class="el" href="classMiniSat_1_1Solver.html#a70a7ffd14675ce9d3f1d445a79505278">getClauses</a> () const
<li>const std::vector< <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * > & <a class="el" href="classMiniSat_1_1Solver.html#aadbf5bfce16879745ac1fc7e5226957c">getLemmas</a> () const
<li>const std::vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > & <a class="el" href="classMiniSat_1_1Solver.html#a16a71aec47f38eed46547c52ca9b152b">getTrail</a> () const
<li><a class="el" href="classMiniSat_1_1Derivation.html">Derivation</a> * <a class="el" href="classMiniSat_1_1Solver.html#a82e89493435ed86eb83f6af47fc78379">getDerivation</a> ()
<li>const <a class="el" href="structMiniSat_1_1SolverStats.html">SolverStats</a> & <a class="el" href="classMiniSat_1_1Solver.html#ac386ec8bbd27857254bae149db775412">getStats</a> () const
<dl class="el"><dd class="mdescRight">Statistics. <a href="#ac386ec8bbd27857254bae149db775412"></a><br/></dl><li>int <a class="el" href="classMiniSat_1_1Solver.html#af2bc4c7b90705664cf10982944640b3f">nAssigns</a> () const
<li>int <a class="el" href="classMiniSat_1_1Solver.html#af57851d84d9e00837b1b09106bf5db27">nClauses</a> () const
<li>int <a class="el" href="classMiniSat_1_1Solver.html#a2beb4ee59904cb55b5b3e69886a0701c">nLearnts</a> () const
<li>int <a class="el" href="classMiniSat_1_1Solver.html#a679fa13af0d75beca98981dc40f3f2a2">nVars</a> () const
<li>std::string <a class="el" href="classMiniSat_1_1Solver.html#ac4949ee43735e3de2869ff606ccc197c">toString</a> (<a class="el" href="classMiniSat_1_1Lit.html">Lit</a> literal, bool showAssignment) const
<dl class="el"><dd class="mdescRight">String representation: <a href="#ac4949ee43735e3de2869ff606ccc197c"></a><br/></dl><li>std::string <a class="el" href="classMiniSat_1_1Solver.html#a1fb9f09c66fb11ee96a0761ee2869511">toString</a> (const std::vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > &clause, bool showAssignment) const
<li>std::string <a class="el" href="classMiniSat_1_1Solver.html#ad18f5b06217e20ca14269eb41264be1f">toString</a> (const <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> &clause, bool showAssignment) const
<li>void <a class="el" href="classMiniSat_1_1Solver.html#af8254dba6facc2d13c85202d9d09b3f9">printState</a> () const
<li>void <a class="el" href="classMiniSat_1_1Solver.html#ac3d7b1cc4327878d22b91d105ea32409">printDIMACS</a> () const
<li>std::vector< <a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> > <a class="el" href="classMiniSat_1_1Solver.html#aac50fbefa27ff761747fe0873722f927">curAssigns</a> ()
<li>std::vector< std::vector<br class="typebreak"/>
< <a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> > > <a class="el" href="classMiniSat_1_1Solver.html#afb1410338334a3220d95ec28e5a68f71">curClauses</a> ()
</ul>
<h2><a name="pub-static-methods"></a>
Static Public Member Functions</h2>
<ul>
<li>static <a class="el" href="classMiniSat_1_1Solver.html">Solver</a> * <a class="el" href="classMiniSat_1_1Solver.html#a7fce9c6a705405959f91d559a6e06ee4">createFrom</a> (const <a class="el" href="classMiniSat_1_1Solver.html">Solver</a> *solver)
</ul>
<h2><a name="pro-methods"></a>
Protected Member Functions</h2>
<ul>
<li>int <a class="el" href="classMiniSat_1_1Solver.html#a18c18c858ec2b635eede59e396f3b102">decisionLevel</a> () const
<dl class="el"><dd class="mdescRight">Search: <a href="#a18c18c858ec2b635eede59e396f3b102"></a><br/></dl><li>bool <a class="el" href="classMiniSat_1_1Solver.html#a48e255f2f05f6d56518c8e8925b30639">assume</a> (<a class="el" href="classMiniSat_1_1Lit.html">Lit</a> p)
<li>bool <a class="el" href="classMiniSat_1_1Solver.html#a7884b17f0f740781df424864717efac2">enqueue</a> (<a class="el" href="classMiniSat_1_1Lit.html">Lit</a> fact, int decisionLevel, <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> *reason)
<li>void <a class="el" href="classMiniSat_1_1Solver.html#aace9125740233af99f0de4e0288b075e">propagate</a> ()
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a5ff984eddca26831d3057733f3848fdf">propLookahead</a> (const <a class="el" href="structMiniSat_1_1SearchParams.html">SearchParams</a> &params)
<li><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * <a class="el" href="classMiniSat_1_1Solver.html#ab4bacf381f8980c23eb2184c712b882d">analyze</a> (int &out_btlevel)
<dl class="el"><dd class="mdescRight">Conflict handling. <a href="#ab4bacf381f8980c23eb2184c712b882d"></a><br/></dl><li>void <a class="el" href="classMiniSat_1_1Solver.html#affb21521fe39f5d003e61180dc3f5f3c">analyze_minimize</a> (std::vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > &out_learnt, <a class="el" href="classMiniSat_1_1Inference.html">Inference</a> *inference, int &pushID)
<li>bool <a class="el" href="classMiniSat_1_1Solver.html#ab91573c3ebb667e9e94f30f889598434">analyze_removable</a> (<a class="el" href="classMiniSat_1_1Lit.html">Lit</a> p, unsigned int min_level, int pushID)
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a49421463a8047553ffbd5fc9d04c0ad8">backtrack</a> (int level, <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> *clause)
<li>bool <a class="el" href="classMiniSat_1_1Solver.html#a41ac244ff15b83ca4a863ee85cf27814">isConflicting</a> () const
<li>void <a class="el" href="classMiniSat_1_1Solver.html#abe256fba9eac8bb202c8c58c87b1bb82">updateConflict</a> (<a class="el" href="classMiniSat_1_1Clause.html">Clause</a> *clause)
<li>int <a class="el" href="classMiniSat_1_1Solver.html#a4d5144ec81209e86f7374972b8a78aa0">getImplicationLevel</a> (const <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> &clause) const
<li>int <a class="el" href="classMiniSat_1_1Solver.html#a0d0c1aef5c834bc7ba7682ac3fe5b59c">getConflictLevel</a> (const <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> &clause) const
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a22b59f22e9df28fcb892e5873d998c75">resolveTheoryImplication</a> (<a class="el" href="classMiniSat_1_1Lit.html">Lit</a> literal)
<li>std::vector< <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * > & <a class="el" href="classMiniSat_1_1Solver.html#ac8d866ffb2253fdc01fe310558871da3">getWatches</a> (<a class="el" href="classMiniSat_1_1Lit.html">Lit</a> literal)
<dl class="el"><dd class="mdescRight">unit propagation <a href="#ac8d866ffb2253fdc01fe310558871da3"></a><br/></dl><li>const std::vector< <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * > & <a class="el" href="classMiniSat_1_1Solver.html#a8987b0395fc1f850ee7b748e9685560a">getWatches</a> (<a class="el" href="classMiniSat_1_1Lit.html">Lit</a> literal) const
<li>void <a class="el" href="classMiniSat_1_1Solver.html#af3891961fe824bc91b47b59ee1e4a90b">addWatch</a> (<a class="el" href="classMiniSat_1_1Lit.html">Lit</a> literal, <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> *clause)
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a94c3f4932f4c9d17b4a6dc1839c813f5">removeWatch</a> (std::vector< <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * > &ws, <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> *elem)
<dl class="el"><dd class="mdescRight">Conflict handling. <a href="#a94c3f4932f4c9d17b4a6dc1839c813f5"></a><br/></dl><li>void <a class="el" href="classMiniSat_1_1Solver.html#a7a11f6c3676dd169d093a4e7c5af5299">registerVar</a> (<a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> var)
<dl class="el"><dd class="mdescRight">Operations on clauses: <a href="#a7a11f6c3676dd169d093a4e7c5af5299"></a><br/></dl><li>bool <a class="el" href="classMiniSat_1_1Solver.html#a31a0f344abc3fd65ee540f954b014f62">isRegistered</a> (<a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> var)
<dl class="el"><dd class="mdescRight">Operations on clauses: <a href="#a31a0f344abc3fd65ee540f954b014f62"></a><br/></dl><li>void <a class="el" href="classMiniSat_1_1Solver.html#a36711ef6cb28057fa6f00235f58c03ff">addClause</a> (std::vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > &literals, <a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> theorem, int clauseID)
<li>void <a class="el" href="classMiniSat_1_1Solver.html#aa0d36a2c07c88350dd9d54e62b3cef7b">insertClause</a> (<a class="el" href="classMiniSat_1_1Clause.html">Clause</a> *clause)
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a2ba80609ff72dbd93ae116a25923808d">insertLemma</a> (const <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> *lemma, int clauseID, int pushID)
<li>bool <a class="el" href="classMiniSat_1_1Solver.html#abe63b049c7c54b810266baffb315c89b">simplifyClause</a> (std::vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > &literals, int clausePushID) const
<li>void <a class="el" href="classMiniSat_1_1Solver.html#aa8b5dfa883cace427d4b8b89769ca6df">orderClause</a> (std::vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > &literals) const
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a241e960f84c150b1421bf4e3b3a6b073">remove</a> (<a class="el" href="classMiniSat_1_1Clause.html">Clause</a> *c, bool just_dealloc=false)
<li>bool <a class="el" href="classMiniSat_1_1Solver.html#a871c1c054262f9673518c46f7efc8450">isImpliedAt</a> (<a class="el" href="classMiniSat_1_1Lit.html">Lit</a> lit, int clausePushID) const
<li>bool <a class="el" href="classMiniSat_1_1Solver.html#ad64d6215811b4c4ca6c5ac86da4c787d">isPermSatisfied</a> (<a class="el" href="classMiniSat_1_1Clause.html">Clause</a> *c) const
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a07e86f7cb7f6a34c4e28df990cbf43d1">setPushID</a> (<a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> var, <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> *from)
<li>int <a class="el" href="classMiniSat_1_1Solver.html#a4f5805d21238ad316845059fb378a05f">getPushID</a> (<a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> var) const
<li>int <a class="el" href="classMiniSat_1_1Solver.html#aa095aa10adf85a246b525e0bc717e942">getPushID</a> (<a class="el" href="classMiniSat_1_1Lit.html">Lit</a> lit) const
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a2f75013fed205f5b38cd23b9d87dcd1a">pop</a> ()
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a6662641d5c0dea8d89041f5cf9dbc4af">popClauses</a> (const <a class="el" href="structMiniSat_1_1PushEntry.html">PushEntry</a> &pushEntry, std::vector< <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * > &clauses)
<li>void <a class="el" href="classMiniSat_1_1Solver.html#ab4af8739e981ec3caaa5a20ef1eb2f0f">varBumpActivity</a> (<a class="el" href="classMiniSat_1_1Lit.html">Lit</a> p)
<dl class="el"><dd class="mdescRight">Activity: <a href="#ab4af8739e981ec3caaa5a20ef1eb2f0f"></a><br/></dl><li>void <a class="el" href="classMiniSat_1_1Solver.html#a91d54211b76e271e6838b57fca9ecfad">varDecayActivity</a> ()
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a711410b67cec21e4fc1480ea6490f4f2">varRescaleActivity</a> ()
<dl class="el"><dd class="mdescRight">Activity. <a href="#a711410b67cec21e4fc1480ea6490f4f2"></a><br/></dl><li>void <a class="el" href="classMiniSat_1_1Solver.html#a3e6ce9dc49e278926bfcc32289a343c1">claDecayActivity</a> ()
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a3cdc4675e024f72e82d718596159456d">claRescaleActivity</a> ()
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a4154a7c87f54bcbf48e8e1689dae68a9">claBumpActivity</a> (<a class="el" href="classMiniSat_1_1Clause.html">Clause</a> *c)
<li>bool <a class="el" href="classMiniSat_1_1Solver.html#a4d58130f36a501e919bb82f5f1438e32">allClausesSatisfied</a> ()
<dl class="el"><dd class="mdescRight">debugging <a href="#a4d58130f36a501e919bb82f5f1438e32"></a><br/></dl><li>void <a class="el" href="classMiniSat_1_1Solver.html#a09e6b3c658982dbaeec9a18d440dbe7a">checkWatched</a> (const <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> &clause) const
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a6b4bb1db7b767e1368884b178f523dcf">checkWatched</a> () const
<li>void <a class="el" href="classMiniSat_1_1Solver.html#ad4c405a5b6aac64b41c190aaa68004aa">checkClause</a> (const <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> &clause) const
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a9e152e0ed1d83a51f7886df8cd5fe681">checkClauses</a> () const
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a9457fd91045b9496ef5bdcd1a93fcae5">checkTrail</a> () const
<li>void <a class="el" href="classMiniSat_1_1Solver.html#a776adc363c0056e2077fbe659ae6f709">protocolPropagation</a> () const
</ul>
<h2><a name="pro-attribs"></a>
Protected Attributes</h2>
<ul>
<li>bool <a class="el" href="classMiniSat_1_1Solver.html#a53dec8ba9fc22afeeef701f1a329a669">d_inSearch</a>
<dl class="el"><dd class="mdescRight">status <a href="#a53dec8ba9fc22afeeef701f1a329a669"></a><br/></dl><li>bool <a class="el" href="classMiniSat_1_1Solver.html#a813826a370752a20165602e79b18f7c6">d_ok</a>
<li><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * <a class="el" href="classMiniSat_1_1Solver.html#a431f60a202eee24b3928ca6c6195baa5">d_conflict</a>
<li>std::vector< std::vector<br class="typebreak"/>
< <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * > > <a class="el" href="classMiniSat_1_1Solver.html#a6a3e831d47c15ac42fe7a7002c276c0e">d_watches</a>
<dl class="el"><dd class="mdescRight">variable assignments, and pending propagations <a href="#a6a3e831d47c15ac42fe7a7002c276c0e"></a><br/></dl><li>std::vector< signed char > <a class="el" href="classMiniSat_1_1Solver.html#a8fd906b3d57929f47f9a6eb6740e35e9">d_assigns</a>
<li>std::vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > <a class="el" href="classMiniSat_1_1Solver.html#af092e4552ff6a34e5fcb5f67de96c845">d_trail</a>
<li>std::vector< int > <a class="el" href="classMiniSat_1_1Solver.html#abf42fb28430f7b099c65c4e9b28ffb09">d_trail_lim</a>
<li>std::vector< <a class="el" href="namespaceMiniSat.html#ad579041894c169fecdeb319f9aa5948d">size_type</a> > <a class="el" href="classMiniSat_1_1Solver.html#a31a1d57eabc2169a4a9fc1cf4c87a2a7">d_trail_pos</a>
<li><a class="el" href="namespaceMiniSat.html#ad579041894c169fecdeb319f9aa5948d">size_type</a> <a class="el" href="classMiniSat_1_1Solver.html#a22427732a96158ab53c2ffc61714fca4">d_qhead</a>
<li><a class="el" href="namespaceMiniSat.html#ad579041894c169fecdeb319f9aa5948d">size_type</a> <a class="el" href="classMiniSat_1_1Solver.html#ad9d115b0ec2a84ce5ab3f1de19683f06">d_thead</a>
<li>std::vector< <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * > <a class="el" href="classMiniSat_1_1Solver.html#a4405fbaba3ed712f704d5c85a390b558">d_reason</a>
<li>std::vector< int > <a class="el" href="classMiniSat_1_1Solver.html#a34c9afcb69ae37cebbf43a61505009b3">d_level</a>
<li>std::vector< <a class="el" href="classHash_1_1hash__set.html">Hash::hash_set</a><br class="typebreak"/>
< <a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> > > <a class="el" href="classMiniSat_1_1Solver.html#afc17e3fc6c5eb525504acbe000d9c5ca">d_registeredVars</a>
<li>int <a class="el" href="classMiniSat_1_1Solver.html#ad6e3d6a97a4ae9dda9ac7b9bed97bed8">d_clauseIDCounter</a>
<dl class="el"><dd class="mdescRight">Clauses. <a href="#ad6e3d6a97a4ae9dda9ac7b9bed97bed8"></a><br/></dl><li>std::vector< <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * > <a class="el" href="classMiniSat_1_1Solver.html#ae4d0195d229b334f9d9c2f3122e41bd1">d_clauses</a>
<li>std::vector< <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * > <a class="el" href="classMiniSat_1_1Solver.html#a0c9270be1c0980e631de98b3408a8031">d_learnts</a>
<li>std::queue< <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * > <a class="el" href="classMiniSat_1_1Solver.html#adbae4eb042f37351c6cac493e6743813">d_pendingClauses</a>
<dl class="el"><dd class="mdescRight">Temporary clauses. <a href="#adbae4eb042f37351c6cac493e6743813"></a><br/></dl><li>std::stack< std::pair< int, <br class="typebreak"/>
<a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * > > <a class="el" href="classMiniSat_1_1Solver.html#a587104e3c6bb31d2bc7942bc1fde8b1e">d_theoryExplanations</a>
<li>std::vector< <a class="el" href="structMiniSat_1_1PushEntry.html">PushEntry</a> > <a class="el" href="classMiniSat_1_1Solver.html#a6f9c67d77e57b99fef5de801623245a4">d_pushes</a>
<dl class="el"><dd class="mdescRight">Push / Pop. <a href="#a6f9c67d77e57b99fef5de801623245a4"></a><br/></dl><li>std::vector< <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * > <a class="el" href="classMiniSat_1_1Solver.html#a99b8d67e03c83f148906ff00e8e88851">d_popLemmas</a>
<li>std::vector< int > <a class="el" href="classMiniSat_1_1Solver.html#ab0b2d4e87d57046e30c2cb3554925e2b">d_pushIDs</a>
<li>unsigned int <a class="el" href="classMiniSat_1_1Solver.html#acb6671d85d64f00c04ea17b3b6e144f6">d_popRequests</a>
<li>double <a class="el" href="classMiniSat_1_1Solver.html#a5b10958ebb6b146f8cfb2d6ec08ab667">d_cla_inc</a>
<dl class="el"><dd class="mdescRight">heuristics <a href="#a5b10958ebb6b146f8cfb2d6ec08ab667"></a><br/></dl><li>double <a class="el" href="classMiniSat_1_1Solver.html#a3b0e8d36281ddcfefb54812accad5a55">d_cla_decay</a>
<li>std::vector< double > <a class="el" href="classMiniSat_1_1Solver.html#a0765ad8a98718bb5523e487e32d66ae1">d_activity</a>
<li>double <a class="el" href="classMiniSat_1_1Solver.html#aa9cba0f1df8f31b5ae94f2ce0ccb290f">d_var_inc</a>
<li>double <a class="el" href="classMiniSat_1_1Solver.html#a354cacc000d52901cb2a60d1fe659d26">d_var_decay</a>
<li><a class="el" href="classMiniSat_1_1VarOrder.html">VarOrder</a> <a class="el" href="classMiniSat_1_1Solver.html#aab79cd4bf5792f72c191d8149e77bc93">d_order</a>
<li>int <a class="el" href="classMiniSat_1_1Solver.html#ac114e23a9bd1329c9002eb758c1595b7">d_simpDB_assigns</a>
<li>int64_t <a class="el" href="classMiniSat_1_1Solver.html#a4f2b0a42acb3d470ca9500b2f4fd8077">d_simpDB_props</a>
<li>int <a class="el" href="classMiniSat_1_1Solver.html#ac380f5046f3dddbb0bdebf4107d8d506">d_simpRD_learnts</a>
<li><a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html">SAT::DPLLT::TheoryAPI</a> * <a class="el" href="classMiniSat_1_1Solver.html#a8336c93fe51668a8cd322f9a059d5137">d_theoryAPI</a>
<dl class="el"><dd class="mdescRight">CVC interface. <a href="#a8336c93fe51668a8cd322f9a059d5137"></a><br/></dl><li><a class="el" href="classSAT_1_1DPLLT_1_1Decider.html">SAT::DPLLT::Decider</a> * <a class="el" href="classMiniSat_1_1Solver.html#a18b5a09a43e43ae4bde40537e652e987">d_decider</a>
<li><a class="el" href="classMiniSat_1_1Derivation.html">Derivation</a> * <a class="el" href="classMiniSat_1_1Solver.html#ad2d7fa92335dfd68f8598a5a41d17e93">d_derivation</a>
<dl class="el"><dd class="mdescRight">proof logging <a href="#ad2d7fa92335dfd68f8598a5a41d17e93"></a><br/></dl><li><a class="el" href="structMiniSat_1_1SearchParams.html">SearchParams</a> <a class="el" href="classMiniSat_1_1Solver.html#aece892bd1701b50038331c77b70d0949">d_default_params</a>
<dl class="el"><dd class="mdescRight">Mode of operation: <a href="#aece892bd1701b50038331c77b70d0949"></a><br/></dl><li>bool <a class="el" href="classMiniSat_1_1Solver.html#a4ecef2c87d4be7bf5a0ba8b4e800e09c">d_expensive_ccmin</a>
<li>std::vector< char > <a class="el" href="classMiniSat_1_1Solver.html#ae2fd56e35cc318aed56d10fc7e5af484">d_analyze_seen</a>
<dl class="el"><dd class="mdescRight">Temporaries (to reduce allocation overhead). <a href="#ae2fd56e35cc318aed56d10fc7e5af484"></a><br/></dl><li>std::vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > <a class="el" href="classMiniSat_1_1Solver.html#aede680f26ad5344891484b6f821de222">d_analyze_stack</a>
<li>std::vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > <a class="el" href="classMiniSat_1_1Solver.html#a81ed0225fec06bae415c6d86c86781f1">d_analyze_redundant</a>
<li><a class="el" href="structMiniSat_1_1SolverStats.html">SolverStats</a> <a class="el" href="classMiniSat_1_1Solver.html#ac2c0d8b62a85616add0930b4947c8f96">d_stats</a>
</ul>
<h2><a name="pro-static-attribs"></a>
Static Protected Attributes</h2>
<ul>
<li>static const int <a class="el" href="classMiniSat_1_1Solver.html#a160ccfc80ff29cd6947b0d009400e434">d_rootLevel</a> = 0
<dl class="el"><dd class="mdescRight">variables <a href="#a160ccfc80ff29cd6947b0d009400e434"></a><br/></dl></ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00200">200</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="ae192cadcb9b0cace709e816612b42f02"></a><!-- doxytag: member="MiniSat::Solver::Solver" ref="ae192cadcb9b0cace709e816612b42f02" args="(SAT::DPLLT::TheoryAPI *theoryAPI, SAT::DPLLT::Decider *decider, bool logDerivation)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">Solver::Solver </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html">SAT::DPLLT::TheoryAPI</a> * </td>
<td class="paramname"><em>theoryAPI</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classSAT_1_1DPLLT_1_1Decider.html">SAT::DPLLT::Decider</a> * </td>
<td class="paramname"><em>decider</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>logDerivation</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Initialization. </p>
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00158">158</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00397">d_derivation</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00248">createFrom()</a>.</p>
</div>
</div>
<a class="anchor" id="aba52d3c92fafceb6fe39f937f2d73db3"></a><!-- doxytag: member="MiniSat::Solver::~Solver" ref="aba52d3c92fafceb6fe39f937f2d73db3" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">Solver::~Solver </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00292">292</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00303">d_clauses</a>, <a class="el" href="minisat__solver_8h_source.html#l00397">d_derivation</a>, <a class="el" href="minisat__solver_8h_source.html#l00306">d_learnts</a>, <a class="el" href="minisat__solver_8h_source.html#l00314">d_pendingClauses</a>, <a class="el" href="minisat__solver_8h_source.html#l00319">d_theoryExplanations</a>, and <a class="el" href="minisat__global_8h_source.html#l00080">MiniSat::xfree()</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="a18c18c858ec2b635eede59e396f3b102"></a><!-- doxytag: member="MiniSat::Solver::decisionLevel" ref="a18c18c858ec2b635eede59e396f3b102" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int MiniSat::Solver::decisionLevel </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline, protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Search: </p>
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00424">424</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00260">d_trail_lim</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01473">assume()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01481">backtrack()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00935">getConflictLevel()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00910">getImplicationLevel()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02641">popTheories()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01950">propLookahead()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01937">protocolPropagation()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a48e255f2f05f6d56518c8e8925b30639"></a><!-- doxytag: member="MiniSat::Solver::assume" ref="a48e255f2f05f6d56518c8e8925b30639" args="(Lit p)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Solver::assume </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>p</em></td><td>)</td>
<td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l01473">1473</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00417">d_stats</a>, <a class="el" href="minisat__solver_8h_source.html#l00256">d_trail</a>, <a class="el" href="minisat__solver_8h_source.html#l00260">d_trail_lim</a>, <a class="el" href="minisat__types_8cpp_source.html#l00054">MiniSat::Clause::Decision()</a>, <a class="el" href="minisat__solver_8h_source.html#l00424">decisionLevel()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01575">enqueue()</a>, <a class="el" href="minisat__global_8h_source.html#l00059">MiniSat::max()</a>, and <a class="el" href="minisat__solver_8h_source.html#l00163">MiniSat::SolverStats::max_level</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01950">propLookahead()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a7884b17f0f740781df424864717efac2"></a><!-- doxytag: member="MiniSat::Solver::enqueue" ref="a7884b17f0f740781df424864717efac2" args="(Lit fact, int decisionLevel, Clause *reason)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Solver::enqueue </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>fact</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>decisionLevel</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * </td>
<td class="paramname"><em>reason</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l01575">1575</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00251">d_assigns</a>, <a class="el" href="minisat__solver_8h_source.html#l00397">d_derivation</a>, <a class="el" href="minisat__solver_8h_source.html#l00278">d_reason</a>, <a class="el" href="minisat__solver_8h_source.html#l00256">d_trail</a>, <a class="el" href="minisat__solver_8h_source.html#l00264">d_trail_pos</a>, <a class="el" href="minisat__solver_8h_source.html#l00699">getValue()</a>, <a class="el" href="minisat__global_8h_source.html#l00215">MiniSat::l_False</a>, <a class="el" href="minisat__global_8h_source.html#l00216">MiniSat::l_Undef</a>, <a class="el" href="minisat__solver_8h_source.html#l00707">setLevel()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02496">setPushID()</a>, <a class="el" href="minisat__types_8h_source.html#l00068">MiniSat::Lit::sign()</a>, <a class="el" href="minisat__global_8h_source.html#l00211">MiniSat::toInt()</a>, and <a class="el" href="minisat__types_8h_source.html#l00069">MiniSat::Lit::var()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01473">assume()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00750">insertClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00190">insertLemma()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01689">propagate()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="aace9125740233af99f0de4e0288b075e"></a><!-- doxytag: member="MiniSat::Solver::propagate" ref="aace9125740233af99f0de4e0288b075e" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::propagate </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l01689">1689</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00485">addWatch()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a3b3ef70567e0298cd3e971fd57d26fa6">SAT::DPLLT::TheoryAPI::assertLit()</a>, <a class="el" href="minisat__solver_8h_source.html#l00269">d_qhead</a>, <a class="el" href="minisat__solver_8h_source.html#l00205">d_rootLevel</a>, <a class="el" href="minisat__solver_8h_source.html#l00378">d_simpDB_assigns</a>, <a class="el" href="minisat__solver_8h_source.html#l00380">d_simpDB_props</a>, <a class="el" href="minisat__solver_8h_source.html#l00417">d_stats</a>, <a class="el" href="minisat__solver_8h_source.html#l00273">d_thead</a>, <a class="el" href="minisat__solver_8h_source.html#l00388">d_theoryAPI</a>, <a class="el" href="minisat__solver_8h_source.html#l00256">d_trail</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00063">defer_theory_propagation</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01575">enqueue()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00910">getImplicationLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00703">getLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00699">getValue()</a>, <a class="el" href="minisat__solver_8h_source.html#l00478">getWatches()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="minisat__global_8h_source.html#l00215">MiniSat::l_False</a>, <a class="el" href="minisat__global_8h_source.html#l00214">MiniSat::l_True</a>, <a class="el" href="minisat__solver_8h_source.html#l00132">MiniSat::miniSatToCVC()</a>, <a class="el" href="minisat__solver_8h_source.html#l00163">MiniSat::SolverStats::propagations</a>, <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00977">updateConflict()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01950">propLookahead()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a5ff984eddca26831d3057733f3848fdf"></a><!-- doxytag: member="MiniSat::Solver::propLookahead" ref="a5ff984eddca26831d3057733f3848fdf" args="(const SearchParams &params)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::propLookahead </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="structMiniSat_1_1SearchParams.html">SearchParams</a> & </td>
<td class="paramname"><em>params</em></td><td>)</td>
<td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l01950">1950</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8cpp_source.html#l01473">assume()</a>, <a class="el" href="minisat__solver_8h_source.html#l00251">d_assigns</a>, <a class="el" href="minisat__solver_8h_source.html#l00373">d_order</a>, <a class="el" href="minisat__solver_8h_source.html#l00269">d_qhead</a>, <a class="el" href="minisat__solver_8h_source.html#l00278">d_reason</a>, <a class="el" href="minisat__solver_8h_source.html#l00256">d_trail</a>, <a class="el" href="minisat__solver_8h_source.html#l00260">d_trail_lim</a>, <a class="el" href="minisat__solver_8h_source.html#l00424">decisionLevel()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00973">isConflicting()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00448">isRegistered()</a>, <a class="el" href="minisat__global_8h_source.html#l00216">MiniSat::l_Undef</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00101">prop_lookahead</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01689">propagate()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01937">protocolPropagation()</a>, <a class="el" href="minisat__solver_8h_source.html#l00194">MiniSat::SearchParams::random_var_freq</a>, <a class="el" href="minisat__varorder_8h_source.html#l00104">MiniSat::VarOrder::select()</a>, <a class="el" href="minisat__global_8h_source.html#l00211">MiniSat::toInt()</a>, <a class="el" href="minisat__varorder_8h_source.html#l00097">MiniSat::VarOrder::undo()</a>, and <a class="el" href="minisat__types_8h_source.html#l00056">MiniSat::var_Undef</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="ab4bacf381f8980c23eb2184c712b882d"></a><!-- doxytag: member="MiniSat::Solver::analyze" ref="ab4bacf381f8980c23eb2184c712b882d" args="(int &out_btlevel)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * Solver::analyze </td>
<td>(</td>
<td class="paramtype">int & </td>
<td class="paramname"><em>out_btlevel</em></td><td>)</td>
<td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Conflict handling. </p>
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l01091">1091</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__derivation_8h_source.html#l00058">MiniSat::Inference::add()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01278">analyze_minimize()</a>, <a class="el" href="minisat__solver_8h_source.html#l00558">claBumpActivity()</a>, <a class="el" href="minisat__solver_8h_source.html#l00414">d_analyze_redundant</a>, <a class="el" href="minisat__solver_8h_source.html#l00412">d_analyze_seen</a>, <a class="el" href="minisat__solver_8h_source.html#l00241">d_conflict</a>, <a class="el" href="minisat__solver_8h_source.html#l00205">d_rootLevel</a>, <a class="el" href="minisat__solver_8h_source.html#l00256">d_trail</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="minisat__types_8cpp_source.html#l00054">MiniSat::Clause::Decision()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00935">getConflictLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00731">getDerivation()</a>, <a class="el" href="minisat__solver_8h_source.html#l00703">getLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00715">getReason()</a>, <a class="el" href="minisat__solver_8h_source.html#l00699">getValue()</a>, <a class="el" href="minisat__types_8h_source.html#l00138">MiniSat::Clause::id()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="minisat__global_8h_source.html#l00215">MiniSat::l_False</a>, <a class="el" href="minisat__types_8cpp_source.html#l00049">MiniSat::Lemma_new()</a>, <a class="el" href="namespaceMiniSat.html#a120ea2f17b58215d657cd7b005edcd85">MiniSat::lit_Undef()</a>, <a class="el" href="minisat__global_8h_source.html#l00059">MiniSat::max()</a>, <a class="el" href="minisat__solver_8h_source.html#l00636">nextClauseID()</a>, <a class="el" href="minisat__types_8h_source.html#l00143">MiniSat::Clause::pushID()</a>, <a class="el" href="minisat__derivation_8h_source.html#l00168">MiniSat::Derivation::registerInference()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00999">resolveTheoryImplication()</a>, <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>, <a class="el" href="minisat__types_8cpp_source.html#l00063">MiniSat::Clause::TheoryImplication()</a>, <a class="el" href="minisat__types_8h_source.html#l00069">MiniSat::Lit::var()</a>, and <a class="el" href="minisat__solver_8h_source.html#l00550">varBumpActivity()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="affb21521fe39f5d003e61180dc3f5f3c"></a><!-- doxytag: member="MiniSat::Solver::analyze_minimize" ref="affb21521fe39f5d003e61180dc3f5f3c" args="(std::vector< Lit > &out_learnt, Inference *inference, int &pushID)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::analyze_minimize </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > & </td>
<td class="paramname"><em>out_learnt</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Inference.html">Inference</a> * </td>
<td class="paramname"><em>inference</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int & </td>
<td class="paramname"><em>pushID</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l01278">1278</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__derivation_8h_source.html#l00058">MiniSat::Inference::add()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01395">analyze_removable()</a>, <a class="el" href="minisat__solver_8h_source.html#l00414">d_analyze_redundant</a>, <a class="el" href="minisat__solver_8h_source.html#l00412">d_analyze_seen</a>, <a class="el" href="minisat__solver_8h_source.html#l00406">d_expensive_ccmin</a>, <a class="el" href="minisat__solver_8h_source.html#l00325">d_pushes</a>, <a class="el" href="minisat__solver_8h_source.html#l00205">d_rootLevel</a>, <a class="el" href="minisat__solver_8h_source.html#l00264">d_trail_pos</a>, <a class="el" href="minisat__types_8cpp_source.html#l00054">MiniSat::Clause::Decision()</a>, <a class="el" href="minisat__solver_8h_source.html#l00731">getDerivation()</a>, <a class="el" href="minisat__solver_8h_source.html#l00703">getLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00540">getPushID()</a>, <a class="el" href="minisat__solver_8h_source.html#l00715">getReason()</a>, <a class="el" href="minisat__global_8h_source.html#l00059">MiniSat::max()</a>, <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>, and <a class="el" href="minisat__types_8h_source.html#l00069">MiniSat::Lit::var()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01091">analyze()</a>.</p>
</div>
</div>
<a class="anchor" id="ab91573c3ebb667e9e94f30f889598434"></a><!-- doxytag: member="MiniSat::Solver::analyze_removable" ref="ab91573c3ebb667e9e94f30f889598434" args="(Lit p, unsigned int min_level, int pushID)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Solver::analyze_removable </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>p</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">unsigned int </td>
<td class="paramname"><em>min_level</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>pushID</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l01395">1395</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00414">d_analyze_redundant</a>, <a class="el" href="minisat__solver_8h_source.html#l00412">d_analyze_seen</a>, <a class="el" href="minisat__solver_8h_source.html#l00413">d_analyze_stack</a>, <a class="el" href="minisat__solver_8h_source.html#l00205">d_rootLevel</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="minisat__types_8cpp_source.html#l00054">MiniSat::Clause::Decision()</a>, <a class="el" href="minisat__solver_8h_source.html#l00703">getLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00715">getReason()</a>, <a class="el" href="minisat__types_8cpp_source.html#l00063">MiniSat::Clause::TheoryImplication()</a>, and <a class="el" href="minisat__types_8h_source.html#l00069">MiniSat::Lit::var()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01278">analyze_minimize()</a>.</p>
</div>
</div>
<a class="anchor" id="a49421463a8047553ffbd5fc9d04c0ad8"></a><!-- doxytag: member="MiniSat::Solver::backtrack" ref="a49421463a8047553ffbd5fc9d04c0ad8" args="(int level, Clause *clause)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::backtrack </td>
<td>(</td>
<td class="paramtype">int </td>
<td class="paramname"><em>level</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * </td>
<td class="paramname"><em>clause</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l01481">1481</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8cpp_source.html#l00671">addClause()</a>, <a class="el" href="minisat__solver_8h_source.html#l00251">d_assigns</a>, <a class="el" href="minisat__solver_8h_source.html#l00397">d_derivation</a>, <a class="el" href="minisat__solver_8h_source.html#l00373">d_order</a>, <a class="el" href="minisat__solver_8h_source.html#l00314">d_pendingClauses</a>, <a class="el" href="minisat__solver_8h_source.html#l00269">d_qhead</a>, <a class="el" href="minisat__solver_8h_source.html#l00278">d_reason</a>, <a class="el" href="minisat__solver_8h_source.html#l00205">d_rootLevel</a>, <a class="el" href="minisat__solver_8h_source.html#l00273">d_thead</a>, <a class="el" href="minisat__solver_8h_source.html#l00388">d_theoryAPI</a>, <a class="el" href="minisat__solver_8h_source.html#l00319">d_theoryExplanations</a>, <a class="el" href="minisat__solver_8h_source.html#l00256">d_trail</a>, <a class="el" href="minisat__solver_8h_source.html#l00260">d_trail_lim</a>, <a class="el" href="minisat__solver_8h_source.html#l00264">d_trail_pos</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="minisat__solver_8h_source.html#l00424">decisionLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00703">getLevel()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00750">insertClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00973">isConflicting()</a>, <a class="el" href="minisat__global_8h_source.html#l00216">MiniSat::l_Undef</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a51a08aab04c2185513676a316aee14b4">SAT::DPLLT::TheoryAPI::pop()</a>, <a class="el" href="minisat__global_8h_source.html#l00211">MiniSat::toInt()</a>, <a class="el" href="minisat__varorder_8h_source.html#l00097">MiniSat::VarOrder::undo()</a>, and <a class="el" href="minisat__global_8h_source.html#l00080">MiniSat::xfree()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a41ac244ff15b83ca4a863ee85cf27814"></a><!-- doxytag: member="MiniSat::Solver::isConflicting" ref="a41ac244ff15b83ca4a863ee85cf27814" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Solver::isConflicting </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00973">973</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00241">d_conflict</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01481">backtrack()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00248">createFrom()</a>, <a class="el" href="minisat__solver_8h_source.html#l00671">isConsistent()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01950">propLookahead()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l01816">simplifyDB()</a>.</p>
</div>
</div>
<a class="anchor" id="abe256fba9eac8bb202c8c58c87b1bb82"></a><!-- doxytag: member="MiniSat::Solver::updateConflict" ref="abe256fba9eac8bb202c8c58c87b1bb82" args="(Clause *clause)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::updateConflict </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * </td>
<td class="paramname"><em>clause</em></td><td>)</td>
<td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00977">977</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00241">d_conflict</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="minisat__solver_8h_source.html#l00699">getValue()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="minisat__global_8h_source.html#l00215">MiniSat::l_False</a>, and <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00750">insertClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00190">insertLemma()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l01689">propagate()</a>.</p>
</div>
</div>
<a class="anchor" id="a4d5144ec81209e86f7374972b8a78aa0"></a><!-- doxytag: member="MiniSat::Solver::getImplicationLevel" ref="a4d5144ec81209e86f7374972b8a78aa0" args="(const Clause &clause) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int Solver::getImplicationLevel </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> & </td>
<td class="paramname"><em>clause</em></td><td>)</td>
<td> const<code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00910">910</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00205">d_rootLevel</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="minisat__solver_8h_source.html#l00424">decisionLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00703">getLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00699">getValue()</a>, <a class="el" href="minisat__global_8h_source.html#l00215">MiniSat::l_False</a>, and <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00750">insertClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01689">propagate()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00999">resolveTheoryImplication()</a>.</p>
</div>
</div>
<a class="anchor" id="a0d0c1aef5c834bc7ba7682ac3fe5b59c"></a><!-- doxytag: member="MiniSat::Solver::getConflictLevel" ref="a0d0c1aef5c834bc7ba7682ac3fe5b59c" args="(const Clause &clause) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int Solver::getConflictLevel </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> & </td>
<td class="paramname"><em>clause</em></td><td>)</td>
<td> const<code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00935">935</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00205">d_rootLevel</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="minisat__solver_8h_source.html#l00424">decisionLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00703">getLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00699">getValue()</a>, <a class="el" href="minisat__global_8h_source.html#l00215">MiniSat::l_False</a>, and <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01091">analyze()</a>.</p>
</div>
</div>
<a class="anchor" id="a22b59f22e9df28fcb892e5873d998c75"></a><!-- doxytag: member="MiniSat::Solver::resolveTheoryImplication" ref="a22b59f22e9df28fcb892e5873d998c75" args="(Lit literal)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::resolveTheoryImplication </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>literal</em></td><td>)</td>
<td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00999">999</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8cpp_source.html#l00671">addClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00139">cvcToMiniSat()</a>, <a class="el" href="minisat__solver_8h_source.html#l00278">d_reason</a>, <a class="el" href="minisat__solver_8h_source.html#l00319">d_theoryExplanations</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00070">eager_explanation</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00910">getImplicationLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00699">getValue()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00076">keep_lazy_explanation</a>, <a class="el" href="minisat__global_8h_source.html#l00215">MiniSat::l_False</a>, <a class="el" href="minisat__global_8h_source.html#l00214">MiniSat::l_True</a>, <a class="el" href="minisat__solver_8h_source.html#l00636">nextClauseID()</a>, <a class="el" href="minisat__solver_8h_source.html#l00707">setLevel()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02496">setPushID()</a>, <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>, <a class="el" href="minisat__types_8cpp_source.html#l00063">MiniSat::Clause::TheoryImplication()</a>, <a class="el" href="minisat__types_8h_source.html#l00069">MiniSat::Lit::var()</a>, and <a class="el" href="minisat__global_8h_source.html#l00080">MiniSat::xfree()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01091">analyze()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00950">getReason()</a>.</p>
</div>
</div>
<a class="anchor" id="ac8d866ffb2253fdc01fe310558871da3"></a><!-- doxytag: member="MiniSat::Solver::getWatches" ref="ac8d866ffb2253fdc01fe310558871da3" args="(Lit literal)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classMiniSat_1_1Clause.html">Clause</a>*>& MiniSat::Solver::getWatches </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>literal</em></td><td>)</td>
<td><code> [inline, protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>unit propagation </p>
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00478">478</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00248">d_watches</a>, and <a class="el" href="minisat__types_8h_source.html#l00070">MiniSat::Lit::index()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8h_source.html#l00485">addWatch()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02313">allClausesSatisfied()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02359">checkWatched()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01689">propagate()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00869">remove()</a>.</p>
</div>
</div>
<a class="anchor" id="a8987b0395fc1f850ee7b748e9685560a"></a><!-- doxytag: member="MiniSat::Solver::getWatches" ref="a8987b0395fc1f850ee7b748e9685560a" args="(Lit literal) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const std::vector<<a class="el" href="classMiniSat_1_1Clause.html">Clause</a>*>& MiniSat::Solver::getWatches </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>literal</em></td><td>)</td>
<td> const<code> [inline, protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00481">481</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00248">d_watches</a>, and <a class="el" href="minisat__types_8h_source.html#l00070">MiniSat::Lit::index()</a>.</p>
</div>
</div>
<a class="anchor" id="af3891961fe824bc91b47b59ee1e4a90b"></a><!-- doxytag: member="MiniSat::Solver::addWatch" ref="af3891961fe824bc91b47b59ee1e4a90b" args="(Lit literal, Clause *clause)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void MiniSat::Solver::addWatch </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>literal</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * </td>
<td class="paramname"><em>clause</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline, protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00485">485</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00478">getWatches()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00750">insertClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00190">insertLemma()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l01689">propagate()</a>.</p>
</div>
</div>
<a class="anchor" id="a94c3f4932f4c9d17b4a6dc1839c813f5"></a><!-- doxytag: member="MiniSat::Solver::removeWatch" ref="a94c3f4932f4c9d17b4a6dc1839c813f5" args="(std::vector< Clause * > &ws, Clause *elem)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::removeWatch </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * > & </td>
<td class="paramname"><em>ws</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * </td>
<td class="paramname"><em>elem</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Conflict handling. </p>
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00889">889</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00869">remove()</a>.</p>
</div>
</div>
<a class="anchor" id="a7a11f6c3676dd169d093a4e7c5af5299"></a><!-- doxytag: member="MiniSat::Solver::registerVar" ref="a7a11f6c3676dd169d093a4e7c5af5299" args="(Var var)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::registerVar </td>
<td>(</td>
<td class="paramtype"><a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> </td>
<td class="paramname"><em>var</em></td><td>)</td>
<td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Operations on clauses: </p>
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00457">457</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00366">d_activity</a>, <a class="el" href="minisat__solver_8h_source.html#l00412">d_analyze_seen</a>, <a class="el" href="minisat__solver_8h_source.html#l00251">d_assigns</a>, <a class="el" href="minisat__solver_8h_source.html#l00397">d_derivation</a>, <a class="el" href="minisat__solver_8h_source.html#l00284">d_level</a>, <a class="el" href="minisat__solver_8h_source.html#l00373">d_order</a>, <a class="el" href="minisat__solver_8h_source.html#l00343">d_pushIDs</a>, <a class="el" href="minisat__solver_8h_source.html#l00278">d_reason</a>, <a class="el" href="minisat__solver_8h_source.html#l00294">d_registeredVars</a>, <a class="el" href="minisat__solver_8h_source.html#l00256">d_trail</a>, <a class="el" href="minisat__solver_8h_source.html#l00264">d_trail_pos</a>, <a class="el" href="minisat__solver_8h_source.html#l00248">d_watches</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00448">isRegistered()</a>, <a class="el" href="minisat__global_8h_source.html#l00216">MiniSat::l_Undef</a>, <a class="el" href="minisat__varorder_8h_source.html#l00079">MiniSat::VarOrder::newVar()</a>, <a class="el" href="minisat__solver_8h_source.html#l00749">nVars()</a>, and <a class="el" href="minisat__global_8h_source.html#l00211">MiniSat::toInt()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00671">addClause()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00190">insertLemma()</a>.</p>
</div>
</div>
<a class="anchor" id="a31a0f344abc3fd65ee540f954b014f62"></a><!-- doxytag: member="MiniSat::Solver::isRegistered" ref="a31a0f344abc3fd65ee540f954b014f62" args="(Var var)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Solver::isRegistered </td>
<td>(</td>
<td class="paramtype"><a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> </td>
<td class="paramname"><em>var</em></td><td>)</td>
<td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Operations on clauses: </p>
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00448">448</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00294">d_registeredVars</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01950">propLookahead()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00457">registerVar()</a>.</p>
</div>
</div>
<a class="anchor" id="a36711ef6cb28057fa6f00235f58c03ff"></a><!-- doxytag: member="MiniSat::Solver::addClause" ref="a36711ef6cb28057fa6f00235f58c03ff" args="(std::vector< Lit > &literals, CVC3::Theorem theorem, int clauseID)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::addClause </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > & </td>
<td class="paramname"><em>literals</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> </td>
<td class="paramname"><em>theorem</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>clauseID</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00671">671</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__derivation_8h_source.html#l00058">MiniSat::Inference::add()</a>, <a class="el" href="minisat__types_8cpp_source.html#l00044">MiniSat::Clause_new()</a>, <a class="el" href="minisat__solver_8h_source.html#l00278">d_reason</a>, <a class="el" href="minisat__solver_8h_source.html#l00731">getDerivation()</a>, <a class="el" href="minisat__solver_8h_source.html#l00715">getReason()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00750">insertClause()</a>, <a class="el" href="minisat__types_8h_source.html#l00134">MiniSat::Clause::learnt()</a>, <a class="el" href="minisat__solver_8h_source.html#l00636">nextClauseID()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00588">orderClause()</a>, <a class="el" href="minisat__derivation_8h_source.html#l00126">MiniSat::Derivation::registerClause()</a>, <a class="el" href="minisat__derivation_8h_source.html#l00168">MiniSat::Derivation::registerInference()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00457">registerVar()</a>, <a class="el" href="minisat__derivation_8h_source.html#l00162">MiniSat::Derivation::removedClause()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00545">simplifyClause()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00482">addClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00529">addFormula()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01481">backtrack()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00248">createFrom()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00999">resolveTheoryImplication()</a>.</p>
</div>
</div>
<a class="anchor" id="aa0d36a2c07c88350dd9d54e62b3cef7b"></a><!-- doxytag: member="MiniSat::Solver::insertClause" ref="aa0d36a2c07c88350dd9d54e62b3cef7b" args="(Clause *clause)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::insertClause </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * </td>
<td class="paramname"><em>clause</em></td><td>)</td>
<td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00750">750</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00485">addWatch()</a>, <a class="el" href="minisat__solver_8h_source.html#l00558">claBumpActivity()</a>, <a class="el" href="minisat__solver_8h_source.html#l00164">MiniSat::SolverStats::clauses_literals</a>, <a class="el" href="minisat__solver_8h_source.html#l00303">d_clauses</a>, <a class="el" href="minisat__solver_8h_source.html#l00241">d_conflict</a>, <a class="el" href="minisat__solver_8h_source.html#l00306">d_learnts</a>, <a class="el" href="minisat__solver_8h_source.html#l00213">d_ok</a>, <a class="el" href="minisat__solver_8h_source.html#l00314">d_pendingClauses</a>, <a class="el" href="minisat__solver_8h_source.html#l00205">d_rootLevel</a>, <a class="el" href="minisat__solver_8h_source.html#l00417">d_stats</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01575">enqueue()</a>, <a class="el" href="minisat__solver_8h_source.html#l00731">getDerivation()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00910">getImplicationLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00703">getLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00699">getValue()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="minisat__global_8h_source.html#l00215">MiniSat::l_False</a>, <a class="el" href="minisat__global_8h_source.html#l00214">MiniSat::l_True</a>, <a class="el" href="minisat__global_8h_source.html#l00216">MiniSat::l_Undef</a>, <a class="el" href="minisat__types_8h_source.html#l00134">MiniSat::Clause::learnt()</a>, <a class="el" href="minisat__solver_8h_source.html#l00164">MiniSat::SolverStats::learnts_literals</a>, <a class="el" href="minisat__global_8h_source.html#l00059">MiniSat::max()</a>, <a class="el" href="minisat__solver_8h_source.html#l00164">MiniSat::SolverStats::max_literals</a>, <a class="el" href="minisat__derivation_8h_source.html#l00126">MiniSat::Derivation::registerClause()</a>, <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00977">updateConflict()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00671">addClause()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l01481">backtrack()</a>.</p>
</div>
</div>
<a class="anchor" id="a2ba80609ff72dbd93ae116a25923808d"></a><!-- doxytag: member="MiniSat::Solver::insertLemma" ref="a2ba80609ff72dbd93ae116a25923808d" args="(const Clause *lemma, int clauseID, int pushID)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::insertLemma </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * </td>
<td class="paramname"><em>lemma</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>clauseID</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>pushID</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00190">190</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__types_8h_source.html#l00144">MiniSat::Clause::activity()</a>, <a class="el" href="minisat__solver_8h_source.html#l00485">addWatch()</a>, <a class="el" href="minisat__solver_8h_source.html#l00306">d_learnts</a>, <a class="el" href="minisat__solver_8h_source.html#l00205">d_rootLevel</a>, <a class="el" href="minisat__solver_8h_source.html#l00417">d_stats</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01575">enqueue()</a>, <a class="el" href="minisat__solver_8h_source.html#l00731">getDerivation()</a>, <a class="el" href="minisat__solver_8h_source.html#l00699">getValue()</a>, <a class="el" href="minisat__global_8h_source.html#l00215">MiniSat::l_False</a>, <a class="el" href="minisat__solver_8h_source.html#l00164">MiniSat::SolverStats::learnts_literals</a>, <a class="el" href="minisat__types_8cpp_source.html#l00049">MiniSat::Lemma_new()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00588">orderClause()</a>, <a class="el" href="minisat__derivation_8h_source.html#l00126">MiniSat::Derivation::registerClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00457">registerVar()</a>, <a class="el" href="minisat__types_8h_source.html#l00148">MiniSat::Clause::setActivity()</a>, <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>, <a class="el" href="minisat__types_8cpp_source.html#l00072">MiniSat::Clause::toLit()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00977">updateConflict()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00248">createFrom()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>.</p>
</div>
</div>
<a class="anchor" id="abe63b049c7c54b810266baffb315c89b"></a><!-- doxytag: member="MiniSat::Solver::simplifyClause" ref="abe63b049c7c54b810266baffb315c89b" args="(std::vector< Lit > &literals, int clausePushID) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Solver::simplifyClause </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > & </td>
<td class="paramname"><em>literals</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>clausePushID</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td> const<code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00545">545</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00205">d_rootLevel</a>, <a class="el" href="minisat__solver_8h_source.html#l00703">getLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00699">getValue()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01443">isImpliedAt()</a>, <a class="el" href="minisat__global_8h_source.html#l00215">MiniSat::l_False</a>, and <a class="el" href="minisat__global_8h_source.html#l00214">MiniSat::l_True</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00671">addClause()</a>.</p>
</div>
</div>
<a class="anchor" id="aa8b5dfa883cace427d4b8b89769ca6df"></a><!-- doxytag: member="MiniSat::Solver::orderClause" ref="aa8b5dfa883cace427d4b8b89769ca6df" args="(std::vector< Lit > &literals) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::orderClause </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > & </td>
<td class="paramname"><em>literals</em></td><td>)</td>
<td> const<code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00588">588</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00703">getLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00699">getValue()</a>, <a class="el" href="minisat__global_8h_source.html#l00215">MiniSat::l_False</a>, and <a class="el" href="minisat__global_8h_source.html#l00214">MiniSat::l_True</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00671">addClause()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00190">insertLemma()</a>.</p>
</div>
</div>
<a class="anchor" id="a241e960f84c150b1421bf4e3b3a6b073"></a><!-- doxytag: member="MiniSat::Solver::remove" ref="a241e960f84c150b1421bf4e3b3a6b073" args="(Clause *c, bool just_dealloc=false)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::remove </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * </td>
<td class="paramname"><em>c</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>just_dealloc</em> = <code>false</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00869">869</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00164">MiniSat::SolverStats::clauses_literals</a>, <a class="el" href="minisat__solver_8h_source.html#l00417">d_stats</a>, <a class="el" href="minisat__solver_8h_source.html#l00731">getDerivation()</a>, <a class="el" href="minisat__solver_8h_source.html#l00478">getWatches()</a>, <a class="el" href="minisat__types_8h_source.html#l00134">MiniSat::Clause::learnt()</a>, <a class="el" href="minisat__solver_8h_source.html#l00164">MiniSat::SolverStats::learnts_literals</a>, <a class="el" href="minisat__derivation_8h_source.html#l00162">MiniSat::Derivation::removedClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00889">removeWatch()</a>, <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>, and <a class="el" href="minisat__global_8h_source.html#l00080">MiniSat::xfree()</a>.</p>
</div>
</div>
<a class="anchor" id="a871c1c054262f9673518c46f7efc8450"></a><!-- doxytag: member="MiniSat::Solver::isImpliedAt" ref="a871c1c054262f9673518c46f7efc8450" args="(Lit lit, int clausePushID) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Solver::isImpliedAt </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>lit</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>clausePushID</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td> const<code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l01443">1443</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00325">d_pushes</a>, and <a class="el" href="minisat__solver_8h_source.html#l00540">getPushID()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01458">isPermSatisfied()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00545">simplifyClause()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l01816">simplifyDB()</a>.</p>
</div>
</div>
<a class="anchor" id="ad64d6215811b4c4ca6c5ac86da4c787d"></a><!-- doxytag: member="MiniSat::Solver::isPermSatisfied" ref="ad64d6215811b4c4ca6c5ac86da4c787d" args="(Clause *c) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Solver::isPermSatisfied </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * </td>
<td class="paramname"><em>c</em></td><td>)</td>
<td> const<code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l01458">1458</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00205">d_rootLevel</a>, <a class="el" href="minisat__solver_8h_source.html#l00703">getLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00699">getValue()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01443">isImpliedAt()</a>, <a class="el" href="minisat__global_8h_source.html#l00214">MiniSat::l_True</a>, <a class="el" href="minisat__types_8h_source.html#l00143">MiniSat::Clause::pushID()</a>, and <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>.</p>
</div>
</div>
<a class="anchor" id="a07e86f7cb7f6a34c4e28df990cbf43d1"></a><!-- doxytag: member="MiniSat::Solver::setPushID" ref="a07e86f7cb7f6a34c4e28df990cbf43d1" args="(Var var, Clause *from)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::setPushID </td>
<td>(</td>
<td class="paramtype"><a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> </td>
<td class="paramname"><em>var</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * </td>
<td class="paramname"><em>from</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l02496">2496</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00343">d_pushIDs</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="minisat__types_8cpp_source.html#l00054">MiniSat::Clause::Decision()</a>, <a class="el" href="minisat__solver_8h_source.html#l00540">getPushID()</a>, <a class="el" href="minisat__solver_8h_source.html#l00715">getReason()</a>, <a class="el" href="minisat__global_8h_source.html#l00059">MiniSat::max()</a>, <a class="el" href="minisat__types_8h_source.html#l00143">MiniSat::Clause::pushID()</a>, <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>, and <a class="el" href="minisat__types_8cpp_source.html#l00063">MiniSat::Clause::TheoryImplication()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01575">enqueue()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00999">resolveTheoryImplication()</a>.</p>
</div>
</div>
<a class="anchor" id="a4f5805d21238ad316845059fb378a05f"></a><!-- doxytag: member="MiniSat::Solver::getPushID" ref="a4f5805d21238ad316845059fb378a05f" args="(Var var) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int MiniSat::Solver::getPushID </td>
<td>(</td>
<td class="paramtype"><a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> </td>
<td class="paramname"><em>var</em></td><td>)</td>
<td> const<code> [inline, protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00540">540</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00343">d_pushIDs</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01278">analyze_minimize()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01443">isImpliedAt()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02496">setPushID()</a>.</p>
</div>
</div>
<a class="anchor" id="aa095aa10adf85a246b525e0bc717e942"></a><!-- doxytag: member="MiniSat::Solver::getPushID" ref="aa095aa10adf85a246b525e0bc717e942" args="(Lit lit) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int MiniSat::Solver::getPushID </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>lit</em></td><td>)</td>
<td> const<code> [inline, protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00541">541</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00541">getPushID()</a>, and <a class="el" href="minisat__types_8h_source.html#l00069">MiniSat::Lit::var()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8h_source.html#l00541">getPushID()</a>.</p>
</div>
</div>
<a class="anchor" id="a2f75013fed205f5b38cd23b9d87dcd1a"></a><!-- doxytag: member="MiniSat::Solver::pop" ref="a2f75013fed205f5b38cd23b9d87dcd1a" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::pop </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l02668">2668</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00251">d_assigns</a>, <a class="el" href="minisat__solver_8h_source.html#l00177">MiniSat::PushEntry::d_clauseID</a>, <a class="el" href="minisat__solver_8h_source.html#l00303">d_clauses</a>, <a class="el" href="minisat__solver_8h_source.html#l00241">d_conflict</a>, <a class="el" href="minisat__solver_8h_source.html#l00397">d_derivation</a>, <a class="el" href="minisat__solver_8h_source.html#l00210">d_inSearch</a>, <a class="el" href="minisat__solver_8h_source.html#l00306">d_learnts</a>, <a class="el" href="minisat__solver_8h_source.html#l00183">MiniSat::PushEntry::d_ok</a>, <a class="el" href="minisat__solver_8h_source.html#l00213">d_ok</a>, <a class="el" href="minisat__solver_8h_source.html#l00373">d_order</a>, <a class="el" href="minisat__solver_8h_source.html#l00314">d_pendingClauses</a>, <a class="el" href="minisat__solver_8h_source.html#l00328">d_popLemmas</a>, <a class="el" href="minisat__solver_8h_source.html#l00350">d_popRequests</a>, <a class="el" href="minisat__solver_8h_source.html#l00325">d_pushes</a>, <a class="el" href="minisat__solver_8h_source.html#l00180">MiniSat::PushEntry::d_qhead</a>, <a class="el" href="minisat__solver_8h_source.html#l00269">d_qhead</a>, <a class="el" href="minisat__solver_8h_source.html#l00278">d_reason</a>, <a class="el" href="minisat__solver_8h_source.html#l00294">d_registeredVars</a>, <a class="el" href="minisat__solver_8h_source.html#l00417">d_stats</a>, <a class="el" href="minisat__solver_8h_source.html#l00181">MiniSat::PushEntry::d_thead</a>, <a class="el" href="minisat__solver_8h_source.html#l00273">d_thead</a>, <a class="el" href="minisat__solver_8h_source.html#l00319">d_theoryExplanations</a>, <a class="el" href="minisat__solver_8h_source.html#l00256">d_trail</a>, <a class="el" href="minisat__solver_8h_source.html#l00260">d_trail_lim</a>, <a class="el" href="minisat__solver_8h_source.html#l00179">MiniSat::PushEntry::d_trailSize</a>, <a class="el" href="minisat__solver_8h_source.html#l00164">MiniSat::SolverStats::debug</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="minisat__solver_8h_source.html#l00478">getWatches()</a>, <a class="el" href="minisat__solver_8h_source.html#l00712">isReason()</a>, <a class="el" href="minisat__global_8h_source.html#l00216">MiniSat::l_Undef</a>, <a class="el" href="minisat__solver_8h_source.html#l00164">MiniSat::SolverStats::learnts_literals</a>, <a class="el" href="minisat__derivation_8cpp_source.html#l00406">MiniSat::Derivation::pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02647">popClauses()</a>, <a class="el" href="minisat__types_8h_source.html#l00143">MiniSat::Clause::pushID()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00889">removeWatch()</a>, <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>, <a class="el" href="minisat__global_8h_source.html#l00211">MiniSat::toInt()</a>, and <a class="el" href="minisat__varorder_8h_source.html#l00097">MiniSat::VarOrder::undo()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02630">doPops()</a>.</p>
</div>
</div>
<a class="anchor" id="a6662641d5c0dea8d89041f5cf9dbc4af"></a><!-- doxytag: member="MiniSat::Solver::popClauses" ref="a6662641d5c0dea8d89041f5cf9dbc4af" args="(const PushEntry &pushEntry, std::vector< Clause * > &clauses)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::popClauses </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="structMiniSat_1_1PushEntry.html">PushEntry</a> & </td>
<td class="paramname"><em>pushEntry</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * > & </td>
<td class="paramname"><em>clauses</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l02647">2647</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00177">MiniSat::PushEntry::d_clauseID</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>.</p>
</div>
</div>
<a class="anchor" id="ab4af8739e981ec3caaa5a20ef1eb2f0f"></a><!-- doxytag: member="MiniSat::Solver::varBumpActivity" ref="ab4af8739e981ec3caaa5a20ef1eb2f0f" args="(Lit p)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void MiniSat::Solver::varBumpActivity </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>p</em></td><td>)</td>
<td><code> [inline, protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Activity: </p>
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00550">550</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00366">d_activity</a>, <a class="el" href="minisat__solver_8h_source.html#l00373">d_order</a>, <a class="el" href="minisat__solver_8h_source.html#l00371">d_var_decay</a>, <a class="el" href="minisat__solver_8h_source.html#l00368">d_var_inc</a>, <a class="el" href="minisat__varorder_8h_source.html#l00091">MiniSat::VarOrder::update()</a>, <a class="el" href="minisat__types_8h_source.html#l00069">MiniSat::Lit::var()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02290">varRescaleActivity()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01091">analyze()</a>.</p>
</div>
</div>
<a class="anchor" id="a91d54211b76e271e6838b57fca9ecfad"></a><!-- doxytag: member="MiniSat::Solver::varDecayActivity" ref="a91d54211b76e271e6838b57fca9ecfad" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void MiniSat::Solver::varDecayActivity </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00554">554</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00371">d_var_decay</a>, and <a class="el" href="minisat__solver_8h_source.html#l00368">d_var_inc</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a711410b67cec21e4fc1480ea6490f4f2"></a><!-- doxytag: member="MiniSat::Solver::varRescaleActivity" ref="a711410b67cec21e4fc1480ea6490f4f2" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::varRescaleActivity </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Activity. </p>
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l02290">2290</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00366">d_activity</a>, <a class="el" href="minisat__solver_8h_source.html#l00368">d_var_inc</a>, and <a class="el" href="minisat__solver_8h_source.html#l00749">nVars()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8h_source.html#l00550">varBumpActivity()</a>.</p>
</div>
</div>
<a class="anchor" id="a3e6ce9dc49e278926bfcc32289a343c1"></a><!-- doxytag: member="MiniSat::Solver::claDecayActivity" ref="a3e6ce9dc49e278926bfcc32289a343c1" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void MiniSat::Solver::claDecayActivity </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00556">556</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00361">d_cla_decay</a>, and <a class="el" href="minisat__solver_8h_source.html#l00359">d_cla_inc</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a3cdc4675e024f72e82d718596159456d"></a><!-- doxytag: member="MiniSat::Solver::claRescaleActivity" ref="a3cdc4675e024f72e82d718596159456d" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::claRescaleActivity </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l02299">2299</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00359">d_cla_inc</a>, and <a class="el" href="minisat__solver_8h_source.html#l00306">d_learnts</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8h_source.html#l00558">claBumpActivity()</a>.</p>
</div>
</div>
<a class="anchor" id="a4154a7c87f54bcbf48e8e1689dae68a9"></a><!-- doxytag: member="MiniSat::Solver::claBumpActivity" ref="a4154a7c87f54bcbf48e8e1689dae68a9" args="(Clause *c)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void MiniSat::Solver::claBumpActivity </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * </td>
<td class="paramname"><em>c</em></td><td>)</td>
<td><code> [inline, protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00558">558</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__types_8h_source.html#l00144">MiniSat::Clause::activity()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02299">claRescaleActivity()</a>, <a class="el" href="minisat__solver_8h_source.html#l00359">d_cla_inc</a>, and <a class="el" href="minisat__types_8h_source.html#l00148">MiniSat::Clause::setActivity()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01091">analyze()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00750">insertClause()</a>.</p>
</div>
</div>
<a class="anchor" id="a4d58130f36a501e919bb82f5f1438e32"></a><!-- doxytag: member="MiniSat::Solver::allClausesSatisfied" ref="a4d58130f36a501e919bb82f5f1438e32" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Solver::allClausesSatisfied </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>debugging </p>
<p>expensive debug checks </p>
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l02313">2313</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00303">d_clauses</a>, <a class="el" href="minisat__solver_8h_source.html#l00205">d_rootLevel</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00112">debug_full</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="minisat__solver_8h_source.html#l00703">getLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00699">getValue()</a>, <a class="el" href="minisat__solver_8h_source.html#l00478">getWatches()</a>, <a class="el" href="minisat__global_8h_source.html#l00214">MiniSat::l_True</a>, <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00319">toString()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a09e6b3c658982dbaeec9a18d440dbe7a"></a><!-- doxytag: member="MiniSat::Solver::checkWatched" ref="a09e6b3c658982dbaeec9a18d440dbe7a" args="(const Clause &clause) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::checkWatched </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> & </td>
<td class="paramname"><em>clause</em></td><td>)</td>
<td> const<code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l02359">2359</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00205">d_rootLevel</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, <a class="el" href="minisat__solver_8h_source.html#l00703">getLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00478">getWatches()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00375">printState()</a>, <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00319">toString()</a>.</p>
</div>
</div>
<a class="anchor" id="a6b4bb1db7b767e1368884b178f523dcf"></a><!-- doxytag: member="MiniSat::Solver::checkWatched" ref="a6b4bb1db7b767e1368884b178f523dcf" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::checkWatched </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l02384">2384</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00303">d_clauses</a>, <a class="el" href="minisat__solver_8h_source.html#l00306">d_learnts</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00112">debug_full</a>.</p>
</div>
</div>
<a class="anchor" id="ad4c405a5b6aac64b41c190aaa68004aa"></a><!-- doxytag: member="MiniSat::Solver::checkClause" ref="ad4c405a5b6aac64b41c190aaa68004aa" args="(const Clause &clause) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::checkClause </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> & </td>
<td class="paramname"><em>clause</em></td><td>)</td>
<td> const<code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l02398">2398</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, <a class="el" href="minisat__solver_8h_source.html#l00699">getValue()</a>, <a class="el" href="minisat__global_8h_source.html#l00215">MiniSat::l_False</a>, <a class="el" href="minisat__global_8h_source.html#l00214">MiniSat::l_True</a>, <a class="el" href="minisat__global_8h_source.html#l00216">MiniSat::l_Undef</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00375">printState()</a>, <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00319">toString()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02432">checkClauses()</a>.</p>
</div>
</div>
<a class="anchor" id="a9e152e0ed1d83a51f7886df8cd5fe681"></a><!-- doxytag: member="MiniSat::Solver::checkClauses" ref="a9e152e0ed1d83a51f7886df8cd5fe681" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::checkClauses </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l02432">2432</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8cpp_source.html#l02398">checkClause()</a>, <a class="el" href="minisat__solver_8h_source.html#l00303">d_clauses</a>, <a class="el" href="minisat__solver_8h_source.html#l00306">d_learnts</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00112">debug_full</a>.</p>
</div>
</div>
<a class="anchor" id="a9457fd91045b9496ef5bdcd1a93fcae5"></a><!-- doxytag: member="MiniSat::Solver::checkTrail" ref="a9457fd91045b9496ef5bdcd1a93fcae5" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::checkTrail </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l02446">2446</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00251">d_assigns</a>, <a class="el" href="minisat__solver_8h_source.html#l00278">d_reason</a>, <a class="el" href="minisat__solver_8h_source.html#l00256">d_trail</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00112">debug_full</a>, <a class="el" href="minisat__types_8cpp_source.html#l00054">MiniSat::Clause::Decision()</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, <a class="el" href="minisat__solver_8h_source.html#l00703">getLevel()</a>, <a class="el" href="minisat__types_8h_source.html#l00068">MiniSat::Lit::sign()</a>, <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>, <a class="el" href="minisat__types_8cpp_source.html#l00063">MiniSat::Clause::TheoryImplication()</a>, <a class="el" href="minisat__global_8h_source.html#l00211">MiniSat::toInt()</a>, and <a class="el" href="minisat__types_8h_source.html#l00069">MiniSat::Lit::var()</a>.</p>
</div>
</div>
<a class="anchor" id="a776adc363c0056e2077fbe659ae6f709"></a><!-- doxytag: member="MiniSat::Solver::protocolPropagation" ref="a776adc363c0056e2077fbe659ae6f709" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::protocolPropagation </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l01937">1937</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00269">d_qhead</a>, <a class="el" href="minisat__solver_8h_source.html#l00256">d_trail</a>, <a class="el" href="minisat__types_8cpp_source.html#l00054">MiniSat::Clause::Decision()</a>, <a class="el" href="minisat__solver_8h_source.html#l00424">decisionLevel()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="minisat__solver_8h_source.html#l00703">getLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00715">getReason()</a>, <a class="el" href="minisat__types_8h_source.html#l00070">MiniSat::Lit::index()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00105">protocol</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00319">toString()</a>, and <a class="el" href="minisat__types_8h_source.html#l00069">MiniSat::Lit::var()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01950">propLookahead()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a7fce9c6a705405959f91d559a6e06ee4"></a><!-- doxytag: member="MiniSat::Solver::createFrom" ref="a7fce9c6a705405959f91d559a6e06ee4" args="(const Solver *solver)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classMiniSat_1_1Solver.html">Solver</a> * Solver::createFrom </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classMiniSat_1_1Solver.html">Solver</a> * </td>
<td class="paramname"><em>solver</em></td><td>)</td>
<td><code> [static]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00248">248</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8cpp_source.html#l00671">addClause()</a>, <a class="el" href="minisat__solver_8h_source.html#l00366">d_activity</a>, <a class="el" href="minisat__solver_8h_source.html#l00359">d_cla_inc</a>, <a class="el" href="minisat__solver_8h_source.html#l00391">d_decider</a>, <a class="el" href="minisat__solver_8h_source.html#l00397">d_derivation</a>, <a class="el" href="minisat__solver_8h_source.html#l00388">d_theoryAPI</a>, <a class="el" href="minisat__solver_8h_source.html#l00368">d_var_inc</a>, <a class="el" href="minisat__solver_8h_source.html#l00722">getClauses()</a>, <a class="el" href="minisat__solver_8h_source.html#l00725">getLemmas()</a>, <a class="el" href="minisat__solver_8h_source.html#l00728">getTrail()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00190">insertLemma()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00973">isConflicting()</a>, <a class="el" href="minisat__solver_8h_source.html#l00636">nextClauseID()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00158">Solver()</a>.</p>
<p>Referenced by <a class="el" href="dpllt__minisat_8cpp_source.html#l00056">SAT::DPLLTMiniSat::pushSolver()</a>.</p>
</div>
</div>
<a class="anchor" id="abbb1190222cc3ad99638caf6e86ee698"></a><!-- doxytag: member="MiniSat::Solver::cvcToMiniSat" ref="abbb1190222cc3ad99638caf6e86ee698" args="(const SAT::Clause &clause, int id)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * Solver::cvcToMiniSat </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classSAT_1_1Clause.html">SAT::Clause</a> & </td>
<td class="paramname"><em>clause</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>id</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>problem specification </p>
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00139">139</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__types_8cpp_source.html#l00044">MiniSat::Clause_new()</a>, <a class="el" href="minisat__solver_8h_source.html#l00128">MiniSat::cvcToMiniSat()</a>, and <a class="el" href="cnf_8h_source.html#l00108">SAT::Clause::getClauseTheorem()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00999">resolveTheoryImplication()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="af3e9229206719e24e2a951be84c33a42"></a><!-- doxytag: member="MiniSat::Solver::addClause" ref="af3e9229206719e24e2a951be84c33a42" args="(Lit p, CVC3::Theorem theorem)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::addClause </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>p</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Theorem.html">CVC3::Theorem</a> </td>
<td class="paramname"><em>theorem</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00482">482</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8cpp_source.html#l00671">addClause()</a>, and <a class="el" href="minisat__solver_8h_source.html#l00636">nextClauseID()</a>.</p>
</div>
</div>
<a class="anchor" id="a03e24ae79c2068ab70b8c9633829777c"></a><!-- doxytag: member="MiniSat::Solver::addClause" ref="a03e24ae79c2068ab70b8c9633829777c" args="(const Clause &clause, bool keepClauseID)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::addClause </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> & </td>
<td class="paramname"><em>clause</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>keepClauseID</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00507">507</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8cpp_source.html#l00671">addClause()</a>, <a class="el" href="minisat__types_8h_source.html#l00153">MiniSat::Clause::getTheorem()</a>, <a class="el" href="minisat__types_8h_source.html#l00138">MiniSat::Clause::id()</a>, <a class="el" href="minisat__solver_8h_source.html#l00636">nextClauseID()</a>, and <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>.</p>
</div>
</div>
<a class="anchor" id="a27b79e9b52cd9850e3e21cd2e2af9a04"></a><!-- doxytag: member="MiniSat::Solver::addClause" ref="a27b79e9b52cd9850e3e21cd2e2af9a04" args="(const SAT::Clause &clause, bool isTheoryClause)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::addClause </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classSAT_1_1Clause.html">SAT::Clause</a> & </td>
<td class="paramname"><em>clause</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>isTheoryClause</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00488">488</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8cpp_source.html#l00671">addClause()</a>, <a class="el" href="minisat__solver_8h_source.html#l00128">MiniSat::cvcToMiniSat()</a>, <a class="el" href="cnf_8h_source.html#l00108">SAT::Clause::getClauseTheorem()</a>, <a class="el" href="minisat__solver_8h_source.html#l00731">getDerivation()</a>, <a class="el" href="minisat__solver_8h_source.html#l00636">nextClauseID()</a>, and <a class="el" href="minisat__derivation_8h_source.html#l00155">MiniSat::Derivation::registerInputClause()</a>.</p>
</div>
</div>
<a class="anchor" id="ab7ceeed839df517256ce77c126f28e00"></a><!-- doxytag: member="MiniSat::Solver::addFormula" ref="ab7ceeed839df517256ce77c126f28e00" args="(const SAT::CNF_Formula &cnf, bool isTheoryClause)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::addFormula </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classSAT_1_1CNF__Formula.html">SAT::CNF_Formula</a> & </td>
<td class="paramname"><em>cnf</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>isTheoryClause</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00529">529</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8cpp_source.html#l00671">addClause()</a>, <a class="el" href="classSAT_1_1CNF__Formula.html#a69dfc94796b23b6913c44a4d6d60f0d8">SAT::CNF_Formula::begin()</a>, and <a class="el" href="classSAT_1_1CNF__Formula.html#a6631cf3c5a6938f655360f7f63522b79">SAT::CNF_Formula::end()</a>.</p>
<p>Referenced by <a class="el" href="dpllt__minisat_8cpp_source.html#l00223">SAT::DPLLTMiniSat::addAssertion()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00131">SAT::DPLLTMiniSat::checkSat()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00154">SAT::DPLLTMiniSat::continueCheck()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a7323aff4aaa93c01e6008e8e033d2b8f"></a><!-- doxytag: member="MiniSat::Solver::nextClauseID" ref="a7323aff4aaa93c01e6008e8e033d2b8f" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int MiniSat::Solver::nextClauseID </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00636">636</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00300">d_clauseIDCounter</a>, and <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00482">addClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01091">analyze()</a>, <a class="el" href="minisat__derivation_8cpp_source.html#l00062">MiniSat::Derivation::computeRootReason()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00248">createFrom()</a>, <a class="el" href="minisat__derivation_8cpp_source.html#l00115">MiniSat::Derivation::finish()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00999">resolveTheoryImplication()</a>.</p>
</div>
</div>
<a class="anchor" id="a4e6b8a057747d66f650e6e785f8fc334"></a><!-- doxytag: member="MiniSat::Solver::simplifyDB" ref="a4e6b8a057747d66f650e6e785f8fc334" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::simplifyDB </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l01816">1816</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00164">MiniSat::SolverStats::clauses_literals</a>, <a class="el" href="minisat__solver_8h_source.html#l00303">d_clauses</a>, <a class="el" href="minisat__solver_8h_source.html#l00306">d_learnts</a>, <a class="el" href="minisat__solver_8h_source.html#l00269">d_qhead</a>, <a class="el" href="minisat__solver_8h_source.html#l00205">d_rootLevel</a>, <a class="el" href="minisat__solver_8h_source.html#l00378">d_simpDB_assigns</a>, <a class="el" href="minisat__solver_8h_source.html#l00380">d_simpDB_props</a>, <a class="el" href="minisat__solver_8h_source.html#l00417">d_stats</a>, <a class="el" href="minisat__solver_8h_source.html#l00256">d_trail</a>, <a class="el" href="minisat__solver_8h_source.html#l00164">MiniSat::SolverStats::db_simpl</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="minisat__solver_8h_source.html#l00164">MiniSat::SolverStats::del_clauses</a>, <a class="el" href="minisat__solver_8h_source.html#l00703">getLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00699">getValue()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00973">isConflicting()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01443">isImpliedAt()</a>, <a class="el" href="minisat__solver_8h_source.html#l00712">isReason()</a>, <a class="el" href="minisat__global_8h_source.html#l00215">MiniSat::l_False</a>, <a class="el" href="minisat__global_8h_source.html#l00214">MiniSat::l_True</a>, <a class="el" href="minisat__solver_8h_source.html#l00164">MiniSat::SolverStats::learnts_literals</a>, <a class="el" href="minisat__types_8h_source.html#l00143">MiniSat::Clause::pushID()</a>, and <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a62eea2c00917497fbfb843bf9ca4482e"></a><!-- doxytag: member="MiniSat::Solver::reduceDB" ref="a62eea2c00917497fbfb843bf9ca4482e" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::reduceDB </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l01781">1781</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00359">d_cla_inc</a>, <a class="el" href="minisat__solver_8h_source.html#l00306">d_learnts</a>, <a class="el" href="minisat__solver_8h_source.html#l00382">d_simpRD_learnts</a>, <a class="el" href="minisat__solver_8h_source.html#l00417">d_stats</a>, <a class="el" href="minisat__solver_8h_source.html#l00164">MiniSat::SolverStats::del_lemmas</a>, <a class="el" href="minisat__solver_8h_source.html#l00712">isReason()</a>, and <a class="el" href="minisat__solver_8h_source.html#l00164">MiniSat::SolverStats::lm_simpl</a>.</p>
</div>
</div>
<a class="anchor" id="af43d31ac67426e7b3b699491b02d62c1"></a><!-- doxytag: member="MiniSat::Solver::search" ref="af43d31ac67426e7b3b699491b02d62c1" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">CVC3::QueryResult</a> Solver::search </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>search </p>
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l02005">2005</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="queryresult_8h_source.html#l00037">CVC3::ABORT</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00529">addFormula()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02313">allClausesSatisfied()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01091">analyze()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a3b3ef70567e0298cd3e971fd57d26fa6">SAT::DPLLT::TheoryAPI::assertLit()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01473">assume()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01481">backtrack()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a4b3f4a97dbac21236e479a157d866545">SAT::DPLLT::TheoryAPI::checkConsistent()</a>, <a class="el" href="minisat__solver_8h_source.html#l00556">claDecayActivity()</a>, <a class="el" href="minisat__solver_8h_source.html#l00194">MiniSat::SearchParams::clause_decay</a>, <a class="el" href="minisat__solver_8h_source.html#l00163">MiniSat::SolverStats::conflicts</a>, <a class="el" href="dpllt_8h_source.html#l00026">SAT::DPLLT::CONSISTENT</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00139">cvcToMiniSat()</a>, <a class="el" href="minisat__solver_8h_source.html#l00361">d_cla_decay</a>, <a class="el" href="minisat__solver_8h_source.html#l00241">d_conflict</a>, <a class="el" href="minisat__solver_8h_source.html#l00391">d_decider</a>, <a class="el" href="minisat__solver_8h_source.html#l00403">d_default_params</a>, <a class="el" href="minisat__solver_8h_source.html#l00210">d_inSearch</a>, <a class="el" href="minisat__solver_8h_source.html#l00213">d_ok</a>, <a class="el" href="minisat__solver_8h_source.html#l00373">d_order</a>, <a class="el" href="minisat__solver_8h_source.html#l00350">d_popRequests</a>, <a class="el" href="minisat__solver_8h_source.html#l00325">d_pushes</a>, <a class="el" href="minisat__solver_8h_source.html#l00269">d_qhead</a>, <a class="el" href="minisat__solver_8h_source.html#l00205">d_rootLevel</a>, <a class="el" href="minisat__solver_8h_source.html#l00417">d_stats</a>, <a class="el" href="minisat__solver_8h_source.html#l00273">d_thead</a>, <a class="el" href="minisat__solver_8h_source.html#l00388">d_theoryAPI</a>, <a class="el" href="minisat__solver_8h_source.html#l00256">d_trail</a>, <a class="el" href="minisat__solver_8h_source.html#l00260">d_trail_lim</a>, <a class="el" href="minisat__solver_8h_source.html#l00371">d_var_decay</a>, <a class="el" href="minisat__solver_8h_source.html#l00164">MiniSat::SolverStats::debug</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="minisat__solver_8h_source.html#l00424">decisionLevel()</a>, <a class="el" href="minisat__solver_8h_source.html#l00163">MiniSat::SolverStats::decisions</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00063">defer_theory_propagation</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00070">eager_explanation</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01575">enqueue()</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, <a class="el" href="minisat__derivation_8cpp_source.html#l00115">MiniSat::Derivation::finish()</a>, <a class="el" href="minisat__solver_8h_source.html#l00731">getDerivation()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#ab7a85a15823cb0771d1e9bb4c0ce0703">SAT::DPLLT::TheoryAPI::getExplanation()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#ad61236a10860b9771e1e09505ab501b5">SAT::DPLLT::TheoryAPI::getImplication()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a7d4bf4b22f7e9f19174a4f2813294acd">SAT::DPLLT::TheoryAPI::getNewClauses()</a>, <a class="el" href="minisat__solver_8h_source.html#l00699">getValue()</a>, <a class="el" href="dpllt_8h_source.html#l00026">SAT::DPLLT::INCONSISTENT</a>, <a class="el" href="minisat__types_8h_source.html#l00070">MiniSat::Lit::index()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00973">isConflicting()</a>, <a class="el" href="cnf_8h_source.html#l00063">SAT::Lit::isNull()</a>, <a class="el" href="minisat__global_8h_source.html#l00216">MiniSat::l_Undef</a>, <a class="el" href="namespaceMiniSat.html#a120ea2f17b58215d657cd7b005edcd85">MiniSat::lit_Undef()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1Decider.html#a9a15df2a6d6fdd38d9719f5681c068f2">SAT::DPLLT::Decider::makeDecision()</a>, <a class="el" href="dpllt_8h_source.html#l00026">SAT::DPLLT::MAYBE_CONSISTENT</a>, <a class="el" href="minisat__solver_8h_source.html#l00132">MiniSat::miniSatToCVC()</a>, <a class="el" href="minisat__solver_8h_source.html#l00739">nAssigns()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a6484231750edf5bd9d10d9408c6b5a59">SAT::DPLLT::TheoryAPI::outOfResources()</a>, <a class="el" href="cnf_8cpp_source.html#l00085">SAT::CNF_Formula::print()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00375">printState()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01689">propagate()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01950">propLookahead()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00105">protocol</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01937">protocolPropagation()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a771e84ea6308cb7d3f7d02e7858b37db">SAT::DPLLT::TheoryAPI::push()</a>, <a class="el" href="minisat__solver_8h_source.html#l00194">MiniSat::SearchParams::random_var_freq</a>, <a class="el" href="cnf_8cpp_source.html#l00174">SAT::CNF_Formula_Impl::reset()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00055">SATISFIABLE</a>, <a class="el" href="minisat__varorder_8h_source.html#l00104">MiniSat::VarOrder::select()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01816">simplifyDB()</a>, <a class="el" href="minisat__solver_8h_source.html#l00163">MiniSat::SolverStats::starts</a>, <a class="el" href="minisat__solver_8h_source.html#l00163">MiniSat::SolverStats::theory_conflicts</a>, <a class="el" href="minisat__types_8cpp_source.html#l00063">MiniSat::Clause::TheoryImplication()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00319">toString()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00054">UNSATISFIABLE</a>, <a class="el" href="minisat__solver_8h_source.html#l00194">MiniSat::SearchParams::var_decay</a>, <a class="el" href="minisat__types_8h_source.html#l00056">MiniSat::var_Undef</a>, and <a class="el" href="minisat__solver_8h_source.html#l00554">varDecayActivity()</a>.</p>
<p>Referenced by <a class="el" href="dpllt__minisat_8cpp_source.html#l00065">SAT::DPLLTMiniSat::search()</a>.</p>
</div>
</div>
<a class="anchor" id="ac051d3f7a6f6e93269769f2ff8eb9878"></a><!-- doxytag: member="MiniSat::Solver::getProof" ref="ac051d3f7a6f6e93269769f2ff8eb9878" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classMiniSat_1_1Derivation.html">Derivation</a>* MiniSat::Solver::getProof </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
</div>
</div>
<a class="anchor" id="ae28b9db22e418c5907fb82dbe49a6832"></a><!-- doxytag: member="MiniSat::Solver::inSearch" ref="ae28b9db22e418c5907fb82dbe49a6832" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool MiniSat::Solver::inSearch </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00668">668</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00210">d_inSearch</a>, and <a class="el" href="minisat__solver_8h_source.html#l00350">d_popRequests</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>.</p>
</div>
</div>
<a class="anchor" id="a7eb95fc222427a795a3b5ae48e94518e"></a><!-- doxytag: member="MiniSat::Solver::isConsistent" ref="a7eb95fc222427a795a3b5ae48e94518e" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool MiniSat::Solver::isConsistent </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00671">671</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8cpp_source.html#l00973">isConflicting()</a>.</p>
<p>Referenced by <a class="el" href="dpllt__minisat_8cpp_source.html#l00223">SAT::DPLLTMiniSat::addAssertion()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02621">requestPop()</a>.</p>
</div>
</div>
<a class="anchor" id="aec12c38c0c17d7067e12da239353ebc8"></a><!-- doxytag: member="MiniSat::Solver::push" ref="aec12c38c0c17d7067e12da239353ebc8" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::push </td>
<td>(</td>
<td class="paramtype">void </td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Push / Pop. </p>
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l02510">2510</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8cpp_source.html#l00529">addFormula()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a3b3ef70567e0298cd3e971fd57d26fa6">SAT::DPLLT::TheoryAPI::assertLit()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00139">cvcToMiniSat()</a>, <a class="el" href="minisat__solver_8h_source.html#l00300">d_clauseIDCounter</a>, <a class="el" href="minisat__solver_8h_source.html#l00397">d_derivation</a>, <a class="el" href="minisat__solver_8h_source.html#l00213">d_ok</a>, <a class="el" href="minisat__solver_8h_source.html#l00328">d_popLemmas</a>, <a class="el" href="minisat__solver_8h_source.html#l00325">d_pushes</a>, <a class="el" href="minisat__solver_8h_source.html#l00269">d_qhead</a>, <a class="el" href="minisat__solver_8h_source.html#l00294">d_registeredVars</a>, <a class="el" href="minisat__solver_8h_source.html#l00417">d_stats</a>, <a class="el" href="minisat__solver_8h_source.html#l00273">d_thead</a>, <a class="el" href="minisat__solver_8h_source.html#l00388">d_theoryAPI</a>, <a class="el" href="minisat__solver_8h_source.html#l00256">d_trail</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="minisat__solver_8h_source.html#l00424">decisionLevel()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00063">defer_theory_propagation</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00070">eager_explanation</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01575">enqueue()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#ab7a85a15823cb0771d1e9bb4c0ce0703">SAT::DPLLT::TheoryAPI::getExplanation()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#ad61236a10860b9771e1e09505ab501b5">SAT::DPLLT::TheoryAPI::getImplication()</a>, <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a7d4bf4b22f7e9f19174a4f2813294acd">SAT::DPLLT::TheoryAPI::getNewClauses()</a>, <a class="el" href="minisat__types_8h_source.html#l00138">MiniSat::Clause::id()</a>, <a class="el" href="minisat__types_8h_source.html#l00070">MiniSat::Lit::index()</a>, <a class="el" href="minisat__solver_8h_source.html#l00668">inSearch()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00190">insertLemma()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00973">isConflicting()</a>, <a class="el" href="cnf_8h_source.html#l00063">SAT::Lit::isNull()</a>, <a class="el" href="minisat__solver_8h_source.html#l00164">MiniSat::SolverStats::learnts_literals</a>, <a class="el" href="minisat__solver_8h_source.html#l00132">MiniSat::miniSatToCVC()</a>, <a class="el" href="cnf_8cpp_source.html#l00085">SAT::CNF_Formula::print()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00375">printState()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01689">propagate()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00105">protocol</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01937">protocolPropagation()</a>, <a class="el" href="minisat__derivation_8cpp_source.html#l00402">MiniSat::Derivation::push()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00095">push_theory_clause</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00091">push_theory_implication</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00087">push_theory_propagation</a>, <a class="el" href="minisat__types_8h_source.html#l00143">MiniSat::Clause::pushID()</a>, <a class="el" href="cnf_8cpp_source.html#l00174">SAT::CNF_Formula_Impl::reset()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01816">simplifyDB()</a>, <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>, and <a class="el" href="minisat__types_8cpp_source.html#l00063">MiniSat::Clause::TheoryImplication()</a>.</p>
<p>Referenced by <a class="el" href="dpllt__minisat_8cpp_source.html#l00179">SAT::DPLLTMiniSat::push()</a>.</p>
</div>
</div>
<a class="anchor" id="a80f70ef105eabcf61758427d041281d6"></a><!-- doxytag: member="MiniSat::Solver::popTheories" ref="a80f70ef105eabcf61758427d041281d6" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::popTheories </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l02641">2641</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00205">d_rootLevel</a>, <a class="el" href="minisat__solver_8h_source.html#l00388">d_theoryAPI</a>, <a class="el" href="minisat__solver_8h_source.html#l00424">decisionLevel()</a>, and <a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html#a51a08aab04c2185513676a316aee14b4">SAT::DPLLT::TheoryAPI::pop()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02621">requestPop()</a>.</p>
</div>
</div>
<a class="anchor" id="a8be8edbecd5a07bd39990ee7ba0918e3"></a><!-- doxytag: member="MiniSat::Solver::requestPop" ref="a8be8edbecd5a07bd39990ee7ba0918e3" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::requestPop </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l02621">2621</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00350">d_popRequests</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="minisat__solver_8h_source.html#l00692">inPush()</a>, <a class="el" href="minisat__solver_8h_source.html#l00671">isConsistent()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02641">popTheories()</a>.</p>
<p>Referenced by <a class="el" href="dpllt__minisat_8cpp_source.html#l00192">SAT::DPLLTMiniSat::pop()</a>.</p>
</div>
</div>
<a class="anchor" id="a8cc5207e3580ab0f09c6e9c225eaebff"></a><!-- doxytag: member="MiniSat::Solver::doPops" ref="a8cc5207e3580ab0f09c6e9c225eaebff" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::doPops </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l02630">2630</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00350">d_popRequests</a>, <a class="el" href="minisat__solver_8h_source.html#l00325">d_pushes</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>.</p>
<p>Referenced by <a class="el" href="dpllt__minisat_8cpp_source.html#l00223">SAT::DPLLTMiniSat::addAssertion()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00131">SAT::DPLLTMiniSat::checkSat()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00154">SAT::DPLLTMiniSat::continueCheck()</a>, and <a class="el" href="dpllt__minisat_8cpp_source.html#l00179">SAT::DPLLTMiniSat::push()</a>.</p>
</div>
</div>
<a class="anchor" id="a1bcf27269a8286f82b3235d982e4724e"></a><!-- doxytag: member="MiniSat::Solver::inPush" ref="a1bcf27269a8286f82b3235d982e4724e" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool MiniSat::Solver::inPush </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00692">692</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00350">d_popRequests</a>, and <a class="el" href="minisat__solver_8h_source.html#l00325">d_pushes</a>.</p>
<p>Referenced by <a class="el" href="dpllt__minisat_8cpp_source.html#l00154">SAT::DPLLTMiniSat::continueCheck()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00192">SAT::DPLLTMiniSat::pop()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02621">requestPop()</a>.</p>
</div>
</div>
<a class="anchor" id="adc9d01899ff6c1eefea8749a1a97309b"></a><!-- doxytag: member="MiniSat::Solver::getValue" ref="adc9d01899ff6c1eefea8749a1a97309b" args="(Var x) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classMiniSat_1_1lbool.html">lbool</a> MiniSat::Solver::getValue </td>
<td>(</td>
<td class="paramtype"><a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> </td>
<td class="paramname"><em>x</em></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>clauses / assignment </p>
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00699">699</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00251">d_assigns</a>, and <a class="el" href="minisat__global_8h_source.html#l00212">MiniSat::toLbool()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02313">allClausesSatisfied()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01091">analyze()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02398">checkClause()</a>, <a class="el" href="minisat__derivation_8cpp_source.html#l00062">MiniSat::Derivation::computeRootReason()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01575">enqueue()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00935">getConflictLevel()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00910">getImplicationLevel()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00950">getReason()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00244">SAT::DPLLTMiniSat::getValue()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00750">insertClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00190">insertLemma()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01458">isPermSatisfied()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00588">orderClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01689">propagate()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00999">resolveTheoryImplication()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00545">simplifyClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01816">simplifyDB()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00319">toString()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00977">updateConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="a2c6d2ce4210d3bfbc3d659dd724d02f0"></a><!-- doxytag: member="MiniSat::Solver::getValue" ref="a2c6d2ce4210d3bfbc3d659dd724d02f0" args="(Lit p) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classMiniSat_1_1lbool.html">lbool</a> MiniSat::Solver::getValue </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>p</em></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00700">700</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00700">getValue()</a>, <a class="el" href="minisat__types_8h_source.html#l00068">MiniSat::Lit::sign()</a>, and <a class="el" href="minisat__types_8h_source.html#l00069">MiniSat::Lit::var()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8h_source.html#l00700">getValue()</a>.</p>
</div>
</div>
<a class="anchor" id="a68a7d96223af2e9b67d8b25d047284e4"></a><!-- doxytag: member="MiniSat::Solver::getLevel" ref="a68a7d96223af2e9b67d8b25d047284e4" args="(Var var) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int MiniSat::Solver::getLevel </td>
<td>(</td>
<td class="paramtype"><a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> </td>
<td class="paramname"><em>var</em></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00703">703</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00284">d_level</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02313">allClausesSatisfied()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01091">analyze()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01278">analyze_minimize()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01395">analyze_removable()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01481">backtrack()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02446">checkTrail()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02359">checkWatched()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00935">getConflictLevel()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00910">getImplicationLevel()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00750">insertClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01458">isPermSatisfied()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00588">orderClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01689">propagate()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01937">protocolPropagation()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00545">simplifyClause()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l01816">simplifyDB()</a>.</p>
</div>
</div>
<a class="anchor" id="a70b4f991bd7a679be32a89aa1d22eb8d"></a><!-- doxytag: member="MiniSat::Solver::getLevel" ref="a70b4f991bd7a679be32a89aa1d22eb8d" args="(Lit lit) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int MiniSat::Solver::getLevel </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>lit</em></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00704">704</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00704">getLevel()</a>, and <a class="el" href="minisat__types_8h_source.html#l00069">MiniSat::Lit::var()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8h_source.html#l00704">getLevel()</a>.</p>
</div>
</div>
<a class="anchor" id="adf6fbd3cddfa511acae41f180b187454"></a><!-- doxytag: member="MiniSat::Solver::setLevel" ref="adf6fbd3cddfa511acae41f180b187454" args="(Var var, int level)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void MiniSat::Solver::setLevel </td>
<td>(</td>
<td class="paramtype"><a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> </td>
<td class="paramname"><em>var</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>level</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00707">707</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00284">d_level</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01575">enqueue()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00999">resolveTheoryImplication()</a>.</p>
</div>
</div>
<a class="anchor" id="aae4dc01729a30c592f939d7d922f5774"></a><!-- doxytag: member="MiniSat::Solver::setLevel" ref="aae4dc01729a30c592f939d7d922f5774" args="(Lit lit, int level)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void MiniSat::Solver::setLevel </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>lit</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>level</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00708">708</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00708">setLevel()</a>, and <a class="el" href="minisat__types_8h_source.html#l00069">MiniSat::Lit::var()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8h_source.html#l00708">setLevel()</a>.</p>
</div>
</div>
<a class="anchor" id="a344d9206f065425f276b408e86b7e1d3"></a><!-- doxytag: member="MiniSat::Solver::isReason" ref="a344d9206f065425f276b408e86b7e1d3" args="(const Clause *c) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool MiniSat::Solver::isReason </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * </td>
<td class="paramname"><em>c</em></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00712">712</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00278">d_reason</a>, and <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01781">reduceDB()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l01816">simplifyDB()</a>.</p>
</div>
</div>
<a class="anchor" id="a8660c6ceafa236f5533e432bb859aeba"></a><!-- doxytag: member="MiniSat::Solver::getReason" ref="a8660c6ceafa236f5533e432bb859aeba" args="(Var var) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a>* MiniSat::Solver::getReason </td>
<td>(</td>
<td class="paramtype"><a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a> </td>
<td class="paramname"><em>var</em></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00715">715</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00278">d_reason</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00671">addClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01091">analyze()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01278">analyze_minimize()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01395">analyze_removable()</a>, <a class="el" href="minisat__derivation_8cpp_source.html#l00062">MiniSat::Derivation::computeRootReason()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00405">printDIMACS()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00375">printState()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01937">protocolPropagation()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02496">setPushID()</a>.</p>
</div>
</div>
<a class="anchor" id="a031fbfd0b0f291ad294dc9e49a8e7ec7"></a><!-- doxytag: member="MiniSat::Solver::getReason" ref="a031fbfd0b0f291ad294dc9e49a8e7ec7" args="(Lit literal, bool resolveTheoryImplication=true)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a> * Solver::getReason </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>literal</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>resolveTheoryImplication</em> = <code>true</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00950">950</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00278">d_reason</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="minisat__solver_8h_source.html#l00699">getValue()</a>, <a class="el" href="minisat__global_8h_source.html#l00214">MiniSat::l_True</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00999">resolveTheoryImplication()</a>, <a class="el" href="minisat__types_8cpp_source.html#l00063">MiniSat::Clause::TheoryImplication()</a>, and <a class="el" href="minisat__types_8h_source.html#l00069">MiniSat::Lit::var()</a>.</p>
</div>
</div>
<a class="anchor" id="a70a7ffd14675ce9d3f1d445a79505278"></a><!-- doxytag: member="MiniSat::Solver::getClauses" ref="a70a7ffd14675ce9d3f1d445a79505278" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const std::vector<<a class="el" href="classMiniSat_1_1Clause.html">Clause</a>*>& MiniSat::Solver::getClauses </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00722">722</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00303">d_clauses</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00248">createFrom()</a>, and <a class="el" href="dpllt__minisat_8cpp_source.html#l00065">SAT::DPLLTMiniSat::search()</a>.</p>
</div>
</div>
<a class="anchor" id="aadbf5bfce16879745ac1fc7e5226957c"></a><!-- doxytag: member="MiniSat::Solver::getLemmas" ref="aadbf5bfce16879745ac1fc7e5226957c" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const std::vector<<a class="el" href="classMiniSat_1_1Clause.html">Clause</a>*>& MiniSat::Solver::getLemmas </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00725">725</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00306">d_learnts</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00248">createFrom()</a>, and <a class="el" href="dpllt__minisat_8cpp_source.html#l00065">SAT::DPLLTMiniSat::search()</a>.</p>
</div>
</div>
<a class="anchor" id="a16a71aec47f38eed46547c52ca9b152b"></a><!-- doxytag: member="MiniSat::Solver::getTrail" ref="a16a71aec47f38eed46547c52ca9b152b" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const std::vector<<a class="el" href="classMiniSat_1_1Lit.html">Lit</a>>& MiniSat::Solver::getTrail </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00728">728</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00256">d_trail</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00248">createFrom()</a>.</p>
</div>
</div>
<a class="anchor" id="a82e89493435ed86eb83f6af47fc78379"></a><!-- doxytag: member="MiniSat::Solver::getDerivation" ref="a82e89493435ed86eb83f6af47fc78379" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classMiniSat_1_1Derivation.html">Derivation</a>* MiniSat::Solver::getDerivation </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00731">731</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00397">d_derivation</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00488">addClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01091">analyze()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01278">analyze_minimize()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00750">insertClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00190">insertLemma()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00869">remove()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="ac386ec8bbd27857254bae149db775412"></a><!-- doxytag: member="MiniSat::Solver::getStats" ref="ac386ec8bbd27857254bae149db775412" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="structMiniSat_1_1SolverStats.html">SolverStats</a>& MiniSat::Solver::getStats </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Statistics. </p>
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00736">736</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00417">d_stats</a>.</p>
<p>Referenced by <a class="el" href="dpllt__minisat_8cpp_source.html#l00065">SAT::DPLLTMiniSat::search()</a>.</p>
</div>
</div>
<a class="anchor" id="af2bc4c7b90705664cf10982944640b3f"></a><!-- doxytag: member="MiniSat::Solver::nAssigns" ref="af2bc4c7b90705664cf10982944640b3f" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int MiniSat::Solver::nAssigns </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00739">739</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00256">d_trail</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="af57851d84d9e00837b1b09106bf5db27"></a><!-- doxytag: member="MiniSat::Solver::nClauses" ref="af57851d84d9e00837b1b09106bf5db27" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int MiniSat::Solver::nClauses </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00742">742</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00303">d_clauses</a>.</p>
</div>
</div>
<a class="anchor" id="a2beb4ee59904cb55b5b3e69886a0701c"></a><!-- doxytag: member="MiniSat::Solver::nLearnts" ref="a2beb4ee59904cb55b5b3e69886a0701c" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int MiniSat::Solver::nLearnts </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00745">745</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00306">d_learnts</a>.</p>
</div>
</div>
<a class="anchor" id="a679fa13af0d75beca98981dc40f3f2a2"></a><!-- doxytag: member="MiniSat::Solver::nVars" ref="a679fa13af0d75beca98981dc40f3f2a2" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int MiniSat::Solver::nVars </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const<code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00749">749</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00251">d_assigns</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00405">printDIMACS()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00457">registerVar()</a>, <a class="el" href="dpllt__minisat_8cpp_source.html#l00065">SAT::DPLLTMiniSat::search()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02290">varRescaleActivity()</a>.</p>
</div>
</div>
<a class="anchor" id="ac4949ee43735e3de2869ff606ccc197c"></a><!-- doxytag: member="MiniSat::Solver::toString" ref="ac4949ee43735e3de2869ff606ccc197c" args="(Lit literal, bool showAssignment) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string Solver::toString </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classMiniSat_1_1Lit.html">Lit</a> </td>
<td class="paramname"><em>literal</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>showAssignment</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>String representation: </p>
<p>String representation </p>
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00319">319</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00699">getValue()</a>, <a class="el" href="minisat__global_8h_source.html#l00215">MiniSat::l_False</a>, <a class="el" href="minisat__global_8h_source.html#l00214">MiniSat::l_True</a>, and <a class="el" href="minisat__types_8h_source.html#l00082">MiniSat::Lit::toString()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02313">allClausesSatisfied()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02398">checkClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02359">checkWatched()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00405">printDIMACS()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00375">printState()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01937">protocolPropagation()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00334">toString()</a>.</p>
</div>
</div>
<a class="anchor" id="a1fb9f09c66fb11ee96a0761ee2869511"></a><!-- doxytag: member="MiniSat::Solver::toString" ref="a1fb9f09c66fb11ee96a0761ee2869511" args="(const std::vector< Lit > &clause, bool showAssignment) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string Solver::toString </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classMiniSat_1_1Lit.html">Lit</a> > & </td>
<td class="paramname"><em>clause</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>showAssignment</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00334">334</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00319">toString()</a>.</p>
</div>
</div>
<a class="anchor" id="ad18f5b06217e20ca14269eb41264be1f"></a><!-- doxytag: member="MiniSat::Solver::toString" ref="ad18f5b06217e20ca14269eb41264be1f" args="(const Clause &clause, bool showAssignment) const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string Solver::toString </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classMiniSat_1_1Clause.html">Clause</a> & </td>
<td class="paramname"><em>clause</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>showAssignment</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00344">344</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__types_8cpp_source.html#l00072">MiniSat::Clause::toLit()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00319">toString()</a>.</p>
</div>
</div>
<a class="anchor" id="af8254dba6facc2d13c85202d9d09b3f9"></a><!-- doxytag: member="MiniSat::Solver::printState" ref="af8254dba6facc2d13c85202d9d09b3f9" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::printState </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00375">375</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00303">d_clauses</a>, <a class="el" href="minisat__solver_8h_source.html#l00306">d_learnts</a>, <a class="el" href="minisat__solver_8h_source.html#l00256">d_trail</a>, <a class="el" href="minisat__types_8cpp_source.html#l00054">MiniSat::Clause::Decision()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="minisat__solver_8h_source.html#l00715">getReason()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00319">toString()</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02398">checkClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02359">checkWatched()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="ac3d7b1cc4327878d22b91d105ea32409"></a><!-- doxytag: member="MiniSat::Solver::printDIMACS" ref="ac3d7b1cc4327878d22b91d105ea32409" args="() const " -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Solver::printDIMACS </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00405">405</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00303">d_clauses</a>, <a class="el" href="minisat__solver_8h_source.html#l00256">d_trail</a>, <a class="el" href="minisat__types_8cpp_source.html#l00054">MiniSat::Clause::Decision()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="minisat__solver_8h_source.html#l00715">getReason()</a>, <a class="el" href="minisat__solver_8h_source.html#l00749">nVars()</a>, <a class="el" href="minisat__types_8h_source.html#l00133">MiniSat::Clause::size()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00319">toString()</a>, and <a class="el" href="minisat__types_8h_source.html#l00069">MiniSat::Lit::var()</a>.</p>
</div>
</div>
<a class="anchor" id="aac50fbefa27ff761747fe0873722f927"></a><!-- doxytag: member="MiniSat::Solver::curAssigns" ref="aac50fbefa27ff761747fe0873722f927" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector< <a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> > Solver::curAssigns </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00351">351</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00256">d_trail</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, and <a class="el" href="minisat__solver_8h_source.html#l00132">MiniSat::miniSatToCVC()</a>.</p>
<p>Referenced by <a class="el" href="dpllt__minisat_8cpp_source.html#l00215">SAT::DPLLTMiniSat::getCurAssignments()</a>.</p>
</div>
</div>
<a class="anchor" id="afb1410338334a3220d95ec28e5a68f71"></a><!-- doxytag: member="MiniSat::Solver::curClauses" ref="afb1410338334a3220d95ec28e5a68f71" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector< std::vector< <a class="el" href="classSAT_1_1Lit.html">SAT::Lit</a> > > Solver::curClauses </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8cpp_source.html#l00360">360</a> of file <a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a>.</p>
<p>References <a class="el" href="minisat__solver_8h_source.html#l00303">d_clauses</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, and <a class="el" href="minisat__solver_8h_source.html#l00132">MiniSat::miniSatToCVC()</a>.</p>
<p>Referenced by <a class="el" href="dpllt__minisat_8cpp_source.html#l00219">SAT::DPLLTMiniSat::getCurClauses()</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="a160ccfc80ff29cd6947b0d009400e434"></a><!-- doxytag: member="MiniSat::Solver::d_rootLevel" ref="a160ccfc80ff29cd6947b0d009400e434" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const int <a class="el" href="classMiniSat_1_1Solver.html#a160ccfc80ff29cd6947b0d009400e434">MiniSat::Solver::d_rootLevel</a> = 0<code> [static, protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>variables </p>
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00205">205</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02313">allClausesSatisfied()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01091">analyze()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01278">analyze_minimize()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01395">analyze_removable()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01481">backtrack()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02359">checkWatched()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00935">getConflictLevel()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00910">getImplicationLevel()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00750">insertClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00190">insertLemma()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01458">isPermSatisfied()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02641">popTheories()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01689">propagate()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00545">simplifyClause()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l01816">simplifyDB()</a>.</p>
</div>
</div>
<a class="anchor" id="a53dec8ba9fc22afeeef701f1a329a669"></a><!-- doxytag: member="MiniSat::Solver::d_inSearch" ref="a53dec8ba9fc22afeeef701f1a329a669" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classMiniSat_1_1Solver.html#a53dec8ba9fc22afeeef701f1a329a669">MiniSat::Solver::d_inSearch</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>status </p>
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00210">210</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8h_source.html#l00668">inSearch()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a813826a370752a20165602e79b18f7c6"></a><!-- doxytag: member="MiniSat::Solver::d_ok" ref="a813826a370752a20165602e79b18f7c6" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classMiniSat_1_1Solver.html#a813826a370752a20165602e79b18f7c6">MiniSat::Solver::d_ok</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00213">213</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00750">insertClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a431f60a202eee24b3928ca6c6195baa5"></a><!-- doxytag: member="MiniSat::Solver::d_conflict" ref="a431f60a202eee24b3928ca6c6195baa5" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classMiniSat_1_1Clause.html">Clause</a>* <a class="el" href="classMiniSat_1_1Solver.html#a431f60a202eee24b3928ca6c6195baa5">MiniSat::Solver::d_conflict</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00241">241</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01091">analyze()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00750">insertClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00973">isConflicting()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00977">updateConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="a6a3e831d47c15ac42fe7a7002c276c0e"></a><!-- doxytag: member="MiniSat::Solver::d_watches" ref="a6a3e831d47c15ac42fe7a7002c276c0e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<std::vector<<a class="el" href="classMiniSat_1_1Clause.html">Clause</a>*> > <a class="el" href="classMiniSat_1_1Solver.html#a6a3e831d47c15ac42fe7a7002c276c0e">MiniSat::Solver::d_watches</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>variable assignments, and pending propagations </p>
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00248">248</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8h_source.html#l00478">getWatches()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00457">registerVar()</a>.</p>
</div>
</div>
<a class="anchor" id="a8fd906b3d57929f47f9a6eb6740e35e9"></a><!-- doxytag: member="MiniSat::Solver::d_assigns" ref="a8fd906b3d57929f47f9a6eb6740e35e9" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<signed char> <a class="el" href="classMiniSat_1_1Solver.html#a8fd906b3d57929f47f9a6eb6740e35e9">MiniSat::Solver::d_assigns</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00251">251</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01481">backtrack()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02446">checkTrail()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01575">enqueue()</a>, <a class="el" href="minisat__solver_8h_source.html#l00699">getValue()</a>, <a class="el" href="minisat__solver_8h_source.html#l00749">nVars()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01950">propLookahead()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00457">registerVar()</a>.</p>
</div>
</div>
<a class="anchor" id="af092e4552ff6a34e5fcb5f67de96c845"></a><!-- doxytag: member="MiniSat::Solver::d_trail" ref="af092e4552ff6a34e5fcb5f67de96c845" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classMiniSat_1_1Lit.html">Lit</a>> <a class="el" href="classMiniSat_1_1Solver.html#af092e4552ff6a34e5fcb5f67de96c845">MiniSat::Solver::d_trail</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00256">256</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01091">analyze()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01473">assume()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01481">backtrack()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02446">checkTrail()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00351">curAssigns()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01575">enqueue()</a>, <a class="el" href="minisat__solver_8h_source.html#l00728">getTrail()</a>, <a class="el" href="minisat__solver_8h_source.html#l00739">nAssigns()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00405">printDIMACS()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00375">printState()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01689">propagate()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01950">propLookahead()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01937">protocolPropagation()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00457">registerVar()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l01816">simplifyDB()</a>.</p>
</div>
</div>
<a class="anchor" id="abf42fb28430f7b099c65c4e9b28ffb09"></a><!-- doxytag: member="MiniSat::Solver::d_trail_lim" ref="abf42fb28430f7b099c65c4e9b28ffb09" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<int> <a class="el" href="classMiniSat_1_1Solver.html#abf42fb28430f7b099c65c4e9b28ffb09">MiniSat::Solver::d_trail_lim</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00260">260</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01473">assume()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01481">backtrack()</a>, <a class="el" href="minisat__solver_8h_source.html#l00424">decisionLevel()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01950">propLookahead()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a31a1d57eabc2169a4a9fc1cf4c87a2a7"></a><!-- doxytag: member="MiniSat::Solver::d_trail_pos" ref="a31a1d57eabc2169a4a9fc1cf4c87a2a7" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="namespaceMiniSat.html#ad579041894c169fecdeb319f9aa5948d">size_type</a>> <a class="el" href="classMiniSat_1_1Solver.html#a31a1d57eabc2169a4a9fc1cf4c87a2a7">MiniSat::Solver::d_trail_pos</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00264">264</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01278">analyze_minimize()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01481">backtrack()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01575">enqueue()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00457">registerVar()</a>.</p>
</div>
</div>
<a class="anchor" id="a22427732a96158ab53c2ffc61714fca4"></a><!-- doxytag: member="MiniSat::Solver::d_qhead" ref="a22427732a96158ab53c2ffc61714fca4" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceMiniSat.html#ad579041894c169fecdeb319f9aa5948d">size_type</a> <a class="el" href="classMiniSat_1_1Solver.html#a22427732a96158ab53c2ffc61714fca4">MiniSat::Solver::d_qhead</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00269">269</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01481">backtrack()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01689">propagate()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01950">propLookahead()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01937">protocolPropagation()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l01816">simplifyDB()</a>.</p>
</div>
</div>
<a class="anchor" id="ad9d115b0ec2a84ce5ab3f1de19683f06"></a><!-- doxytag: member="MiniSat::Solver::d_thead" ref="ad9d115b0ec2a84ce5ab3f1de19683f06" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceMiniSat.html#ad579041894c169fecdeb319f9aa5948d">size_type</a> <a class="el" href="classMiniSat_1_1Solver.html#ad9d115b0ec2a84ce5ab3f1de19683f06">MiniSat::Solver::d_thead</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00273">273</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01481">backtrack()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01689">propagate()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a4405fbaba3ed712f704d5c85a390b558"></a><!-- doxytag: member="MiniSat::Solver::d_reason" ref="a4405fbaba3ed712f704d5c85a390b558" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classMiniSat_1_1Clause.html">Clause</a>*> <a class="el" href="classMiniSat_1_1Solver.html#a4405fbaba3ed712f704d5c85a390b558">MiniSat::Solver::d_reason</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00278">278</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00671">addClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01481">backtrack()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02446">checkTrail()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01575">enqueue()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00950">getReason()</a>, <a class="el" href="minisat__solver_8h_source.html#l00712">isReason()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01950">propLookahead()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00457">registerVar()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00999">resolveTheoryImplication()</a>.</p>
</div>
</div>
<a class="anchor" id="a34c9afcb69ae37cebbf43a61505009b3"></a><!-- doxytag: member="MiniSat::Solver::d_level" ref="a34c9afcb69ae37cebbf43a61505009b3" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<int> <a class="el" href="classMiniSat_1_1Solver.html#a34c9afcb69ae37cebbf43a61505009b3">MiniSat::Solver::d_level</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00284">284</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8h_source.html#l00703">getLevel()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00457">registerVar()</a>, and <a class="el" href="minisat__solver_8h_source.html#l00707">setLevel()</a>.</p>
</div>
</div>
<a class="anchor" id="afc17e3fc6c5eb525504acbe000d9c5ca"></a><!-- doxytag: member="MiniSat::Solver::d_registeredVars" ref="afc17e3fc6c5eb525504acbe000d9c5ca" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classHash_1_1hash__set.html">Hash::hash_set</a><<a class="el" href="namespaceMiniSat.html#a0d9722420b2afd308dceda22c1b05a5e">Var</a>> > <a class="el" href="classMiniSat_1_1Solver.html#afc17e3fc6c5eb525504acbe000d9c5ca">MiniSat::Solver::d_registeredVars</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00294">294</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00448">isRegistered()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00457">registerVar()</a>.</p>
</div>
</div>
<a class="anchor" id="ad6e3d6a97a4ae9dda9ac7b9bed97bed8"></a><!-- doxytag: member="MiniSat::Solver::d_clauseIDCounter" ref="ad6e3d6a97a4ae9dda9ac7b9bed97bed8" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classMiniSat_1_1Solver.html#ad6e3d6a97a4ae9dda9ac7b9bed97bed8">MiniSat::Solver::d_clauseIDCounter</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Clauses. </p>
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00300">300</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8h_source.html#l00636">nextClauseID()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>.</p>
</div>
</div>
<a class="anchor" id="ae4d0195d229b334f9d9c2f3122e41bd1"></a><!-- doxytag: member="MiniSat::Solver::d_clauses" ref="ae4d0195d229b334f9d9c2f3122e41bd1" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classMiniSat_1_1Clause.html">Clause</a>*> <a class="el" href="classMiniSat_1_1Solver.html#ae4d0195d229b334f9d9c2f3122e41bd1">MiniSat::Solver::d_clauses</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00303">303</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02313">allClausesSatisfied()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02432">checkClauses()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02384">checkWatched()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00360">curClauses()</a>, <a class="el" href="minisat__solver_8h_source.html#l00722">getClauses()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00750">insertClause()</a>, <a class="el" href="minisat__solver_8h_source.html#l00742">nClauses()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00405">printDIMACS()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00375">printState()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01816">simplifyDB()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00292">~Solver()</a>.</p>
</div>
</div>
<a class="anchor" id="a0c9270be1c0980e631de98b3408a8031"></a><!-- doxytag: member="MiniSat::Solver::d_learnts" ref="a0c9270be1c0980e631de98b3408a8031" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classMiniSat_1_1Clause.html">Clause</a>*> <a class="el" href="classMiniSat_1_1Solver.html#a0c9270be1c0980e631de98b3408a8031">MiniSat::Solver::d_learnts</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00306">306</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02432">checkClauses()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02384">checkWatched()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02299">claRescaleActivity()</a>, <a class="el" href="minisat__solver_8h_source.html#l00725">getLemmas()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00750">insertClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00190">insertLemma()</a>, <a class="el" href="minisat__solver_8h_source.html#l00745">nLearnts()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00375">printState()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01781">reduceDB()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01816">simplifyDB()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00292">~Solver()</a>.</p>
</div>
</div>
<a class="anchor" id="adbae4eb042f37351c6cac493e6743813"></a><!-- doxytag: member="MiniSat::Solver::d_pendingClauses" ref="adbae4eb042f37351c6cac493e6743813" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::queue<<a class="el" href="classMiniSat_1_1Clause.html">Clause</a>*> <a class="el" href="classMiniSat_1_1Solver.html#adbae4eb042f37351c6cac493e6743813">MiniSat::Solver::d_pendingClauses</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Temporary clauses. </p>
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00314">314</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01481">backtrack()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00750">insertClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00292">~Solver()</a>.</p>
</div>
</div>
<a class="anchor" id="a587104e3c6bb31d2bc7942bc1fde8b1e"></a><!-- doxytag: member="MiniSat::Solver::d_theoryExplanations" ref="a587104e3c6bb31d2bc7942bc1fde8b1e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::stack<std::pair<int, <a class="el" href="classMiniSat_1_1Clause.html">Clause</a>*> > <a class="el" href="classMiniSat_1_1Solver.html#a587104e3c6bb31d2bc7942bc1fde8b1e">MiniSat::Solver::d_theoryExplanations</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00319">319</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01481">backtrack()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00999">resolveTheoryImplication()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00292">~Solver()</a>.</p>
</div>
</div>
<a class="anchor" id="a6f9c67d77e57b99fef5de801623245a4"></a><!-- doxytag: member="MiniSat::Solver::d_pushes" ref="a6f9c67d77e57b99fef5de801623245a4" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="structMiniSat_1_1PushEntry.html">PushEntry</a>> <a class="el" href="classMiniSat_1_1Solver.html#a6f9c67d77e57b99fef5de801623245a4">MiniSat::Solver::d_pushes</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Push / Pop. </p>
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00325">325</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01278">analyze_minimize()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02630">doPops()</a>, <a class="el" href="minisat__solver_8h_source.html#l00692">inPush()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01443">isImpliedAt()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a99b8d67e03c83f148906ff00e8e88851"></a><!-- doxytag: member="MiniSat::Solver::d_popLemmas" ref="a99b8d67e03c83f148906ff00e8e88851" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classMiniSat_1_1Clause.html">Clause</a>*> <a class="el" href="classMiniSat_1_1Solver.html#a99b8d67e03c83f148906ff00e8e88851">MiniSat::Solver::d_popLemmas</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00328">328</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>.</p>
</div>
</div>
<a class="anchor" id="ab0b2d4e87d57046e30c2cb3554925e2b"></a><!-- doxytag: member="MiniSat::Solver::d_pushIDs" ref="ab0b2d4e87d57046e30c2cb3554925e2b" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<int> <a class="el" href="classMiniSat_1_1Solver.html#ab0b2d4e87d57046e30c2cb3554925e2b">MiniSat::Solver::d_pushIDs</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00343">343</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8h_source.html#l00540">getPushID()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00457">registerVar()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02496">setPushID()</a>.</p>
</div>
</div>
<a class="anchor" id="acb6671d85d64f00c04ea17b3b6e144f6"></a><!-- doxytag: member="MiniSat::Solver::d_popRequests" ref="acb6671d85d64f00c04ea17b3b6e144f6" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned int <a class="el" href="classMiniSat_1_1Solver.html#acb6671d85d64f00c04ea17b3b6e144f6">MiniSat::Solver::d_popRequests</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00350">350</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02630">doPops()</a>, <a class="el" href="minisat__solver_8h_source.html#l00692">inPush()</a>, <a class="el" href="minisat__solver_8h_source.html#l00668">inSearch()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02621">requestPop()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a5b10958ebb6b146f8cfb2d6ec08ab667"></a><!-- doxytag: member="MiniSat::Solver::d_cla_inc" ref="a5b10958ebb6b146f8cfb2d6ec08ab667" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">double <a class="el" href="classMiniSat_1_1Solver.html#a5b10958ebb6b146f8cfb2d6ec08ab667">MiniSat::Solver::d_cla_inc</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>heuristics </p>
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00359">359</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8h_source.html#l00558">claBumpActivity()</a>, <a class="el" href="minisat__solver_8h_source.html#l00556">claDecayActivity()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02299">claRescaleActivity()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00248">createFrom()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l01781">reduceDB()</a>.</p>
</div>
</div>
<a class="anchor" id="a3b0e8d36281ddcfefb54812accad5a55"></a><!-- doxytag: member="MiniSat::Solver::d_cla_decay" ref="a3b0e8d36281ddcfefb54812accad5a55" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">double <a class="el" href="classMiniSat_1_1Solver.html#a3b0e8d36281ddcfefb54812accad5a55">MiniSat::Solver::d_cla_decay</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00361">361</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8h_source.html#l00556">claDecayActivity()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a0765ad8a98718bb5523e487e32d66ae1"></a><!-- doxytag: member="MiniSat::Solver::d_activity" ref="a0765ad8a98718bb5523e487e32d66ae1" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<double> <a class="el" href="classMiniSat_1_1Solver.html#a0765ad8a98718bb5523e487e32d66ae1">MiniSat::Solver::d_activity</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00366">366</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00248">createFrom()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00457">registerVar()</a>, <a class="el" href="minisat__solver_8h_source.html#l00550">varBumpActivity()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02290">varRescaleActivity()</a>.</p>
</div>
</div>
<a class="anchor" id="aa9cba0f1df8f31b5ae94f2ce0ccb290f"></a><!-- doxytag: member="MiniSat::Solver::d_var_inc" ref="aa9cba0f1df8f31b5ae94f2ce0ccb290f" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">double <a class="el" href="classMiniSat_1_1Solver.html#aa9cba0f1df8f31b5ae94f2ce0ccb290f">MiniSat::Solver::d_var_inc</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00368">368</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00248">createFrom()</a>, <a class="el" href="minisat__solver_8h_source.html#l00550">varBumpActivity()</a>, <a class="el" href="minisat__solver_8h_source.html#l00554">varDecayActivity()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02290">varRescaleActivity()</a>.</p>
</div>
</div>
<a class="anchor" id="a354cacc000d52901cb2a60d1fe659d26"></a><!-- doxytag: member="MiniSat::Solver::d_var_decay" ref="a354cacc000d52901cb2a60d1fe659d26" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">double <a class="el" href="classMiniSat_1_1Solver.html#a354cacc000d52901cb2a60d1fe659d26">MiniSat::Solver::d_var_decay</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00371">371</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>, <a class="el" href="minisat__solver_8h_source.html#l00550">varBumpActivity()</a>, and <a class="el" href="minisat__solver_8h_source.html#l00554">varDecayActivity()</a>.</p>
</div>
</div>
<a class="anchor" id="aab79cd4bf5792f72c191d8149e77bc93"></a><!-- doxytag: member="MiniSat::Solver::d_order" ref="aab79cd4bf5792f72c191d8149e77bc93" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classMiniSat_1_1VarOrder.html">VarOrder</a> <a class="el" href="classMiniSat_1_1Solver.html#aab79cd4bf5792f72c191d8149e77bc93">MiniSat::Solver::d_order</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00373">373</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01481">backtrack()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01950">propLookahead()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00457">registerVar()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>, and <a class="el" href="minisat__solver_8h_source.html#l00550">varBumpActivity()</a>.</p>
</div>
</div>
<a class="anchor" id="ac114e23a9bd1329c9002eb758c1595b7"></a><!-- doxytag: member="MiniSat::Solver::d_simpDB_assigns" ref="ac114e23a9bd1329c9002eb758c1595b7" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classMiniSat_1_1Solver.html#ac114e23a9bd1329c9002eb758c1595b7">MiniSat::Solver::d_simpDB_assigns</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00378">378</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01689">propagate()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l01816">simplifyDB()</a>.</p>
</div>
</div>
<a class="anchor" id="a4f2b0a42acb3d470ca9500b2f4fd8077"></a><!-- doxytag: member="MiniSat::Solver::d_simpDB_props" ref="a4f2b0a42acb3d470ca9500b2f4fd8077" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int64_t <a class="el" href="classMiniSat_1_1Solver.html#a4f2b0a42acb3d470ca9500b2f4fd8077">MiniSat::Solver::d_simpDB_props</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00380">380</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01689">propagate()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l01816">simplifyDB()</a>.</p>
</div>
</div>
<a class="anchor" id="ac380f5046f3dddbb0bdebf4107d8d506"></a><!-- doxytag: member="MiniSat::Solver::d_simpRD_learnts" ref="ac380f5046f3dddbb0bdebf4107d8d506" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classMiniSat_1_1Solver.html#ac380f5046f3dddbb0bdebf4107d8d506">MiniSat::Solver::d_simpRD_learnts</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00382">382</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01781">reduceDB()</a>.</p>
</div>
</div>
<a class="anchor" id="a8336c93fe51668a8cd322f9a059d5137"></a><!-- doxytag: member="MiniSat::Solver::d_theoryAPI" ref="a8336c93fe51668a8cd322f9a059d5137" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1DPLLT_1_1TheoryAPI.html">SAT::DPLLT::TheoryAPI</a>* <a class="el" href="classMiniSat_1_1Solver.html#a8336c93fe51668a8cd322f9a059d5137">MiniSat::Solver::d_theoryAPI</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>CVC interface. </p>
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00388">388</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01481">backtrack()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00248">createFrom()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02641">popTheories()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01689">propagate()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a18b5a09a43e43ae4bde40537e652e987"></a><!-- doxytag: member="MiniSat::Solver::d_decider" ref="a18b5a09a43e43ae4bde40537e652e987" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classSAT_1_1DPLLT_1_1Decider.html">SAT::DPLLT::Decider</a>* <a class="el" href="classMiniSat_1_1Solver.html#a18b5a09a43e43ae4bde40537e652e987">MiniSat::Solver::d_decider</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00391">391</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l00248">createFrom()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="ad2d7fa92335dfd68f8598a5a41d17e93"></a><!-- doxytag: member="MiniSat::Solver::d_derivation" ref="ad2d7fa92335dfd68f8598a5a41d17e93" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classMiniSat_1_1Derivation.html">Derivation</a>* <a class="el" href="classMiniSat_1_1Solver.html#ad2d7fa92335dfd68f8598a5a41d17e93">MiniSat::Solver::d_derivation</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>proof logging </p>
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00397">397</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01481">backtrack()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00248">createFrom()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01575">enqueue()</a>, <a class="el" href="minisat__solver_8h_source.html#l00731">getDerivation()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00457">registerVar()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00158">Solver()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00292">~Solver()</a>.</p>
</div>
</div>
<a class="anchor" id="aece892bd1701b50038331c77b70d0949"></a><!-- doxytag: member="MiniSat::Solver::d_default_params" ref="aece892bd1701b50038331c77b70d0949" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="structMiniSat_1_1SearchParams.html">SearchParams</a> <a class="el" href="classMiniSat_1_1Solver.html#aece892bd1701b50038331c77b70d0949">MiniSat::Solver::d_default_params</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Mode of operation: </p>
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00403">403</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>.</p>
</div>
</div>
<a class="anchor" id="a4ecef2c87d4be7bf5a0ba8b4e800e09c"></a><!-- doxytag: member="MiniSat::Solver::d_expensive_ccmin" ref="a4ecef2c87d4be7bf5a0ba8b4e800e09c" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classMiniSat_1_1Solver.html#a4ecef2c87d4be7bf5a0ba8b4e800e09c">MiniSat::Solver::d_expensive_ccmin</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00406">406</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01278">analyze_minimize()</a>.</p>
</div>
</div>
<a class="anchor" id="ae2fd56e35cc318aed56d10fc7e5af484"></a><!-- doxytag: member="MiniSat::Solver::d_analyze_seen" ref="ae2fd56e35cc318aed56d10fc7e5af484" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<char> <a class="el" href="classMiniSat_1_1Solver.html#ae2fd56e35cc318aed56d10fc7e5af484">MiniSat::Solver::d_analyze_seen</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Temporaries (to reduce allocation overhead). </p>
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00412">412</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01091">analyze()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01278">analyze_minimize()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01395">analyze_removable()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l00457">registerVar()</a>.</p>
</div>
</div>
<a class="anchor" id="aede680f26ad5344891484b6f821de222"></a><!-- doxytag: member="MiniSat::Solver::d_analyze_stack" ref="aede680f26ad5344891484b6f821de222" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classMiniSat_1_1Lit.html">Lit</a>> <a class="el" href="classMiniSat_1_1Solver.html#aede680f26ad5344891484b6f821de222">MiniSat::Solver::d_analyze_stack</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00413">413</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01395">analyze_removable()</a>.</p>
</div>
</div>
<a class="anchor" id="a81ed0225fec06bae415c6d86c86781f1"></a><!-- doxytag: member="MiniSat::Solver::d_analyze_redundant" ref="a81ed0225fec06bae415c6d86c86781f1" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classMiniSat_1_1Lit.html">Lit</a>> <a class="el" href="classMiniSat_1_1Solver.html#a81ed0225fec06bae415c6d86c86781f1">MiniSat::Solver::d_analyze_redundant</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00414">414</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01091">analyze()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01278">analyze_minimize()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l01395">analyze_removable()</a>.</p>
</div>
</div>
<a class="anchor" id="ac2c0d8b62a85616add0930b4947c8f96"></a><!-- doxytag: member="MiniSat::Solver::d_stats" ref="ac2c0d8b62a85616add0930b4947c8f96" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="structMiniSat_1_1SolverStats.html">SolverStats</a> <a class="el" href="classMiniSat_1_1Solver.html#ac2c0d8b62a85616add0930b4947c8f96">MiniSat::Solver::d_stats</a><code> [protected]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="minisat__solver_8h_source.html#l00417">417</a> of file <a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a>.</p>
<p>Referenced by <a class="el" href="minisat__solver_8cpp_source.html#l01473">assume()</a>, <a class="el" href="minisat__solver_8h_source.html#l00736">getStats()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00750">insertClause()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00190">insertLemma()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02668">pop()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01689">propagate()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02510">push()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l01781">reduceDB()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l00869">remove()</a>, <a class="el" href="minisat__solver_8cpp_source.html#l02005">search()</a>, and <a class="el" href="minisat__solver_8cpp_source.html#l01816">simplifyDB()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="minisat__solver_8h_source.html">minisat_solver.h</a></li>
<li><a class="el" href="minisat__solver_8cpp_source.html">minisat_solver.cpp</a></li>
</ul>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
