<!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_sat.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_sat.h</div> </div>
</div>
<div class="contents">
<a href="search__sat_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><span class="comment"></span>
<a name="l00002"></a>00002 <span class="comment">/*!</span>
<a name="l00003"></a>00003 <span class="comment"> *\file search_sat.h</span>
<a name="l00004"></a>00004 <span class="comment"> *\brief Search engine that uses an external SAT engine</span>
<a name="l00005"></a>00005 <span class="comment"> *</span>
<a name="l00006"></a>00006 <span class="comment"> * Author: Clark Barrett</span>
<a name="l00007"></a>00007 <span class="comment"> *</span>
<a name="l00008"></a>00008 <span class="comment"> * Created: Mon Dec 5 17:52:05 2005</span>
<a name="l00009"></a>00009 <span class="comment"> *</span>
<a name="l00010"></a>00010 <span class="comment"> * <hr></span>
<a name="l00011"></a>00011 <span class="comment"> *</span>
<a name="l00012"></a>00012 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00013"></a>00013 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00014"></a>00014 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00015"></a>00015 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00016"></a>00016 <span class="comment"> *</span>
<a name="l00017"></a>00017 <span class="comment"> * <hr></span>
<a name="l00018"></a>00018 <span class="comment"> *</span>
<a name="l00019"></a>00019 <span class="comment"> */</span>
<a name="l00020"></a>00020 <span class="comment">/*****************************************************************************/</span>
<a name="l00021"></a>00021
<a name="l00022"></a>00022 <span class="preprocessor">#ifndef _cvc3__include__search_sat_h_</span>
<a name="l00023"></a>00023 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__search_sat_h_</span>
<a name="l00024"></a>00024 <span class="preprocessor"></span>
<a name="l00025"></a>00025 <span class="preprocessor">#include <vector></span>
<a name="l00026"></a>00026 <span class="preprocessor">#include <set></span>
<a name="l00027"></a>00027 <span class="preprocessor">#include "<a class="code" href="search_8h.html" title="Abstract API to the proof search engine.">search.h</a>"</span>
<a name="l00028"></a>00028 <span class="preprocessor">#include "<a class="code" href="smartcdo_8h.html" title="Smart context-dependent object wrapper.">smartcdo.h</a>"</span>
<a name="l00029"></a>00029 <span class="preprocessor">#include "<a class="code" href="cdlist_8h.html">cdlist.h</a>"</span>
<a name="l00030"></a>00030 <span class="preprocessor">#include "<a class="code" href="cnf__manager_8h.html" title="Manager for conversion to and traversal of CNF formulas.">cnf_manager.h</a>"</span>
<a name="l00031"></a>00031 <span class="preprocessor">#include "<a class="code" href="expr_8h.html" title="Definition of the API to expression package. See class Expr for details.">expr.h</a>"</span>
<a name="l00032"></a>00032 <span class="preprocessor">#include "<a class="code" href="dpllt_8h.html" title="Generic DPLL(T) module.">dpllt.h</a>"</span>
<a name="l00033"></a>00033 <span class="preprocessor">#include "<a class="code" href="theory__core_8h.html">theory_core.h</a>"</span>
<a name="l00034"></a>00034 <span class="preprocessor">#include "<a class="code" href="formula__value_8h.html" title="enumerated type for value of formulas">formula_value.h</a>"</span>
<a name="l00035"></a>00035
<a name="l00036"></a>00036 <span class="keyword">namespace </span>CVC3 {
<a name="l00037"></a>00037 <span class="comment"></span>
<a name="l00038"></a>00038 <span class="comment">//! Search engine that connects to a generic SAT reasoning module</span>
<a name="l00039"></a>00039 <span class="comment"></span><span class="comment">/*! \ingroup SE */</span>
<a name="l00040"></a><a class="code" href="classCVC3_1_1SearchSat.html">00040</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchSat.html" title="Search engine that connects to a generic SAT reasoning module.">SearchSat</a> :<span class="keyword">public</span> <a class="code" href="classCVC3_1_1SearchEngine.html" title="API to to a generic proof search engine.">SearchEngine</a> {
<a name="l00041"></a>00041 <span class="comment"></span>
<a name="l00042"></a>00042 <span class="comment"> //! Name of search engine</span>
<a name="l00043"></a><a class="code" href="classCVC3_1_1SearchSat.html#ab7dd09d7a8ea0c87e2e1ec42a837160b">00043</a> <span class="comment"></span> std::string <a class="code" href="classCVC3_1_1SearchSat.html#ab7dd09d7a8ea0c87e2e1ec42a837160b" title="Name of search engine.">d_name</a>;
<a name="l00044"></a>00044 <span class="comment"></span>
<a name="l00045"></a>00045 <span class="comment"> //! Bottom scope for current query</span>
<a name="l00046"></a><a class="code" href="classCVC3_1_1SearchSat.html#a8153b8d7b772217bafddf3d92be4759b">00046</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<int></a> <a class="code" href="classCVC3_1_1SearchSat.html#a8153b8d7b772217bafddf3d92be4759b" title="Bottom scope for current query.">d_bottomScope</a>;
<a name="l00047"></a>00047 <span class="comment"></span>
<a name="l00048"></a>00048 <span class="comment"> //! Last expr checked for validity</span>
<a name="l00049"></a><a class="code" href="classCVC3_1_1SearchSat.html#ac318c6520fbea766517991127affaafc">00049</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<Expr></a> <a class="code" href="classCVC3_1_1SearchSat.html#ac318c6520fbea766517991127affaafc" title="Last expr checked for validity.">d_lastCheck</a>;
<a name="l00050"></a>00050 <span class="comment"></span>
<a name="l00051"></a>00051 <span class="comment"> /*! @brief Theorem from the last successful checkValid call. It is</span>
<a name="l00052"></a>00052 <span class="comment"> used by getProof and getAssumptions. */</span>
<a name="l00053"></a><a class="code" href="classCVC3_1_1SearchSat.html#ab41637f4522c5e3f318993392adf84bb">00053</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<Theorem></a> <a class="code" href="classCVC3_1_1SearchSat.html#ab41637f4522c5e3f318993392adf84bb" title="Theorem from the last successful checkValid call. It is used by getProof and getAssumptions.">d_lastValid</a>;
<a name="l00054"></a>00054 <span class="comment"></span>
<a name="l00055"></a>00055 <span class="comment"> //! List of all user assumptions</span>
<a name="l00056"></a><a class="code" href="classCVC3_1_1SearchSat.html#a3b9b2371a24908e62ec71b6f141afea8">00056</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Theorem></a> <a class="code" href="classCVC3_1_1SearchSat.html#a3b9b2371a24908e62ec71b6f141afea8" title="List of all user assumptions.">d_userAssumptions</a>;
<a name="l00057"></a>00057 <span class="comment"></span>
<a name="l00058"></a>00058 <span class="comment"> //! List of all internal assumptions</span>
<a name="l00059"></a><a class="code" href="classCVC3_1_1SearchSat.html#ad3b9879d655cf3fce1a70de7b1d6fedc">00059</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Theorem></a> <a class="code" href="classCVC3_1_1SearchSat.html#ad3b9879d655cf3fce1a70de7b1d6fedc" title="List of all internal assumptions.">d_intAssumptions</a>;
<a name="l00060"></a>00060 <span class="comment"></span>
<a name="l00061"></a>00061 <span class="comment"> //! Index to where unprocessed assumptions start</span>
<a name="l00062"></a><a class="code" href="classCVC3_1_1SearchSat.html#a23b0c38d89ce24f463f2c2fc929df879">00062</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned></a> <a class="code" href="classCVC3_1_1SearchSat.html#a23b0c38d89ce24f463f2c2fc929df879" title="Index to where unprocessed assumptions start.">d_idxUserAssump</a>;
<a name="l00063"></a>00063
<a name="l00064"></a><a class="code" href="classCVC3_1_1SearchSat.html#aab55d9ceeb2a938841230c920762ba77">00064</a> <a class="code" href="classCVC3_1_1TheoryCore_1_1CoreSatAPI.html" title="Interface class for callbacks to SAT from Core.">TheoryCore::CoreSatAPI</a>* <a class="code" href="classCVC3_1_1SearchSat.html#aab55d9ceeb2a938841230c920762ba77">d_coreSatAPI</a>;
<a name="l00065"></a>00065 <span class="comment"></span>
<a name="l00066"></a>00066 <span class="comment"> //! Pointer to DPLLT implementation</span>
<a name="l00067"></a><a class="code" href="classCVC3_1_1SearchSat.html#a884c103ef1313d56a3a42d4e3e8468cb">00067</a> <span class="comment"></span> <a class="code" href="classSAT_1_1DPLLT.html">SAT::DPLLT</a>* <a class="code" href="classCVC3_1_1SearchSat.html#a884c103ef1313d56a3a42d4e3e8468cb" title="Pointer to DPLLT implementation.">d_dpllt</a>;
<a name="l00068"></a>00068 <span class="comment"></span>
<a name="l00069"></a>00069 <span class="comment"> //! Implementation of TheoryAPI for DPLLT</span>
<a name="l00070"></a><a class="code" href="classCVC3_1_1SearchSat.html#a8abc1b647affa60cc367e0eeaa52cdf4">00070</a> <span class="comment"></span> <a class="code" href="classSAT_1_1DPLLT_1_1TheoryAPI.html">SAT::DPLLT::TheoryAPI</a>* <a class="code" href="classCVC3_1_1SearchSat.html#a8abc1b647affa60cc367e0eeaa52cdf4" title="Implementation of TheoryAPI for DPLLT.">d_theoryAPI</a>;
<a name="l00071"></a>00071 <span class="comment"></span>
<a name="l00072"></a>00072 <span class="comment"> //! Implementation of Decider for DPLLT</span>
<a name="l00073"></a><a class="code" href="classCVC3_1_1SearchSat.html#aa4be1d02557a46fbbdc32deefc4f3a32">00073</a> <span class="comment"></span> <a class="code" href="classSAT_1_1DPLLT_1_1Decider.html">SAT::DPLLT::Decider</a>* <a class="code" href="classCVC3_1_1SearchSat.html#aa4be1d02557a46fbbdc32deefc4f3a32" title="Implementation of Decider for DPLLT.">d_decider</a>;
<a name="l00074"></a>00074 <span class="comment"></span>
<a name="l00075"></a>00075 <span class="comment"> //! Store of theorems for expressions sent to DPLLT</span>
<a name="l00076"></a><a class="code" href="classCVC3_1_1SearchSat.html#a3e6b8d2d1d9513329fbbb80464053b39">00076</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr, Theorem></a> <a class="code" href="classCVC3_1_1SearchSat.html#a3e6b8d2d1d9513329fbbb80464053b39" title="Store of theorems for expressions sent to DPLLT.">d_theorems</a>;
<a name="l00077"></a>00077 <span class="comment"></span>
<a name="l00078"></a>00078 <span class="comment"> //! Manages CNF formula and its relationship to original Exprs and Theorems</span>
<a name="l00079"></a><a class="code" href="classCVC3_1_1SearchSat.html#a996335737d383fd882b6f1085f72b964">00079</a> <span class="comment"></span> <a class="code" href="classSAT_1_1CNF__Manager.html">SAT::CNF_Manager</a> *<a class="code" href="classCVC3_1_1SearchSat.html#a996335737d383fd882b6f1085f72b964" title="Manages CNF formula and its relationship to original Exprs and Theorems.">d_cnfManager</a>;
<a name="l00080"></a>00080 <span class="comment"></span>
<a name="l00081"></a>00081 <span class="comment"> //! Callback for CNF_Manager</span>
<a name="l00082"></a><a class="code" href="classCVC3_1_1SearchSat.html#a158485ff14b490fc2c91936a4e72bf5b">00082</a> <span class="comment"></span> <a class="code" href="classSAT_1_1CNF__Manager_1_1CNFCallback.html" title="Abstract class for callbacks.">SAT::CNF_Manager::CNFCallback</a> *<a class="code" href="classCVC3_1_1SearchSat.html#a158485ff14b490fc2c91936a4e72bf5b" title="Callback for CNF_Manager.">d_cnfCallback</a>;
<a name="l00083"></a>00083 <span class="comment"></span>
<a name="l00084"></a>00084 <span class="comment"> //! Cached values of variables</span>
<a name="l00085"></a><a class="code" href="classCVC3_1_1SearchSat.html#a455c295a13215ddc99b8df18f4598af4">00085</a> <span class="comment"></span> std::vector<SAT::Var::Val> <a class="code" href="classCVC3_1_1SearchSat.html#a455c295a13215ddc99b8df18f4598af4" title="Cached values of variables.">d_vars</a>;
<a name="l00086"></a>00086 <span class="comment"></span>
<a name="l00087"></a>00087 <span class="comment"> //! Whether we are currently in a call to dpllt->checkSat</span>
<a name="l00088"></a><a class="code" href="classCVC3_1_1SearchSat.html#a00573a594dd2b83cbb6f2997516862d3">00088</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1SearchSat.html#a00573a594dd2b83cbb6f2997516862d3" title="Whether we are currently in a call to dpllt->checkSat.">d_inCheckSat</a>;
<a name="l00089"></a>00089 <span class="comment"></span>
<a name="l00090"></a>00090 <span class="comment"> //! CNF Formula used for theory lemmas</span>
<a name="l00091"></a><a class="code" href="classCVC3_1_1SearchSat.html#aed781537ef3315ffa019cdd7f02f0f8e">00091</a> <span class="comment"></span> <a class="code" href="classSAT_1_1CD__CNF__Formula.html">SAT::CD_CNF_Formula</a> <a class="code" href="classCVC3_1_1SearchSat.html#aed781537ef3315ffa019cdd7f02f0f8e" title="CNF Formula used for theory lemmas.">d_lemmas</a>;
<a name="l00092"></a>00092 <span class="comment"></span>
<a name="l00093"></a>00093 <span class="comment"> //! Lemmas waiting to be translated since last call to getNewClauses()</span>
<a name="l00094"></a><a class="code" href="classCVC3_1_1SearchSat.html#a3997be227d7cd36e1f29f71a683f1428">00094</a> <span class="comment"></span> std::vector<std::pair<Theorem, int> > <a class="code" href="classCVC3_1_1SearchSat.html#a3997be227d7cd36e1f29f71a683f1428" title="Lemmas waiting to be translated since last call to getNewClauses()">d_pendingLemmas</a>;
<a name="l00095"></a>00095 <span class="comment"></span>
<a name="l00096"></a>00096 <span class="comment"> //! Scope parameter for lemmas waiting to be translated since last call to getNewClauses()</span>
<a name="l00097"></a><a class="code" href="classCVC3_1_1SearchSat.html#a83bb96cd69f2673e370e536a7946c5c3">00097</a> <span class="comment"></span> std::vector<bool> <a class="code" href="classCVC3_1_1SearchSat.html#a83bb96cd69f2673e370e536a7946c5c3" title="Scope parameter for lemmas waiting to be translated since last call to getNewClauses()">d_pendingScopes</a>;
<a name="l00098"></a>00098 <span class="comment"></span>
<a name="l00099"></a>00099 <span class="comment"> //! Backtracking size of d_pendingLemmas</span>
<a name="l00100"></a><a class="code" href="classCVC3_1_1SearchSat.html#ab309591a57e34a9166c3baa056e2857f">00100</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned></a> <a class="code" href="classCVC3_1_1SearchSat.html#ab309591a57e34a9166c3baa056e2857f" title="Backtracking size of d_pendingLemmas.">d_pendingLemmasSize</a>;
<a name="l00101"></a>00101 <span class="comment"></span>
<a name="l00102"></a>00102 <span class="comment"> //! Backtracking next item in d_pendingLemmas</span>
<a name="l00103"></a><a class="code" href="classCVC3_1_1SearchSat.html#a8de03d523c9b0304eb95e72ec923274b">00103</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned></a> <a class="code" href="classCVC3_1_1SearchSat.html#a8de03d523c9b0304eb95e72ec923274b" title="Backtracking next item in d_pendingLemmas.">d_pendingLemmasNext</a>;
<a name="l00104"></a>00104 <span class="comment"></span>
<a name="l00105"></a>00105 <span class="comment"> //! Current position in d_lemmas</span>
<a name="l00106"></a><a class="code" href="classCVC3_1_1SearchSat.html#a819ee9729fd633651eb2cf27f7175d8a">00106</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned></a> <a class="code" href="classCVC3_1_1SearchSat.html#a819ee9729fd633651eb2cf27f7175d8a" title="Current position in d_lemmas.">d_lemmasNext</a>;
<a name="l00107"></a>00107 <span class="comment"></span>
<a name="l00108"></a>00108 <span class="comment"> //! List for backtracking var values</span>
<a name="l00109"></a><a class="code" href="classCVC3_1_1SearchSat.html#a78ea4f3b48395a88f42bb4db58c44541">00109</a> <span class="comment"></span> std::vector<unsigned> <a class="code" href="classCVC3_1_1SearchSat.html#a78ea4f3b48395a88f42bb4db58c44541" title="List for backtracking var values.">d_varsUndoList</a>;
<a name="l00110"></a>00110 <span class="comment"></span>
<a name="l00111"></a>00111 <span class="comment"> //! Backtracking size of d_varsUndoList</span>
<a name="l00112"></a><a class="code" href="classCVC3_1_1SearchSat.html#a6c7fadcd8cd61189c6c3c38a28035993">00112</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned></a> <a class="code" href="classCVC3_1_1SearchSat.html#a6c7fadcd8cd61189c6c3c38a28035993" title="Backtracking size of d_varsUndoList.">d_varsUndoListSize</a>;
<a name="l00113"></a>00113
<a name="l00114"></a>00114 <span class="keyword">public</span>:<span class="comment"></span>
<a name="l00115"></a>00115 <span class="comment"> //! Pair of Lit and priority of this Lit</span>
<a name="l00116"></a><a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html">00116</a> <span class="comment"></span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html" title="Pair of Lit and priority of this Lit.">LitPriorityPair</a> {
<a name="l00117"></a><a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#adb293dd66bfb682cc70e8261c9920ec3">00117</a> <a class="code" href="classSAT_1_1Lit.html">SAT::Lit</a> <a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#adb293dd66bfb682cc70e8261c9920ec3">d_lit</a>;
<a name="l00118"></a><a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a58ee953d415954051680b4bbfd620e38">00118</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a58ee953d415954051680b4bbfd620e38">d_priority</a>;
<a name="l00119"></a><a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a5e6570cbdb63cf05dc4849a10f614440">00119</a> <a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a5e6570cbdb63cf05dc4849a10f614440">LitPriorityPair</a>() {}
<a name="l00120"></a>00120 <span class="keyword">public</span>:
<a name="l00121"></a><a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a693e54e7ed50745cf2f5954ae1143ea0">00121</a> <a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a5e6570cbdb63cf05dc4849a10f614440">LitPriorityPair</a>(<a class="code" href="classSAT_1_1Lit.html">SAT::Lit</a> lit, <span class="keywordtype">int</span> priority)
<a name="l00122"></a>00122 : <a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#adb293dd66bfb682cc70e8261c9920ec3">d_lit</a>(lit), <a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a58ee953d415954051680b4bbfd620e38">d_priority</a>(priority) {}
<a name="l00123"></a><a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a6b3a395df128bdf30ba375a1b55d76da">00123</a> <a class="code" href="classSAT_1_1Lit.html">SAT::Lit</a> <a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a6b3a395df128bdf30ba375a1b55d76da">getLit</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#adb293dd66bfb682cc70e8261c9920ec3">d_lit</a>; }
<a name="l00124"></a><a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#ad71d50229df3338a2ad460ddf4120b31">00124</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#ad71d50229df3338a2ad460ddf4120b31">getPriority</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a58ee953d415954051680b4bbfd620e38">d_priority</a>; }
<a name="l00125"></a>00125 <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a137e0aec1bf2c43561b29838af397031">operator<</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html" title="Pair of Lit and priority of this Lit.">LitPriorityPair</a>& p1,
<a name="l00126"></a>00126 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html" title="Pair of Lit and priority of this Lit.">LitPriorityPair</a>& p2);
<a name="l00127"></a>00127 };
<a name="l00128"></a>00128
<a name="l00129"></a>00129 <span class="keyword">private</span>:<span class="comment"></span>
<a name="l00130"></a>00130 <span class="comment"> //! Used to determine order to find splitters</span>
<a name="l00131"></a><a class="code" href="classCVC3_1_1SearchSat.html#ab4dbd42cf98469a2abb679024a402b77">00131</a> <span class="comment"></span> std::set<LitPriorityPair> <a class="code" href="classCVC3_1_1SearchSat.html#ab4dbd42cf98469a2abb679024a402b77" title="Used to determine order to find splitters.">d_prioritySet</a>;<span class="comment"></span>
<a name="l00132"></a>00132 <span class="comment"> //! Current position in prioritySet</span>
<a name="l00133"></a><a class="code" href="classCVC3_1_1SearchSat.html#ad7b3c57fadbc655bddd204b9ea122a62">00133</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<std::set<LitPriorityPair>::const_iterator</a>> <a class="code" href="classCVC3_1_1SearchSat.html#ad7b3c57fadbc655bddd204b9ea122a62" title="Current position in prioritySet.">d_prioritySetStart</a>;<span class="comment"></span>
<a name="l00134"></a>00134 <span class="comment"> //! Backtracking size of priority set entries</span>
<a name="l00135"></a><a class="code" href="classCVC3_1_1SearchSat.html#a3495b7cac1dc81f07f54dc8d0b17b17a">00135</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned></a> <a class="code" href="classCVC3_1_1SearchSat.html#a3495b7cac1dc81f07f54dc8d0b17b17a" title="Backtracking size of priority set entries.">d_prioritySetEntriesSize</a>;<span class="comment"></span>
<a name="l00136"></a>00136 <span class="comment"> //! Entries in priority set in insertion order (so set can be backtracked)</span>
<a name="l00137"></a><a class="code" href="classCVC3_1_1SearchSat.html#ab57f9f48af74c9a6493986b8cb0c720d">00137</a> <span class="comment"></span> std::vector<std::set<LitPriorityPair>::iterator> <a class="code" href="classCVC3_1_1SearchSat.html#ab57f9f48af74c9a6493986b8cb0c720d" title="Entries in priority set in insertion order (so set can be backtracked)">d_prioritySetEntries</a>;<span class="comment"></span>
<a name="l00138"></a>00138 <span class="comment"> //! Backtracking size of priority set entries at bottom scope</span>
<a name="l00139"></a><a class="code" href="classCVC3_1_1SearchSat.html#a99063dd2470eae948fa85d460a9b3868">00139</a> <span class="comment"></span> std::vector<unsigned> <a class="code" href="classCVC3_1_1SearchSat.html#a99063dd2470eae948fa85d460a9b3868" title="Backtracking size of priority set entries at bottom scope.">d_prioritySetBottomEntriesSizeStack</a>;<span class="comment"></span>
<a name="l00140"></a>00140 <span class="comment"> //! Current size of bottom entries</span>
<a name="l00141"></a><a class="code" href="classCVC3_1_1SearchSat.html#ab8e5996fd3e75c5b3c45f611d3639535">00141</a> <span class="comment"></span> <span class="keywordtype">unsigned</span> <a class="code" href="classCVC3_1_1SearchSat.html#ab8e5996fd3e75c5b3c45f611d3639535" title="Current size of bottom entries.">d_prioritySetBottomEntriesSize</a>;<span class="comment"></span>
<a name="l00142"></a>00142 <span class="comment"> //! Entries in priority set in insertion order (so set can be backtracked)</span>
<a name="l00143"></a><a class="code" href="classCVC3_1_1SearchSat.html#a6d963065a2df65795626cf6d70f8fe99">00143</a> <span class="comment"></span> std::vector<std::set<LitPriorityPair>::iterator> <a class="code" href="classCVC3_1_1SearchSat.html#a6d963065a2df65795626cf6d70f8fe99" title="Entries in priority set in insertion order (so set can be backtracked)">d_prioritySetBottomEntries</a>;
<a name="l00144"></a>00144 <span class="comment"></span>
<a name="l00145"></a>00145 <span class="comment"> //! Last Var registered with core theory</span>
<a name="l00146"></a><a class="code" href="classCVC3_1_1SearchSat.html#a217f464659b186330934d046aa7cc764">00146</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned></a> <a class="code" href="classCVC3_1_1SearchSat.html#a217f464659b186330934d046aa7cc764" title="Last Var registered with core theory.">d_lastRegisteredVar</a>;
<a name="l00147"></a>00147 <span class="comment"></span>
<a name="l00148"></a>00148 <span class="comment"> //! Whether it's OK to call DPLLT solver from the current scope</span>
<a name="l00149"></a><a class="code" href="classCVC3_1_1SearchSat.html#af0953025654043f6f76040df7abf2658">00149</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<bool></a> <a class="code" href="classCVC3_1_1SearchSat.html#af0953025654043f6f76040df7abf2658" title="Whether it's OK to call DPLLT solver from the current scope.">d_dplltReady</a>;
<a name="l00150"></a>00150
<a name="l00151"></a><a class="code" href="classCVC3_1_1SearchSat.html#ae97f61c9a0ae9ed8186929e15892ad73">00151</a> <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned></a> <a class="code" href="classCVC3_1_1SearchSat.html#ae97f61c9a0ae9ed8186929e15892ad73">d_nextImpliedLiteral</a>;
<a name="l00152"></a>00152 <span class="comment"></span>
<a name="l00153"></a>00153 <span class="comment"> //! Helper class for resetting DPLLT engine</span>
<a name="l00154"></a>00154 <span class="comment"></span><span class="comment"> /*! We need to be notified when the scope goes below the scope from</span>
<a name="l00155"></a>00155 <span class="comment"> * which the last invalid call to checkValid originated. This helper class</span>
<a name="l00156"></a>00156 <span class="comment"> * ensures that this happens.</span>
<a name="l00157"></a>00157 <span class="comment"> */</span>
<a name="l00158"></a><a class="code" href="classCVC3_1_1SearchSat.html#aa9f952c8606458f1e777d9a05b11550d">00158</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html">Restorer</a>;
<a name="l00159"></a><a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html">00159</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html">Restorer</a> :<span class="keyword">public</span> <a class="code" href="classCVC3_1_1ContextNotifyObj.html">ContextNotifyObj</a> {
<a name="l00160"></a><a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html#a4c5124e80744f2d60b408328c648d85a">00160</a> <a class="code" href="classCVC3_1_1SearchSat.html" title="Search engine that connects to a generic SAT reasoning module.">SearchSat</a>* <a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html#a4c5124e80744f2d60b408328c648d85a">d_ss</a>;
<a name="l00161"></a>00161 <span class="keyword">public</span>:
<a name="l00162"></a><a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html#a60db1d8baa0ef8723379d512481d51d9">00162</a> <a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html#a60db1d8baa0ef8723379d512481d51d9">Restorer</a>(<a class="code" href="classCVC3_1_1Context.html">Context</a>* context, <a class="code" href="classCVC3_1_1SearchSat.html" title="Search engine that connects to a generic SAT reasoning module.">SearchSat</a>* ss)
<a name="l00163"></a>00163 : <a class="code" href="classCVC3_1_1ContextNotifyObj.html">ContextNotifyObj</a>(context), <a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html#a4c5124e80744f2d60b408328c648d85a">d_ss</a>(ss) {}
<a name="l00164"></a><a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html#a482cb3047c1bba972a8ca6d7e474b9e9">00164</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html#a482cb3047c1bba972a8ca6d7e474b9e9">notifyPre</a>() { <a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html#a4c5124e80744f2d60b408328c648d85a">d_ss</a>-><a class="code" href="classCVC3_1_1SearchSat.html#aff33fe25d0761167062aa871e1992ded" title="Get rid of bottom scope entries in prioritySet.">restorePre</a>(); }
<a name="l00165"></a><a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html#a3ef0a65d1c37d83f9b3733c8d20c7c3d">00165</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html#a3ef0a65d1c37d83f9b3733c8d20c7c3d">notify</a>() { <a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html#a4c5124e80744f2d60b408328c648d85a">d_ss</a>-><a class="code" href="classCVC3_1_1SearchSat.html#a41d79aff18a635a5cdc2c789bb784a0a" title="Get rid of entries in prioritySet and pendingLemmas added since last push.">restore</a>(); }
<a name="l00166"></a>00166 };<span class="comment"></span>
<a name="l00167"></a>00167 <span class="comment"> //! Instance of Restorer class</span>
<a name="l00168"></a><a class="code" href="classCVC3_1_1SearchSat.html#a5b7313c3933e04b894089b1c2e09c57e">00168</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html">Restorer</a> <a class="code" href="classCVC3_1_1SearchSat.html#a5b7313c3933e04b894089b1c2e09c57e" title="Instance of Restorer class.">d_restorer</a>;
<a name="l00169"></a>00169
<a name="l00170"></a>00170 <span class="keyword">private</span>:
<a name="l00171"></a>00171 <span class="comment"></span>
<a name="l00172"></a>00172 <span class="comment"> //! Get rid of bottom scope entries in prioritySet</span>
<a name="l00173"></a>00173 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#aff33fe25d0761167062aa871e1992ded" title="Get rid of bottom scope entries in prioritySet.">restorePre</a>();<span class="comment"></span>
<a name="l00174"></a>00174 <span class="comment"> //! Get rid of entries in prioritySet and pendingLemmas added since last push</span>
<a name="l00175"></a>00175 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#a41d79aff18a635a5cdc2c789bb784a0a" title="Get rid of entries in prioritySet and pendingLemmas added since last push.">restore</a>();<span class="comment"></span>
<a name="l00176"></a>00176 <span class="comment"> //! Helper for addLemma and check</span>
<a name="l00177"></a>00177 <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1SearchSat.html#a0f3b2311296e520c22aea55c68c4b477" title="Helper for addLemma and check.">recordNewRootLit</a>(<a class="code" href="classSAT_1_1Lit.html">SAT::Lit</a> lit, <span class="keywordtype">int</span> priority = 0, <span class="keywordtype">bool</span> atBottomScope = <span class="keyword">false</span>);
<a name="l00178"></a>00178
<a name="l00179"></a><a class="code" href="classCVC3_1_1SearchSat.html#a71c71132ecb225ad44dd66fc2c3505f3">00179</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchSatCoreSatAPI.html">SearchSatCoreSatAPI</a>;
<a name="l00180"></a><a class="code" href="classCVC3_1_1SearchSat.html#acfd18b3733ce33513e1e5ddaad615624">00180</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchSatCNFCallback.html">SearchSatCNFCallback</a>;<span class="comment"></span>
<a name="l00181"></a>00181 <span class="comment"> //! Core theory callback which adds a new lemma from the core theory</span>
<a name="l00182"></a>00182 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#ad7abbaa4ca4528eb0cdfcbce26d05ea4" title="Core theory callback which adds a new lemma from the core theory.">addLemma</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm, <span class="keywordtype">int</span> priority = 0, <span class="keywordtype">bool</span> atBotomScope = <span class="keyword">false</span>);<span class="comment"></span>
<a name="l00183"></a>00183 <span class="comment"> //! Core theory callback which asks for the bottom scope for current query</span>
<a name="l00184"></a><a class="code" href="classCVC3_1_1SearchSat.html#a7dd555ba6043bd8019091ac6289233d6">00184</a> <span class="comment"></span> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1SearchSat.html#a7dd555ba6043bd8019091ac6289233d6" title="Core theory callback which asks for the bottom scope for current query.">getBottomScope</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1SearchSat.html#a8153b8d7b772217bafddf3d92be4759b" title="Bottom scope for current query.">d_bottomScope</a>; }<span class="comment"></span>
<a name="l00185"></a>00185 <span class="comment"> //! Core theory callback which suggests a splitter</span>
<a name="l00186"></a>00186 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#a98359a6ceb891ac5d12030aa42210b3d" title="Core theory callback which suggests a splitter.">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="l00187"></a>00187
<a name="l00188"></a><a class="code" href="classCVC3_1_1SearchSat.html#a8cb09d5d17839a0377e369713fcbbedf">00188</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html">SearchSatTheoryAPI</a>;<span class="comment"></span>
<a name="l00189"></a>00189 <span class="comment"> //! DPLLT callback to inform theory that a literal has been assigned</span>
<a name="l00190"></a>00190 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#a14cf6695839ff6ac2a0fc0f134c26d47" title="DPLLT callback to inform theory that a literal has been assigned.">assertLit</a>(<a class="code" href="classSAT_1_1Lit.html">SAT::Lit</a> l);<span class="comment"></span>
<a name="l00191"></a>00191 <span class="comment"> //! DPLLT callback to ask if theory has detected inconsistency.</span>
<a name="l00192"></a>00192 <span class="comment"></span> <a class="code" href="classSAT_1_1DPLLT.html#ac612908684032ffe76ad97f04afd0ca8">SAT::DPLLT::ConsistentResult</a> <a class="code" href="classCVC3_1_1SearchSat.html#aba13a4e3105c6d8ed6ae960a35ac0831" title="DPLLT callback to ask if theory has detected inconsistency.">checkConsistent</a>(<a class="code" href="classSAT_1_1CNF__Formula.html">SAT::CNF_Formula</a>& cnf, <span class="keywordtype">bool</span> fullEffort);<span class="comment"></span>
<a name="l00193"></a>00193 <span class="comment"> //! DPLLT callback to get theory propagations.</span>
<a name="l00194"></a>00194 <span class="comment"></span> <a class="code" href="classSAT_1_1Lit.html">SAT::Lit</a> <a class="code" href="classCVC3_1_1SearchSat.html#a87c52cad8178ab644a84e31ab0290f95" title="DPLLT callback to get theory propagations.">getImplication</a>();<span class="comment"></span>
<a name="l00195"></a>00195 <span class="comment"> //! DPLLT callback to explain a theory propagation.</span>
<a name="l00196"></a>00196 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#a6347fa89942c705786dece8175c2bf6c" title="DPLLT callback to explain a theory propagation.">getExplanation</a>(<a class="code" href="classSAT_1_1Lit.html">SAT::Lit</a> l, <a class="code" href="classSAT_1_1CNF__Formula.html">SAT::CNF_Formula</a>& cnf);<span class="comment"></span>
<a name="l00197"></a>00197 <span class="comment"> //! DPLLT callback to get more general theory clauses.</span>
<a name="l00198"></a>00198 <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1SearchSat.html#a858da2f6e8aefe2aeb124eececd45e3a" title="DPLLT callback to get more general theory clauses.">getNewClauses</a>(<a class="code" href="classSAT_1_1CNF__Formula.html">SAT::CNF_Formula</a>& cnf);
<a name="l00199"></a>00199
<a name="l00200"></a><a class="code" href="classCVC3_1_1SearchSat.html#a447de240c99ed9d998d211b07609bc5d">00200</a> <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchSatDecider.html">SearchSatDecider</a>;<span class="comment"></span>
<a name="l00201"></a>00201 <span class="comment"> //! DPLLT callback to decide which literal to split on next</span>
<a name="l00202"></a>00202 <span class="comment"></span> <a class="code" href="classSAT_1_1Lit.html">SAT::Lit</a> <a class="code" href="classCVC3_1_1SearchSat.html#afa9bdddd9bef64500f6a958d90682c37" title="DPLLT callback to decide which literal to split on next.">makeDecision</a>();
<a name="l00203"></a>00203 <span class="comment"></span>
<a name="l00204"></a>00204 <span class="comment"> //! Recursively traverse DAG looking for a splitter</span>
<a name="l00205"></a>00205 <span class="comment"></span><span class="comment"> /*! Returns true if a splitter is found, false otherwise. The splitter is</span>
<a name="l00206"></a>00206 <span class="comment"> * returned in lit (lit should be set to true). Nodes whose current value is</span>
<a name="l00207"></a>00207 <span class="comment"> * fully justified are marked by calling setFlag to avoid searching them in</span>
<a name="l00208"></a>00208 <span class="comment"> * the future.</span>
<a name="l00209"></a>00209 <span class="comment"> */</span>
<a name="l00210"></a>00210 <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1SearchSat.html#a9b9c34dcc6d7deab8d54c1d03e5b7a2e" title="Recursively traverse DAG looking for a splitter.">findSplitterRec</a>(<a class="code" href="classSAT_1_1Lit.html">SAT::Lit</a> lit, <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">SAT::Var::Val</a> value,
<a name="l00211"></a>00211 <a class="code" href="classSAT_1_1Lit.html">SAT::Lit</a>* litDecision);
<a name="l00212"></a>00212 <span class="comment"></span>
<a name="l00213"></a>00213 <span class="comment"> //! Get the value of a CNF Literal</span>
<a name="l00214"></a><a class="code" href="classCVC3_1_1SearchSat.html#ad0e5b15a0bee268c25db7ee980320e67">00214</a> <span class="comment"></span> <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">SAT::Var::Val</a> <a class="code" href="classCVC3_1_1SearchSat.html#ad0e5b15a0bee268c25db7ee980320e67" title="Get the value of a CNF Literal.">getValue</a>(<a class="code" href="classSAT_1_1Lit.html">SAT::Lit</a> c) {
<a name="l00215"></a>00215 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!c.<a class="code" href="classSAT_1_1Lit.html#ad5f6236c582c95356d720a7401623f36">isNull</a>() &&
<a name="l00216"></a>00216 (!c.<a class="code" href="classSAT_1_1Lit.html#aeb84cef22c7dbf459f95dff9b7cbb4a7">isVar</a>() || unsigned(c.<a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">getVar</a>()) < <a class="code" href="classCVC3_1_1SearchSat.html#a455c295a13215ddc99b8df18f4598af4" title="Cached values of variables.">d_vars</a>.size()),
<a name="l00217"></a>00217 <span class="stringliteral">"Lit out of bounds in getValue"</span>);
<a name="l00218"></a>00218 <span class="keywordflow">return</span> c.<a class="code" href="classSAT_1_1Lit.html#ada14f3ca2b88500b5c2500d60e7f554b">isPositive</a>() ? <a class="code" href="classCVC3_1_1SearchSat.html#a455c295a13215ddc99b8df18f4598af4" title="Cached values of variables.">d_vars</a>[c.<a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">getVar</a>()] :
<a name="l00219"></a>00219 c.<a class="code" href="classSAT_1_1Lit.html#ae6fbaf94176fd32347ff14ba3cbc3363">isInverted</a>() ? <a class="code" href="classSAT_1_1Var.html#a6925789c47aff6619853a1f47592fee5">SAT::Var::invertValue</a>(<a class="code" href="classCVC3_1_1SearchSat.html#a455c295a13215ddc99b8df18f4598af4" title="Cached values of variables.">d_vars</a>[c.<a class="code" href="classSAT_1_1Lit.html#a57e2e6e37cad9595c3edbea88a41262f">getVar</a>()]) :
<a name="l00220"></a>00220 c.<a class="code" href="classSAT_1_1Lit.html#a770e1901858f699490f50e9d2ff1d070">isTrue</a>() ? <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5aea9e61954c8499a11875554e5583da88b7">SAT::Var::TRUE_VAL</a> : <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfa047662472190c5c32f81cb409b2139bc">SAT::Var::FALSE_VAL</a>;
<a name="l00221"></a>00221 }
<a name="l00222"></a>00222
<a name="l00223"></a><a class="code" href="classCVC3_1_1SearchSat.html#a333a205198c7df1975fe460bce80ae6a">00223</a> <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">SAT::Var::Val</a> <a class="code" href="classCVC3_1_1SearchSat.html#a333a205198c7df1975fe460bce80ae6a">getValue</a>(<a class="code" href="classSAT_1_1Var.html">SAT::Var</a> v) {
<a name="l00224"></a>00224 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(v.<a class="code" href="classSAT_1_1Var.html#a685cd5d7b11f6ce00074de3e1241c708">isVar</a>() && unsigned(v) < <a class="code" href="classCVC3_1_1SearchSat.html#a455c295a13215ddc99b8df18f4598af4" title="Cached values of variables.">d_vars</a>.size(), <span class="stringliteral">"Var out of bounds in getValue"</span>);
<a name="l00225"></a>00225 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1SearchSat.html#a455c295a13215ddc99b8df18f4598af4" title="Cached values of variables.">d_vars</a>[v];
<a name="l00226"></a>00226 }
<a name="l00227"></a>00227 <span class="comment"></span>
<a name="l00228"></a>00228 <span class="comment"> //! Set the value of a variable</span>
<a name="l00229"></a><a class="code" href="classCVC3_1_1SearchSat.html#a94c52626fff5a5c7563285f3571ddcc5">00229</a> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#a94c52626fff5a5c7563285f3571ddcc5" title="Set the value of a variable.">setValue</a>(<a class="code" href="classSAT_1_1Var.html">SAT::Var</a> v, <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5ae">SAT::Var::Val</a> val) {
<a name="l00230"></a>00230 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!v.<a class="code" href="classSAT_1_1Var.html#a95b8a85adb5fa5eba0fc090c240558b9">isNull</a>(), <span class="stringliteral">"expected non-null Var"</span>);
<a name="l00231"></a>00231 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keywordtype">unsigned</span>(v) < <a class="code" href="classCVC3_1_1SearchSat.html#a455c295a13215ddc99b8df18f4598af4" title="Cached values of variables.">d_vars</a>.size(), <span class="stringliteral">"Var out of bounds in getValue"</span>);
<a name="l00232"></a>00232 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1SearchSat.html#a455c295a13215ddc99b8df18f4598af4" title="Cached values of variables.">d_vars</a>[v] == <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5aea98bec3ab0d44524d1ea379c9209b9b1a">SAT::Var::UNKNOWN</a>, <span class="stringliteral">"Expected unknown"</span>);
<a name="l00233"></a>00233 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(val != <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5aea98bec3ab0d44524d1ea379c9209b9b1a">SAT::Var::UNKNOWN</a>, <span class="stringliteral">"Expected set to non-unknown"</span>);
<a name="l00234"></a>00234 <a class="code" href="classCVC3_1_1SearchSat.html#a455c295a13215ddc99b8df18f4598af4" title="Cached values of variables.">d_vars</a>[v] = val;
<a name="l00235"></a>00235 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<a class="code" href="classCVC3_1_1SearchSat.html#a6c7fadcd8cd61189c6c3c38a28035993" title="Backtracking size of d_varsUndoList.">d_varsUndoListSize</a> == <a class="code" href="classCVC3_1_1SearchSat.html#a78ea4f3b48395a88f42bb4db58c44541" title="List for backtracking var values.">d_varsUndoList</a>.size(), <span class="stringliteral">"Size mismatch"</span>);
<a name="l00236"></a>00236 <a class="code" href="classCVC3_1_1SearchSat.html#a78ea4f3b48395a88f42bb4db58c44541" title="List for backtracking var values.">d_varsUndoList</a>.push_back(<span class="keywordtype">unsigned</span>(v));
<a name="l00237"></a>00237 <a class="code" href="classCVC3_1_1SearchSat.html#a6c7fadcd8cd61189c6c3c38a28035993" title="Backtracking size of d_varsUndoList.">d_varsUndoListSize</a> = <a class="code" href="classCVC3_1_1SearchSat.html#a6c7fadcd8cd61189c6c3c38a28035993" title="Backtracking size of d_varsUndoList.">d_varsUndoListSize</a> + 1;
<a name="l00238"></a>00238 }
<a name="l00239"></a>00239 <span class="comment"></span>
<a name="l00240"></a>00240 <span class="comment"> //! Check whether this variable's value is justified</span>
<a name="l00241"></a><a class="code" href="classCVC3_1_1SearchSat.html#a74be94781b15e4c9c7787161264066c9">00241</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1SearchSat.html#a74be94781b15e4c9c7787161264066c9" title="Check whether this variable's value is justified.">checkJustified</a>(<a class="code" href="classSAT_1_1Var.html">SAT::Var</a> v)
<a name="l00242"></a>00242 { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1SearchSat.html#a996335737d383fd882b6f1085f72b964" title="Manages CNF formula and its relationship to original Exprs and Theorems.">d_cnfManager</a>-><a class="code" href="classSAT_1_1CNF__Manager.html#a42c3cbd432324757f09ffd622ab1f057" title="Convert a CNF literal to an Expr literal.">concreteLit</a>(<a class="code" href="classSAT_1_1Lit.html">SAT::Lit</a>(v)).<a class="code" href="group__ExprPkg.html#ga3cf472ba2fa033f3e1401e4b67a3f8a0">isJustified</a>(); }
<a name="l00243"></a>00243 <span class="comment"></span>
<a name="l00244"></a>00244 <span class="comment"> //! Mark this variable as justified</span>
<a name="l00245"></a><a class="code" href="classCVC3_1_1SearchSat.html#a628753b6aaaabd0e67a7405d543f8ed0">00245</a> <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#a628753b6aaaabd0e67a7405d543f8ed0" title="Mark this variable as justified.">setJustified</a>(<a class="code" href="classSAT_1_1Var.html">SAT::Var</a> v)
<a name="l00246"></a>00246 { <a class="code" href="classCVC3_1_1SearchSat.html#a996335737d383fd882b6f1085f72b964" title="Manages CNF formula and its relationship to original Exprs and Theorems.">d_cnfManager</a>-><a class="code" href="classSAT_1_1CNF__Manager.html#a42c3cbd432324757f09ffd622ab1f057" title="Convert a CNF literal to an Expr literal.">concreteLit</a>(<a class="code" href="classSAT_1_1Lit.html">SAT::Lit</a>(v)).<a class="code" href="group__ExprPkg.html#ga98a725d64a530023a36be8045d87863a">setJustified</a>(); }
<a name="l00247"></a>00247 <span class="comment"></span>
<a name="l00248"></a>00248 <span class="comment"> //! Main checking procedure shared by checkValid and restart</span>
<a name="l00249"></a>00249 <span class="comment"></span> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="classCVC3_1_1SearchSat.html#a720aba611f6cf6fd78bc3a0ede54564b" title="Main checking procedure shared by checkValid and restart.">check</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 class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& result, <span class="keywordtype">bool</span> isRestart = <span class="keyword">false</span>);
<a name="l00250"></a>00250 <span class="comment"></span>
<a name="l00251"></a>00251 <span class="comment"> //! Helper for newUserAssumptionInt</span>
<a name="l00252"></a>00252 <span class="comment"></span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#a4bc91d2be335eabdcd6174cf634fe9e3" title="Helper for newUserAssumptionInt.">newUserAssumptionIntHelper</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm, <a class="code" href="classSAT_1_1CNF__Formula__Impl.html">SAT::CNF_Formula_Impl</a>& cnf,
<a name="l00253"></a>00253 <span class="keywordtype">bool</span> atBottomScope);<span class="comment"></span>
<a name="l00254"></a>00254 <span class="comment"> //! Helper for newUserAssumption</span>
<a name="l00255"></a>00255 <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1SearchSat.html#ab9c866f4bb3ba8f3662a8ee99760f257" title="Helper for newUserAssumption.">newUserAssumptionInt</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 class="code" href="classSAT_1_1CNF__Formula__Impl.html">SAT::CNF_Formula_Impl</a>& cnf,
<a name="l00256"></a>00256 <span class="keywordtype">bool</span> atBottomScope);
<a name="l00257"></a>00257
<a name="l00258"></a>00258 <span class="keyword">public</span>:
<a name="l00259"></a>00259 <span class="comment"></span>
<a name="l00260"></a>00260 <span class="comment"> //! Constructor</span>
<a name="l00261"></a>00261 <span class="comment"> //! name is the name of the dpllt engine to use, as returned by getName()</span>
<a name="l00262"></a>00262 <span class="comment"></span> <a class="code" href="classCVC3_1_1SearchSat.html#a8298bda3d71fc4f613476d49c8270ecc">SearchSat</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="keyword">const</span> std::string& name);
<a name="l00263"></a>00263 <span class="comment"></span>
<a name="l00264"></a>00264 <span class="comment"> //! Destructor</span>
<a name="l00265"></a>00265 <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1SearchSat.html#ad2e00c54dd9d8d8f1e674065f255a28b" title="Destructor.">~SearchSat</a>();
<a name="l00266"></a>00266
<a name="l00267"></a>00267 <span class="comment">// Implementation of virtual SearchEngine methods</span>
<a name="l00268"></a><a class="code" href="classCVC3_1_1SearchSat.html#a40df6c2ecc6cf95be36169849da3fd3a">00268</a> <span class="keyword">virtual</span> <span class="keyword">const</span> std::string& <a class="code" href="classCVC3_1_1SearchSat.html#a40df6c2ecc6cf95be36169849da3fd3a" title="Name of this search engine.">getName</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1SearchSat.html#ab7dd09d7a8ea0c87e2e1ec42a837160b" title="Name of search engine.">d_name</a>; }
<a name="l00269"></a>00269 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#a2ca4a66d1bf7d0227e646edd3c9b9964" title="Register an atomic formula of interest.">registerAtom</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="l00270"></a>00270 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1SearchSat.html#a737cf8f3791197c405017db18163ce6b" title="Return next literal implied by last assertion. Null Expr if none.">getImpliedLiteral</a>();
<a name="l00271"></a><a class="code" href="classCVC3_1_1SearchSat.html#a9f129c2415d3eef0d73ad6d98ff13d44">00271</a> <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#a9f129c2415d3eef0d73ad6d98ff13d44" title="Push a checkpoint.">push</a>() { <a class="code" href="classCVC3_1_1SearchSat.html#a884c103ef1313d56a3a42d4e3e8468cb" title="Pointer to DPLLT implementation.">d_dpllt</a>-><a class="code" href="classSAT_1_1DPLLT.html#aa074d69f0937b579b5f6cfefabadd083" title="Set a checkpoint for backtracking.">push</a>(); }
<a name="l00272"></a><a class="code" href="classCVC3_1_1SearchSat.html#a5c3eeec4b2c970f9d503b2892c9eb770">00272</a> <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#a5c3eeec4b2c970f9d503b2892c9eb770" title="Restore last checkpoint.">pop</a>() { <a class="code" href="classCVC3_1_1SearchSat.html#a884c103ef1313d56a3a42d4e3e8468cb" title="Pointer to DPLLT implementation.">d_dpllt</a>-><a class="code" href="classSAT_1_1DPLLT.html#a59925cdeed3751c4fe4b5d759ebd755c" title="Restore checkpoint.">pop</a>(); }
<a name="l00273"></a><a class="code" href="classCVC3_1_1SearchSat.html#a2921a84d2f2f33413ccda78789f40147">00273</a> <span class="keyword">virtual</span> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="classCVC3_1_1SearchSat.html#a2921a84d2f2f33413ccda78789f40147" title="Checks the validity of a formula in the current context.">checkValid</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 class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& result)
<a name="l00274"></a>00274 { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1SearchSat.html#a720aba611f6cf6fd78bc3a0ede54564b" title="Main checking procedure shared by checkValid and restart.">check</a>(e, result); }
<a name="l00275"></a><a class="code" href="classCVC3_1_1SearchSat.html#ae7bf52f7780c6f2e085cf23c507fc3e1">00275</a> <span class="keyword">virtual</span> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="classCVC3_1_1SearchSat.html#ae7bf52f7780c6f2e085cf23c507fc3e1" title="Reruns last check with e as an additional assumption.">restart</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 class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& result)
<a name="l00276"></a>00276 { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1SearchSat.html#a720aba611f6cf6fd78bc3a0ede54564b" title="Main checking procedure shared by checkValid and restart.">check</a>(e, result, <span class="keyword">true</span>); }
<a name="l00277"></a>00277 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#a43a09dbf7232bfdb6f10aee4df1add94" title="Returns to context immediately before last call to checkValid.">returnFromCheck</a>();
<a name="l00278"></a><a class="code" href="classCVC3_1_1SearchSat.html#a0828289ad2b19cc7fac453b41287ca50">00278</a> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1SearchSat.html#a0828289ad2b19cc7fac453b41287ca50" title="Returns the result of the most recent valid theorem.">lastThm</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1SearchSat.html#ab41637f4522c5e3f318993392adf84bb" title="Theorem from the last successful checkValid call. It is used by getProof and getAssumptions.">d_lastValid</a>; }
<a name="l00279"></a>00279 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1SearchSat.html#a859331cc6fc93adfdd09cb848cd6de0b" title="Generate and add an assumption to the set of assumptions in the current context.">newUserAssumption</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="l00280"></a>00280 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#a7344ad67225c0d6e30f8c2215bc7e0b0" title="Get all user assumptions made in this and all previous contexts.">getUserAssumptions</a>(std::vector<Expr>& assumptions);
<a name="l00281"></a>00281 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#acee513ead4033fd5bfc16cbab7951dc7" title="Get assumptions made internally in this and all previous contexts.">getInternalAssumptions</a>(std::vector<Expr>& assumptions);
<a name="l00282"></a>00282 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#a63ffdace5647b9d783e4a4a0dd90fb0b" title="Get all assumptions made in this and all previous contexts.">getAssumptions</a>(std::vector<Expr>& assumptions);
<a name="l00283"></a>00283 <span class="keyword">virtual</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1SearchSat.html#a4ec713d6bbbd5d4bd6a9fcacc42a044e" title="Check if the formula has already been assumed previously.">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="l00284"></a>00284 <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1SearchSat.html#af2296bfb7f363cb9b83ca2fa6042d496" title="Will return the set of assertions which make the queried formula false.">getCounterExample</a>(std::vector<Expr>& assertions,
<a name="l00285"></a>00285 <span class="keywordtype">bool</span> inOrder = <span class="keyword">true</span>);
<a name="l00286"></a>00286 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Proof.html">Proof</a> <a class="code" href="classCVC3_1_1SearchSat.html#aa8b7c9812f7f61fc567c502ef3240d85" title="Returns the proof term for the last proven query.">getProof</a>();
<a name="l00287"></a>00287
<a name="l00288"></a>00288 <span class="comment">//:ALEX:</span>
<a name="l00289"></a><a class="code" href="classCVC3_1_1SearchSat.html#ad3267f576f114e049609a8c3c4f01118">00289</a> <span class="keyword">virtual</span> <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bf">FormulaValue</a> <a class="code" href="classCVC3_1_1SearchSat.html#ad3267f576f114e049609a8c3c4f01118">getValue</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">CVC3::Expr</a>& e) {
<a name="l00290"></a>00290 <a class="code" href="classSAT_1_1Lit.html">SAT::Lit</a> l = <a class="code" href="classCVC3_1_1SearchSat.html#a996335737d383fd882b6f1085f72b964" title="Manages CNF formula and its relationship to original Exprs and Theorems.">d_cnfManager</a>-><a class="code" href="classSAT_1_1CNF__Manager.html#a78c85b8b8b747f72d973ed0835294c5e" title="Look up the CNF literal for an Expr.">getCNFLit</a>(e);
<a name="l00291"></a>00291
<a name="l00292"></a>00292 <span class="keywordflow">if</span> (l.<a class="code" href="classSAT_1_1Lit.html#ad5f6236c582c95356d720a7401623f36">isNull</a>()) {
<a name="l00293"></a>00293 <span class="comment">//:DEBUG:</span>
<a name="l00294"></a>00294 std::cout << <span class="stringliteral">"No lit for expr: "</span> << e.<a class="code" href="group__ExprPkg.html#gaf3028bb1619f8cc69b66ec712e1adb54" title="Print the expression to a string.">toString</a>() << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">std::endl</a>;
<a name="l00295"></a>00295 <a class="code" href="debug_8h.html#a2637b2fffa22e3c9fad40cda8fcc3bce" title="If something goes horribly wrong, print a message and abort immediately with exit(1).">FatalAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"getValue"</span>);
<a name="l00296"></a>00296 <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfadb6455bbcb14daca672dfcc52df342d7">UNKNOWN_VAL</a>;
<a name="l00297"></a>00297 } <span class="keywordflow">else</span> {
<a name="l00298"></a>00298 <span class="keywordflow">switch</span> (<a class="code" href="classCVC3_1_1SearchSat.html#ad0e5b15a0bee268c25db7ee980320e67" title="Get the value of a CNF Literal.">getValue</a>(l)) {
<a name="l00299"></a>00299 <span class="keywordflow">case</span> <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5aea9e61954c8499a11875554e5583da88b7">SAT::Var::TRUE_VAL</a>: <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfafbdc0d362f5bc36703903ef24ebbd30b">TRUE_VAL</a>;
<a name="l00300"></a>00300 <span class="keywordflow">case</span> <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5aea008d21718d47e187cbc98a0fcd8fbc03">SAT::Var::FALSE_VAL</a>: <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfa047662472190c5c32f81cb409b2139bc">FALSE_VAL</a>;
<a name="l00301"></a>00301 <span class="keywordflow">case</span> <a class="code" href="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5aea98bec3ab0d44524d1ea379c9209b9b1a">SAT::Var::UNKNOWN</a>: <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfadb6455bbcb14daca672dfcc52df342d7">UNKNOWN_VAL</a>;
<a name="l00302"></a>00302 <span class="keywordflow">default</span>:
<a name="l00303"></a>00303 <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"unreachable"</span>);
<a name="l00304"></a>00304 <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfadb6455bbcb14daca672dfcc52df342d7">UNKNOWN_VAL</a>;
<a name="l00305"></a>00305 }
<a name="l00306"></a>00306 }
<a name="l00307"></a>00307 }
<a name="l00308"></a>00308
<a name="l00309"></a>00309 };
<a name="l00310"></a>00310
<a name="l00311"></a><a class="code" href="namespaceCVC3.html#a9d5504b16aa74dbc6e57c5e928b4ed84">00311</a> <span class="keyword">inline</span> <span class="keywordtype">bool</span> <a class="code" href="namespaceCVC3.html#ad3e3964a0b8cd9e2749de47b053b9d97">operator<</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html" title="Pair of Lit and priority of this Lit.">SearchSat::LitPriorityPair</a>& p1,
<a name="l00312"></a>00312 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html" title="Pair of Lit and priority of this Lit.">SearchSat::LitPriorityPair</a>& p2)
<a name="l00313"></a>00313 {
<a name="l00314"></a>00314 <span class="keywordflow">if</span> (p1.<a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a58ee953d415954051680b4bbfd620e38">d_priority</a> > p2.<a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a58ee953d415954051680b4bbfd620e38">d_priority</a>) <span class="keywordflow">return</span> <span class="keyword">true</span>;
<a name="l00315"></a>00315 <span class="keywordflow">if</span> (p1.<a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a58ee953d415954051680b4bbfd620e38">d_priority</a> < p2.<a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a58ee953d415954051680b4bbfd620e38">d_priority</a>) <span class="keywordflow">return</span> <span class="keyword">false</span>;
<a name="l00316"></a>00316 <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#a39fc111339d6dffdc98d6a25b68dff0e">abs</a>(p1.<a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#adb293dd66bfb682cc70e8261c9920ec3">d_lit</a>.<a class="code" href="classSAT_1_1Lit.html#a744e350c39286a2ea093c3c5f1d083a4">getID</a>()) < <a class="code" href="namespaceCVC3.html#a39fc111339d6dffdc98d6a25b68dff0e">abs</a>(p2.<a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#adb293dd66bfb682cc70e8261c9920ec3">d_lit</a>.<a class="code" href="classSAT_1_1Lit.html#a744e350c39286a2ea093c3c5f1d083a4">getID</a>()) ||
<a name="l00317"></a>00317 (<a class="code" href="namespaceCVC3.html#a39fc111339d6dffdc98d6a25b68dff0e">abs</a>(p1.<a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#adb293dd66bfb682cc70e8261c9920ec3">d_lit</a>.<a class="code" href="classSAT_1_1Lit.html#a744e350c39286a2ea093c3c5f1d083a4">getID</a>()) == <a class="code" href="namespaceCVC3.html#a39fc111339d6dffdc98d6a25b68dff0e">abs</a>(p2.<a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#adb293dd66bfb682cc70e8261c9920ec3">d_lit</a>.<a class="code" href="classSAT_1_1Lit.html#a744e350c39286a2ea093c3c5f1d083a4">getID</a>()) && p1.<a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#adb293dd66bfb682cc70e8261c9920ec3">d_lit</a>.<a class="code" href="classSAT_1_1Lit.html#a744e350c39286a2ea093c3c5f1d083a4">getID</a>() > 0 && (!(p2.<a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#adb293dd66bfb682cc70e8261c9920ec3">d_lit</a>.<a class="code" href="classSAT_1_1Lit.html#a744e350c39286a2ea093c3c5f1d083a4">getID</a>() > 0)));
<a name="l00318"></a>00318 }
<a name="l00319"></a>00319
<a name="l00320"></a>00320 }
<a name="l00321"></a>00321
<a name="l00322"></a>00322 <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>
