<!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: search_fast.h Source File</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 class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div class="header">
<div class="headertitle">
<div class="title">search_fast.h</div> </div>
</div>
<div class="contents">
<a href="search__fast_8h.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00002"></a>00002 <span class="comment"></span><span class="comment">/*!</span>
<a name="l00003"></a>00003 <span class="comment"> * \file search_fast.h</span>
<a name="l00004"></a>00004 <span class="comment"> *</span>
<a name="l00005"></a>00005 <span class="comment"> * Author: Mark Zavislak</span>
<a name="l00006"></a>00006 <span class="comment"> *</span>
<a name="l00007"></a>00007 <span class="comment"> * Created: Mon Jul 21 17:33:18 UTC 2003</span>
<a name="l00008"></a>00008 <span class="comment"> *</span>
<a name="l00009"></a>00009 <span class="comment"> * <hr></span>
<a name="l00010"></a>00010 <span class="comment"> *</span>
<a name="l00011"></a>00011 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00012"></a>00012 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00013"></a>00013 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00014"></a>00014 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00015"></a>00015 <span class="comment"> *</span>
<a name="l00016"></a>00016 <span class="comment"> * <hr></span>
<a name="l00017"></a>00017 <span class="comment"> *</span>
<a name="l00018"></a>00018 <span class="comment"> * A faster implementation of the proof search engine</span>
<a name="l00019"></a>00019 <span class="comment"> */</span><span class="comment"></span>
<a name="l00020"></a>00020 <span class="comment">///////////////////////////////////////////////////////////////////////////////</span>
<a name="l00021"></a>00021 <span class="comment"></span>
<a name="l00022"></a>00022 <span class="preprocessor">#ifndef _cvc3__include__search_fast_h_</span>
<a name="l00023"></a>00023 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__search_fast_h_</span>
<a name="l00024"></a>00024 <span class="preprocessor"></span>
<a name="l00025"></a>00025 <span class="preprocessor">#include <deque></span>
<a name="l00026"></a>00026 <span class="preprocessor">#include <utility></span>
<a name="l00027"></a>00027 <span class="preprocessor">#include "<a class="code" href="search__impl__base_8h.html" title="Abstract API to the proof search engine.">search_impl_base.h</a>"</span>
<a name="l00028"></a>00028 <span class="preprocessor">#include "<a class="code" href="variable_8h.html">variable.h</a>"</span>
<a name="l00029"></a>00029 <span class="preprocessor">#include "<a class="code" href="circuit_8h.html" title="Circuit class.">circuit.h</a>"</span>
<a name="l00030"></a>00030 <span class="preprocessor">#include "<a class="code" href="statistics_8h.html" title="Description: Counters and flags for collecting run-time statistics.">statistics.h</a>"</span>
<a name="l00031"></a>00031 <span class="preprocessor">#include <set></span>
<a name="l00032"></a>00032 <span class="preprocessor">#include "<a class="code" href="smartcdo_8h.html" title="Smart context-dependent object wrapper.">smartcdo.h</a>"</span>
<a name="l00033"></a>00033
<a name="l00034"></a>00034 <span class="keyword">namespace </span>CVC3 {
<a name="l00035"></a>00035
<a name="l00036"></a>00036 <span class="keyword">class </span>VariableManager;
<a name="l00037"></a>00037 <span class="keyword">class </span>DecisionEngine;
<a name="l00038"></a>00038 <span class="comment"></span>
<a name="l00039"></a>00039 <span class="comment">////////////////////////////////////////////////////////////////////////////</span>
<a name="l00040"></a>00040 <span class="comment">//////////// Definition of modules (groups) for doxygen ////////////////////</span>
<a name="l00041"></a>00041 <span class="comment">////////////////////////////////////////////////////////////////////////////</span>
<a name="l00042"></a>00042 <span class="comment"></span><span class="comment"></span>
<a name="l00043"></a>00043 <span class="comment">/*!</span>
<a name="l00044"></a>00044 <span class="comment"> * \defgroup SE_Fast Fast Search Engine</span>
<a name="l00045"></a>00045 <span class="comment"> * \ingroup SE</span>
<a name="l00046"></a>00046 <span class="comment"> *</span>
<a name="l00047"></a>00047 <span class="comment"> * This module includes all the components of the fast search</span>
<a name="l00048"></a>00048 <span class="comment"> * engine.</span>
<a name="l00049"></a>00049 <span class="comment"> * @{</span>
<a name="l00050"></a>00050 <span class="comment"> */</span>
<a name="l00051"></a>00051 <span class="comment"></span>
<a name="l00052"></a>00052 <span class="comment"> //! Implementation of a faster search engine, using newer techniques.</span>
<a name="l00053"></a>00053 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00054"></a>00054 <span class="comment"></span>
<a name="l00055"></a>00055 <span class="comment"> This search engine is engineered for greater speed. It seeks to</span>
<a name="l00056"></a>00056 <span class="comment"> eliminate the use of recursion, and instead replace it with</span>
<a name="l00057"></a>00057 <span class="comment"> iterative procedures that have cleanly defined invariants. This</span>
<a name="l00058"></a>00058 <span class="comment"> will hopefully not only eliminate bugs or inefficiencies that have</span>
<a name="l00059"></a>00059 <span class="comment"> been difficult to track down in the default version, but it should</span>
<a name="l00060"></a>00060 <span class="comment"> also make it easier to trace, read, and understand. It strives to</span>
<a name="l00061"></a>00061 <span class="comment"> be in line with the most modern SAT techniques.</span>
<a name="l00062"></a>00062 <span class="comment"></span>
<a name="l00063"></a>00063 <span class="comment"> There are three other significant changes.</span>
<a name="l00064"></a>00064 <span class="comment"></span>
<a name="l00065"></a>00065 <span class="comment"> One, we want to improve the performance on heavily non-CNF problems.</span>
<a name="l00066"></a>00066 <span class="comment"> Unlike the older CVC, CVC3 does not expand problems into CNF and</span>
<a name="l00067"></a>00067 <span class="comment"> solve, but rather uses decision procedures to effect the same thing,</span>
<a name="l00068"></a>00068 <span class="comment"> but often much more slowly. This search engine will leverage off</span>
<a name="l00069"></a>00069 <span class="comment"> knowledge gained from the DPs in the form of conflict clauses as</span>
<a name="l00070"></a>00070 <span class="comment"> much as possible.</span>
<a name="l00071"></a>00071 <span class="comment"></span>
<a name="l00072"></a>00072 <span class="comment"> Two, the solver has traditionally had a difficult time getting</span>
<a name="l00073"></a>00073 <span class="comment"> started on non-CNF problems. Modern satsolvers also have this</span>
<a name="l00074"></a>00074 <span class="comment"> problem, and so they employ "restarts" to try solving the problem</span>
<a name="l00075"></a>00075 <span class="comment"> again after gaining more knowledge about the problem at hand. This</span>
<a name="l00076"></a>00076 <span class="comment"> allows a more accurate choice of splitters, and in the case of</span>
<a name="l00077"></a>00077 <span class="comment"> non-CNF problems, the solver can immediately leverage off CNF</span>
<a name="l00078"></a>00078 <span class="comment"> conflict clauses that were not initially available.</span>
<a name="l00079"></a>00079 <span class="comment"></span>
<a name="l00080"></a>00080 <span class="comment"> Third, this code is specifically designed to deal with the new</span>
<a name="l00081"></a>00081 <span class="comment"> dependency tracking. Lazy maps will be eliminated in favor implicit</span>
<a name="l00082"></a>00082 <span class="comment"> conflict graphs, reducing computation time in two different ways.</span>
<a name="l00083"></a>00083 <span class="comment"></span>
<a name="l00084"></a>00084 <span class="comment"> */</span>
<a name="l00085"></a>00085
<a name="l00086"></a><a class="code" href="classCVC3_1_1SearchEngineFast.html">00086</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchEngineFast.html" title="Implementation of a faster search engine, using newer techniques.">SearchEngineFast</a> : <span class="keyword">public</span> <a class="code" href="classCVC3_1_1SearchImplBase.html" title="API to to a generic proof search engine (a.k.a. SAT solver)">SearchImplBase</a> {
<a name="l00087"></a>00087
<a name="l00088"></a><a class="code" href="classCVC3_1_1SearchEngineFast.html#a120b136c2c9bc1938e0cd2cca80d91e4">00088</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Circuit.html">Circuit</a>;
<a name="l00089"></a>00089 <span class="comment"></span>
<a name="l00090"></a>00090 <span class="comment"> /*! \addtogroup SE_Fast</span>
<a name="l00091"></a>00091 <span class="comment"> * @{</span>
<a name="l00092"></a>00092 <span class="comment"> */</span>
<a name="l00093"></a>00093 <span class="comment"></span>
<a name="l00094"></a>00094 <span class="comment"> //! Name</span>
<a name="l00095"></a><a class="code" href="group__SE__Fast.html#ga91ff4e54d0b66c31eb0d2653fad650cb">00095</a> <span class="comment"></span> std::string <a class="code" href="group__SE__Fast.html#ga91ff4e54d0b66c31eb0d2653fad650cb" title="Name.">d_name</a>;<span class="comment"></span>
<a name="l00096"></a>00096 <span class="comment"> //! Decision Engine</span>
<a name="l00097"></a><a class="code" href="group__SE__Fast.html#gafa042a51f718c312ea7728f175958e35">00097</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1DecisionEngine.html">DecisionEngine</a> *<a class="code" href="group__SE__Fast.html#gafa042a51f718c312ea7728f175958e35" title="Decision Engine.">d_decisionEngine</a>;<span class="comment"></span>
<a name="l00098"></a>00098 <span class="comment"> //! Total number of unit propagations</span>
<a name="l00099"></a><a class="code" href="group__SE__Fast.html#ga29e749a0ca7cbe86118a0d72e02e0696">00099</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="code" href="group__SE__Fast.html#ga29e749a0ca7cbe86118a0d72e02e0696" title="Total number of unit propagations.">d_unitPropCount</a>;<span class="comment"></span>
<a name="l00100"></a>00100 <span class="comment"> //! Total number of circuit propagations</span>
<a name="l00101"></a><a class="code" href="group__SE__Fast.html#ga749d335e3d18b71aa951d37e943fbf50">00101</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="code" href="group__SE__Fast.html#ga749d335e3d18b71aa951d37e943fbf50" title="Total number of circuit propagations.">d_circuitPropCount</a>;<span class="comment"></span>
<a name="l00102"></a>00102 <span class="comment"> //! Total number of conflicts</span>
<a name="l00103"></a><a class="code" href="group__SE__Fast.html#gaecd7cc2115fe235653a62acf93ccb1e5">00103</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="code" href="group__SE__Fast.html#gaecd7cc2115fe235653a62acf93ccb1e5" title="Total number of conflicts.">d_conflictCount</a>;<span class="comment"></span>
<a name="l00104"></a>00104 <span class="comment"> //! Total number of conflict clauses generated (not all may be active)</span>
<a name="l00105"></a><a class="code" href="group__SE__Fast.html#ga483cb3c4c889013b03e2c923977d4ae5">00105</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1StatCounter.html">StatCounter</a> <a class="code" href="group__SE__Fast.html#ga483cb3c4c889013b03e2c923977d4ae5" title="Total number of conflict clauses generated (not all may be active)">d_conflictClauseCount</a>;
<a name="l00106"></a>00106 <span class="comment"></span>
<a name="l00107"></a>00107 <span class="comment"> //! Backtrackable list of clauses.</span>
<a name="l00108"></a>00108 <span class="comment"></span><span class="comment"> /*! New clauses may come into play</span>
<a name="l00109"></a>00109 <span class="comment"> from the decision procedures that are context dependent. */</span>
<a name="l00110"></a><a class="code" href="group__SE__Fast.html#gaa1dd9a29eac4c7da6c669d7888909ca5">00110</a> <a class="code" href="classCVC3_1_1CDList.html">CDList<ClauseOwner></a> <a class="code" href="group__SE__Fast.html#gaa1dd9a29eac4c7da6c669d7888909ca5" title="Backtrackable list of clauses.">d_clauses</a>;
<a name="l00111"></a>00111 <span class="comment"></span>
<a name="l00112"></a>00112 <span class="comment"> //! Backtrackable set of pending unprocessed literals.</span>
<a name="l00113"></a>00113 <span class="comment"></span><span class="comment"> /*! These can be discovered at any scope level during conflict</span>
<a name="l00114"></a>00114 <span class="comment"> analysis. */</span>
<a name="l00115"></a><a class="code" href="group__SE__Fast.html#gabe8dbaf4592793c49cd58ff93a897a06">00115</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,Theorem></a> <a class="code" href="group__SE__Fast.html#gabe8dbaf4592793c49cd58ff93a897a06" title="Backtrackable set of pending unprocessed literals.">d_unreportedLits</a>;
<a name="l00116"></a><a class="code" href="group__SE__Fast.html#ga8217149b882d328384bd7a04a5e5c5f3">00116</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,bool></a> <a class="code" href="group__SE__Fast.html#ga8217149b882d328384bd7a04a5e5c5f3">d_unreportedLitsHandled</a>;
<a name="l00117"></a>00117 <span class="comment"></span>
<a name="l00118"></a>00118 <span class="comment"> //! Backtrackable list of non-literals (non-CNF formulas).</span>
<a name="l00119"></a>00119 <span class="comment"></span><span class="comment"> /*! We treat nonliterals like clauses, because they are a superset</span>
<a name="l00120"></a>00120 <span class="comment"> of clauses. We stick the real clauses into d_clauses, but all</span>
<a name="l00121"></a>00121 <span class="comment"> the rest have to be stored elsewhere. */</span>
<a name="l00122"></a><a class="code" href="group__SE__Fast.html#ga07c8e260b60d83042c97453892a15f38">00122</a> <a class="code" href="classCVC3_1_1CDList.html">CDList<SmartCDO<Theorem></a> > <a class="code" href="group__SE__Fast.html#ga07c8e260b60d83042c97453892a15f38" title="Backtrackable list of non-literals (non-CNF formulas).">d_nonLiterals</a>;
<a name="l00123"></a><a class="code" href="group__SE__Fast.html#gae88240871407db238ad8c6a795ba6b91">00123</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,Theorem></a> <a class="code" href="group__SE__Fast.html#gae88240871407db238ad8c6a795ba6b91" title="prevent reprocessing">d_nonLiteralsSaved</a>; <span class="comment">//!< prevent reprocessing</span>
<a name="l00124"></a>00124 <span class="comment"></span> <span class="comment">// CDMap<Expr,bool> d_nonLiteralSimplified; //!< Simplified non-literals</span>
<a name="l00125"></a>00125 <span class="comment"></span>
<a name="l00126"></a>00126 <span class="comment"> //! Theorem which records simplification of the last query</span>
<a name="l00127"></a><a class="code" href="group__SE__Fast.html#gaa8b578a017bcddd578e943add44c2940">00127</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<Theorem></a> <a class="code" href="group__SE__Fast.html#gaa8b578a017bcddd578e943add44c2940" title="Theorem which records simplification of the last query.">d_simplifiedThm</a>;
<a name="l00128"></a>00128 <span class="comment"></span>
<a name="l00129"></a>00129 <span class="comment"> //! Size of d_nonLiterals before most recent query</span>
<a name="l00130"></a><a class="code" href="group__SE__Fast.html#gae4a9e9926613365979d36e2a98769381">00130</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned></a> <a class="code" href="group__SE__Fast.html#gae4a9e9926613365979d36e2a98769381" title="Size of d_nonLiterals before most recent query.">d_nonlitQueryStart</a>;<span class="comment"></span>
<a name="l00131"></a>00131 <span class="comment"> //! Size of d_nonLiterals after query (not including DP-generated non-literals)</span>
<a name="l00132"></a><a class="code" href="group__SE__Fast.html#ga8472c82be89057f32c68a0f0423215a2">00132</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned></a> <a class="code" href="group__SE__Fast.html#ga8472c82be89057f32c68a0f0423215a2" title="Size of d_nonLiterals after query (not including DP-generated non-literals)">d_nonlitQueryEnd</a>;<span class="comment"></span>
<a name="l00133"></a>00133 <span class="comment"> //! Size of d_clauses before most recent query</span>
<a name="l00134"></a><a class="code" href="group__SE__Fast.html#ga71a2e31fe2a16420a416b5aeced09455">00134</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned></a> <a class="code" href="group__SE__Fast.html#ga71a2e31fe2a16420a416b5aeced09455" title="Size of d_clauses before most recent query.">d_clausesQueryStart</a>;<span class="comment"></span>
<a name="l00135"></a>00135 <span class="comment"> //! Size of d_clauses after query</span>
<a name="l00136"></a><a class="code" href="group__SE__Fast.html#ga6dbfd2cd66dee5634f096593f26c47e7">00136</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned></a> <a class="code" href="group__SE__Fast.html#ga6dbfd2cd66dee5634f096593f26c47e7" title="Size of d_clauses after query.">d_clausesQueryEnd</a>;
<a name="l00137"></a>00137 <span class="comment"></span>
<a name="l00138"></a>00138 <span class="comment"> //! Array of conflict clauses: one deque for each outstanding query</span>
<a name="l00139"></a><a class="code" href="group__SE__Fast.html#ga8e96b8f24bd89c190e561f387a4a30ee">00139</a> <span class="comment"></span> std::vector<std::deque<ClauseOwner>* > <a class="code" href="group__SE__Fast.html#ga8e96b8f24bd89c190e561f387a4a30ee" title="Array of conflict clauses: one deque for each outstanding query.">d_conflictClauseStack</a>;<span class="comment"></span>
<a name="l00140"></a>00140 <span class="comment"> //! Reference to top deque of conflict clauses</span>
<a name="l00141"></a><a class="code" href="group__SE__Fast.html#gad79601e3b2032aee4d23dc4bbd785fc3">00141</a> <span class="comment"></span> std::deque<ClauseOwner>* <a class="code" href="group__SE__Fast.html#gad79601e3b2032aee4d23dc4bbd785fc3" title="Reference to top deque of conflict clauses.">d_conflictClauses</a>;
<a name="l00142"></a>00142 <span class="comment"></span>
<a name="l00143"></a>00143 <span class="comment"> //! Helper class for managing conflict clauses</span>
<a name="l00144"></a>00144 <span class="comment"></span><span class="comment"> /*! Conflict clauses should only get popped when the context in which a</span>
<a name="l00145"></a>00145 <span class="comment"> * call to checkValid originates is popped. This helper class checks</span>
<a name="l00146"></a>00146 <span class="comment"> * every time there's a pop to see if the conflict clauses need to be</span>
<a name="l00147"></a>00147 <span class="comment"> * restored.</span>
<a name="l00148"></a>00148 <span class="comment"> */</span>
<a name="l00149"></a><a class="code" href="group__SE__Fast.html#ga771f251de98c5689b33e123d5603722d">00149</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchEngineFast_1_1ConflictClauseManager.html">ConflictClauseManager</a>;
<a name="l00150"></a><a class="code" href="classCVC3_1_1SearchEngineFast_1_1ConflictClauseManager.html">00150</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchEngineFast_1_1ConflictClauseManager.html">ConflictClauseManager</a> :<span class="keyword">public</span> <a class="code" href="classCVC3_1_1ContextNotifyObj.html">ContextNotifyObj</a> {
<a name="l00151"></a><a class="code" href="classCVC3_1_1SearchEngineFast_1_1ConflictClauseManager.html#aa6fcf7c07d399650f4e71e5d3fa488ba">00151</a> <a class="code" href="classCVC3_1_1SearchEngineFast.html" title="Implementation of a faster search engine, using newer techniques.">SearchEngineFast</a>* <a class="code" href="classCVC3_1_1SearchEngineFast_1_1ConflictClauseManager.html#aa6fcf7c07d399650f4e71e5d3fa488ba">d_se</a>;
<a name="l00152"></a><a class="code" href="classCVC3_1_1SearchEngineFast_1_1ConflictClauseManager.html#a90f8a2406642cbf3b0dcdd4ea70c8a38">00152</a> std::vector<int> <a class="code" href="classCVC3_1_1SearchEngineFast_1_1ConflictClauseManager.html#a90f8a2406642cbf3b0dcdd4ea70c8a38">d_restorePoints</a>;
<a name="l00153"></a>00153 <span class="keyword">public</span>:
<a name="l00154"></a><a class="code" href="classCVC3_1_1SearchEngineFast_1_1ConflictClauseManager.html#a67d461bc0dcf278235e30d3d93608e2b">00154</a> <a class="code" href="classCVC3_1_1SearchEngineFast_1_1ConflictClauseManager.html#a67d461bc0dcf278235e30d3d93608e2b">ConflictClauseManager</a>(<a class="code" href="classCVC3_1_1Context.html">Context</a>* context, <a class="code" href="classCVC3_1_1SearchEngineFast.html" title="Implementation of a faster search engine, using newer techniques.">SearchEngineFast</a>* se)
<a name="l00155"></a>00155 : <a class="code" href="classCVC3_1_1ContextNotifyObj.html">ContextNotifyObj</a>(context), <a class="code" href="classCVC3_1_1SearchEngineFast_1_1ConflictClauseManager.html#aa6fcf7c07d399650f4e71e5d3fa488ba">d_se</a>(se) {}
<a name="l00156"></a>00156 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchEngineFast_1_1ConflictClauseManager.html#ab6f279d5486d100804dcd8e749cb6665">setRestorePoint</a>();
<a name="l00157"></a>00157 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchEngineFast_1_1ConflictClauseManager.html#a71dce237fa65a2954f2ab4000369d8cc">notify</a>();
<a name="l00158"></a>00158 };
<a name="l00159"></a><a class="code" href="group__SE__Fast.html#gaab577b22f09d51b9b15954b9a529c05d">00159</a> <a class="code" href="classCVC3_1_1SearchEngineFast_1_1ConflictClauseManager.html">ConflictClauseManager</a> <a class="code" href="group__SE__Fast.html#gaab577b22f09d51b9b15954b9a529c05d">d_conflictClauseManager</a>;
<a name="l00160"></a>00160 <span class="comment"></span>
<a name="l00161"></a>00161 <span class="comment"> //! Unprocessed unit conflict clauses</span>
<a name="l00162"></a>00162 <span class="comment"></span><span class="comment"> /*! When we find unit conflict clauses, we are automatically going</span>
<a name="l00163"></a>00163 <span class="comment"> to jump back to the original scope. Hopefully we won't find</span>
<a name="l00164"></a>00164 <span class="comment"> multiple ones, but you never know with those wacky decision</span>
<a name="l00165"></a>00165 <span class="comment"> procedures just spitting new information out. These are then</span>
<a name="l00166"></a>00166 <span class="comment"> directly asserted then promptly forgotten about. Chaff keeps</span>
<a name="l00167"></a>00167 <span class="comment"> them around (for correctness maybe), but we already have the</span>
<a name="l00168"></a>00168 <span class="comment"> proofs stored in the literals themselves. */</span>
<a name="l00169"></a><a class="code" href="group__SE__Fast.html#gad05f577d00e93fefed74eb0c19015090">00169</a> std::vector<Clause> <a class="code" href="group__SE__Fast.html#gad05f577d00e93fefed74eb0c19015090" title="Unprocessed unit conflict clauses.">d_unitConflictClauses</a>;
<a name="l00170"></a>00170
<a name="l00171"></a>00171 <span class="comment"></span>
<a name="l00172"></a>00172 <span class="comment"> //! Set of literals to be processed by bcp.</span>
<a name="l00173"></a>00173 <span class="comment"></span><span class="comment"> /*! These are emptied out upon backtracking, because they can only</span>
<a name="l00174"></a>00174 <span class="comment"> be valid if they were already all processed without conflicts.</span>
<a name="l00175"></a>00175 <span class="comment"> Therefore, they don't need to be context dependent. */</span>
<a name="l00176"></a><a class="code" href="group__SE__Fast.html#gaa6a69bd3df4bb72abd1e9b0fe868fc0d">00176</a> std::vector<Literal> <a class="code" href="group__SE__Fast.html#gaa6a69bd3df4bb72abd1e9b0fe868fc0d" title="Set of literals to be processed by bcp.">d_literals</a>;<span class="comment"></span>
<a name="l00177"></a>00177 <span class="comment"> //! Set of asserted literals which may survive accross checkValid() calls</span>
<a name="l00178"></a>00178 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00179"></a>00179 <span class="comment"> * When a literal is asserted outside of checkValid() call, its</span>
<a name="l00180"></a>00180 <span class="comment"> * value is remembered in a Literal database, but the literal</span>
<a name="l00181"></a>00181 <span class="comment"> * queue for BCP is cleared. We add literals to this set at the</span>
<a name="l00182"></a>00182 <span class="comment"> * proper scope levels, and propagate them at the beginning of a</span>
<a name="l00183"></a>00183 <span class="comment"> * checkValid() call.</span>
<a name="l00184"></a>00184 <span class="comment"> */</span>
<a name="l00185"></a><a class="code" href="group__SE__Fast.html#gaf720bf50e81fc4e2561b587d97ec2839">00185</a> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,Literal></a> <a class="code" href="group__SE__Fast.html#gaf720bf50e81fc4e2561b587d97ec2839" title="Set of asserted literals which may survive accross checkValid() calls.">d_literalSet</a>;
<a name="l00186"></a>00186 <span class="comment"></span>
<a name="l00187"></a>00187 <span class="comment"> //! Queue of derived facts to be sent to DPs</span>
<a name="l00188"></a>00188 <span class="comment"></span><span class="comment"> /*! \sa addFact() and commitFacts() */</span>
<a name="l00189"></a><a class="code" href="group__SE__Fast.html#ga4b05dccebac3de019dc112ab3dffc988">00189</a> std::vector<Theorem> <a class="code" href="group__SE__Fast.html#ga4b05dccebac3de019dc112ab3dffc988" title="Queue of derived facts to be sent to DPs.">d_factQueue</a>;<span class="comment"></span>
<a name="l00190"></a>00190 <span class="comment"> /*! @brief When true, use TheoryCore::enqueueFact() instead of</span>
<a name="l00191"></a>00191 <span class="comment"> * addFact() in commitFacts()</span>
<a name="l00192"></a>00192 <span class="comment"> */</span>
<a name="l00193"></a><a class="code" href="group__SE__Fast.html#gaa1ea8707c10a13a631402860eff87026">00193</a> <span class="keywordtype">bool</span> <a class="code" href="group__SE__Fast.html#gaa1ea8707c10a13a631402860eff87026" title="When true, use TheoryCore::enqueueFact() instead of addFact() in commitFacts()">d_useEnqueueFact</a>;<span class="comment"></span>
<a name="l00194"></a>00194 <span class="comment"> //! True when checkSAT() is running</span>
<a name="l00195"></a>00195 <span class="comment"></span><span class="comment"> /*! Used by addLiteralFact() to determine whether to BCP the</span>
<a name="l00196"></a>00196 <span class="comment"> * literals immediately (outside of checkSAT()) or not.</span>
<a name="l00197"></a>00197 <span class="comment"> */</span>
<a name="l00198"></a><a class="code" href="group__SE__Fast.html#ga6368ec56b20c12896000e370bbb4a3b6">00198</a> <span class="keywordtype">bool</span> <a class="code" href="group__SE__Fast.html#ga6368ec56b20c12896000e370bbb4a3b6" title="True when checkSAT() is running.">d_inCheckSAT</a>;
<a name="l00199"></a>00199
<a name="l00200"></a>00200 <span class="comment"></span>
<a name="l00201"></a>00201 <span class="comment"> //! Set of alive literals that shouldn't be garbage-collected</span>
<a name="l00202"></a>00202 <span class="comment"></span><span class="comment"> /*! Unfortunately, I have a keep-alive issue. I think literals</span>
<a name="l00203"></a>00203 <span class="comment"> actually have to hang around, so I assert them to a separate</span>
<a name="l00204"></a>00204 <span class="comment"> d_litsAlive CDList. */</span>
<a name="l00205"></a><a class="code" href="group__SE__Fast.html#ga0214c0205e48fd792c4d01d3428cd333">00205</a> <a class="code" href="classCVC3_1_1CDList.html">CDList<Literal></a> <a class="code" href="group__SE__Fast.html#ga0214c0205e48fd792c4d01d3428cd333" title="Set of alive literals that shouldn't be garbage-collected.">d_litsAlive</a>;
<a name="l00206"></a>00206 <span class="comment"></span>
<a name="l00207"></a>00207 <span class="comment"> /*! @brief Mappings of literals to vectors of pointers to the</span>
<a name="l00208"></a>00208 <span class="comment"> corresponding watched literals. */</span><span class="comment"></span>
<a name="l00209"></a>00209 <span class="comment"> /*! A pointer is a pair (clause,i), where 'i' in {0,1} is the index</span>
<a name="l00210"></a>00210 <span class="comment"> of the watch pointer in the clause.</span>
<a name="l00211"></a>00211 <span class="comment"> */</span>
<a name="l00212"></a>00212 <span class="comment">// ExprHashMap<std::vector<std::pair<Clause, int> > > d_wp;</span>
<a name="l00213"></a>00213
<a name="l00214"></a><a class="code" href="group__SE__Fast.html#ga5db32a771408c468676e407075184b64">00214</a> std::vector<Circuit*> <a class="code" href="group__SE__Fast.html#ga5db32a771408c468676e407075184b64" title="Mappings of literals to vectors of pointers to the corresponding watched literals.">d_circuits</a>;
<a name="l00215"></a><a class="code" href="group__SE__Fast.html#ga84bfa366c43221ba288e0a1bd716efc6">00215</a> <a class="code" href="classCVC3_1_1ExprHashMap.html">ExprHashMap<std::vector<Circuit*></a> > <a class="code" href="group__SE__Fast.html#ga84bfa366c43221ba288e0a1bd716efc6">d_circuitsByExpr</a>;
<a name="l00216"></a>00216 <span class="comment"></span>
<a name="l00217"></a>00217 <span class="comment"> //! The scope of the last conflict</span>
<a name="l00218"></a>00218 <span class="comment"></span><span class="comment"> /*! This is the true scope of the conflict, not necessarily the</span>
<a name="l00219"></a>00219 <span class="comment"> scope where the conflict was detected. */</span>
<a name="l00220"></a><a class="code" href="group__SE__Fast.html#gab27227ee9e005ab22a9e2a251bc7c6d1">00220</a> <span class="keywordtype">int</span> <a class="code" href="group__SE__Fast.html#gab27227ee9e005ab22a9e2a251bc7c6d1" title="The scope of the last conflict.">d_lastConflictScope</a>;<span class="comment"></span>
<a name="l00221"></a>00221 <span class="comment"> //! The last conflict clause (for checkSAT()). May be Null.</span>
<a name="l00222"></a>00222 <span class="comment"></span><span class="comment"> /*! It records which conflict clause must be processed by BCP after</span>
<a name="l00223"></a>00223 <span class="comment"> backtracking from a conflict. A conflict may generate several</span>
<a name="l00224"></a>00224 <span class="comment"> conflict clauses, but only one of them will cause a unit</span>
<a name="l00225"></a>00225 <span class="comment"> propagation.</span>
<a name="l00226"></a>00226 <span class="comment"> */</span>
<a name="l00227"></a><a class="code" href="group__SE__Fast.html#ga46e91bb5d782794c6dca6abaa99dc4f9">00227</a> <a class="code" href="classCVC3_1_1Clause.html" title="A class representing a CNF clause (a smart pointer)">Clause</a> <a class="code" href="group__SE__Fast.html#ga46e91bb5d782794c6dca6abaa99dc4f9" title="The last conflict clause (for checkSAT()). May be Null.">d_lastConflictClause</a>;<span class="comment"></span>
<a name="l00228"></a>00228 <span class="comment"> //! Theorem(FALSE) which generated a conflict</span>
<a name="l00229"></a><a class="code" href="group__SE__Fast.html#gae961b4fb4bb059a1d867447fc487aaee">00229</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="group__SE__Fast.html#gae961b4fb4bb059a1d867447fc487aaee" title="Theorem(FALSE) which generated a conflict.">d_conflictTheorem</a>;
<a name="l00230"></a>00230 <span class="comment"></span>
<a name="l00231"></a>00231 <span class="comment"> /*! @brief Return a ref to the vector of watched literals. If no</span>
<a name="l00232"></a>00232 <span class="comment"> such vector exists, create it. */</span>
<a name="l00233"></a>00233 std::vector<std::pair<Clause, int> >& <a class="code" href="group__SE__Fast.html#ga8f4353c8f8c65ed00806861471bd857f" title="Return a ref to the vector of watched literals. If no such vector exists, create it.">wp</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Literal.html">Literal</a>& literal);
<a name="l00234"></a>00234 <span class="comment"></span>
<a name="l00235"></a>00235 <span class="comment"> /*! @brief \return true if SAT, false otherwise.</span>
<a name="l00236"></a>00236 <span class="comment"> *</span>
<a name="l00237"></a>00237 <span class="comment"> * When false is returned, proof is saved in d_lastConflictTheorem */</span>
<a name="l00238"></a>00238 <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="group__SE__Fast.html#gac68652e5ed46a097f846ba9a86fcd630">checkSAT</a>();
<a name="l00239"></a>00239 <span class="comment"></span>
<a name="l00240"></a>00240 <span class="comment"> //! Choose a splitter.</span>
<a name="l00241"></a>00241 <span class="comment"></span><span class="comment"> /*! Preconditions: The current context is consistent.</span>
<a name="l00242"></a>00242 <span class="comment"> *</span>
<a name="l00243"></a>00243 <span class="comment"> * \return true if splitter available, and it asserts it through</span>
<a name="l00244"></a>00244 <span class="comment"> * newIntAssumption() after first pushing a new context.</span>
<a name="l00245"></a>00245 <span class="comment"> *</span>
<a name="l00246"></a>00246 <span class="comment"> * \return false if no splitters are available, which means the</span>
<a name="l00247"></a>00247 <span class="comment"> * context is SAT.</span>
<a name="l00248"></a>00248 <span class="comment"> *</span>
<a name="l00249"></a>00249 <span class="comment"> * Postconditions: A literal has been asserted through</span>
<a name="l00250"></a>00250 <span class="comment"> * newIntAssumption().</span>
<a name="l00251"></a>00251 <span class="comment"> */</span>
<a name="l00252"></a>00252 <span class="keywordtype">bool</span> <a class="code" href="group__SE__Fast.html#ga6d05128f71cc4e239030fe0434cda727" title="Choose a splitter.">split</a>();
<a name="l00253"></a>00253
<a name="l00254"></a>00254 <span class="comment">// Moved from the decision engine:</span><span class="comment"></span>
<a name="l00255"></a>00255 <span class="comment"> //! Returns a splitter</span>
<a name="l00256"></a>00256 <span class="comment"></span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="group__SE__Fast.html#ga711544b769f4c0a5713df247de927019" title="Returns a splitter.">findSplitter</a>();<span class="comment"></span>
<a name="l00257"></a>00257 <span class="comment"> //! Position of a literal with max score in d_litsByScores</span>
<a name="l00258"></a><a class="code" href="group__SE__Fast.html#gad80c2b69b88a04c8c78309859abd3f76">00258</a> <span class="comment"></span> <span class="keywordtype">unsigned</span> <a class="code" href="group__SE__Fast.html#gad80c2b69b88a04c8c78309859abd3f76" title="Position of a literal with max score in d_litsByScores.">d_litsMaxScorePos</a>;<span class="comment"></span>
<a name="l00259"></a>00259 <span class="comment"> //! Vector of literals sorted by score</span>
<a name="l00260"></a><a class="code" href="group__SE__Fast.html#ga57c1c1e58ebd2c1d23a57db97880fbbc">00260</a> <span class="comment"></span> std::vector<Literal> <a class="code" href="group__SE__Fast.html#ga57c1c1e58ebd2c1d23a57db97880fbbc" title="Vector of literals sorted by score.">d_litsByScores</a>;
<a name="l00261"></a>00261 <span class="comment">/*</span><span class="comment"></span>
<a name="l00262"></a>00262 <span class="comment"> //! Mapping of literals to scores</span>
<a name="l00263"></a>00263 <span class="comment"></span> ExprHashMap<unsigned> d_litScores;<span class="comment"></span>
<a name="l00264"></a>00264 <span class="comment"> //! Mapping of literals to their counters</span>
<a name="l00265"></a>00265 <span class="comment"></span> ExprHashMap<unsigned> d_litCounts;<span class="comment"></span>
<a name="l00266"></a>00266 <span class="comment"> //! Mapping of literals to previous counters (what's that, anyway?)</span>
<a name="l00267"></a>00267 <span class="comment"></span> ExprHashMap<unsigned> d_litCountPrev;
<a name="l00268"></a>00268 */<span class="comment"></span>
<a name="l00269"></a>00269 <span class="comment"> //! Internal splitter counter for delaying updateLitScores()</span>
<a name="l00270"></a><a class="code" href="group__SE__Fast.html#ga52c9c181bcd623a36ab594e0ee16a67e">00270</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="group__SE__Fast.html#ga52c9c181bcd623a36ab594e0ee16a67e" title="Internal splitter counter for delaying updateLitScores()">d_splitterCount</a>;<span class="comment"></span>
<a name="l00271"></a>00271 <span class="comment"> //! Internal (decrementing) count of added splitters, to sort d_litByScores</span>
<a name="l00272"></a><a class="code" href="group__SE__Fast.html#ga2d54fdadc1b167dbbb366e37e0b97a58">00272</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="group__SE__Fast.html#ga2d54fdadc1b167dbbb366e37e0b97a58" title="Internal (decrementing) count of added splitters, to sort d_litByScores.">d_litSortCount</a>;
<a name="l00273"></a>00273 <span class="comment"></span>
<a name="l00274"></a>00274 <span class="comment"> //! Flag to switch on/off the berkmin heuristic</span>
<a name="l00275"></a><a class="code" href="group__SE__Fast.html#ga3877f82445d777c19c60b6ec117335e2">00275</a> <span class="comment"></span> <span class="keyword">const</span> <span class="keywordtype">bool</span> <a class="code" href="group__SE__Fast.html#ga3877f82445d777c19c60b6ec117335e2" title="Flag to switch on/off the berkmin heuristic.">d_berkminFlag</a>;
<a name="l00276"></a>00276 <span class="comment"></span>
<a name="l00277"></a>00277 <span class="comment"> //! Clear the list of asserted literals (d_literals)</span>
<a name="l00278"></a>00278 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE__Fast.html#gadf72861b6482f6c585f3199d1436f7be" title="Clear the list of asserted literals (d_literals)">clearLiterals</a>();
<a name="l00279"></a>00279
<a name="l00280"></a>00280 <span class="keywordtype">void</span> <a class="code" href="group__SE__Fast.html#ga453b1d390ee3b7af68fe8e915443d1ad">updateLitScores</a>(<span class="keywordtype">bool</span> firstTime);<span class="comment"></span>
<a name="l00281"></a>00281 <span class="comment"> //! Add the literals of a new clause to d_litsByScores</span>
<a name="l00282"></a>00282 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE__Fast.html#ga775b06e155128cc8817f254bc293c6c6" title="Add the literals of a new clause to d_litsByScores.">updateLitCounts</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Clause.html" title="A class representing a CNF clause (a smart pointer)">Clause</a>& c);
<a name="l00283"></a>00283
<a name="l00284"></a>00284 <span class="comment"></span>
<a name="l00285"></a>00285 <span class="comment"> //! Boolean constraint propagation.</span>
<a name="l00286"></a>00286 <span class="comment"></span><span class="comment"> /*! Preconditions: On every run besides the first, the CNF clause</span>
<a name="l00287"></a>00287 <span class="comment"> * database must not have any unit or unsat clauses, and there</span>
<a name="l00288"></a>00288 <span class="comment"> * must be a literal queued up for processing. The current</span>
<a name="l00289"></a>00289 <span class="comment"> * context must be consistent. Any and all assertions and</span>
<a name="l00290"></a>00290 <span class="comment"> * assignments must actually be made within the bcp loop. Other</span>
<a name="l00291"></a>00291 <span class="comment"> * parts of the solver may queue new facts with addLiteralFact()</span>
<a name="l00292"></a>00292 <span class="comment"> * and addNonLiteralFact(). bcp() will either process them, or</span>
<a name="l00293"></a>00293 <span class="comment"> * it will find a conflict, in which case they will no longer be</span>
<a name="l00294"></a>00294 <span class="comment"> * valid and will be dumped. Any nonLiterals must already be</span>
<a name="l00295"></a>00295 <span class="comment"> * simplified.</span>
<a name="l00296"></a>00296 <span class="comment"> *</span>
<a name="l00297"></a>00297 <span class="comment"> * Description: BCP will systematically work through all the</span>
<a name="l00298"></a>00298 <span class="comment"> * literals and nonliterals, using boolean constraint propagation</span>
<a name="l00299"></a>00299 <span class="comment"> * by detecting unit clauses and using addLiteralFact() on the</span>
<a name="l00300"></a>00300 <span class="comment"> * unit literal while also marking the clause as SAT. Any</span>
<a name="l00301"></a>00301 <span class="comment"> * clauses marked SAT are guaranteed to be SAT, but clauses not</span>
<a name="l00302"></a>00302 <span class="comment"> * marked SAT are not guaranteed to be unsat.</span>
<a name="l00303"></a>00303 <span class="comment"> *</span>
<a name="l00304"></a>00304 <span class="comment"> * \return false if a conflict is found, true otherwise.</span>
<a name="l00305"></a>00305 <span class="comment"> *</span>
<a name="l00306"></a>00306 <span class="comment"> * Postconditions: False indicates conflict. If the conflict was</span>
<a name="l00307"></a>00307 <span class="comment"> * discovered in CNF, we call the proof rule, then store that</span>
<a name="l00308"></a>00308 <span class="comment"> * clause pointer so fixConflict() can skip over it during the</span>
<a name="l00309"></a>00309 <span class="comment"> * search (when we finally change dependency tracking).</span>
<a name="l00310"></a>00310 <span class="comment"> *</span>
<a name="l00311"></a>00311 <span class="comment"> * True indicates success. All literals and nonLiterals have</span>
<a name="l00312"></a>00312 <span class="comment"> * been processed without causing a conflict. Processing</span>
<a name="l00313"></a>00313 <span class="comment"> * nonliterals implies running simplify on them, immediately</span>
<a name="l00314"></a>00314 <span class="comment"> * asserting any simplifications back to the core, and marking</span>
<a name="l00315"></a>00315 <span class="comment"> * the original nonLiteral as simplified, to be ignored by all</span>
<a name="l00316"></a>00316 <span class="comment"> * future (this context or deeper) splitters and bcp runs.</span>
<a name="l00317"></a>00317 <span class="comment"> * Therefore, there will be no unsimplified nonliterals</span>
<a name="l00318"></a>00318 <span class="comment"> * remaining.</span>
<a name="l00319"></a>00319 <span class="comment"> */</span>
<a name="l00320"></a>00320 <span class="keywordtype">bool</span> <a class="code" href="group__SE__Fast.html#gac6d49471ba5c76fffc7581e01e423218" title="Boolean constraint propagation.">bcp</a>();
<a name="l00321"></a>00321 <span class="comment"></span>
<a name="l00322"></a>00322 <span class="comment"> //! Determines backtracking level and adds conflict clauses.</span>
<a name="l00323"></a>00323 <span class="comment"></span><span class="comment"> /*! Preconditions: The current context is inconsistent. If it</span>
<a name="l00324"></a>00324 <span class="comment"> * resulted from a conflictRule() application, then the theorem</span>
<a name="l00325"></a>00325 <span class="comment"> * is stored inside d_lastConflictTheorem.</span>
<a name="l00326"></a>00326 <span class="comment"> *</span>
<a name="l00327"></a>00327 <span class="comment"> * If this was caused from bcp, we obtain the conflictRule()</span>
<a name="l00328"></a>00328 <span class="comment"> * theorem from the d_lastConflictTheorem instance variable.</span>
<a name="l00329"></a>00329 <span class="comment"> * From here we build conflict clauses and determine the correct</span>
<a name="l00330"></a>00330 <span class="comment"> * backtracking level, at which point we actually backtrack</span>
<a name="l00331"></a>00331 <span class="comment"> * there. Finally, we also call addLiteralFact() on the "failure</span>
<a name="l00332"></a>00332 <span class="comment"> * driven assertion" literal so that bcp has some place to begin</span>
<a name="l00333"></a>00333 <span class="comment"> * (and it satisfies the bcp preconditions)</span>
<a name="l00334"></a>00334 <span class="comment"> *</span>
<a name="l00335"></a>00335 <span class="comment"> * Postconditions: If True is returned: The current context is</span>
<a name="l00336"></a>00336 <span class="comment"> * consistent, and a literal is queued up for bcp to process. If</span>
<a name="l00337"></a>00337 <span class="comment"> * False is returned: The context cannot be made consistent</span>
<a name="l00338"></a>00338 <span class="comment"> * without backtracking past the original one, so the formula is</span>
<a name="l00339"></a>00339 <span class="comment"> * unsat.</span>
<a name="l00340"></a>00340 <span class="comment"> */</span>
<a name="l00341"></a>00341 <span class="keywordtype">bool</span> <a class="code" href="group__SE__Fast.html#ga4490cc372993398612e7556e14222ff3" title="Determines backtracking level and adds conflict clauses.">fixConflict</a>();<span class="comment"></span>
<a name="l00342"></a>00342 <span class="comment"> //! FIXME: document this</span>
<a name="l00343"></a>00343 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE__Fast.html#gaf7daf6eac739438b5b25175bc7d63a71" title="FIXME: document this.">assertAssumptions</a>();<span class="comment"></span>
<a name="l00344"></a>00344 <span class="comment"> //! Queue up a fact to assert to the DPs later</span>
<a name="l00345"></a>00345 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE__Fast.html#ga2c71aa94289db9ece678963617660640" title="Queue up a fact to assert to the DPs later.">enqueueFact</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);<span class="comment"></span>
<a name="l00346"></a>00346 <span class="comment"> //! Set the context inconsistent. Takes Theorem(FALSE).</span>
<a name="l00347"></a>00347 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE__Fast.html#ga33ff53b3eeb9811b1510fffd3cdcf234" title="Set the context inconsistent. Takes Theorem(FALSE).">setInconsistent</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);<span class="comment"></span>
<a name="l00348"></a>00348 <span class="comment"> //! Commit all the enqueued facts to the DPs</span>
<a name="l00349"></a>00349 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE__Fast.html#ga6d190905fefb2a36650306e5b577dd9a" title="Commit all the enqueued facts to the DPs.">commitFacts</a>();<span class="comment"></span>
<a name="l00350"></a>00350 <span class="comment"> //! Clear the local fact queue</span>
<a name="l00351"></a>00351 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE__Fast.html#gafa7937cc0b7d14c0aafb1f9c20abf011" title="Clear the local fact queue.">clearFacts</a>();
<a name="l00352"></a>00352 <span class="comment"></span>
<a name="l00353"></a>00353 <span class="comment"> /*! @name Processing a Conflict */</span><span class="comment"></span>
<a name="l00354"></a>00354 <span class="comment"> //@{</span>
<a name="l00355"></a>00355 <span class="comment"></span><span class="comment"> /*! @brief Take a conflict in the form of Literal, or</span>
<a name="l00356"></a>00356 <span class="comment"> Theorem, and generate all the necessary conflict clauses. */</span>
<a name="l00357"></a>00357 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="group__SE__Fast.html#ga2535b1eabb9eb7e7f3a6197dbb377cb4" title="Take a conflict in the form of Literal, or Theorem, and generate all the necessary conflict clauses...">processConflict</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Literal.html">Literal</a>& l);
<a name="l00358"></a>00358 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="group__SE__Fast.html#ga2535b1eabb9eb7e7f3a6197dbb377cb4" title="Take a conflict in the form of Literal, or Theorem, and generate all the necessary conflict clauses...">processConflict</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);<span class="comment"></span>
<a name="l00359"></a>00359 <span class="comment"> //@}</span>
<a name="l00360"></a>00360 <span class="comment"></span><span class="comment"></span>
<a name="l00361"></a>00361 <span class="comment"> //! Auxiliary function for unit propagation</span>
<a name="l00362"></a>00362 <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="group__SE__Fast.html#gad7548d572241f215212176af0216cb94" title="Auxiliary function for unit propagation.">propagate</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Clause.html" title="A class representing a CNF clause (a smart pointer)">Clause</a> &c, <span class="keywordtype">int</span> idx, <span class="keywordtype">bool</span>& wpUpdated);<span class="comment"></span>
<a name="l00363"></a>00363 <span class="comment"> //! Do the unit propagation for the clause</span>
<a name="l00364"></a>00364 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE__Fast.html#ga88d524fb175ae8156696cc73cb182ffd" title="Do the unit propagation for the clause.">unitPropagation</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Clause.html" title="A class representing a CNF clause (a smart pointer)">Clause</a> &c, <span class="keywordtype">unsigned</span> idx);<span class="comment"></span>
<a name="l00365"></a>00365 <span class="comment"> //! Analyse the conflict, find the UIPs, etc.</span>
<a name="l00366"></a>00366 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE__Fast.html#gaac9cb2de28ec162fe5ecfe042ad7b101" title="Analyse the conflict, find the UIPs, etc.">analyzeUIPs</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> &falseThm, <span class="keywordtype">int</span> conflictScope);
<a name="l00367"></a>00367 <span class="comment"></span>
<a name="l00368"></a>00368 <span class="comment"> /////////////////////////////</span>
<a name="l00369"></a>00369 <span class="comment"></span> <span class="comment">// New convenience methods //</span><span class="comment"></span>
<a name="l00370"></a>00370 <span class="comment"> /////////////////////////////</span>
<a name="l00371"></a>00371 <span class="comment"></span><span class="comment"></span>
<a name="l00372"></a>00372 <span class="comment"> //! Go through all the clauses and check the watch pointers (for debugging)</span>
<a name="l00373"></a>00373 <span class="comment"></span> <a class="code" href="debug_8h.html#a600cb2d68efe7cc413cccbb5714c7016">IF_DEBUG</a>(<span class="keywordtype">void</span> fullCheck();)<span class="comment"></span>
<a name="l00374"></a>00374 <span class="comment"> //! Set up the watch pointers for the new clause</span>
<a name="l00375"></a>00375 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE__Fast.html#ga6e64b8f0a42bd4b42d22b50b351219c9" title="Go through all the clauses and check the watch pointers (for debugging)">addNewClause</a>(<a class="code" href="classCVC3_1_1Clause.html" title="A class representing a CNF clause (a smart pointer)">Clause</a> &c);<span class="comment"></span>
<a name="l00376"></a>00376 <span class="comment"> //! Process a new derived fact (auxiliary function)</span>
<a name="l00377"></a>00377 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE__Fast.html#ga2ec0e19a01ac0926b690c50a3206c5a3" title="Process a new derived fact (auxiliary function)">recordFact</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);
<a name="l00378"></a>00378 <span class="comment"></span>
<a name="l00379"></a>00379 <span class="comment"> //! First pass in conflict analysis; takes a theorem of FALSE</span>
<a name="l00380"></a>00380 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE__Fast.html#gab3f2a42375c5b3875ad18acd47ee124d" title="First pass in conflict analysis; takes a theorem of FALSE.">traceConflict</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& conflictThm);<span class="comment"></span>
<a name="l00381"></a>00381 <span class="comment"> //! Private helper function for checkValid and restart</span>
<a name="l00382"></a>00382 <span class="comment"></span> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="group__SE__Fast.html#gaac7ba666d67d3d4808642c5c7858db95" title="Private helper function for checkValid and restart.">checkValidMain</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e2);
<a name="l00383"></a>00383
<a name="l00384"></a>00384 <span class="keyword">public</span>:<span class="comment"></span>
<a name="l00385"></a>00385 <span class="comment"> //! The main Constructor</span>
<a name="l00386"></a>00386 <span class="comment"></span> <a class="code" href="group__SE__Fast.html#ga8869c248ac69ea02656c95b40c99ed24" title="The main Constructor.">SearchEngineFast</a>(<a class="code" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">TheoryCore</a>* core);<span class="comment"></span>
<a name="l00387"></a>00387 <span class="comment"> //! Destructor</span>
<a name="l00388"></a>00388 <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="group__SE__Fast.html#ga8f8c0138aa4f31355dad949f604e3927" title="Destructor.">~SearchEngineFast</a>();
<a name="l00389"></a>00389
<a name="l00390"></a><a class="code" href="group__SE__Fast.html#ga3f564001c310c9e4ff519da68f8ea670">00390</a> <span class="keyword">const</span> std::string& <a class="code" href="group__SE__Fast.html#ga3f564001c310c9e4ff519da68f8ea670" title="Name of this search engine.">getName</a>() { <span class="keywordflow">return</span> <a class="code" href="group__SE__Fast.html#ga91ff4e54d0b66c31eb0d2653fad650cb" title="Name.">d_name</a>; }<span class="comment"></span>
<a name="l00391"></a>00391 <span class="comment"> //! Implementation of the API call</span>
<a name="l00392"></a>00392 <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="group__SE__Fast.html#ga1db688bc99f93a978079b3d2efd1bd9f" title="Implementation of the API call.">checkValidInternal</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00393"></a>00393 <span class="keyword">virtual</span> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="group__SE__Fast.html#ga99dd1f1c52ecae319bd0b5a3b689a31d" title="Reruns last check with e as an additional assumption.">restartInternal</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);<span class="comment"></span>
<a name="l00394"></a>00394 <span class="comment"> //! Redefine the counterexample generation.</span>
<a name="l00395"></a>00395 <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="group__SE__Fast.html#ga104e5e0abacb4c9492b0cb818b7d968a" title="Redefine the counterexample generation.">getCounterExample</a>(std::vector<Expr>& assertions);<span class="comment"></span>
<a name="l00396"></a>00396 <span class="comment"> //! Notify the search engine about a new literal fact.</span>
<a name="l00397"></a>00397 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE__Fast.html#gaef3113afb8dc9ea1b06217ab77f5d713" title="Notify the search engine about a new literal fact.">addLiteralFact</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);<span class="comment"></span>
<a name="l00398"></a>00398 <span class="comment"> //! Notify the search engine about a new non-literal fact.</span>
<a name="l00399"></a>00399 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="group__SE__Fast.html#ga03501a968c3c7122a999b1f57d6640a0" title="Notify the search engine about a new non-literal fact.">addNonLiteralFact</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);<span class="comment"></span>
<a name="l00400"></a>00400 <span class="comment"> /*! @brief Redefine newIntAssumption(): we need to add the new theorem</span>
<a name="l00401"></a>00401 <span class="comment"> to the appropriate Literal */</span>
<a name="l00402"></a>00402 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="group__SE__Fast.html#gaf54422149559aa048f32723a3dc6fcce" title="Redefine newIntAssumption(): we need to add the new theorem to the appropriate Literal.">newIntAssumption</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00403"></a>00403 <span class="keyword">virtual</span> <span class="keywordtype">bool</span> <a class="code" href="group__SE__Fast.html#ga4b55b5f49d921ca4b63f874d8404c4d5" title="Check if the formula has been assumed.">isAssumption</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);
<a name="l00404"></a>00404 <span class="keywordtype">void</span> <a class="code" href="group__SE__Fast.html#ga40b361c2f9374c541282feca1e237dba" title="Suggest a splitter to the SearchEngine.">addSplitter</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keywordtype">int</span> priority);
<a name="l00405"></a>00405 <span class="comment"></span>
<a name="l00406"></a>00406 <span class="comment"> /*! @} */</span> <span class="comment">// end of addtogroup SE_Fast</span>
<a name="l00407"></a>00407 <span class="comment"></span>
<a name="l00408"></a>00408 <span class="comment"> //! Return next clause whose satisfiability is unknown</span>
<a name="l00409"></a>00409 <span class="comment"></span> <span class="comment">//virtual Clause nextClause();</span><span class="comment"></span>
<a name="l00410"></a>00410 <span class="comment"> //! Return next non-clause which does not reduce to false</span>
<a name="l00411"></a>00411 <span class="comment"></span> <span class="comment">//virtual Expr nextNonClause();</span>
<a name="l00412"></a>00412 };<span class="comment"></span>
<a name="l00413"></a>00413 <span class="comment">/*! @} */</span> <span class="comment">// end of SE_Fast</span>
<a name="l00414"></a>00414 }
<a name="l00415"></a>00415
<a name="l00416"></a>00416
<a name="l00417"></a>00417 <span class="preprocessor">#endif</span>
</pre></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>
