<!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: Fast Search Engine</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><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#nested-classes">Classes</a> |
<a href="#func-members">Functions</a> |
<a href="#var-members">Variables</a> |
<a href="#friend-members">Friends</a> </div>
<div class="headertitle">
<div class="title">Fast Search Engine</div> </div>
<div class="ingroups"><a class="el" href="group__SE.html">Search Engine</a></div></div>
<div class="contents">
<h2><a name="nested-classes"></a>
Classes</h2>
<ul>
<li>class <a class="el" href="classCVC3_1_1SearchEngineFast.html">CVC3::SearchEngineFast</a>
<dl class="el"><dd class="mdescRight">Implementation of a faster search engine, using newer techniques. <a href="classCVC3_1_1SearchEngineFast.html#details">More...</a><br/></dl><li>class <a class="el" href="classCVC3_1_1SearchEngineFast_1_1ConflictClauseManager.html">CVC3::SearchEngineFast::ConflictClauseManager</a>
</ul>
<h2><a name="func-members"></a>
Functions</h2>
<ul>
<li>std::vector< std::pair< <a class="el" href="classCVC3_1_1Clause.html">Clause</a>, <br class="typebreak"/>
int > > & <a class="el" href="group__SE__Fast.html#ga8f4353c8f8c65ed00806861471bd857f">CVC3::SearchEngineFast::wp</a> (const <a class="el" href="classCVC3_1_1Literal.html">Literal</a> &literal)
<dl class="el"><dd class="mdescRight">Return a ref to the vector of watched literals. If no such vector exists, create it. <a href="#ga8f4353c8f8c65ed00806861471bd857f"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="el" href="group__SE__Fast.html#gac68652e5ed46a097f846ba9a86fcd630">CVC3::SearchEngineFast::checkSAT</a> ()
<li>bool <a class="el" href="group__SE__Fast.html#ga6d05128f71cc4e239030fe0434cda727">CVC3::SearchEngineFast::split</a> ()
<dl class="el"><dd class="mdescRight">Choose a splitter. <a href="#ga6d05128f71cc4e239030fe0434cda727"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__SE__Fast.html#ga711544b769f4c0a5713df247de927019">CVC3::SearchEngineFast::findSplitter</a> ()
<dl class="el"><dd class="mdescRight">Returns a splitter. <a href="#ga711544b769f4c0a5713df247de927019"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#gadf72861b6482f6c585f3199d1436f7be">CVC3::SearchEngineFast::clearLiterals</a> ()
<dl class="el"><dd class="mdescRight">Clear the list of asserted literals (d_literals) <a href="#gadf72861b6482f6c585f3199d1436f7be"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#ga453b1d390ee3b7af68fe8e915443d1ad">CVC3::SearchEngineFast::updateLitScores</a> (bool firstTime)
<li>void <a class="el" href="group__SE__Fast.html#ga775b06e155128cc8817f254bc293c6c6">CVC3::SearchEngineFast::updateLitCounts</a> (const <a class="el" href="classCVC3_1_1Clause.html">Clause</a> &c)
<dl class="el"><dd class="mdescRight">Add the literals of a new clause to d_litsByScores. <a href="#ga775b06e155128cc8817f254bc293c6c6"></a><br/></dl><li>bool <a class="el" href="group__SE__Fast.html#gac6d49471ba5c76fffc7581e01e423218">CVC3::SearchEngineFast::bcp</a> ()
<dl class="el"><dd class="mdescRight">Boolean constraint propagation. <a href="#gac6d49471ba5c76fffc7581e01e423218"></a><br/></dl><li>bool <a class="el" href="group__SE__Fast.html#ga4490cc372993398612e7556e14222ff3">CVC3::SearchEngineFast::fixConflict</a> ()
<dl class="el"><dd class="mdescRight">Determines backtracking level and adds conflict clauses. <a href="#ga4490cc372993398612e7556e14222ff3"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#gaf7daf6eac739438b5b25175bc7d63a71">CVC3::SearchEngineFast::assertAssumptions</a> ()
<dl class="el"><dd class="mdescRight">FIXME: document this. <a href="#gaf7daf6eac739438b5b25175bc7d63a71"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#ga2c71aa94289db9ece678963617660640">CVC3::SearchEngineFast::enqueueFact</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<dl class="el"><dd class="mdescRight">Queue up a fact to assert to the DPs later. <a href="#ga2c71aa94289db9ece678963617660640"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#ga33ff53b3eeb9811b1510fffd3cdcf234">CVC3::SearchEngineFast::setInconsistent</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<dl class="el"><dd class="mdescRight">Set the context inconsistent. Takes Theorem(FALSE). <a href="#ga33ff53b3eeb9811b1510fffd3cdcf234"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#ga6d190905fefb2a36650306e5b577dd9a">CVC3::SearchEngineFast::commitFacts</a> ()
<dl class="el"><dd class="mdescRight">Commit all the enqueued facts to the DPs. <a href="#ga6d190905fefb2a36650306e5b577dd9a"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#gafa7937cc0b7d14c0aafb1f9c20abf011">CVC3::SearchEngineFast::clearFacts</a> ()
<dl class="el"><dd class="mdescRight">Clear the local fact queue. <a href="#gafa7937cc0b7d14c0aafb1f9c20abf011"></a><br/></dl><li>bool <a class="el" href="group__SE__Fast.html#gad7548d572241f215212176af0216cb94">CVC3::SearchEngineFast::propagate</a> (const <a class="el" href="classCVC3_1_1Clause.html">Clause</a> &c, int idx, bool &wpUpdated)
<dl class="el"><dd class="mdescRight">Auxiliary function for unit propagation. <a href="#gad7548d572241f215212176af0216cb94"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#ga88d524fb175ae8156696cc73cb182ffd">CVC3::SearchEngineFast::unitPropagation</a> (const <a class="el" href="classCVC3_1_1Clause.html">Clause</a> &c, unsigned idx)
<dl class="el"><dd class="mdescRight">Do the unit propagation for the clause. <a href="#ga88d524fb175ae8156696cc73cb182ffd"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#gaac9cb2de28ec162fe5ecfe042ad7b101">CVC3::SearchEngineFast::analyzeUIPs</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &falseThm, int conflictScope)
<dl class="el"><dd class="mdescRight">Analyse the conflict, find the UIPs, etc. <a href="#gaac9cb2de28ec162fe5ecfe042ad7b101"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#ga6e64b8f0a42bd4b42d22b50b351219c9">CVC3::SearchEngineFast::addNewClause</a> (<a class="el" href="classCVC3_1_1Clause.html">Clause</a> &c)
<dl class="el"><dd class="mdescRight">Go through all the clauses and check the watch pointers (for debugging) <a href="#ga6e64b8f0a42bd4b42d22b50b351219c9"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#ga2ec0e19a01ac0926b690c50a3206c5a3">CVC3::SearchEngineFast::recordFact</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<dl class="el"><dd class="mdescRight">Process a new derived fact (auxiliary function) <a href="#ga2ec0e19a01ac0926b690c50a3206c5a3"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#gab3f2a42375c5b3875ad18acd47ee124d">CVC3::SearchEngineFast::traceConflict</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &conflictThm)
<dl class="el"><dd class="mdescRight">First pass in conflict analysis; takes a theorem of FALSE. <a href="#gab3f2a42375c5b3875ad18acd47ee124d"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="el" href="group__SE__Fast.html#gaac7ba666d67d3d4808642c5c7858db95">CVC3::SearchEngineFast::checkValidMain</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e2)
<dl class="el"><dd class="mdescRight">Private helper function for checkValid and restart. <a href="#gaac7ba666d67d3d4808642c5c7858db95"></a><br/></dl><li><a class="el" href="group__SE__Fast.html#ga8869c248ac69ea02656c95b40c99ed24">CVC3::SearchEngineFast::SearchEngineFast</a> (<a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> *core)
<dl class="el"><dd class="mdescRight">The main Constructor. <a href="#ga8869c248ac69ea02656c95b40c99ed24"></a><br/></dl><li>virtual <a class="el" href="group__SE__Fast.html#ga8f8c0138aa4f31355dad949f604e3927">CVC3::SearchEngineFast::~SearchEngineFast</a> ()
<dl class="el"><dd class="mdescRight">Destructor. <a href="#ga8f8c0138aa4f31355dad949f604e3927"></a><br/></dl><li>const std::string & <a class="el" href="group__SE__Fast.html#ga3f564001c310c9e4ff519da68f8ea670">CVC3::SearchEngineFast::getName</a> ()
<dl class="el"><dd class="mdescRight">Name of this search engine. <a href="#ga3f564001c310c9e4ff519da68f8ea670"></a><br/></dl><li>virtual <a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="el" href="group__SE__Fast.html#ga1db688bc99f93a978079b3d2efd1bd9f">CVC3::SearchEngineFast::checkValidInternal</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Implementation of the API call. <a href="#ga1db688bc99f93a978079b3d2efd1bd9f"></a><br/></dl><li>virtual <a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="el" href="group__SE__Fast.html#ga99dd1f1c52ecae319bd0b5a3b689a31d">CVC3::SearchEngineFast::restartInternal</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Reruns last check with e as an additional assumption. <a href="#ga99dd1f1c52ecae319bd0b5a3b689a31d"></a><br/></dl><li>virtual void <a class="el" href="group__SE__Fast.html#ga104e5e0abacb4c9492b0cb818b7d968a">CVC3::SearchEngineFast::getCounterExample</a> (std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &assertions)
<dl class="el"><dd class="mdescRight">Redefine the counterexample generation. <a href="#ga104e5e0abacb4c9492b0cb818b7d968a"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#gaef3113afb8dc9ea1b06217ab77f5d713">CVC3::SearchEngineFast::addLiteralFact</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<dl class="el"><dd class="mdescRight">Notify the search engine about a new literal fact. <a href="#gaef3113afb8dc9ea1b06217ab77f5d713"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#ga03501a968c3c7122a999b1f57d6640a0">CVC3::SearchEngineFast::addNonLiteralFact</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<dl class="el"><dd class="mdescRight">Notify the search engine about a new non-literal fact. <a href="#ga03501a968c3c7122a999b1f57d6640a0"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="group__SE__Fast.html#gaf54422149559aa048f32723a3dc6fcce">CVC3::SearchEngineFast::newIntAssumption</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Redefine <a class="el" href="group__SE__Fast.html#gaf54422149559aa048f32723a3dc6fcce" title="Redefine newIntAssumption(): we need to add the new theorem to the appropriate Literal.">newIntAssumption()</a>: we need to add the new theorem to the appropriate <a class="el" href="classCVC3_1_1Literal.html">Literal</a>. <a href="#gaf54422149559aa048f32723a3dc6fcce"></a><br/></dl><li>virtual bool <a class="el" href="group__SE__Fast.html#ga4b55b5f49d921ca4b63f874d8404c4d5">CVC3::SearchEngineFast::isAssumption</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Check if the formula has been assumed. <a href="#ga4b55b5f49d921ca4b63f874d8404c4d5"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#ga40b361c2f9374c541282feca1e237dba">CVC3::SearchEngineFast::addSplitter</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int priority)
<dl class="el"><dd class="mdescRight">Suggest a splitter to the <a class="el" href="classCVC3_1_1SearchEngine.html" title="API to to a generic proof search engine.">SearchEngine</a>. <a href="#ga40b361c2f9374c541282feca1e237dba"></a><br/></dl></ul>
<h2><a name="var-members"></a>
Variables</h2>
<ul>
<li>std::string <a class="el" href="group__SE__Fast.html#ga91ff4e54d0b66c31eb0d2653fad650cb">CVC3::SearchEngineFast::d_name</a>
<dl class="el"><dd class="mdescRight">Name. <a href="#ga91ff4e54d0b66c31eb0d2653fad650cb"></a><br/></dl><li>DecisionEngine * <a class="el" href="group__SE__Fast.html#gafa042a51f718c312ea7728f175958e35">CVC3::SearchEngineFast::d_decisionEngine</a>
<dl class="el"><dd class="mdescRight">Decision Engine. <a href="#gafa042a51f718c312ea7728f175958e35"></a><br/></dl><li>StatCounter <a class="el" href="group__SE__Fast.html#ga29e749a0ca7cbe86118a0d72e02e0696">CVC3::SearchEngineFast::d_unitPropCount</a>
<dl class="el"><dd class="mdescRight">Total number of unit propagations. <a href="#ga29e749a0ca7cbe86118a0d72e02e0696"></a><br/></dl><li>StatCounter <a class="el" href="group__SE__Fast.html#ga749d335e3d18b71aa951d37e943fbf50">CVC3::SearchEngineFast::d_circuitPropCount</a>
<dl class="el"><dd class="mdescRight">Total number of circuit propagations. <a href="#ga749d335e3d18b71aa951d37e943fbf50"></a><br/></dl><li>StatCounter <a class="el" href="group__SE__Fast.html#gaecd7cc2115fe235653a62acf93ccb1e5">CVC3::SearchEngineFast::d_conflictCount</a>
<dl class="el"><dd class="mdescRight">Total number of conflicts. <a href="#gaecd7cc2115fe235653a62acf93ccb1e5"></a><br/></dl><li>StatCounter <a class="el" href="group__SE__Fast.html#ga483cb3c4c889013b03e2c923977d4ae5">CVC3::SearchEngineFast::d_conflictClauseCount</a>
<dl class="el"><dd class="mdescRight">Total number of conflict clauses generated (not all may be active) <a href="#ga483cb3c4c889013b03e2c923977d4ae5"></a><br/></dl><li>CDList< ClauseOwner > <a class="el" href="group__SE__Fast.html#gaa1dd9a29eac4c7da6c669d7888909ca5">CVC3::SearchEngineFast::d_clauses</a>
<dl class="el"><dd class="mdescRight">Backtrackable list of clauses. <a href="#gaa1dd9a29eac4c7da6c669d7888909ca5"></a><br/></dl><li>CDMap< Expr, Theorem > <a class="el" href="group__SE__Fast.html#gabe8dbaf4592793c49cd58ff93a897a06">CVC3::SearchEngineFast::d_unreportedLits</a>
<dl class="el"><dd class="mdescRight">Backtrackable set of pending unprocessed literals. <a href="#gabe8dbaf4592793c49cd58ff93a897a06"></a><br/></dl><li>CDMap< Expr, bool > <a class="el" href="group__SE__Fast.html#ga8217149b882d328384bd7a04a5e5c5f3">CVC3::SearchEngineFast::d_unreportedLitsHandled</a>
<li>CDList< SmartCDO< Theorem > > <a class="el" href="group__SE__Fast.html#ga07c8e260b60d83042c97453892a15f38">CVC3::SearchEngineFast::d_nonLiterals</a>
<dl class="el"><dd class="mdescRight">Backtrackable list of non-literals (non-CNF formulas). <a href="#ga07c8e260b60d83042c97453892a15f38"></a><br/></dl><li>CDMap< Expr, Theorem > <a class="el" href="group__SE__Fast.html#gae88240871407db238ad8c6a795ba6b91">CVC3::SearchEngineFast::d_nonLiteralsSaved</a>
<dl class="el"><dd class="mdescRight">prevent reprocessing <a href="#gae88240871407db238ad8c6a795ba6b91"></a><br/></dl><li>CDO< Theorem > <a class="el" href="group__SE__Fast.html#gaa8b578a017bcddd578e943add44c2940">CVC3::SearchEngineFast::d_simplifiedThm</a>
<dl class="el"><dd class="mdescRight"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> which records simplification of the last query. <a href="#gaa8b578a017bcddd578e943add44c2940"></a><br/></dl><li>CDO< unsigned > <a class="el" href="group__SE__Fast.html#gae4a9e9926613365979d36e2a98769381">CVC3::SearchEngineFast::d_nonlitQueryStart</a>
<dl class="el"><dd class="mdescRight">Size of d_nonLiterals before most recent query. <a href="#gae4a9e9926613365979d36e2a98769381"></a><br/></dl><li>CDO< unsigned > <a class="el" href="group__SE__Fast.html#ga8472c82be89057f32c68a0f0423215a2">CVC3::SearchEngineFast::d_nonlitQueryEnd</a>
<dl class="el"><dd class="mdescRight">Size of d_nonLiterals after query (not including DP-generated non-literals) <a href="#ga8472c82be89057f32c68a0f0423215a2"></a><br/></dl><li>CDO< unsigned > <a class="el" href="group__SE__Fast.html#ga71a2e31fe2a16420a416b5aeced09455">CVC3::SearchEngineFast::d_clausesQueryStart</a>
<dl class="el"><dd class="mdescRight">Size of d_clauses before most recent query. <a href="#ga71a2e31fe2a16420a416b5aeced09455"></a><br/></dl><li>CDO< unsigned > <a class="el" href="group__SE__Fast.html#ga6dbfd2cd66dee5634f096593f26c47e7">CVC3::SearchEngineFast::d_clausesQueryEnd</a>
<dl class="el"><dd class="mdescRight">Size of d_clauses after query. <a href="#ga6dbfd2cd66dee5634f096593f26c47e7"></a><br/></dl><li>std::vector< std::deque<br class="typebreak"/>
< ClauseOwner > * > <a class="el" href="group__SE__Fast.html#ga8e96b8f24bd89c190e561f387a4a30ee">CVC3::SearchEngineFast::d_conflictClauseStack</a>
<dl class="el"><dd class="mdescRight">Array of conflict clauses: one deque for each outstanding query. <a href="#ga8e96b8f24bd89c190e561f387a4a30ee"></a><br/></dl><li>std::deque< ClauseOwner > * <a class="el" href="group__SE__Fast.html#gad79601e3b2032aee4d23dc4bbd785fc3">CVC3::SearchEngineFast::d_conflictClauses</a>
<dl class="el"><dd class="mdescRight">Reference to top deque of conflict clauses. <a href="#gad79601e3b2032aee4d23dc4bbd785fc3"></a><br/></dl><li>ConflictClauseManager <a class="el" href="group__SE__Fast.html#gaab577b22f09d51b9b15954b9a529c05d">CVC3::SearchEngineFast::d_conflictClauseManager</a>
<li>std::vector< Clause > <a class="el" href="group__SE__Fast.html#gad05f577d00e93fefed74eb0c19015090">CVC3::SearchEngineFast::d_unitConflictClauses</a>
<dl class="el"><dd class="mdescRight">Unprocessed unit conflict clauses. <a href="#gad05f577d00e93fefed74eb0c19015090"></a><br/></dl><li>std::vector< Literal > <a class="el" href="group__SE__Fast.html#gaa6a69bd3df4bb72abd1e9b0fe868fc0d">CVC3::SearchEngineFast::d_literals</a>
<dl class="el"><dd class="mdescRight">Set of literals to be processed by bcp. <a href="#gaa6a69bd3df4bb72abd1e9b0fe868fc0d"></a><br/></dl><li>CDMap< Expr, Literal > <a class="el" href="group__SE__Fast.html#gaf720bf50e81fc4e2561b587d97ec2839">CVC3::SearchEngineFast::d_literalSet</a>
<dl class="el"><dd class="mdescRight">Set of asserted literals which may survive accross <a class="el" href="group__SE.html#ga83d82b8cf43e9dc8240e762b180f6343" title="Similar to checkValidInternal(), only returns Theorem(e) or Null.">checkValid()</a> calls. <a href="#gaf720bf50e81fc4e2561b587d97ec2839"></a><br/></dl><li>std::vector< Theorem > <a class="el" href="group__SE__Fast.html#ga4b05dccebac3de019dc112ab3dffc988">CVC3::SearchEngineFast::d_factQueue</a>
<dl class="el"><dd class="mdescRight">Queue of derived facts to be sent to DPs. <a href="#ga4b05dccebac3de019dc112ab3dffc988"></a><br/></dl><li>bool <a class="el" href="group__SE__Fast.html#gaa1ea8707c10a13a631402860eff87026">CVC3::SearchEngineFast::d_useEnqueueFact</a>
<dl class="el"><dd class="mdescRight">When true, use <a class="el" href="classCVC3_1_1TheoryCore.html#a479141bc26a125b758a2acc6420274f9" title="Enqueue a new fact.">TheoryCore::enqueueFact()</a> instead of <a class="el" href="group__SE.html#gac6e807418fb26dee354f7f934eb432ba" title="Add a new fact to the search engine from the core.">addFact()</a> in <a class="el" href="group__SE__Fast.html#ga6d190905fefb2a36650306e5b577dd9a" title="Commit all the enqueued facts to the DPs.">commitFacts()</a> <a href="#gaa1ea8707c10a13a631402860eff87026"></a><br/></dl><li>bool <a class="el" href="group__SE__Fast.html#ga6368ec56b20c12896000e370bbb4a3b6">CVC3::SearchEngineFast::d_inCheckSAT</a>
<dl class="el"><dd class="mdescRight">True when <a class="el" href="group__SE__Fast.html#gac68652e5ed46a097f846ba9a86fcd630">checkSAT()</a> is running. <a href="#ga6368ec56b20c12896000e370bbb4a3b6"></a><br/></dl><li>CDList< Literal > <a class="el" href="group__SE__Fast.html#ga0214c0205e48fd792c4d01d3428cd333">CVC3::SearchEngineFast::d_litsAlive</a>
<dl class="el"><dd class="mdescRight">Set of alive literals that shouldn't be garbage-collected. <a href="#ga0214c0205e48fd792c4d01d3428cd333"></a><br/></dl><li>std::vector< Circuit * > <a class="el" href="group__SE__Fast.html#ga5db32a771408c468676e407075184b64">CVC3::SearchEngineFast::d_circuits</a>
<dl class="el"><dd class="mdescRight">Mappings of literals to vectors of pointers to the corresponding watched literals. <a href="#ga5db32a771408c468676e407075184b64"></a><br/></dl><li>ExprHashMap< std::vector<br class="typebreak"/>
< Circuit * > > <a class="el" href="group__SE__Fast.html#ga84bfa366c43221ba288e0a1bd716efc6">CVC3::SearchEngineFast::d_circuitsByExpr</a>
<li>int <a class="el" href="group__SE__Fast.html#gab27227ee9e005ab22a9e2a251bc7c6d1">CVC3::SearchEngineFast::d_lastConflictScope</a>
<dl class="el"><dd class="mdescRight">The scope of the last conflict. <a href="#gab27227ee9e005ab22a9e2a251bc7c6d1"></a><br/></dl><li>Clause <a class="el" href="group__SE__Fast.html#ga46e91bb5d782794c6dca6abaa99dc4f9">CVC3::SearchEngineFast::d_lastConflictClause</a>
<dl class="el"><dd class="mdescRight">The last conflict clause (for <a class="el" href="group__SE__Fast.html#gac68652e5ed46a097f846ba9a86fcd630">checkSAT()</a>). May be Null. <a href="#ga46e91bb5d782794c6dca6abaa99dc4f9"></a><br/></dl><li>Theorem <a class="el" href="group__SE__Fast.html#gae961b4fb4bb059a1d867447fc487aaee">CVC3::SearchEngineFast::d_conflictTheorem</a>
<dl class="el"><dd class="mdescRight">Theorem(FALSE) which generated a conflict. <a href="#gae961b4fb4bb059a1d867447fc487aaee"></a><br/></dl><li>unsigned <a class="el" href="group__SE__Fast.html#gad80c2b69b88a04c8c78309859abd3f76">CVC3::SearchEngineFast::d_litsMaxScorePos</a>
<dl class="el"><dd class="mdescRight">Position of a literal with max score in d_litsByScores. <a href="#gad80c2b69b88a04c8c78309859abd3f76"></a><br/></dl><li>std::vector< Literal > <a class="el" href="group__SE__Fast.html#ga57c1c1e58ebd2c1d23a57db97880fbbc">CVC3::SearchEngineFast::d_litsByScores</a>
<dl class="el"><dd class="mdescRight">Vector of literals sorted by score. <a href="#ga57c1c1e58ebd2c1d23a57db97880fbbc"></a><br/></dl><li>int <a class="el" href="group__SE__Fast.html#ga52c9c181bcd623a36ab594e0ee16a67e">CVC3::SearchEngineFast::d_splitterCount</a>
<dl class="el"><dd class="mdescRight">Internal splitter counter for delaying <a class="el" href="group__SE__Fast.html#ga453b1d390ee3b7af68fe8e915443d1ad">updateLitScores()</a> <a href="#ga52c9c181bcd623a36ab594e0ee16a67e"></a><br/></dl><li>int <a class="el" href="group__SE__Fast.html#ga2d54fdadc1b167dbbb366e37e0b97a58">CVC3::SearchEngineFast::d_litSortCount</a>
<dl class="el"><dd class="mdescRight">Internal (decrementing) count of added splitters, to sort d_litByScores. <a href="#ga2d54fdadc1b167dbbb366e37e0b97a58"></a><br/></dl><li>const bool <a class="el" href="group__SE__Fast.html#ga3877f82445d777c19c60b6ec117335e2">CVC3::SearchEngineFast::d_berkminFlag</a>
<dl class="el"><dd class="mdescRight">Flag to switch on/off the berkmin heuristic. <a href="#ga3877f82445d777c19c60b6ec117335e2"></a><br/></dl></ul>
<h2><a name="friend-members"></a>
Friends</h2>
<ul>
<li>class <a class="el" href="group__SE__Fast.html#ga771f251de98c5689b33e123d5603722d">CVC3::SearchEngineFast::ConflictClauseManager</a>
<dl class="el"><dd class="mdescRight">Helper class for managing conflict clauses. <a href="#ga771f251de98c5689b33e123d5603722d"></a><br/></dl></ul>
<h2><a name="member-group"></a>
Processing a Conflict</h2>
<ul>
<li>Theorem <a class="el" href="group__SE__Fast.html#ga2535b1eabb9eb7e7f3a6197dbb377cb4">CVC3::SearchEngineFast::processConflict</a> (const Literal &l)
<dl class="el"><dd class="mdescRight">Take a conflict in the form of <a class="el" href="classCVC3_1_1Literal.html">Literal</a>, or <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>, and generate all the necessary conflict clauses. <a href="#ga2535b1eabb9eb7e7f3a6197dbb377cb4"></a><br/></dl><li>Theorem <a class="el" href="group__SE__Fast.html#ga3a60df36c6707139c0f6662f32270765">CVC3::SearchEngineFast::processConflict</a> (const Theorem &thm)
<dl class="el"><dd class="mdescRight">Take a conflict in the form of <a class="el" href="classCVC3_1_1Literal.html">Literal</a>, or <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>, and generate all the necessary conflict clauses. <a href="#ga3a60df36c6707139c0f6662f32270765"></a><br/></dl></ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<p>This module includes all the components of the fast search engine. </p>
<hr/><h2>Function Documentation</h2>
<a class="anchor" id="ga8f4353c8f8c65ed00806861471bd857f"></a><!-- doxytag: member="CVC3::SearchEngineFast::wp" ref="ga8f4353c8f8c65ed00806861471bd857f" args="(const Literal &literal)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">vector< std::pair< <a class="el" href="classCVC3_1_1Clause.html">Clause</a>, int > > & SearchEngineFast::wp </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Literal.html">Literal</a> & </td>
<td class="paramname"><em>literal</em></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Return a ref to the vector of watched literals. If no such vector exists, create it. </p>
<p>This function is normally used when the value of 'literal' becomes false. The vector contains pointers to all clauses where this literal occurs, and therefore, these clauses may cause unit propagation. In any case, the watch pointers in these clauses need to be updated. </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l00136">136</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00176">CVC3::Literal::wp()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01069">CVC3::SearchEngineFast::addNewClause()</a>, <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00816">CVC3::SearchEngineFast::propagate()</a>.</p>
</div>
</div>
<a class="anchor" id="gac68652e5ed46a097f846ba9a86fcd630"></a><!-- doxytag: member="CVC3::SearchEngineFast::checkSAT" ref="gac68652e5ed46a097f846ba9a86fcd630" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> SearchEngineFast::checkSAT </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<dl class="return"><dt><b>Returns:</b></dt><dd>true if <a class="el" href="namespaceSAT.html">SAT</a>, false otherwise.</dd></dl>
<p>When false is returned, proof is saved in d_lastConflictTheorem </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l00186">186</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="queryresult_8h_source.html#l00037">CVC3::ABORT</a>, <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="search__fast_8h_source.html#l00097">CVC3::SearchEngineFast::d_decisionEngine</a>, <a class="el" href="search__fast_8h_source.html#l00189">CVC3::SearchEngineFast::d_factQueue</a>, <a class="el" href="search__fast_8h_source.html#l00198">CVC3::SearchEngineFast::d_inCheckSAT</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>, <a class="el" href="group__DE.html#ga7910d09d94bd27c02f53a3f7e0a9af00">CVC3::DecisionEngine::goalSatisfied()</a>, <a class="el" href="theory__core_8h_source.html#l00435">CVC3::TheoryCore::incomplete()</a>, <a class="el" href="theory__core_8h_source.html#l00492">CVC3::TheoryCore::outOfResources()</a>, <a class="el" href="queryresult_8h_source.html#l00033">CVC3::SATISFIABLE</a>, <a class="el" href="search__fast_8cpp_source.html#l00254">CVC3::SearchEngineFast::split()</a>, <a class="el" href="queryresult_8h_source.html#l00038">CVC3::UNKNOWN</a>, and <a class="el" href="queryresult_8h_source.html#l00036">CVC3::UNSATISFIABLE</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>.</p>
</div>
</div>
<a class="anchor" id="ga6d05128f71cc4e239030fe0434cda727"></a><!-- doxytag: member="CVC3::SearchEngineFast::split" ref="ga6d05128f71cc4e239030fe0434cda727" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool SearchEngineFast::split </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Choose a splitter. </p>
<p>Preconditions: The current context is consistent.</p>
<dl class="return"><dt><b>Returns:</b></dt><dd>true if splitter available, and it asserts it through <a class="el" href="group__SE__Fast.html#gaf54422149559aa048f32723a3dc6fcce" title="Redefine newIntAssumption(): we need to add the new theorem to the appropriate Literal.">newIntAssumption()</a> after first pushing a new context.</dd>
<dd>
false if no splitters are available, which means the context is <a class="el" href="namespaceSAT.html">SAT</a>.</dd></dl>
<p>Postconditions: A literal has been asserted through <a class="el" href="group__SE__Fast.html#gaf54422149559aa048f32723a3dc6fcce" title="Redefine newIntAssumption(): we need to add the new theorem to the appropriate Literal.">newIntAssumption()</a>. </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l00254">254</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="theory__core_8cpp_source.html#l03468">CVC3::TheoryCore::addFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l01530">CVC3::SearchEngineFast::addLiteralFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, <a class="el" href="theory__core_8cpp_source.html#l03507">CVC3::TheoryCore::checkSATCore()</a>, <a class="el" href="statistics_8h_source.html#l00163">CVC3::Statistics::counter()</a>, <a class="el" href="search_8h_source.html#l00061">CVC3::SearchEngine::d_commonRules</a>, <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="search__fast_8h_source.html#l00097">CVC3::SearchEngineFast::d_decisionEngine</a>, <a class="el" href="search__fast_8h_source.html#l00176">CVC3::SearchEngineFast::d_literals</a>, <a class="el" href="search__fast_8h_source.html#l00270">CVC3::SearchEngineFast::d_splitterCount</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="variable_8h_source.html#l00164">CVC3::Literal::deriveTheorem()</a>, <a class="el" href="search__fast_8cpp_source.html#l00438">CVC3::SearchEngineFast::findSplitter()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="theory__core_8h_source.html#l00351">CVC3::TheoryCore::getStatistics()</a>, <a class="el" href="variable_8h_source.html#l00144">CVC3::Literal::getValue()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a11b56754024b56844336954cf789a63a">CVC3::CommonProofRules::iffFalseElim()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#ad2edb920405666bf6e9d21ae496ff6b3">CVC3::CommonProofRules::iffTrueElim()</a>, <a class="el" href="theory__core_8h_source.html#l00422">CVC3::TheoryCore::inconsistent()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="expr_8h_source.html#l00357">CVC3::Expr::isBoolConst()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="expr_8h_source.html#l01223">CVC3::Expr::isNull()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>, <a class="el" href="search__impl__base_8h_source.html#l00120">CVC3::SearchImplBase::newLiteral()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#ace6786234994faf89bc1b0ac8575278a">CVC3::CommonProofRules::notNotElim()</a>, <a class="el" href="decision__engine_8cpp_source.html#l00128">CVC3::DecisionEngine::pushDecision()</a>, <a class="el" href="theory__core_8cpp_source.html#l00184">CVC3::TheoryCore::simplify()</a>, <a class="el" href="variable_8cpp_source.html#l00211">CVC3::Literal::toString()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, and <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00186">CVC3::SearchEngineFast::checkSAT()</a>.</p>
</div>
</div>
<a class="anchor" id="ga711544b769f4c0a5713df247de927019"></a><!-- doxytag: member="CVC3::SearchEngineFast::findSplitter" ref="ga711544b769f4c0a5713df247de927019" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> SearchEngineFast::findSplitter </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Returns a splitter. </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l00438">438</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="search__fast_8h_source.html#l00275">CVC3::SearchEngineFast::d_berkminFlag</a>, <a class="el" href="search__fast_8h_source.html#l00141">CVC3::SearchEngineFast::d_conflictClauses</a>, <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="search__fast_8h_source.html#l00097">CVC3::SearchEngineFast::d_decisionEngine</a>, <a class="el" href="search__fast_8h_source.html#l00260">CVC3::SearchEngineFast::d_litsByScores</a>, <a class="el" href="search__fast_8h_source.html#l00258">CVC3::SearchEngineFast::d_litsMaxScorePos</a>, <a class="el" href="search__fast_8h_source.html#l00122">CVC3::SearchEngineFast::d_nonLiterals</a>, <a class="el" href="search__fast_8h_source.html#l00270">CVC3::SearchEngineFast::d_splitterCount</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="group__DE.html#ga6f191a7f4edb645e8df7c1f005a50bf8">CVC3::DecisionEngine::findSplitter()</a>, <a class="el" href="variable_8h_source.html#l00140">CVC3::Literal::getExpr()</a>, <a class="el" href="variable_8h_source.html#l00144">CVC3::Literal::getValue()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="expr_8h_source.html#l00357">CVC3::Expr::isBoolConst()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00711">CVC3::SearchImplBase::isGoodSplitter()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>, <a class="el" href="variable_8h_source.html#l00168">CVC3::Literal::score()</a>, <a class="el" href="theory_8h_source.html#l00430">CVC3::Theory::simplifyExpr()</a>, <a class="el" href="cdlist_8h_source.html#l00064">CVC3::CDList< T >::size()</a>, <a class="el" href="clause_8h_source.html#l00113">CVC3::Clause::size()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>, and <a class="el" href="search__fast_8cpp_source.html#l00345">CVC3::SearchEngineFast::updateLitScores()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00254">CVC3::SearchEngineFast::split()</a>.</p>
</div>
</div>
<a class="anchor" id="gadf72861b6482f6c585f3199d1436f7be"></a><!-- doxytag: member="CVC3::SearchEngineFast::clearLiterals" ref="gadf72861b6482f6c585f3199d1436f7be" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineFast::clearLiterals </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Clear the list of asserted literals (d_literals) </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l00631">631</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="search__fast_8h_source.html#l00176">CVC3::SearchEngineFast::d_literals</a>, and <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="ga453b1d390ee3b7af68fe8e915443d1ad"></a><!-- doxytag: member="CVC3::SearchEngineFast::updateLitScores" ref="ga453b1d390ee3b7af68fe8e915443d1ad" args="(bool firstTime)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineFast::updateLitScores </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>firstTime</em></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Recompute the scores for all known literals. This is a relatively expensive procedure, so it should not be called too often. Currently, it is called once per 100 splitters. </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l00345">345</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00169">CVC3::Literal::added()</a>, <a class="el" href="search__fast_8cpp_source.html#l00323">compareLits()</a>, <a class="el" href="variable_8h_source.html#l00166">CVC3::Literal::count()</a>, <a class="el" href="variable_8h_source.html#l00167">CVC3::Literal::countPrev()</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="search__fast_8cpp_source.html#l00039">followChaff</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="variable_8h_source.html#l00168">CVC3::Literal::score()</a>, <a class="el" href="variable_8cpp_source.html#l00211">CVC3::Literal::toString()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00438">CVC3::SearchEngineFast::findSplitter()</a>.</p>
</div>
</div>
<a class="anchor" id="ga775b06e155128cc8817f254bc293c6c6"></a><!-- doxytag: member="CVC3::SearchEngineFast::updateLitCounts" ref="ga775b06e155128cc8817f254bc293c6c6" args="(const Clause &c)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineFast::updateLitCounts </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Clause.html">Clause</a> & </td>
<td class="paramname"><em>c</em></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Add the literals of a new clause to d_litsByScores. </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l00412">412</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="variable_8h_source.html#l00169">CVC3::Literal::added()</a>, <a class="el" href="search__fast_8cpp_source.html#l00323">compareLits()</a>, <a class="el" href="search__fast_8h_source.html#l00260">CVC3::SearchEngineFast::d_litsByScores</a>, <a class="el" href="search__fast_8h_source.html#l00272">CVC3::SearchEngineFast::d_litSortCount</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="variable_8h_source.html#l00140">CVC3::Literal::getExpr()</a>, <a class="el" href="expr_8h_source.html#l00406">CVC3::Expr::isAbsLiteral()</a>, <a class="el" href="clause_8h_source.html#l00113">CVC3::Clause::size()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, and <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01069">CVC3::SearchEngineFast::addNewClause()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>.</p>
</div>
</div>
<a class="anchor" id="gac6d49471ba5c76fffc7581e01e423218"></a><!-- doxytag: member="CVC3::SearchEngineFast::bcp" ref="gac6d49471ba5c76fffc7581e01e423218" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool SearchEngineFast::bcp </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Boolean constraint propagation. </p>
<p>Preconditions: On every run besides the first, the CNF clause database must not have any unit or unsat clauses, and there must be a literal queued up for processing. The current context must be consistent. Any and all assertions and assignments must actually be made within the bcp loop. Other parts of the solver may queue new facts with <a class="el" href="group__SE__Fast.html#gaef3113afb8dc9ea1b06217ab77f5d713" title="Notify the search engine about a new literal fact.">addLiteralFact()</a> and <a class="el" href="group__SE__Fast.html#ga03501a968c3c7122a999b1f57d6640a0" title="Notify the search engine about a new non-literal fact.">addNonLiteralFact()</a>. <a class="el" href="group__SE__Fast.html#gac6d49471ba5c76fffc7581e01e423218" title="Boolean constraint propagation.">bcp()</a> will either process them, or it will find a conflict, in which case they will no longer be valid and will be dumped. Any nonLiterals must already be simplified.</p>
<p>Description: BCP will systematically work through all the literals and nonliterals, using boolean constraint propagation by detecting unit clauses and using <a class="el" href="group__SE__Fast.html#gaef3113afb8dc9ea1b06217ab77f5d713" title="Notify the search engine about a new literal fact.">addLiteralFact()</a> on the unit literal while also marking the clause as <a class="el" href="namespaceSAT.html">SAT</a>. Any clauses marked <a class="el" href="namespaceSAT.html">SAT</a> are guaranteed to be <a class="el" href="namespaceSAT.html">SAT</a>, but clauses not marked <a class="el" href="namespaceSAT.html">SAT</a> are not guaranteed to be unsat.</p>
<dl class="return"><dt><b>Returns:</b></dt><dd>false if a conflict is found, true otherwise.</dd></dl>
<p>Postconditions: False indicates conflict. If the conflict was discovered in CNF, we call the proof rule, then store that clause pointer so <a class="el" href="group__SE__Fast.html#ga4490cc372993398612e7556e14222ff3" title="Determines backtracking level and adds conflict clauses.">fixConflict()</a> can skip over it during the search (when we finally change dependency tracking).</p>
<p>True indicates success. All literals and nonLiterals have been processed without causing a conflict. Processing nonliterals implies running simplify on them, immediately asserting any simplifications back to the core, and marking the original nonLiteral as simplified, to be ignored by all future (this context or deeper) splitters and bcp runs. Therefore, there will be no unsimplified nonliterals remaining. </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l00637">637</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="search__fast_8cpp_source.html#l01063">CVC3::SearchEngineFast::clearFacts()</a>, <a class="el" href="search__fast_8cpp_source.html#l00631">CVC3::SearchEngineFast::clearLiterals()</a>, <a class="el" href="search__fast_8cpp_source.html#l01050">CVC3::SearchEngineFast::commitFacts()</a>, <a class="el" href="search__fast_8h_source.html#l00215">CVC3::SearchEngineFast::d_circuitsByExpr</a>, <a class="el" href="search_8h_source.html#l00061">CVC3::SearchEngine::d_commonRules</a>, <a class="el" href="search__fast_8h_source.html#l00229">CVC3::SearchEngineFast::d_conflictTheorem</a>, <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="search__fast_8h_source.html#l00189">CVC3::SearchEngineFast::d_factQueue</a>, <a class="el" href="search__fast_8h_source.html#l00176">CVC3::SearchEngineFast::d_literals</a>, <a class="el" href="search__fast_8h_source.html#l00205">CVC3::SearchEngineFast::d_litsAlive</a>, <a class="el" href="search__fast_8h_source.html#l00122">CVC3::SearchEngineFast::d_nonLiterals</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="clause_8h_source.html#l00212">CVC3::Clause::deleted()</a>, <a class="el" href="search__fast_8cpp_source.html#l01031">CVC3::SearchEngineFast::enqueueFact()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="variable_8h_source.html#l00140">CVC3::Literal::getExpr()</a>, <a class="el" href="theory__core_8h_source.html#l00350">CVC3::TheoryCore::getFlags()</a>, <a class="el" href="variable_8h_source.html#l00144">CVC3::Literal::getValue()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="theory__core_8h_source.html#l00422">CVC3::TheoryCore::inconsistent()</a>, <a class="el" href="theory__core_8h_source.html#l00425">CVC3::TheoryCore::inconsistentThm()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="expr_8h_source.html#l00406">CVC3::Expr::isAbsLiteral()</a>, <a class="el" href="expr_8h_source.html#l00429">CVC3::Expr::isExists()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>, <a class="el" href="search__fast_8cpp_source.html#l00816">CVC3::SearchEngineFast::propagate()</a>, <a class="el" href="cdlist_8h_source.html#l00066">CVC3::CDList< T >::push_back()</a>, <a class="el" href="clause_8h_source.html#l00187">CVC3::Clause::sat()</a>, <a class="el" href="search__impl__base_8h_source.html#l00192">CVC3::SearchImplBase::scopeLevel()</a>, <a class="el" href="search__fast_8cpp_source.html#l01043">CVC3::SearchEngineFast::setInconsistent()</a>, <a class="el" href="search__impl__base_8h_source.html#l00124">CVC3::SearchImplBase::simplify()</a>, <a class="el" href="cdlist_8h_source.html#l00064">CVC3::CDList< T >::size()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a015539886185195ba5d98c60cd7e8f66">CVC3::CommonProofRules::skolemize()</a>, <a class="el" href="variable_8cpp_source.html#l00211">CVC3::Literal::toString()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>, <a class="el" href="clause_8h_source.html#l00151">CVC3::Clause::watched()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00136">CVC3::SearchEngineFast::wp()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01530">CVC3::SearchEngineFast::addLiteralFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l00186">CVC3::SearchEngineFast::checkSAT()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00254">CVC3::SearchEngineFast::split()</a>.</p>
</div>
</div>
<a class="anchor" id="ga4490cc372993398612e7556e14222ff3"></a><!-- doxytag: member="CVC3::SearchEngineFast::fixConflict" ref="ga4490cc372993398612e7556e14222ff3" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool SearchEngineFast::fixConflict </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Determines backtracking level and adds conflict clauses. </p>
<p>Preconditions: The current context is inconsistent. If it resulted from a conflictRule() application, then the theorem is stored inside d_lastConflictTheorem.</p>
<p>If this was caused from bcp, we obtain the conflictRule() theorem from the d_lastConflictTheorem instance variable. From here we build conflict clauses and determine the correct backtracking level, at which point we actually backtrack there. Finally, we also call <a class="el" href="group__SE__Fast.html#gaef3113afb8dc9ea1b06217ab77f5d713" title="Notify the search engine about a new literal fact.">addLiteralFact()</a> on the "failure
driven assertion" literal so that bcp has some place to begin (and it satisfies the bcp preconditions)</p>
<p>Postconditions: If True is returned: The current context is consistent, and a literal is queued up for bcp to process. If False is returned: The context cannot be made consistent without backtracking past the original one, so the formula is unsat. </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l00939">939</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="search__fast_8cpp_source.html#l00631">CVC3::SearchEngineFast::clearLiterals()</a>, <a class="el" href="search__fast_8cpp_source.html#l01050">CVC3::SearchEngineFast::commitFacts()</a>, <a class="el" href="search__impl__base_8h_source.html#l00049">CVC3::SearchImplBase::d_bottomScope</a>, <a class="el" href="search_8h_source.html#l00061">CVC3::SearchEngine::d_commonRules</a>, <a class="el" href="search__fast_8h_source.html#l00103">CVC3::SearchEngineFast::d_conflictCount</a>, <a class="el" href="search__fast_8h_source.html#l00229">CVC3::SearchEngineFast::d_conflictTheorem</a>, <a class="el" href="search__fast_8h_source.html#l00097">CVC3::SearchEngineFast::d_decisionEngine</a>, <a class="el" href="search__fast_8h_source.html#l00227">CVC3::SearchEngineFast::d_lastConflictClause</a>, <a class="el" href="search__fast_8h_source.html#l00220">CVC3::SearchEngineFast::d_lastConflictScope</a>, <a class="el" href="search__fast_8h_source.html#l00258">CVC3::SearchEngineFast::d_litsMaxScorePos</a>, <a class="el" href="search__fast_8h_source.html#l00169">CVC3::SearchEngineFast::d_unitConflictClauses</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="search__fast_8cpp_source.html#l01031">CVC3::SearchEngineFast::enqueueFact()</a>, <a class="el" href="variable_8h_source.html#l00140">CVC3::Literal::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00486">CVC3::Theorem::getScope()</a>, <a class="el" href="clause_8h_source.html#l00117">CVC3::Clause::getTheorem()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#aebbcd4a194e4fdca0bcd16143fb03a75">CVC3::CommonProofRules::iffMP()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="expr_8h_source.html#l01223">CVC3::Expr::isNull()</a>, <a class="el" href="clause_8h_source.html#l00111">CVC3::Clause::isNull()</a>, <a class="el" href="expr_8h_source.html#l00422">CVC3::Expr::isOr()</a>, <a class="el" href="decision__engine_8cpp_source.html#l00157">CVC3::DecisionEngine::popTo()</a>, <a class="el" href="theorem_8h_source.html#l00140">CVC3::Theorem::printDebug()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#aa3cfb7d47a6d6bc84c85c7fa6a3e1242">CVC3::CommonProofRules::rewriteOr()</a>, <a class="el" href="search__impl__base_8h_source.html#l00192">CVC3::SearchImplBase::scopeLevel()</a>, <a class="el" href="clause_8h_source.html#l00113">CVC3::Clause::size()</a>, <a class="el" href="variable_8cpp_source.html#l00211">CVC3::Literal::toString()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>, <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00915">CVC3::SearchEngineFast::unitPropagation()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00186">CVC3::SearchEngineFast::checkSAT()</a>.</p>
</div>
</div>
<a class="anchor" id="gaf7daf6eac739438b5b25175bc7d63a71"></a><!-- doxytag: member="CVC3::SearchEngineFast::assertAssumptions" ref="gaf7daf6eac739438b5b25175bc7d63a71" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::SearchEngineFast::assertAssumptions </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>FIXME: document this. </p>
</div>
</div>
<a class="anchor" id="ga2c71aa94289db9ece678963617660640"></a><!-- doxytag: member="CVC3::SearchEngineFast::enqueueFact" ref="ga2c71aa94289db9ece678963617660640" args="(const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineFast::enqueueFact </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Queue up a fact to assert to the DPs later. </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l01031">1031</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="search__fast_8cpp_source.html#l01530">CVC3::SearchEngineFast::addLiteralFact()</a>, <a class="el" href="search__fast_8h_source.html#l00189">CVC3::SearchEngineFast::d_factQueue</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00482">CVC3::Theorem::isAbsLiteral()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, and <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00915">CVC3::SearchEngineFast::unitPropagation()</a>.</p>
</div>
</div>
<a class="anchor" id="ga33ff53b3eeb9811b1510fffd3cdcf234"></a><!-- doxytag: member="CVC3::SearchEngineFast::setInconsistent" ref="ga33ff53b3eeb9811b1510fffd3cdcf234" args="(const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineFast::setInconsistent </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Set the context inconsistent. Takes Theorem(FALSE). </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l01043">1043</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="search__fast_8h_source.html#l00189">CVC3::SearchEngineFast::d_factQueue</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="theory__core_8cpp_source.html#l04245">CVC3::TheoryCore::setInconsistent()</a>, and <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01530">CVC3::SearchEngineFast::addLiteralFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l01445">CVC3::SearchEngineFast::addNonLiteralFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00549">CVC3::SearchEngineFast::recordFact()</a>.</p>
</div>
</div>
<a class="anchor" id="ga6d190905fefb2a36650306e5b577dd9a"></a><!-- doxytag: member="CVC3::SearchEngineFast::commitFacts" ref="ga6d190905fefb2a36650306e5b577dd9a" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineFast::commitFacts </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Commit all the enqueued facts to the DPs. </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l01050">1050</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="theory__core_8cpp_source.html#l03468">CVC3::TheoryCore::addFact()</a>, <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="search__fast_8h_source.html#l00189">CVC3::SearchEngineFast::d_factQueue</a>, <a class="el" href="search__fast_8h_source.html#l00193">CVC3::SearchEngineFast::d_useEnqueueFact</a>, <a class="el" href="theory__core_8cpp_source.html#l04213">CVC3::TheoryCore::enqueueFact()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="gafa7937cc0b7d14c0aafb1f9c20abf011"></a><!-- doxytag: member="CVC3::SearchEngineFast::clearFacts" ref="gafa7937cc0b7d14c0aafb1f9c20abf011" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineFast::clearFacts </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Clear the local fact queue. </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l01063">1063</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="search__fast_8h_source.html#l00189">CVC3::SearchEngineFast::d_factQueue</a>, and <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>.</p>
</div>
</div>
<a class="anchor" id="ga2535b1eabb9eb7e7f3a6197dbb377cb4"></a><!-- doxytag: member="CVC3::SearchEngineFast::processConflict" ref="ga2535b1eabb9eb7e7f3a6197dbb377cb4" args="(const Literal &l)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">Theorem CVC3::SearchEngineFast::processConflict </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Literal.html">Literal</a> & </td>
<td class="paramname"><em>l</em></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Take a conflict in the form of <a class="el" href="classCVC3_1_1Literal.html">Literal</a>, or <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>, and generate all the necessary conflict clauses. </p>
</div>
</div>
<a class="anchor" id="ga3a60df36c6707139c0f6662f32270765"></a><!-- doxytag: member="CVC3::SearchEngineFast::processConflict" ref="ga3a60df36c6707139c0f6662f32270765" args="(const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">Theorem CVC3::SearchEngineFast::processConflict </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Take a conflict in the form of <a class="el" href="classCVC3_1_1Literal.html">Literal</a>, or <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>, and generate all the necessary conflict clauses. </p>
</div>
</div>
<a class="anchor" id="gad7548d572241f215212176af0216cb94"></a><!-- doxytag: member="CVC3::SearchEngineFast::propagate" ref="gad7548d572241f215212176af0216cb94" args="(const Clause &c, int idx, bool &wpUpdated)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool SearchEngineFast::propagate </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Clause.html">Clause</a> & </td>
<td class="paramname"><em>c</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>idx</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool & </td>
<td class="paramname"><em>wpUpdated</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Auxiliary function for unit propagation. </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l00816">816</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="group__SE__Rules.html#ga9c74425b4471d411f58f16781951c441">CVC3::SearchEngineRules::conflictRule()</a>, <a class="el" href="search__fast_8h_source.html#l00229">CVC3::SearchEngineFast::d_conflictTheorem</a>, <a class="el" href="search_8h_source.html#l00064">CVC3::SearchEngine::d_rules</a>, <a class="el" href="search__fast_8h_source.html#l00099">CVC3::SearchEngineFast::d_unitPropCount</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="clause_8h_source.html#l00168">CVC3::Clause::dir()</a>, <a class="el" href="variable_8h_source.html#l00140">CVC3::Literal::getExpr()</a>, <a class="el" href="clause_8h_source.html#l00117">CVC3::Clause::getTheorem()</a>, <a class="el" href="variable_8h_source.html#l00144">CVC3::Literal::getValue()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="expr_8h_source.html#l00406">CVC3::Expr::isAbsLiteral()</a>, <a class="el" href="clause_8h_source.html#l00207">CVC3::Clause::markSat()</a>, <a class="el" href="clause_8h_source.html#l00113">CVC3::Clause::size()</a>, <a class="el" href="clause_8cpp_source.html#l00184">CVC3::CompactClause::toString()</a>, <a class="el" href="clause_8cpp_source.html#l00129">CVC3::Clause::toString()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>, <a class="el" href="search__fast_8cpp_source.html#l00915">CVC3::SearchEngineFast::unitPropagation()</a>, <a class="el" href="clause_8h_source.html#l00151">CVC3::Clause::watched()</a>, <a class="el" href="search__fast_8cpp_source.html#l00136">CVC3::SearchEngineFast::wp()</a>, and <a class="el" href="clause_8h_source.html#l00143">CVC3::Clause::wp()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>.</p>
</div>
</div>
<a class="anchor" id="ga88d524fb175ae8156696cc73cb182ffd"></a><!-- doxytag: member="CVC3::SearchEngineFast::unitPropagation" ref="ga88d524fb175ae8156696cc73cb182ffd" args="(const Clause &c, unsigned idx)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineFast::unitPropagation </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Clause.html">Clause</a> & </td>
<td class="paramname"><em>c</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">unsigned </td>
<td class="paramname"><em>idx</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Do the unit propagation for the clause. </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l00915">915</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="search__fast_8h_source.html#l00176">CVC3::SearchEngineFast::d_literals</a>, <a class="el" href="search_8h_source.html#l00064">CVC3::SearchEngine::d_rules</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="search__fast_8cpp_source.html#l01031">CVC3::SearchEngineFast::enqueueFact()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="clause_8h_source.html#l00117">CVC3::Clause::getTheorem()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="theorem_8cpp_source.html#l00482">CVC3::Theorem::isAbsLiteral()</a>, <a class="el" href="search__impl__base_8h_source.html#l00120">CVC3::SearchImplBase::newLiteral()</a>, <a class="el" href="clause_8h_source.html#l00113">CVC3::Clause::size()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="clause_8cpp_source.html#l00129">CVC3::Clause::toString()</a>, and <a class="el" href="group__SE__Rules.html#gae7221bb8b77313a9b53a4beca9cc0aa0">CVC3::SearchEngineRules::unitProp()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00816">CVC3::SearchEngineFast::propagate()</a>.</p>
</div>
</div>
<a class="anchor" id="gaac9cb2de28ec162fe5ecfe042ad7b101"></a><!-- doxytag: member="CVC3::SearchEngineFast::analyzeUIPs" ref="gaac9cb2de28ec162fe5ecfe042ad7b101" args="(const Theorem &falseThm, int conflictScope)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineFast::analyzeUIPs </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>falseThm</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>conflictScope</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Analyse the conflict, find the UIPs, etc. </p>
<p><b>Finding UIPs (Unique Implication Pointers)</b></p>
<p>This is basically the same as finding hammocks of the subset of the implication graph composed of only the nodes from the current scope. A hammock is a portion of the graph which has a single source and/or sink such that removing that single node makes the graph disconnected.</p>
<p>Conceptually, the algorithm maintains four sets of nodes: literals (named <em>lits</em>), gamma, fringe, and pending. Literals are nodes whose expressions will become literals in the conflict clause of the current hammock, and the nodes in gamma are assumptions from which such conflict clause theorem is derived. Nodes in fringe are intermediate nodes which are ready to be "expanded" (see the algorithm description below). The pending nodes are those which are not yet ready to be processed (they later become literal or fringe nodes).</p>
<p>These sets are maintained as vectors, and are updated in such a way that the nodes in the vectors never repeat. The exception is the pending set, for which only a size counter is maintained. A node belongs to the pending set if it has been visited (isFlagged() method), and its fan-out count is non-zero (stored in the cache, getCachedValue()). In other words, pending nodes are those that have been visited, but not sufficient number of times.</p>
<p>Also, fringe is maintained as a pair of vectors. One vector is always the current fringe, and the other one is built when the current is processed. When processing of the current fringe is finished, it is cleared, and the other vector becomes the current fringe (that is, they swap roles).</p>
<p>A node is expanded if it is marked for expansion (getExpandFlag()). If its fan-out count is not yet zero, it is added to the set of pending nodes.</p>
<p>If a node has a literal flag (getLitFlag()), it goes into literals when its fan-out count reaches zero. Since this will be the last time the node is visited, it is added to the vector only once.</p>
<p>A node neither marked for expansion nor with the literal flag goes into the gamma set. It is added the first time the node is visited (isFlagged() returns false), and therefore, is added to the vector only once. This is an important distinction from the other sets, since a gamma-node may be used by several conflict clauses.</p>
<p>Clearing the gamma set after each UIP requires both clearing the vector and resetting all flags (clearAllFlags()).</p>
<p><b>The algorithm</b></p>
<ol>
<li>
<p class="startli">Initially, the fringe contains exactly the predecessors of falseThm from the current scope which are ready to be expanded (fan-out count is zero). All the other predecessors of falseThm go to the appropriate sets of literals, gamma, and pending.</p>
<p class="endli"></p>
</li>
<li>
<p class="startli">If fringe.size() <= 1 and the set of pending nodes is empty, then the element in the fringe (if it's non-empty) is a UIP. Generate a conflict clause from the UIP and the literals (using gamma as the set of assumptions), empty the sets, and continue with the next step. Note, that the UIP remains in the fringe, and will be expanded in the next step.</p>
<p>The important exception: if the only element in the fringe is marked for expansion, then this is a false UIP (the <a class="el" href="namespaceSAT.html">SAT</a> solver doesn't know about this node), and it should not appear in the conflict clause. In this case, simply proceed to step 3 as if nothing happened.</p>
<p class="endli"></p>
</li>
<li>
<p class="startli">If fringe.size()==0, stop (the set of pending nodes must also be empty at this point). Otherwise, for *every* node in the fringe, decrement the fan-out for each of its predecessors, and empty the fringe. Take the predecessors from the current scope, and add those to the fringe for which fan-out count is zero, and remove them from the set of pending nodes. Add the other predecessors from the current scope to the set of pending nodes. Add the remaining predecessors (not from the current scope) to the literals or gamma, as appropriate. Continue with step 2.</p>
<p class="endli"></p>
</li>
</ol>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l01266">1266</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00151">CVC3::Assumptions::begin()</a>, <a class="el" href="theorem_8cpp_source.html#l00422">CVC3::Theorem::clearAllFlags()</a>, <a class="el" href="group__SE__Rules.html#ga03be39f8ffe84a1bcc09bba60f45245c">CVC3::SearchEngineRules::conflictClause()</a>, <a class="el" href="search__impl__base_8h_source.html#l00049">CVC3::SearchImplBase::d_bottomScope</a>, <a class="el" href="search__fast_8h_source.html#l00105">CVC3::SearchEngineFast::d_conflictClauseCount</a>, <a class="el" href="search__fast_8h_source.html#l00141">CVC3::SearchEngineFast::d_conflictClauses</a>, <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="search__fast_8h_source.html#l00227">CVC3::SearchEngineFast::d_lastConflictClause</a>, <a class="el" href="search__fast_8h_source.html#l00220">CVC3::SearchEngineFast::d_lastConflictScope</a>, <a class="el" href="search_8h_source.html#l00064">CVC3::SearchEngine::d_rules</a>, <a class="el" href="search__fast_8h_source.html#l00169">CVC3::SearchEngineFast::d_unitConflictClauses</a>, <a class="el" href="search__impl__base_8h_source.html#l00044">CVC3::SearchImplBase::d_vm</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="assumptions_8h_source.html#l00152">CVC3::Assumptions::end()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="clause_8h_source.html#l00122">CVC3::Clause::getScope()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="clause_8h_source.html#l00111">CVC3::Clause::isNull()</a>, <a class="el" href="theorem_8h_source.html#l00140">CVC3::Theorem::printDebug()</a>, <a class="el" href="search__fast_8cpp_source.html#l01108">processNode()</a>, <a class="el" href="clause_8h_source.html#l00113">CVC3::Clause::size()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>, <a class="el" href="search__fast_8cpp_source.html#l00412">CVC3::SearchEngineFast::updateLitCounts()</a>, <a class="el" href="clause_8h_source.html#l00151">CVC3::Clause::watched()</a>, <a class="el" href="search__fast_8cpp_source.html#l00136">CVC3::SearchEngineFast::wp()</a>, and <a class="el" href="clause_8h_source.html#l00143">CVC3::Clause::wp()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="ga6e64b8f0a42bd4b42d22b50b351219c9"></a><!-- doxytag: member="CVC3::SearchEngineFast::addNewClause" ref="ga6e64b8f0a42bd4b42d22b50b351219c9" args="(Clause &c)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineFast::addNewClause </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Clause.html">Clause</a> & </td>
<td class="paramname"><em>c</em></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Go through all the clauses and check the watch pointers (for debugging) </p>
<p>Set up the watch pointers for the new clause </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l01069">1069</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="search__fast_8h_source.html#l00110">CVC3::SearchEngineFast::d_clauses</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cdlist_8h_source.html#l00066">CVC3::CDList< T >::push_back()</a>, <a class="el" href="clause_8h_source.html#l00113">CVC3::Clause::size()</a>, <a class="el" href="search__fast_8cpp_source.html#l00412">CVC3::SearchEngineFast::updateLitCounts()</a>, <a class="el" href="clause_8h_source.html#l00151">CVC3::Clause::watched()</a>, <a class="el" href="search__fast_8cpp_source.html#l00136">CVC3::SearchEngineFast::wp()</a>, and <a class="el" href="clause_8h_source.html#l00143">CVC3::Clause::wp()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01445">CVC3::SearchEngineFast::addNonLiteralFact()</a>.</p>
</div>
</div>
<a class="anchor" id="ga2ec0e19a01ac0926b690c50a3206c5a3"></a><!-- doxytag: member="CVC3::SearchEngineFast::recordFact" ref="ga2ec0e19a01ac0926b690c50a3206c5a3" args="(const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineFast::recordFact </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Process a new derived fact (auxiliary function) </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l00549">549</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="classCVC3_1_1CommonProofRules.html#a1074822d52c22daacaa78b34ac0635ba">CVC3::CommonProofRules::contradictionRule()</a>, <a class="el" href="search_8h_source.html#l00061">CVC3::SearchEngine::d_commonRules</a>, <a class="el" href="search__fast_8h_source.html#l00115">CVC3::SearchEngineFast::d_unreportedLits</a>, <a class="el" href="variable_8h_source.html#l00164">CVC3::Literal::deriveTheorem()</a>, <a class="el" href="variable_8h_source.html#l00140">CVC3::Literal::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="variable_8h_source.html#l00148">CVC3::Literal::getScope()</a>, <a class="el" href="theorem_8cpp_source.html#l00486">CVC3::Theorem::getScope()</a>, <a class="el" href="variable_8h_source.html#l00144">CVC3::Literal::getValue()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="cdmap_8h_source.html#l00190">CVC3::CDMap< Key, Data, HashFcn >::insert()</a>, <a class="el" href="variable_8h_source.html#l00137">CVC3::Literal::isNegative()</a>, <a class="el" href="search__impl__base_8h_source.html#l00120">CVC3::SearchImplBase::newLiteral()</a>, <a class="el" href="search__fast_8cpp_source.html#l01043">CVC3::SearchEngineFast::setInconsistent()</a>, and <a class="el" href="variable_8h_source.html#l00153">CVC3::Literal::setValue()</a>.</p>
<p>Referenced by <a class="el" href="circuit_8cpp_source.html#l00047">CVC3::Circuit::propagate()</a>.</p>
</div>
</div>
<a class="anchor" id="gab3f2a42375c5b3875ad18acd47ee124d"></a><!-- doxytag: member="CVC3::SearchEngineFast::traceConflict" ref="gab3f2a42375c5b3875ad18acd47ee124d" args="(const Theorem &conflictThm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineFast::traceConflict </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>conflictThm</em></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>First pass in conflict analysis; takes a theorem of FALSE. </p>
<p>The purpose of this method is to mark up the assumption graph of the FALSE <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> (conflictThm) for the later UIP analysis. The required flags for each assumption in the graph are:</p>
<p><b>ExpandFlag:</b> whether to "expand" the node or not; that is, whether to consider the current node as a final assumption (either as a conflict clause literal, or a context assumption from <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/>)</p>
<p><b>LitFlag:</b> the node (actually, its inverse) is a literal of the conflict clause</p>
<p><b>CachedValue:</b> the "fanout" count, how many nodes in the assumption graph are derived from the current node.</p>
<p>INVARIANTS (after the method returns):</p>
<ol type="1">
<li>The currect scope is the "true" conflict scope, i.e. <a class="el" href="group__SE.html#gab267d9f29c30c8e26b5c7bcc4d15306a" title="Return the current scope level (for convenience)">scopeLevel()</a> == conflictThm.getScope()</li>
<li>The literals marked with LitFlag (CC literals) are known to the <a class="el" href="namespaceSAT.html">SAT</a> solver, i.e. their <a class="el" href="classCVC3_1_1Literal.html">Literal</a> class has a value == 1</li>
<li>The only CC literal from the current scope is the latest splitter</li>
</ol>
<p>ASSUMPTIONS:</p>
<ol type="1">
<li>The <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> scope of an assumption is the same as its <a class="el" href="classCVC3_1_1Literal.html">Literal</a> scope; i.e. if thm is a splitter, then thm.getScope() == newLiteral(thm.getExpr()).getScope()</li>
</ol>
<p>Algorithm:</p>
<p>First, backtrack to the scope level of the conflict. Then, traverse the implication graph until we either hit a literal known to the <a class="el" href="namespaceSAT.html">SAT</a> solver at a lower scope: newLiteral(e).getScope()<<a class="el" href="group__SE.html#gab267d9f29c30c8e26b5c7bcc4d15306a" title="Return the current scope level (for convenience)">scopeLevel()</a>, or a splitter (assumption), or a fact from the bottom scope. The literals from the first two categories are marked with LitFlag (they'll comprise the conflict clause), and the bottom scope facts will be the assumptions in the conflict clause's theorem.</p>
<p>The traversed nodes are cached by the .isFlagged() flag, and subsequent hits only increase the fanout count of the node.</p>
<p>Notice, that there can only be one literal in the conflict clause from the current scope. Also, even if some intermediate literals were delayed by the DPs and reported to the <a class="el" href="namespaceSAT.html">SAT</a> solver at or below the conflict scope (which may be below their "true" <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> scope), they will be skipped, and their assumptions will be used.</p>
<p>In other words, it is safe to backtrack to the "true" conflict level, since, in the worst case, we traverse the graph all the way to the splitters, and make a conflict clause out of those. The hope is, however, that this wouldn't happen too often. </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l01837">1837</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, <a class="el" href="assumptions_8h_source.html#l00151">CVC3::Assumptions::begin()</a>, <a class="el" href="theorem_8cpp_source.html#l00422">CVC3::Theorem::clearAllFlags()</a>, <a class="el" href="search__impl__base_8h_source.html#l00049">CVC3::SearchImplBase::d_bottomScope</a>, <a class="el" href="search__fast_8h_source.html#l00097">CVC3::SearchEngineFast::d_decisionEngine</a>, <a class="el" href="search__fast_8h_source.html#l00220">CVC3::SearchEngineFast::d_lastConflictScope</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="assumptions_8h_source.html#l00152">CVC3::Assumptions::end()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="variable_8h_source.html#l00148">CVC3::Literal::getScope()</a>, <a class="el" href="theorem_8cpp_source.html#l00486">CVC3::Theorem::getScope()</a>, <a class="el" href="variable_8h_source.html#l00144">CVC3::Literal::getValue()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="search__impl__base_8h_source.html#l00120">CVC3::SearchImplBase::newLiteral()</a>, <a class="el" href="decision__engine_8cpp_source.html#l00157">CVC3::DecisionEngine::popTo()</a>, <a class="el" href="theorem_8h_source.html#l00140">CVC3::Theorem::printDebug()</a>, <a class="el" href="search__impl__base_8h_source.html#l00192">CVC3::SearchImplBase::scopeLevel()</a>, <a class="el" href="theorem_8cpp_source.html#l00435">CVC3::Theorem::setCachedValue()</a>, <a class="el" href="theorem_8cpp_source.html#l00458">CVC3::Theorem::setExpandFlag()</a>, <a class="el" href="clause_8h_source.html#l00113">CVC3::Clause::size()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, and <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="gaac7ba666d67d3d4808642c5c7858db95"></a><!-- doxytag: member="CVC3::SearchEngineFast::checkValidMain" ref="gaac7ba666d67d3d4808642c5c7858db95" args="(const Expr &e2)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> SearchEngineFast::checkValidMain </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e2</em></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Private helper function for checkValid and restart. </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l01624">1624</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="cdmap_8h_source.html#l00257">CVC3::CDMap< Key, Data, HashFcn >::begin()</a>, <a class="el" href="search__fast_8cpp_source.html#l00186">CVC3::SearchEngineFast::checkSAT()</a>, <a class="el" href="expr__map_8h_source.html#l00310">CVC3::ExprHashMap< Data >::clear()</a>, <a class="el" href="search__fast_8cpp_source.html#l01063">CVC3::SearchEngineFast::clearFacts()</a>, <a class="el" href="search__fast_8cpp_source.html#l00631">CVC3::SearchEngineFast::clearLiterals()</a>, <a class="el" href="search__impl__base_8h_source.html#l00084">CVC3::SearchImplBase::d_assumptions</a>, <a class="el" href="search__impl__base_8h_source.html#l00049">CVC3::SearchImplBase::d_bottomScope</a>, <a class="el" href="search__fast_8h_source.html#l00110">CVC3::SearchEngineFast::d_clauses</a>, <a class="el" href="search__fast_8h_source.html#l00136">CVC3::SearchEngineFast::d_clausesQueryEnd</a>, <a class="el" href="search__fast_8h_source.html#l00134">CVC3::SearchEngineFast::d_clausesQueryStart</a>, <a class="el" href="search_8h_source.html#l00061">CVC3::SearchEngine::d_commonRules</a>, <a class="el" href="search__fast_8h_source.html#l00229">CVC3::SearchEngineFast::d_conflictTheorem</a>, <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="search__fast_8h_source.html#l00189">CVC3::SearchEngineFast::d_factQueue</a>, <a class="el" href="search__impl__base_8h_source.html#l00081">CVC3::SearchImplBase::d_lastCounterExample</a>, <a class="el" href="search__impl__base_8h_source.html#l00078">CVC3::SearchImplBase::d_lastValid</a>, <a class="el" href="search__fast_8h_source.html#l00176">CVC3::SearchEngineFast::d_literals</a>, <a class="el" href="search__fast_8h_source.html#l00185">CVC3::SearchEngineFast::d_literalSet</a>, <a class="el" href="search__fast_8h_source.html#l00258">CVC3::SearchEngineFast::d_litsMaxScorePos</a>, <a class="el" href="search__fast_8h_source.html#l00122">CVC3::SearchEngineFast::d_nonLiterals</a>, <a class="el" href="search__fast_8h_source.html#l00132">CVC3::SearchEngineFast::d_nonlitQueryEnd</a>, <a class="el" href="search__fast_8h_source.html#l00130">CVC3::SearchEngineFast::d_nonlitQueryStart</a>, <a class="el" href="search__fast_8h_source.html#l00127">CVC3::SearchEngineFast::d_simplifiedThm</a>, <a class="el" href="search__fast_8h_source.html#l00169">CVC3::SearchEngineFast::d_unitConflictClauses</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cdmap_8h_source.html#l00258">CVC3::CDMap< Key, Data, HashFcn >::end()</a>, <a class="el" href="theory__core_8h_source.html#l00348">CVC3::TheoryCore::getCM()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00274">CVC3::Theorem::getLeafAssumptions()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#af38f25446a561384c3de66392c4d3544">CVC3::CommonProofRules::iffContrapositive()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#aebbcd4a194e4fdca0bcd16143fb03a75">CVC3::CommonProofRules::iffMP()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>, <a class="el" href="context_8h_source.html#l00402">CVC3::ContextManager::pop()</a>, <a class="el" href="context_8h_source.html#l00403">CVC3::ContextManager::popto()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00317">CVC3::SearchImplBase::processResult()</a>, <a class="el" href="queryresult_8h_source.html#l00033">CVC3::SATISFIABLE</a>, <a class="el" href="search__impl__base_8h_source.html#l00124">CVC3::SearchImplBase::simplify()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a0a87e88508f49b73037e0024afa841bf">CVC3::CommonProofRules::symmetryRule()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>, and <a class="el" href="queryresult_8h_source.html#l00036">CVC3::UNSATISFIABLE</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01750">CVC3::SearchEngineFast::restartInternal()</a>.</p>
</div>
</div>
<a class="anchor" id="ga8869c248ac69ea02656c95b40c99ed24"></a><!-- doxytag: member="CVC3::SearchEngineFast::SearchEngineFast" ref="ga8869c248ac69ea02656c95b40c99ed24" args="(TheoryCore *core)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">SearchEngineFast::SearchEngineFast </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> * </td>
<td class="paramname"><em>core</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>The main Constructor. </p>
<p>Constructor. </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l00072">72</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="search__fast_8h_source.html#l00110">CVC3::SearchEngineFast::d_clauses</a>, <a class="el" href="search__fast_8h_source.html#l00141">CVC3::SearchEngineFast::d_conflictClauses</a>, <a class="el" href="search__fast_8h_source.html#l00139">CVC3::SearchEngineFast::d_conflictClauseStack</a>, <a class="el" href="search__fast_8h_source.html#l00097">CVC3::SearchEngineFast::d_decisionEngine</a>, <a class="el" href="search__fast_8h_source.html#l00122">CVC3::SearchEngineFast::d_nonLiterals</a>, and <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>.</p>
</div>
</div>
<a class="anchor" id="ga8f8c0138aa4f31355dad949f604e3927"></a><!-- doxytag: member="CVC3::SearchEngineFast::~SearchEngineFast" ref="ga8f8c0138aa4f31355dad949f604e3927" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">SearchEngineFast::~SearchEngineFast </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Destructor. </p>
<p>We own the proof rules (d_rules) and the variable manager (d_vm); delete them. </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l00118">118</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="search__fast_8h_source.html#l00214">CVC3::SearchEngineFast::d_circuits</a>, <a class="el" href="search__fast_8h_source.html#l00139">CVC3::SearchEngineFast::d_conflictClauseStack</a>, and <a class="el" href="search__fast_8h_source.html#l00097">CVC3::SearchEngineFast::d_decisionEngine</a>.</p>
</div>
</div>
<a class="anchor" id="ga3f564001c310c9e4ff519da68f8ea670"></a><!-- doxytag: member="CVC3::SearchEngineFast::getName" ref="ga3f564001c310c9e4ff519da68f8ea670" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const std::string& CVC3::SearchEngineFast::getName </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Name of this search engine. </p>
<p>Implements <a class="el" href="group__SE.html#ga942b3cc50f5ea9da1b3117ee23eff9c2">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00390">390</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>References <a class="el" href="search__fast_8h_source.html#l00095">CVC3::SearchEngineFast::d_name</a>.</p>
</div>
</div>
<a class="anchor" id="ga1db688bc99f93a978079b3d2efd1bd9f"></a><!-- doxytag: member="CVC3::SearchEngineFast::checkValidInternal" ref="ga1db688bc99f93a978079b3d2efd1bd9f" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> SearchEngineFast::checkValidInternal </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Implementation of the API call. </p>
<p>Implements <a class="el" href="group__SE.html#ga1e6282534845cfe93f245d9983d58761">CVC3::SearchImplBase</a>.</p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l01697">1697</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, <a class="el" href="cdmap_8h_source.html#l00172">CVC3::CDMap< Key, Data, HashFcn >::count()</a>, <a class="el" href="search__impl__base_8h_source.html#l00084">CVC3::SearchImplBase::d_assumptions</a>, <a class="el" href="search__impl__base_8h_source.html#l00049">CVC3::SearchImplBase::d_bottomScope</a>, <a class="el" href="search__fast_8h_source.html#l00110">CVC3::SearchEngineFast::d_clauses</a>, <a class="el" href="search__fast_8h_source.html#l00136">CVC3::SearchEngineFast::d_clausesQueryEnd</a>, <a class="el" href="search__fast_8h_source.html#l00134">CVC3::SearchEngineFast::d_clausesQueryStart</a>, <a class="el" href="search__fast_8h_source.html#l00159">CVC3::SearchEngineFast::d_conflictClauseManager</a>, <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="search__fast_8h_source.html#l00189">CVC3::SearchEngineFast::d_factQueue</a>, <a class="el" href="search__fast_8h_source.html#l00122">CVC3::SearchEngineFast::d_nonLiterals</a>, <a class="el" href="search__fast_8h_source.html#l00132">CVC3::SearchEngineFast::d_nonlitQueryEnd</a>, <a class="el" href="search__fast_8h_source.html#l00130">CVC3::SearchEngineFast::d_nonlitQueryStart</a>, <a class="el" href="search__fast_8h_source.html#l00127">CVC3::SearchEngineFast::d_simplifiedThm</a>, <a class="el" href="search__fast_8h_source.html#l00270">CVC3::SearchEngineFast::d_splitterCount</a>, <a class="el" href="search__fast_8h_source.html#l00169">CVC3::SearchEngineFast::d_unitConflictClauses</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cdo_8h_source.html#l00064">CVC3::CDO< T >::get()</a>, <a class="el" href="theory__core_8h_source.html#l00348">CVC3::TheoryCore::getCM()</a>, <a class="el" href="theory__core_8h_source.html#l00352">CVC3::TheoryCore::getExprTrans()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr_8h_source.html#l00937">CVC3::Expr::negate()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00141">CVC3::SearchImplBase::newUserAssumption()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00079">CVC3::ExprTransform::preprocess()</a>, <a class="el" href="context_8h_source.html#l00401">CVC3::ContextManager::push()</a>, <a class="el" href="search__impl__base_8h_source.html#l00192">CVC3::SearchImplBase::scopeLevel()</a>, <a class="el" href="search__fast_8cpp_source.html#l00042">CVC3::SearchEngineFast::ConflictClauseManager::setRestorePoint()</a>, <a class="el" href="cdlist_8h_source.html#l00064">CVC3::CDList< T >::size()</a>, <a class="el" href="type_8h_source.html#l00080">CVC3::Type::toString()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, and <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>.</p>
</div>
</div>
<a class="anchor" id="ga99dd1f1c52ecae319bd0b5a3b689a31d"></a><!-- doxytag: member="CVC3::SearchEngineFast::restartInternal" ref="ga99dd1f1c52ecae319bd0b5a3b689a31d" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> SearchEngineFast::restartInternal </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reruns last check with e as an additional assumption. </p>
<p>Implements <a class="el" href="group__SE.html#gaf89e6b914a2099b366258953fccb6277">CVC3::SearchImplBase</a>.</p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l01750">1750</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="theory__core_8cpp_source.html#l03468">CVC3::TheoryCore::addFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, <a class="el" href="cdmap_8h_source.html#l00172">CVC3::CDMap< Key, Data, HashFcn >::count()</a>, <a class="el" href="search__impl__base_8h_source.html#l00084">CVC3::SearchImplBase::d_assumptions</a>, <a class="el" href="search__impl__base_8h_source.html#l00049">CVC3::SearchImplBase::d_bottomScope</a>, <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="search__fast_8h_source.html#l00189">CVC3::SearchEngineFast::d_factQueue</a>, <a class="el" href="search__fast_8h_source.html#l00127">CVC3::SearchEngineFast::d_simplifiedThm</a>, <a class="el" href="search__fast_8h_source.html#l00169">CVC3::SearchEngineFast::d_unitConflictClauses</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cdo_8h_source.html#l00064">CVC3::CDO< T >::get()</a>, <a class="el" href="theory__core_8h_source.html#l00348">CVC3::TheoryCore::getCM()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr_8h_source.html#l00937">CVC3::Expr::negate()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00141">CVC3::SearchImplBase::newUserAssumption()</a>, <a class="el" href="context_8h_source.html#l00403">CVC3::ContextManager::popto()</a>, <a class="el" href="type_8h_source.html#l00080">CVC3::Type::toString()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, and <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>.</p>
</div>
</div>
<a class="anchor" id="ga104e5e0abacb4c9492b0cb818b7d968a"></a><!-- doxytag: member="CVC3::SearchEngineFast::getCounterExample" ref="ga104e5e0abacb4c9492b0cb818b7d968a" args="(std::vector< Expr > &assertions)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineFast::getCounterExample </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>assertions</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Redefine the counterexample generation. </p>
<p>FIXME: for now, it just dumps all the assumptions (same as <a class="el" href="group__SE.html#gadadf46fa5200744c9f30ca548080d35d" title="Get all assumptions made in this and all previous contexts.">getAssumptions()</a>). Eventually, it will simplify the related formulas to TRUE, merge all the generated assumptions into d_lastCounterExample, and call the parent's method. </p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l01424">1424</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="search__impl__base_8cpp_source.html#l00205">CVC3::SearchImplBase::getAssumptions()</a>.</p>
</div>
</div>
<a class="anchor" id="gaef3113afb8dc9ea1b06217ab77f5d713"></a><!-- doxytag: member="CVC3::SearchEngineFast::addLiteralFact" ref="gaef3113afb8dc9ea1b06217ab77f5d713" args="(const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineFast::addLiteralFact </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Notify the search engine about a new literal fact. </p>
<p>It should be called by <a class="el" href="classCVC3_1_1TheoryCore.html#a3a897e60d6dd1dfd382870054e5ad777" title="The assumptions for e must be in H or phi. "Core" added to avoid conflict with theory interface funct...">TheoryCore::assertFactCore()</a> </p>
<p>Implements <a class="el" href="group__SE.html#gaed2d918b4d0eb14d99bf63882fe2df1a">CVC3::SearchImplBase</a>.</p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l01530">1530</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a1074822d52c22daacaa78b34ac0635ba">CVC3::CommonProofRules::contradictionRule()</a>, <a class="el" href="search_8h_source.html#l00061">CVC3::SearchEngine::d_commonRules</a>, <a class="el" href="search__fast_8h_source.html#l00198">CVC3::SearchEngineFast::d_inCheckSAT</a>, <a class="el" href="search__fast_8h_source.html#l00176">CVC3::SearchEngineFast::d_literals</a>, <a class="el" href="search__fast_8h_source.html#l00185">CVC3::SearchEngineFast::d_literalSet</a>, <a class="el" href="search__fast_8h_source.html#l00193">CVC3::SearchEngineFast::d_useEnqueueFact</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="cdmap_8h_source.html#l00190">CVC3::CDMap< Key, Data, HashFcn >::insert()</a>, <a class="el" href="theorem_8cpp_source.html#l00482">CVC3::Theorem::isAbsLiteral()</a>, <a class="el" href="search__impl__base_8h_source.html#l00120">CVC3::SearchImplBase::newLiteral()</a>, <a class="el" href="search__impl__base_8h_source.html#l00192">CVC3::SearchImplBase::scopeLevel()</a>, <a class="el" href="search__fast_8cpp_source.html#l01043">CVC3::SearchEngineFast::setInconsistent()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01031">CVC3::SearchEngineFast::enqueueFact()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00254">CVC3::SearchEngineFast::split()</a>.</p>
</div>
</div>
<a class="anchor" id="ga03501a968c3c7122a999b1f57d6640a0"></a><!-- doxytag: member="CVC3::SearchEngineFast::addNonLiteralFact" ref="ga03501a968c3c7122a999b1f57d6640a0" args="(const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineFast::addNonLiteralFact </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Notify the search engine about a new non-literal fact. </p>
<p>It should be called by <a class="el" href="classCVC3_1_1TheoryCore.html#a3a897e60d6dd1dfd382870054e5ad777" title="The assumptions for e must be in H or phi. "Core" added to avoid conflict with theory interface funct...">TheoryCore::assertFactCore()</a>.</p>
<p>If the fact is an AND, we split it into individual conjuncts and add them individually.</p>
<p>If the fact is an OR, we check whether it's a CNF clause; that is, whether all disjuncts are literals. If they are, we add it as a CNF clause.</p>
<p>Otherwise add the fact to d_nonLiterals as it is. </p>
<p>Implements <a class="el" href="group__SE.html#gae95c78de94900637db19e3b7dee5d7c3">CVC3::SearchImplBase</a>.</p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l01445">1445</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="search__fast_8cpp_source.html#l01069">CVC3::SearchEngineFast::addNewClause()</a>, <a class="el" href="kinds_8h_source.html#l00075">AND_R</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a3f3592ac74d0aa0caa3b9224ea7e61f4">CVC3::CommonProofRules::andElim()</a>, <a class="el" href="search__fast_8h_source.html#l00088">CVC3::SearchEngineFast::Circuit</a>, <a class="el" href="group__SE__Rules.html#ga9c74425b4471d411f58f16781951c441">CVC3::SearchEngineRules::conflictRule()</a>, <a class="el" href="cdmap_8h_source.html#l00172">CVC3::CDMap< Key, Data, HashFcn >::count()</a>, <a class="el" href="search__fast_8h_source.html#l00214">CVC3::SearchEngineFast::d_circuits</a>, <a class="el" href="search_8h_source.html#l00061">CVC3::SearchEngine::d_commonRules</a>, <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="search__fast_8h_source.html#l00122">CVC3::SearchEngineFast::d_nonLiterals</a>, <a class="el" href="search__fast_8h_source.html#l00123">CVC3::SearchEngineFast::d_nonLiteralsSaved</a>, <a class="el" href="search_8h_source.html#l00064">CVC3::SearchEngine::d_rules</a>, <a class="el" href="search__impl__base_8h_source.html#l00044">CVC3::SearchImplBase::d_vm</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="variable_8h_source.html#l00164">CVC3::Literal::deriveTheorem()</a>, <a class="el" href="theory__core_8cpp_source.html#l04213">CVC3::TheoryCore::enqueueFact()</a>, <a class="el" href="theory__core_8h_source.html#l00348">CVC3::TheoryCore::getCM()</a>, <a class="el" href="context_8h_source.html#l00406">CVC3::ContextManager::getCurrentContext()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="variable_8h_source.html#l00144">CVC3::Literal::getValue()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="kinds_8h_source.html#l00076">IFF_R</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="kinds_8h_source.html#l00077">ITE_R</a>, <a class="el" href="search__impl__base_8h_source.html#l00120">CVC3::SearchImplBase::newLiteral()</a>, <a class="el" href="cdlist_8h_source.html#l00066">CVC3::CDList< T >::push_back()</a>, <a class="el" href="search__impl__base_8h_source.html#l00192">CVC3::SearchImplBase::scopeLevel()</a>, <a class="el" href="search__fast_8cpp_source.html#l01043">CVC3::SearchEngineFast::setInconsistent()</a>, <a class="el" href="cdmap_8h_source.html#l00171">CVC3::CDMap< Key, Data, HashFcn >::size()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>, and <a class="el" href="group__SE__Rules.html#gae7221bb8b77313a9b53a4beca9cc0aa0">CVC3::SearchEngineRules::unitProp()</a>.</p>
</div>
</div>
<a class="anchor" id="gaf54422149559aa048f32723a3dc6fcce"></a><!-- doxytag: member="CVC3::SearchEngineFast::newIntAssumption" ref="gaf54422149559aa048f32723a3dc6fcce" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> SearchEngineFast::newIntAssumption </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Redefine <a class="el" href="group__SE__Fast.html#gaf54422149559aa048f32723a3dc6fcce" title="Redefine newIntAssumption(): we need to add the new theorem to the appropriate Literal.">newIntAssumption()</a>: we need to add the new theorem to the appropriate <a class="el" href="classCVC3_1_1Literal.html">Literal</a>. </p>
<p>Reimplemented from <a class="el" href="group__SE.html#ga635768498a239f0193de5f1445676f65">CVC3::SearchImplBase</a>.</p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l01573">1573</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="search__fast_8h_source.html#l00176">CVC3::SearchEngineFast::d_literals</a>, <a class="el" href="search__fast_8h_source.html#l00205">CVC3::SearchEngineFast::d_litsAlive</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="variable_8h_source.html#l00140">CVC3::Literal::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="variable_8h_source.html#l00144">CVC3::Literal::getValue()</a>, <a class="el" href="expr_8h_source.html#l00406">CVC3::Expr::isAbsLiteral()</a>, <a class="el" href="theorem_8cpp_source.html#l00395">CVC3::Theorem::isAssump()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00170">CVC3::SearchImplBase::newIntAssumption()</a>, <a class="el" href="search__impl__base_8h_source.html#l00120">CVC3::SearchImplBase::newLiteral()</a>, <a class="el" href="cdlist_8h_source.html#l00066">CVC3::CDList< T >::push_back()</a>, <a class="el" href="search__impl__base_8h_source.html#l00192">CVC3::SearchImplBase::scopeLevel()</a>, <a class="el" href="variable_8h_source.html#l00153">CVC3::Literal::setValue()</a>, <a class="el" href="variable_8cpp_source.html#l00211">CVC3::Literal::toString()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
</div>
</div>
<a class="anchor" id="ga4b55b5f49d921ca4b63f874d8404c4d5"></a><!-- doxytag: member="CVC3::SearchEngineFast::isAssumption" ref="ga4b55b5f49d921ca4b63f874d8404c4d5" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool SearchEngineFast::isAssumption </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Check if the formula has been assumed. </p>
<p>Reimplemented from <a class="el" href="group__SE.html#ga38ec2c19ebab8525ebc3c6249bf97442">CVC3::SearchImplBase</a>.</p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l01594">1594</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="cdmap_8h_source.html#l00172">CVC3::CDMap< Key, Data, HashFcn >::count()</a>, <a class="el" href="search__fast_8h_source.html#l00123">CVC3::SearchEngineFast::d_nonLiteralsSaved</a>, and <a class="el" href="search__impl__base_8cpp_source.html#l00213">CVC3::SearchImplBase::isAssumption()</a>.</p>
</div>
</div>
<a class="anchor" id="ga40b361c2f9374c541282feca1e237dba"></a><!-- doxytag: member="CVC3::SearchEngineFast::addSplitter" ref="ga40b361c2f9374c541282feca1e237dba" args="(const Expr &e, int priority)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngineFast::addSplitter </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>priority</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Suggest a splitter to the <a class="el" href="classCVC3_1_1SearchEngine.html" title="API to to a generic proof search engine.">SearchEngine</a>. </p>
<p>The higher is the priority, the sooner the <a class="el" href="namespaceSAT.html">SAT</a> solver will split on it. It can be positive or negative (default is 0).</p>
<p>The set of suggested splitters is backtracking; that is, a splitter is "forgotten" once the scope is backtracked.</p>
<p>This method can be used either to change the priority of existing splitters, or to introduce new splitters that DPs consider relevant, even though they do not appear in existing formulas. </p>
<p>Reimplemented from <a class="el" href="group__SE.html#ga6c1448b58fb299bc084aa9c522faf36d">CVC3::SearchImplBase</a>.</p>
<p>Definition at line <a class="el" href="search__fast_8cpp_source.html#l01601">1601</a> of file <a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a>.</p>
<p>References <a class="el" href="search__fast_8cpp_source.html#l00323">compareLits()</a>, <a class="el" href="search__impl__base_8h_source.html#l00074">CVC3::SearchImplBase::d_dpSplitters</a>, <a class="el" href="search__fast_8h_source.html#l00260">CVC3::SearchEngineFast::d_litsByScores</a>, <a class="el" href="search__fast_8h_source.html#l00272">CVC3::SearchEngineFast::d_litSortCount</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l00406">CVC3::Expr::isAbsLiteral()</a>, <a class="el" href="search__impl__base_8h_source.html#l00120">CVC3::SearchImplBase::newLiteral()</a>, <a class="el" href="cdlist_8h_source.html#l00066">CVC3::CDList< T >::push_back()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
</div>
</div>
<hr/><h2>Variable Documentation</h2>
<a class="anchor" id="ga91ff4e54d0b66c31eb0d2653fad650cb"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_name" ref="ga91ff4e54d0b66c31eb0d2653fad650cb" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string <a class="el" href="group__SE__Fast.html#ga91ff4e54d0b66c31eb0d2653fad650cb">CVC3::SearchEngineFast::d_name</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Name. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00095">95</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8h_source.html#l00390">CVC3::SearchEngineFast::getName()</a>.</p>
</div>
</div>
<a class="anchor" id="gafa042a51f718c312ea7728f175958e35"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_decisionEngine" ref="gafa042a51f718c312ea7728f175958e35" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">DecisionEngine* <a class="el" href="group__SE__Fast.html#gafa042a51f718c312ea7728f175958e35">CVC3::SearchEngineFast::d_decisionEngine</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Decision Engine. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00097">97</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00186">CVC3::SearchEngineFast::checkSAT()</a>, <a class="el" href="search__fast_8cpp_source.html#l00438">CVC3::SearchEngineFast::findSplitter()</a>, <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>, <a class="el" href="search__fast_8cpp_source.html#l00072">CVC3::SearchEngineFast::SearchEngineFast()</a>, <a class="el" href="search__fast_8cpp_source.html#l00254">CVC3::SearchEngineFast::split()</a>, <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00118">CVC3::SearchEngineFast::~SearchEngineFast()</a>.</p>
</div>
</div>
<a class="anchor" id="ga29e749a0ca7cbe86118a0d72e02e0696"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_unitPropCount" ref="ga29e749a0ca7cbe86118a0d72e02e0696" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">StatCounter <a class="el" href="group__SE__Fast.html#ga29e749a0ca7cbe86118a0d72e02e0696">CVC3::SearchEngineFast::d_unitPropCount</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Total number of unit propagations. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00099">99</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00816">CVC3::SearchEngineFast::propagate()</a>.</p>
</div>
</div>
<a class="anchor" id="ga749d335e3d18b71aa951d37e943fbf50"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_circuitPropCount" ref="ga749d335e3d18b71aa951d37e943fbf50" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">StatCounter <a class="el" href="group__SE__Fast.html#ga749d335e3d18b71aa951d37e943fbf50">CVC3::SearchEngineFast::d_circuitPropCount</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Total number of circuit propagations. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00101">101</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="circuit_8cpp_source.html#l00047">CVC3::Circuit::propagate()</a>.</p>
</div>
</div>
<a class="anchor" id="gaecd7cc2115fe235653a62acf93ccb1e5"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_conflictCount" ref="gaecd7cc2115fe235653a62acf93ccb1e5" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">StatCounter <a class="el" href="group__SE__Fast.html#gaecd7cc2115fe235653a62acf93ccb1e5">CVC3::SearchEngineFast::d_conflictCount</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Total number of conflicts. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00103">103</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="ga483cb3c4c889013b03e2c923977d4ae5"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_conflictClauseCount" ref="ga483cb3c4c889013b03e2c923977d4ae5" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">StatCounter <a class="el" href="group__SE__Fast.html#ga483cb3c4c889013b03e2c923977d4ae5">CVC3::SearchEngineFast::d_conflictClauseCount</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Total number of conflict clauses generated (not all may be active) </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00105">105</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>.</p>
</div>
</div>
<a class="anchor" id="gaa1dd9a29eac4c7da6c669d7888909ca5"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_clauses" ref="gaa1dd9a29eac4c7da6c669d7888909ca5" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CDList<ClauseOwner> <a class="el" href="group__SE__Fast.html#gaa1dd9a29eac4c7da6c669d7888909ca5">CVC3::SearchEngineFast::d_clauses</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Backtrackable list of clauses. </p>
<p>New clauses may come into play from the decision procedures that are context dependent. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00110">110</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01069">CVC3::SearchEngineFast::addNewClause()</a>, <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00072">CVC3::SearchEngineFast::SearchEngineFast()</a>.</p>
</div>
</div>
<a class="anchor" id="gabe8dbaf4592793c49cd58ff93a897a06"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_unreportedLits" ref="gabe8dbaf4592793c49cd58ff93a897a06" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CDMap<Expr,Theorem> <a class="el" href="group__SE__Fast.html#gabe8dbaf4592793c49cd58ff93a897a06">CVC3::SearchEngineFast::d_unreportedLits</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Backtrackable set of pending unprocessed literals. </p>
<p>These can be discovered at any scope level during conflict analysis. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00115">115</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00549">CVC3::SearchEngineFast::recordFact()</a>.</p>
</div>
</div>
<a class="anchor" id="ga8217149b882d328384bd7a04a5e5c5f3"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_unreportedLitsHandled" ref="ga8217149b882d328384bd7a04a5e5c5f3" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CDMap<Expr,bool> <a class="el" href="group__SE__Fast.html#ga8217149b882d328384bd7a04a5e5c5f3">CVC3::SearchEngineFast::d_unreportedLitsHandled</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00116">116</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
</div>
</div>
<a class="anchor" id="ga07c8e260b60d83042c97453892a15f38"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_nonLiterals" ref="ga07c8e260b60d83042c97453892a15f38" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CDList<SmartCDO<Theorem> > <a class="el" href="group__SE__Fast.html#ga07c8e260b60d83042c97453892a15f38">CVC3::SearchEngineFast::d_nonLiterals</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Backtrackable list of non-literals (non-CNF formulas). </p>
<p>We treat nonliterals like clauses, because they are a superset of clauses. We stick the real clauses into d_clauses, but all the rest have to be stored elsewhere. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00122">122</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01445">CVC3::SearchEngineFast::addNonLiteralFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, <a class="el" href="search__fast_8cpp_source.html#l00438">CVC3::SearchEngineFast::findSplitter()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00072">CVC3::SearchEngineFast::SearchEngineFast()</a>.</p>
</div>
</div>
<a class="anchor" id="gae88240871407db238ad8c6a795ba6b91"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_nonLiteralsSaved" ref="gae88240871407db238ad8c6a795ba6b91" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CDMap<Expr,Theorem> <a class="el" href="group__SE__Fast.html#gae88240871407db238ad8c6a795ba6b91">CVC3::SearchEngineFast::d_nonLiteralsSaved</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>prevent reprocessing </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00123">123</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01445">CVC3::SearchEngineFast::addNonLiteralFact()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01594">CVC3::SearchEngineFast::isAssumption()</a>.</p>
</div>
</div>
<a class="anchor" id="gaa8b578a017bcddd578e943add44c2940"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_simplifiedThm" ref="gaa8b578a017bcddd578e943add44c2940" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CDO<Theorem> <a class="el" href="group__SE__Fast.html#gaa8b578a017bcddd578e943add44c2940">CVC3::SearchEngineFast::d_simplifiedThm</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> which records simplification of the last query. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00127">127</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01750">CVC3::SearchEngineFast::restartInternal()</a>.</p>
</div>
</div>
<a class="anchor" id="gae4a9e9926613365979d36e2a98769381"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_nonlitQueryStart" ref="gae4a9e9926613365979d36e2a98769381" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CDO<unsigned> <a class="el" href="group__SE__Fast.html#gae4a9e9926613365979d36e2a98769381">CVC3::SearchEngineFast::d_nonlitQueryStart</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Size of d_nonLiterals before most recent query. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00130">130</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>.</p>
</div>
</div>
<a class="anchor" id="ga8472c82be89057f32c68a0f0423215a2"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_nonlitQueryEnd" ref="ga8472c82be89057f32c68a0f0423215a2" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CDO<unsigned> <a class="el" href="group__SE__Fast.html#ga8472c82be89057f32c68a0f0423215a2">CVC3::SearchEngineFast::d_nonlitQueryEnd</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Size of d_nonLiterals after query (not including DP-generated non-literals) </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00132">132</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>.</p>
</div>
</div>
<a class="anchor" id="ga71a2e31fe2a16420a416b5aeced09455"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_clausesQueryStart" ref="ga71a2e31fe2a16420a416b5aeced09455" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CDO<unsigned> <a class="el" href="group__SE__Fast.html#ga71a2e31fe2a16420a416b5aeced09455">CVC3::SearchEngineFast::d_clausesQueryStart</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Size of d_clauses before most recent query. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00134">134</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>.</p>
</div>
</div>
<a class="anchor" id="ga6dbfd2cd66dee5634f096593f26c47e7"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_clausesQueryEnd" ref="ga6dbfd2cd66dee5634f096593f26c47e7" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CDO<unsigned> <a class="el" href="group__SE__Fast.html#ga6dbfd2cd66dee5634f096593f26c47e7">CVC3::SearchEngineFast::d_clausesQueryEnd</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Size of d_clauses after query. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00136">136</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>.</p>
</div>
</div>
<a class="anchor" id="ga8e96b8f24bd89c190e561f387a4a30ee"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_conflictClauseStack" ref="ga8e96b8f24bd89c190e561f387a4a30ee" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<std::deque<ClauseOwner>* > <a class="el" href="group__SE__Fast.html#ga8e96b8f24bd89c190e561f387a4a30ee">CVC3::SearchEngineFast::d_conflictClauseStack</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Array of conflict clauses: one deque for each outstanding query. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00139">139</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00072">CVC3::SearchEngineFast::SearchEngineFast()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00118">CVC3::SearchEngineFast::~SearchEngineFast()</a>.</p>
</div>
</div>
<a class="anchor" id="gad79601e3b2032aee4d23dc4bbd785fc3"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_conflictClauses" ref="gad79601e3b2032aee4d23dc4bbd785fc3" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::deque<ClauseOwner>* <a class="el" href="group__SE__Fast.html#gad79601e3b2032aee4d23dc4bbd785fc3">CVC3::SearchEngineFast::d_conflictClauses</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Reference to top deque of conflict clauses. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00141">141</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, <a class="el" href="search__fast_8cpp_source.html#l00438">CVC3::SearchEngineFast::findSplitter()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00072">CVC3::SearchEngineFast::SearchEngineFast()</a>.</p>
</div>
</div>
<a class="anchor" id="gaab577b22f09d51b9b15954b9a529c05d"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_conflictClauseManager" ref="gaab577b22f09d51b9b15954b9a529c05d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">ConflictClauseManager <a class="el" href="group__SE__Fast.html#gaab577b22f09d51b9b15954b9a529c05d">CVC3::SearchEngineFast::d_conflictClauseManager</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00159">159</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>.</p>
</div>
</div>
<a class="anchor" id="gad05f577d00e93fefed74eb0c19015090"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_unitConflictClauses" ref="gad05f577d00e93fefed74eb0c19015090" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<Clause> <a class="el" href="group__SE__Fast.html#gad05f577d00e93fefed74eb0c19015090">CVC3::SearchEngineFast::d_unitConflictClauses</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Unprocessed unit conflict clauses. </p>
<p>When we find unit conflict clauses, we are automatically going to jump back to the original scope. Hopefully we won't find multiple ones, but you never know with those wacky decision procedures just spitting new information out. These are then directly asserted then promptly forgotten about. Chaff keeps them around (for correctness maybe), but we already have the proofs stored in the literals themselves. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00169">169</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01750">CVC3::SearchEngineFast::restartInternal()</a>.</p>
</div>
</div>
<a class="anchor" id="gaa6a69bd3df4bb72abd1e9b0fe868fc0d"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_literals" ref="gaa6a69bd3df4bb72abd1e9b0fe868fc0d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<Literal> <a class="el" href="group__SE__Fast.html#gaa6a69bd3df4bb72abd1e9b0fe868fc0d">CVC3::SearchEngineFast::d_literals</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Set of literals to be processed by bcp. </p>
<p>These are emptied out upon backtracking, because they can only be valid if they were already all processed without conflicts. Therefore, they don't need to be context dependent. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00176">176</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01530">CVC3::SearchEngineFast::addLiteralFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, <a class="el" href="search__fast_8cpp_source.html#l00631">CVC3::SearchEngineFast::clearLiterals()</a>, <a class="el" href="search__fast_8cpp_source.html#l01573">CVC3::SearchEngineFast::newIntAssumption()</a>, <a class="el" href="circuit_8cpp_source.html#l00047">CVC3::Circuit::propagate()</a>, <a class="el" href="search__fast_8cpp_source.html#l00254">CVC3::SearchEngineFast::split()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00915">CVC3::SearchEngineFast::unitPropagation()</a>.</p>
</div>
</div>
<a class="anchor" id="gaf720bf50e81fc4e2561b587d97ec2839"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_literalSet" ref="gaf720bf50e81fc4e2561b587d97ec2839" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CDMap<Expr,Literal> <a class="el" href="group__SE__Fast.html#gaf720bf50e81fc4e2561b587d97ec2839">CVC3::SearchEngineFast::d_literalSet</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Set of asserted literals which may survive accross <a class="el" href="group__SE.html#ga83d82b8cf43e9dc8240e762b180f6343" title="Similar to checkValidInternal(), only returns Theorem(e) or Null.">checkValid()</a> calls. </p>
<p>When a literal is asserted outside of <a class="el" href="group__SE.html#ga83d82b8cf43e9dc8240e762b180f6343" title="Similar to checkValidInternal(), only returns Theorem(e) or Null.">checkValid()</a> call, its value is remembered in a <a class="el" href="classCVC3_1_1Literal.html">Literal</a> database, but the literal queue for BCP is cleared. We add literals to this set at the proper scope levels, and propagate them at the beginning of a <a class="el" href="group__SE.html#ga83d82b8cf43e9dc8240e762b180f6343" title="Similar to checkValidInternal(), only returns Theorem(e) or Null.">checkValid()</a> call. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00185">185</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01530">CVC3::SearchEngineFast::addLiteralFact()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>.</p>
</div>
</div>
<a class="anchor" id="ga4b05dccebac3de019dc112ab3dffc988"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_factQueue" ref="ga4b05dccebac3de019dc112ab3dffc988" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<Theorem> <a class="el" href="group__SE__Fast.html#ga4b05dccebac3de019dc112ab3dffc988">CVC3::SearchEngineFast::d_factQueue</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Queue of derived facts to be sent to DPs. </p>
<dl class="see"><dt><b>See also:</b></dt><dd><a class="el" href="group__SE.html#gac6e807418fb26dee354f7f934eb432ba" title="Add a new fact to the search engine from the core.">addFact()</a> and <a class="el" href="group__SE__Fast.html#ga6d190905fefb2a36650306e5b577dd9a" title="Commit all the enqueued facts to the DPs.">commitFacts()</a> </dd></dl>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00189">189</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, <a class="el" href="search__fast_8cpp_source.html#l00186">CVC3::SearchEngineFast::checkSAT()</a>, <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, <a class="el" href="search__fast_8cpp_source.html#l01063">CVC3::SearchEngineFast::clearFacts()</a>, <a class="el" href="search__fast_8cpp_source.html#l01050">CVC3::SearchEngineFast::commitFacts()</a>, <a class="el" href="search__fast_8cpp_source.html#l01031">CVC3::SearchEngineFast::enqueueFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l01750">CVC3::SearchEngineFast::restartInternal()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01043">CVC3::SearchEngineFast::setInconsistent()</a>.</p>
</div>
</div>
<a class="anchor" id="gaa1ea8707c10a13a631402860eff87026"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_useEnqueueFact" ref="gaa1ea8707c10a13a631402860eff87026" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="group__SE__Fast.html#gaa1ea8707c10a13a631402860eff87026">CVC3::SearchEngineFast::d_useEnqueueFact</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>When true, use <a class="el" href="classCVC3_1_1TheoryCore.html#a479141bc26a125b758a2acc6420274f9" title="Enqueue a new fact.">TheoryCore::enqueueFact()</a> instead of <a class="el" href="group__SE.html#gac6e807418fb26dee354f7f934eb432ba" title="Add a new fact to the search engine from the core.">addFact()</a> in <a class="el" href="group__SE__Fast.html#ga6d190905fefb2a36650306e5b577dd9a" title="Commit all the enqueued facts to the DPs.">commitFacts()</a> </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00193">193</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01530">CVC3::SearchEngineFast::addLiteralFact()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01050">CVC3::SearchEngineFast::commitFacts()</a>.</p>
</div>
</div>
<a class="anchor" id="ga6368ec56b20c12896000e370bbb4a3b6"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_inCheckSAT" ref="ga6368ec56b20c12896000e370bbb4a3b6" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="group__SE__Fast.html#ga6368ec56b20c12896000e370bbb4a3b6">CVC3::SearchEngineFast::d_inCheckSAT</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>True when <a class="el" href="group__SE__Fast.html#gac68652e5ed46a097f846ba9a86fcd630">checkSAT()</a> is running. </p>
<p>Used by <a class="el" href="group__SE__Fast.html#gaef3113afb8dc9ea1b06217ab77f5d713" title="Notify the search engine about a new literal fact.">addLiteralFact()</a> to determine whether to BCP the literals immediately (outside of <a class="el" href="group__SE__Fast.html#gac68652e5ed46a097f846ba9a86fcd630">checkSAT()</a>) or not. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00198">198</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01530">CVC3::SearchEngineFast::addLiteralFact()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00186">CVC3::SearchEngineFast::checkSAT()</a>.</p>
</div>
</div>
<a class="anchor" id="ga0214c0205e48fd792c4d01d3428cd333"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_litsAlive" ref="ga0214c0205e48fd792c4d01d3428cd333" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CDList<Literal> <a class="el" href="group__SE__Fast.html#ga0214c0205e48fd792c4d01d3428cd333">CVC3::SearchEngineFast::d_litsAlive</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Set of alive literals that shouldn't be garbage-collected. </p>
<p>Unfortunately, I have a keep-alive issue. I think literals actually have to hang around, so I assert them to a separate d_litsAlive <a class="el" href="classCVC3_1_1CDList.html">CDList</a>. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00205">205</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01573">CVC3::SearchEngineFast::newIntAssumption()</a>.</p>
</div>
</div>
<a class="anchor" id="ga5db32a771408c468676e407075184b64"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_circuits" ref="ga5db32a771408c468676e407075184b64" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<Circuit*> <a class="el" href="group__SE__Fast.html#ga5db32a771408c468676e407075184b64">CVC3::SearchEngineFast::d_circuits</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Mappings of literals to vectors of pointers to the corresponding watched literals. </p>
<p>A pointer is a pair (clause,i), where 'i' in {0,1} is the index of the watch pointer in the clause. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00214">214</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01445">CVC3::SearchEngineFast::addNonLiteralFact()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00118">CVC3::SearchEngineFast::~SearchEngineFast()</a>.</p>
</div>
</div>
<a class="anchor" id="ga84bfa366c43221ba288e0a1bd716efc6"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_circuitsByExpr" ref="ga84bfa366c43221ba288e0a1bd716efc6" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">ExprHashMap<std::vector<Circuit*> > <a class="el" href="group__SE__Fast.html#ga84bfa366c43221ba288e0a1bd716efc6">CVC3::SearchEngineFast::d_circuitsByExpr</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00215">215</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, and <a class="el" href="circuit_8cpp_source.html#l00028">CVC3::Circuit::Circuit()</a>.</p>
</div>
</div>
<a class="anchor" id="gab27227ee9e005ab22a9e2a251bc7c6d1"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_lastConflictScope" ref="gab27227ee9e005ab22a9e2a251bc7c6d1" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="group__SE__Fast.html#gab27227ee9e005ab22a9e2a251bc7c6d1">CVC3::SearchEngineFast::d_lastConflictScope</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>The scope of the last conflict. </p>
<p>This is the true scope of the conflict, not necessarily the scope where the conflict was detected. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00220">220</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="ga46e91bb5d782794c6dca6abaa99dc4f9"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_lastConflictClause" ref="ga46e91bb5d782794c6dca6abaa99dc4f9" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">Clause <a class="el" href="group__SE__Fast.html#ga46e91bb5d782794c6dca6abaa99dc4f9">CVC3::SearchEngineFast::d_lastConflictClause</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>The last conflict clause (for <a class="el" href="group__SE__Fast.html#gac68652e5ed46a097f846ba9a86fcd630">checkSAT()</a>). May be Null. </p>
<p>It records which conflict clause must be processed by BCP after backtracking from a conflict. A conflict may generate several conflict clauses, but only one of them will cause a unit propagation. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00227">227</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="gae961b4fb4bb059a1d867447fc487aaee"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_conflictTheorem" ref="gae961b4fb4bb059a1d867447fc487aaee" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">Theorem <a class="el" href="group__SE__Fast.html#gae961b4fb4bb059a1d867447fc487aaee">CVC3::SearchEngineFast::d_conflictTheorem</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Theorem(FALSE) which generated a conflict. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00229">229</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>, <a class="el" href="search__fast_8cpp_source.html#l00816">CVC3::SearchEngineFast::propagate()</a>, and <a class="el" href="circuit_8cpp_source.html#l00047">CVC3::Circuit::propagate()</a>.</p>
</div>
</div>
<a class="anchor" id="gad80c2b69b88a04c8c78309859abd3f76"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_litsMaxScorePos" ref="gad80c2b69b88a04c8c78309859abd3f76" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">unsigned <a class="el" href="group__SE__Fast.html#gad80c2b69b88a04c8c78309859abd3f76">CVC3::SearchEngineFast::d_litsMaxScorePos</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Position of a literal with max score in d_litsByScores. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00258">258</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, <a class="el" href="search__fast_8cpp_source.html#l00438">CVC3::SearchEngineFast::findSplitter()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="ga57c1c1e58ebd2c1d23a57db97880fbbc"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_litsByScores" ref="ga57c1c1e58ebd2c1d23a57db97880fbbc" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<Literal> <a class="el" href="group__SE__Fast.html#ga57c1c1e58ebd2c1d23a57db97880fbbc">CVC3::SearchEngineFast::d_litsByScores</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Vector of literals sorted by score. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00260">260</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01601">CVC3::SearchEngineFast::addSplitter()</a>, <a class="el" href="search__fast_8cpp_source.html#l00438">CVC3::SearchEngineFast::findSplitter()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00412">CVC3::SearchEngineFast::updateLitCounts()</a>.</p>
</div>
</div>
<a class="anchor" id="ga52c9c181bcd623a36ab594e0ee16a67e"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_splitterCount" ref="ga52c9c181bcd623a36ab594e0ee16a67e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="group__SE__Fast.html#ga52c9c181bcd623a36ab594e0ee16a67e">CVC3::SearchEngineFast::d_splitterCount</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Internal splitter counter for delaying <a class="el" href="group__SE__Fast.html#ga453b1d390ee3b7af68fe8e915443d1ad">updateLitScores()</a> </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00270">270</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l00438">CVC3::SearchEngineFast::findSplitter()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00254">CVC3::SearchEngineFast::split()</a>.</p>
</div>
</div>
<a class="anchor" id="ga2d54fdadc1b167dbbb366e37e0b97a58"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_litSortCount" ref="ga2d54fdadc1b167dbbb366e37e0b97a58" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="group__SE__Fast.html#ga2d54fdadc1b167dbbb366e37e0b97a58">CVC3::SearchEngineFast::d_litSortCount</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Internal (decrementing) count of added splitters, to sort d_litByScores. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00272">272</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01601">CVC3::SearchEngineFast::addSplitter()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00412">CVC3::SearchEngineFast::updateLitCounts()</a>.</p>
</div>
</div>
<a class="anchor" id="ga3877f82445d777c19c60b6ec117335e2"></a><!-- doxytag: member="CVC3::SearchEngineFast::d_berkminFlag" ref="ga3877f82445d777c19c60b6ec117335e2" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const bool <a class="el" href="group__SE__Fast.html#ga3877f82445d777c19c60b6ec117335e2">CVC3::SearchEngineFast::d_berkminFlag</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Flag to switch on/off the berkmin heuristic. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00275">275</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00438">CVC3::SearchEngineFast::findSplitter()</a>.</p>
</div>
</div>
<hr/><h2>Friends</h2>
<a class="anchor" id="ga771f251de98c5689b33e123d5603722d"></a><!-- doxytag: member="CVC3::SearchEngineFast::ConflictClauseManager" ref="ga771f251de98c5689b33e123d5603722d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class ConflictClauseManager<code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Helper class for managing conflict clauses. </p>
<p>Conflict clauses should only get popped when the context in which a call to checkValid originates is popped. This helper class checks every time there's a pop to see if the conflict clauses need to be restored. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00149">149</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
</div>
</div>
</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>
