<!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: CVC3::SearchEngineFast Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="hierarchy.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a> </li>
<li class="navelem"><a class="el" href="classCVC3_1_1SearchEngineFast.html">SearchEngineFast</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#nested-classes">Classes</a> |
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pri-methods">Private Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> |
<a href="#friends">Friends</a> </div>
<div class="headertitle">
<div class="title">CVC3::SearchEngineFast Class Reference<div class="ingroups"><a class="el" href="group__SE__Fast.html">Fast Search Engine</a></div></div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::SearchEngineFast" --><!-- doxytag: inherits="CVC3::SearchImplBase" -->
<p>Implementation of a faster search engine, using newer techniques.
<a href="classCVC3_1_1SearchEngineFast.html#details">More...</a></p>
<p><code>#include <<a class="el" href="search__fast_8h_source.html">search_fast.h</a>></code></p>
<div class="dynheader">
Inheritance diagram for CVC3::SearchEngineFast:</div>
<div class="dyncontent">
<div class="center">
<img src="classCVC3_1_1SearchEngineFast.png" usemap="#CVC3::SearchEngineFast_map" alt=""/>
<map id="CVC3::SearchEngineFast_map" name="CVC3::SearchEngineFast_map">
<area href="classCVC3_1_1SearchImplBase.html" title="API to to a generic proof search engine (a.k.a. SAT solver)" alt="CVC3::SearchImplBase" shape="rect" coords="0,56,156,80"/>
<area href="classCVC3_1_1SearchEngine.html" title="API to to a generic proof search engine." alt="CVC3::SearchEngine" shape="rect" coords="0,0,156,24"/>
</map>
</div></div>
<p><a href="classCVC3_1_1SearchEngineFast-members.html">List of all members.</a></p>
<h2><a name="nested-classes"></a>
Classes</h2>
<ul>
<li>class <a class="el" href="classCVC3_1_1SearchEngineFast_1_1ConflictClauseManager.html">ConflictClauseManager</a>
</ul>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="group__SE__Fast.html#ga8869c248ac69ea02656c95b40c99ed24">SearchEngineFast</a> (<a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> *core)
<dl class="el"><dd class="mdescRight">The main Constructor. <a href="group__SE__Fast.html#ga8869c248ac69ea02656c95b40c99ed24"></a><br/></dl><li>virtual <a class="el" href="group__SE__Fast.html#ga8f8c0138aa4f31355dad949f604e3927">~SearchEngineFast</a> ()
<dl class="el"><dd class="mdescRight">Destructor. <a href="group__SE__Fast.html#ga8f8c0138aa4f31355dad949f604e3927"></a><br/></dl><li>const std::string & <a class="el" href="group__SE__Fast.html#ga3f564001c310c9e4ff519da68f8ea670">getName</a> ()
<dl class="el"><dd class="mdescRight">Name of this search engine. <a href="group__SE__Fast.html#ga3f564001c310c9e4ff519da68f8ea670"></a><br/></dl><li>virtual <a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="el" href="group__SE__Fast.html#ga1db688bc99f93a978079b3d2efd1bd9f">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="group__SE__Fast.html#ga1db688bc99f93a978079b3d2efd1bd9f"></a><br/></dl><li>virtual <a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="el" href="group__SE__Fast.html#ga99dd1f1c52ecae319bd0b5a3b689a31d">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="group__SE__Fast.html#ga99dd1f1c52ecae319bd0b5a3b689a31d"></a><br/></dl><li>virtual void <a class="el" href="group__SE__Fast.html#ga104e5e0abacb4c9492b0cb818b7d968a">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="group__SE__Fast.html#ga104e5e0abacb4c9492b0cb818b7d968a"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#gaef3113afb8dc9ea1b06217ab77f5d713">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="group__SE__Fast.html#gaef3113afb8dc9ea1b06217ab77f5d713"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#ga03501a968c3c7122a999b1f57d6640a0">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="group__SE__Fast.html#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">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="group__SE__Fast.html#gaf54422149559aa048f32723a3dc6fcce"></a><br/></dl><li>virtual bool <a class="el" href="group__SE__Fast.html#ga4b55b5f49d921ca4b63f874d8404c4d5">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="group__SE__Fast.html#ga4b55b5f49d921ca4b63f874d8404c4d5"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#ga40b361c2f9374c541282feca1e237dba">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="group__SE__Fast.html#ga40b361c2f9374c541282feca1e237dba"></a><br/></dl></ul>
<h2><a name="pri-methods"></a>
Private Member 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">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="group__SE__Fast.html#ga8f4353c8f8c65ed00806861471bd857f"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="el" href="group__SE__Fast.html#gac68652e5ed46a097f846ba9a86fcd630">checkSAT</a> ()
<li>bool <a class="el" href="group__SE__Fast.html#ga6d05128f71cc4e239030fe0434cda727">split</a> ()
<dl class="el"><dd class="mdescRight">Choose a splitter. <a href="group__SE__Fast.html#ga6d05128f71cc4e239030fe0434cda727"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="group__SE__Fast.html#ga711544b769f4c0a5713df247de927019">findSplitter</a> ()
<dl class="el"><dd class="mdescRight">Returns a splitter. <a href="group__SE__Fast.html#ga711544b769f4c0a5713df247de927019"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#gadf72861b6482f6c585f3199d1436f7be">clearLiterals</a> ()
<dl class="el"><dd class="mdescRight">Clear the list of asserted literals (d_literals) <a href="group__SE__Fast.html#gadf72861b6482f6c585f3199d1436f7be"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#ga453b1d390ee3b7af68fe8e915443d1ad">updateLitScores</a> (bool firstTime)
<li>void <a class="el" href="group__SE__Fast.html#ga775b06e155128cc8817f254bc293c6c6">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="group__SE__Fast.html#ga775b06e155128cc8817f254bc293c6c6"></a><br/></dl><li>bool <a class="el" href="group__SE__Fast.html#gac6d49471ba5c76fffc7581e01e423218">bcp</a> ()
<dl class="el"><dd class="mdescRight">Boolean constraint propagation. <a href="group__SE__Fast.html#gac6d49471ba5c76fffc7581e01e423218"></a><br/></dl><li>bool <a class="el" href="group__SE__Fast.html#ga4490cc372993398612e7556e14222ff3">fixConflict</a> ()
<dl class="el"><dd class="mdescRight">Determines backtracking level and adds conflict clauses. <a href="group__SE__Fast.html#ga4490cc372993398612e7556e14222ff3"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#gaf7daf6eac739438b5b25175bc7d63a71">assertAssumptions</a> ()
<dl class="el"><dd class="mdescRight">FIXME: document this. <a href="group__SE__Fast.html#gaf7daf6eac739438b5b25175bc7d63a71"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#ga2c71aa94289db9ece678963617660640">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="group__SE__Fast.html#ga2c71aa94289db9ece678963617660640"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#ga33ff53b3eeb9811b1510fffd3cdcf234">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="group__SE__Fast.html#ga33ff53b3eeb9811b1510fffd3cdcf234"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#ga6d190905fefb2a36650306e5b577dd9a">commitFacts</a> ()
<dl class="el"><dd class="mdescRight">Commit all the enqueued facts to the DPs. <a href="group__SE__Fast.html#ga6d190905fefb2a36650306e5b577dd9a"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#gafa7937cc0b7d14c0aafb1f9c20abf011">clearFacts</a> ()
<dl class="el"><dd class="mdescRight">Clear the local fact queue. <a href="group__SE__Fast.html#gafa7937cc0b7d14c0aafb1f9c20abf011"></a><br/></dl><li>bool <a class="el" href="group__SE__Fast.html#gad7548d572241f215212176af0216cb94">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="group__SE__Fast.html#gad7548d572241f215212176af0216cb94"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#ga88d524fb175ae8156696cc73cb182ffd">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="group__SE__Fast.html#ga88d524fb175ae8156696cc73cb182ffd"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#gaac9cb2de28ec162fe5ecfe042ad7b101">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="group__SE__Fast.html#gaac9cb2de28ec162fe5ecfe042ad7b101"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#ga6e64b8f0a42bd4b42d22b50b351219c9">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="group__SE__Fast.html#ga6e64b8f0a42bd4b42d22b50b351219c9"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#ga2ec0e19a01ac0926b690c50a3206c5a3">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="group__SE__Fast.html#ga2ec0e19a01ac0926b690c50a3206c5a3"></a><br/></dl><li>void <a class="el" href="group__SE__Fast.html#gab3f2a42375c5b3875ad18acd47ee124d">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="group__SE__Fast.html#gab3f2a42375c5b3875ad18acd47ee124d"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="el" href="group__SE__Fast.html#gaac7ba666d67d3d4808642c5c7858db95">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="group__SE__Fast.html#gaac7ba666d67d3d4808642c5c7858db95"></a><br/></dl></ul>
<tr><td colspan="2"><div class="groupHeader">Processing a Conflict</div></td></tr>
<ul>
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="group__SE__Fast.html#ga2535b1eabb9eb7e7f3a6197dbb377cb4">processConflict</a> (const <a class="el" href="classCVC3_1_1Literal.html">Literal</a> &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="group__SE__Fast.html#ga2535b1eabb9eb7e7f3a6197dbb377cb4"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="group__SE__Fast.html#ga3a60df36c6707139c0f6662f32270765">processConflict</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &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="group__SE__Fast.html#ga3a60df36c6707139c0f6662f32270765"></a><br/></dl></ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li>std::string <a class="el" href="group__SE__Fast.html#ga91ff4e54d0b66c31eb0d2653fad650cb">d_name</a>
<dl class="el"><dd class="mdescRight">Name. <a href="group__SE__Fast.html#ga91ff4e54d0b66c31eb0d2653fad650cb"></a><br/></dl><li><a class="el" href="classCVC3_1_1DecisionEngine.html">DecisionEngine</a> * <a class="el" href="group__SE__Fast.html#gafa042a51f718c312ea7728f175958e35">d_decisionEngine</a>
<dl class="el"><dd class="mdescRight">Decision Engine. <a href="group__SE__Fast.html#gafa042a51f718c312ea7728f175958e35"></a><br/></dl><li><a class="el" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="el" href="group__SE__Fast.html#ga29e749a0ca7cbe86118a0d72e02e0696">d_unitPropCount</a>
<dl class="el"><dd class="mdescRight">Total number of unit propagations. <a href="group__SE__Fast.html#ga29e749a0ca7cbe86118a0d72e02e0696"></a><br/></dl><li><a class="el" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="el" href="group__SE__Fast.html#ga749d335e3d18b71aa951d37e943fbf50">d_circuitPropCount</a>
<dl class="el"><dd class="mdescRight">Total number of circuit propagations. <a href="group__SE__Fast.html#ga749d335e3d18b71aa951d37e943fbf50"></a><br/></dl><li><a class="el" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="el" href="group__SE__Fast.html#gaecd7cc2115fe235653a62acf93ccb1e5">d_conflictCount</a>
<dl class="el"><dd class="mdescRight">Total number of conflicts. <a href="group__SE__Fast.html#gaecd7cc2115fe235653a62acf93ccb1e5"></a><br/></dl><li><a class="el" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="el" href="group__SE__Fast.html#ga483cb3c4c889013b03e2c923977d4ae5">d_conflictClauseCount</a>
<dl class="el"><dd class="mdescRight">Total number of conflict clauses generated (not all may be active) <a href="group__SE__Fast.html#ga483cb3c4c889013b03e2c923977d4ae5"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDList.html">CDList</a>< <a class="el" href="classCVC3_1_1ClauseOwner.html">ClauseOwner</a> > <a class="el" href="group__SE__Fast.html#gaa1dd9a29eac4c7da6c669d7888909ca5">d_clauses</a>
<dl class="el"><dd class="mdescRight">Backtrackable list of clauses. <a href="group__SE__Fast.html#gaa1dd9a29eac4c7da6c669d7888909ca5"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDMap.html">CDMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > <a class="el" href="group__SE__Fast.html#gabe8dbaf4592793c49cd58ff93a897a06">d_unreportedLits</a>
<dl class="el"><dd class="mdescRight">Backtrackable set of pending unprocessed literals. <a href="group__SE__Fast.html#gabe8dbaf4592793c49cd58ff93a897a06"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDMap.html">CDMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, bool > <a class="el" href="group__SE__Fast.html#ga8217149b882d328384bd7a04a5e5c5f3">d_unreportedLitsHandled</a>
<li><a class="el" href="classCVC3_1_1CDList.html">CDList</a>< <a class="el" href="classCVC3_1_1SmartCDO.html">SmartCDO</a>< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > > <a class="el" href="group__SE__Fast.html#ga07c8e260b60d83042c97453892a15f38">d_nonLiterals</a>
<dl class="el"><dd class="mdescRight">Backtrackable list of non-literals (non-CNF formulas). <a href="group__SE__Fast.html#ga07c8e260b60d83042c97453892a15f38"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDMap.html">CDMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > <a class="el" href="group__SE__Fast.html#gae88240871407db238ad8c6a795ba6b91">d_nonLiteralsSaved</a>
<dl class="el"><dd class="mdescRight">prevent reprocessing <a href="group__SE__Fast.html#gae88240871407db238ad8c6a795ba6b91"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > <a class="el" href="group__SE__Fast.html#gaa8b578a017bcddd578e943add44c2940">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="group__SE__Fast.html#gaa8b578a017bcddd578e943add44c2940"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< unsigned > <a class="el" href="group__SE__Fast.html#gae4a9e9926613365979d36e2a98769381">d_nonlitQueryStart</a>
<dl class="el"><dd class="mdescRight">Size of d_nonLiterals before most recent query. <a href="group__SE__Fast.html#gae4a9e9926613365979d36e2a98769381"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< unsigned > <a class="el" href="group__SE__Fast.html#ga8472c82be89057f32c68a0f0423215a2">d_nonlitQueryEnd</a>
<dl class="el"><dd class="mdescRight">Size of d_nonLiterals after query (not including DP-generated non-literals) <a href="group__SE__Fast.html#ga8472c82be89057f32c68a0f0423215a2"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< unsigned > <a class="el" href="group__SE__Fast.html#ga71a2e31fe2a16420a416b5aeced09455">d_clausesQueryStart</a>
<dl class="el"><dd class="mdescRight">Size of d_clauses before most recent query. <a href="group__SE__Fast.html#ga71a2e31fe2a16420a416b5aeced09455"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDO.html">CDO</a>< unsigned > <a class="el" href="group__SE__Fast.html#ga6dbfd2cd66dee5634f096593f26c47e7">d_clausesQueryEnd</a>
<dl class="el"><dd class="mdescRight">Size of d_clauses after query. <a href="group__SE__Fast.html#ga6dbfd2cd66dee5634f096593f26c47e7"></a><br/></dl><li>std::vector< std::deque<br class="typebreak"/>
< <a class="el" href="classCVC3_1_1ClauseOwner.html">ClauseOwner</a> > * > <a class="el" href="group__SE__Fast.html#ga8e96b8f24bd89c190e561f387a4a30ee">d_conflictClauseStack</a>
<dl class="el"><dd class="mdescRight">Array of conflict clauses: one deque for each outstanding query. <a href="group__SE__Fast.html#ga8e96b8f24bd89c190e561f387a4a30ee"></a><br/></dl><li>std::deque< <a class="el" href="classCVC3_1_1ClauseOwner.html">ClauseOwner</a> > * <a class="el" href="group__SE__Fast.html#gad79601e3b2032aee4d23dc4bbd785fc3">d_conflictClauses</a>
<dl class="el"><dd class="mdescRight">Reference to top deque of conflict clauses. <a href="group__SE__Fast.html#gad79601e3b2032aee4d23dc4bbd785fc3"></a><br/></dl><li><a class="el" href="classCVC3_1_1SearchEngineFast_1_1ConflictClauseManager.html">ConflictClauseManager</a> <a class="el" href="group__SE__Fast.html#gaab577b22f09d51b9b15954b9a529c05d">d_conflictClauseManager</a>
<li>std::vector< <a class="el" href="classCVC3_1_1Clause.html">Clause</a> > <a class="el" href="group__SE__Fast.html#gad05f577d00e93fefed74eb0c19015090">d_unitConflictClauses</a>
<dl class="el"><dd class="mdescRight">Unprocessed unit conflict clauses. <a href="group__SE__Fast.html#gad05f577d00e93fefed74eb0c19015090"></a><br/></dl><li>std::vector< <a class="el" href="classCVC3_1_1Literal.html">Literal</a> > <a class="el" href="group__SE__Fast.html#gaa6a69bd3df4bb72abd1e9b0fe868fc0d">d_literals</a>
<dl class="el"><dd class="mdescRight">Set of literals to be processed by bcp. <a href="group__SE__Fast.html#gaa6a69bd3df4bb72abd1e9b0fe868fc0d"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDMap.html">CDMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="classCVC3_1_1Literal.html">Literal</a> > <a class="el" href="group__SE__Fast.html#gaf720bf50e81fc4e2561b587d97ec2839">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="group__SE__Fast.html#gaf720bf50e81fc4e2561b587d97ec2839"></a><br/></dl><li>std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > <a class="el" href="group__SE__Fast.html#ga4b05dccebac3de019dc112ab3dffc988">d_factQueue</a>
<dl class="el"><dd class="mdescRight">Queue of derived facts to be sent to DPs. <a href="group__SE__Fast.html#ga4b05dccebac3de019dc112ab3dffc988"></a><br/></dl><li>bool <a class="el" href="group__SE__Fast.html#gaa1ea8707c10a13a631402860eff87026">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="group__SE__Fast.html#gaa1ea8707c10a13a631402860eff87026"></a><br/></dl><li>bool <a class="el" href="group__SE__Fast.html#ga6368ec56b20c12896000e370bbb4a3b6">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="group__SE__Fast.html#ga6368ec56b20c12896000e370bbb4a3b6"></a><br/></dl><li><a class="el" href="classCVC3_1_1CDList.html">CDList</a>< <a class="el" href="classCVC3_1_1Literal.html">Literal</a> > <a class="el" href="group__SE__Fast.html#ga0214c0205e48fd792c4d01d3428cd333">d_litsAlive</a>
<dl class="el"><dd class="mdescRight">Set of alive literals that shouldn't be garbage-collected. <a href="group__SE__Fast.html#ga0214c0205e48fd792c4d01d3428cd333"></a><br/></dl><li>std::vector< <a class="el" href="classCVC3_1_1Circuit.html">Circuit</a> * > <a class="el" href="group__SE__Fast.html#ga5db32a771408c468676e407075184b64">d_circuits</a>
<dl class="el"><dd class="mdescRight">Mappings of literals to vectors of pointers to the corresponding watched literals. <a href="group__SE__Fast.html#ga5db32a771408c468676e407075184b64"></a><br/></dl><li><a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>< std::vector<br class="typebreak"/>
< <a class="el" href="classCVC3_1_1Circuit.html">Circuit</a> * > > <a class="el" href="group__SE__Fast.html#ga84bfa366c43221ba288e0a1bd716efc6">d_circuitsByExpr</a>
<li>int <a class="el" href="group__SE__Fast.html#gab27227ee9e005ab22a9e2a251bc7c6d1">d_lastConflictScope</a>
<dl class="el"><dd class="mdescRight">The scope of the last conflict. <a href="group__SE__Fast.html#gab27227ee9e005ab22a9e2a251bc7c6d1"></a><br/></dl><li><a class="el" href="classCVC3_1_1Clause.html">Clause</a> <a class="el" href="group__SE__Fast.html#ga46e91bb5d782794c6dca6abaa99dc4f9">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="group__SE__Fast.html#ga46e91bb5d782794c6dca6abaa99dc4f9"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="group__SE__Fast.html#gae961b4fb4bb059a1d867447fc487aaee">d_conflictTheorem</a>
<dl class="el"><dd class="mdescRight">Theorem(FALSE) which generated a conflict. <a href="group__SE__Fast.html#gae961b4fb4bb059a1d867447fc487aaee"></a><br/></dl><li>unsigned <a class="el" href="group__SE__Fast.html#gad80c2b69b88a04c8c78309859abd3f76">d_litsMaxScorePos</a>
<dl class="el"><dd class="mdescRight">Position of a literal with max score in d_litsByScores. <a href="group__SE__Fast.html#gad80c2b69b88a04c8c78309859abd3f76"></a><br/></dl><li>std::vector< <a class="el" href="classCVC3_1_1Literal.html">Literal</a> > <a class="el" href="group__SE__Fast.html#ga57c1c1e58ebd2c1d23a57db97880fbbc">d_litsByScores</a>
<dl class="el"><dd class="mdescRight">Vector of literals sorted by score. <a href="group__SE__Fast.html#ga57c1c1e58ebd2c1d23a57db97880fbbc"></a><br/></dl><li>int <a class="el" href="group__SE__Fast.html#ga52c9c181bcd623a36ab594e0ee16a67e">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="group__SE__Fast.html#ga52c9c181bcd623a36ab594e0ee16a67e"></a><br/></dl><li>int <a class="el" href="group__SE__Fast.html#ga2d54fdadc1b167dbbb366e37e0b97a58">d_litSortCount</a>
<dl class="el"><dd class="mdescRight">Internal (decrementing) count of added splitters, to sort d_litByScores. <a href="group__SE__Fast.html#ga2d54fdadc1b167dbbb366e37e0b97a58"></a><br/></dl><li>const bool <a class="el" href="group__SE__Fast.html#ga3877f82445d777c19c60b6ec117335e2">d_berkminFlag</a>
<dl class="el"><dd class="mdescRight">Flag to switch on/off the berkmin heuristic. <a href="group__SE__Fast.html#ga3877f82445d777c19c60b6ec117335e2"></a><br/></dl></ul>
<h2><a name="friends"></a>
Friends</h2>
<ul>
<li>class <a class="el" href="classCVC3_1_1SearchEngineFast.html#a120b136c2c9bc1938e0cd2cca80d91e4">Circuit</a>
<li>class <a class="el" href="group__SE__Fast.html#ga771f251de98c5689b33e123d5603722d">ConflictClauseManager</a>
<dl class="el"><dd class="mdescRight">Helper class for managing conflict clauses. <a href="group__SE__Fast.html#ga771f251de98c5689b33e123d5603722d"></a><br/></dl></ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock"><p>Implementation of a faster search engine, using newer techniques. </p>
<p>This search engine is engineered for greater speed. It seeks to eliminate the use of recursion, and instead replace it with iterative procedures that have cleanly defined invariants. This will hopefully not only eliminate bugs or inefficiencies that have been difficult to track down in the default version, but it should also make it easier to trace, read, and understand. It strives to be in line with the most modern <a class="el" href="namespaceSAT.html">SAT</a> techniques.</p>
<p>There are three other significant changes.</p>
<p>One, we want to improve the performance on heavily non-CNF problems. Unlike the older CVC, <a class="el" href="namespaceCVC3.html">CVC3</a> does not expand problems into CNF and solve, but rather uses decision procedures to effect the same thing, but often much more slowly. This search engine will leverage off knowledge gained from the DPs in the form of conflict clauses as much as possible.</p>
<p>Two, the solver has traditionally had a difficult time getting started on non-CNF problems. Modern satsolvers also have this problem, and so they employ "restarts" to try solving the problem again after gaining more knowledge about the problem at hand. This allows a more accurate choice of splitters, and in the case of non-CNF problems, the solver can immediately leverage off CNF conflict clauses that were not initially available.</p>
<p>Third, this code is specifically designed to deal with the new dependency tracking. Lazy maps will be eliminated in favor implicit conflict graphs, reducing computation time in two different ways. </p>
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00086">86</a> of file <a class="el" href="search__fast_8h_source.html">search_fast.h</a>.</p>
</div><hr/><h2>Friends And Related Function Documentation</h2>
<a class="anchor" id="a120b136c2c9bc1938e0cd2cca80d91e4"></a><!-- doxytag: member="CVC3::SearchEngineFast::Circuit" ref="a120b136c2c9bc1938e0cd2cca80d91e4" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">friend class <a class="el" href="classCVC3_1_1Circuit.html">Circuit</a><code> [friend]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="search__fast_8h_source.html#l00088">88</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">addNonLiteralFact()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="search__fast_8h_source.html">search_fast.h</a></li>
<li><a class="el" href="search__fast_8cpp_source.html">search_fast.cpp</a></li>
</ul>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
