<!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"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: search_sat.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<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 id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="dir_68267d1309a1af8e8297ef4c3efbcdba.html">src</a></li><li class="navelem"><a class="el" href="dir_b0856f6b0d80ccb263b2f415c91f9e17.html">include</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">search_sat.h</div> </div>
</div><!--header-->
<div class="contents">
<a href="search__sat_8h.html">Go to the documentation of this file.</a><div class="fragment"><div class="line"><a name="l00001"></a><span class="lineno"> 1</span> <span class="comment">/*****************************************************************************/</span><span class="comment"></span></div>
<div class="line"><a name="l00002"></a><span class="lineno"> 2</span> <span class="comment">/*!</span></div>
<div class="line"><a name="l00003"></a><span class="lineno"> 3</span> <span class="comment"> *\file search_sat.h</span></div>
<div class="line"><a name="l00004"></a><span class="lineno"> 4</span> <span class="comment"> *\brief Search engine that uses an external SAT engine</span></div>
<div class="line"><a name="l00005"></a><span class="lineno"> 5</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00006"></a><span class="lineno"> 6</span> <span class="comment"> * Author: Clark Barrett</span></div>
<div class="line"><a name="l00007"></a><span class="lineno"> 7</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00008"></a><span class="lineno"> 8</span> <span class="comment"> * Created: Mon Dec 5 17:52:05 2005</span></div>
<div class="line"><a name="l00009"></a><span class="lineno"> 9</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00010"></a><span class="lineno"> 10</span> <span class="comment"> * <hr></span></div>
<div class="line"><a name="l00011"></a><span class="lineno"> 11</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00012"></a><span class="lineno"> 12</span> <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span></div>
<div class="line"><a name="l00013"></a><span class="lineno"> 13</span> <span class="comment"> * and its documentation for any purpose is hereby granted without</span></div>
<div class="line"><a name="l00014"></a><span class="lineno"> 14</span> <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span></div>
<div class="line"><a name="l00015"></a><span class="lineno"> 15</span> <span class="comment"> * LICENSE file provided with this distribution.</span></div>
<div class="line"><a name="l00016"></a><span class="lineno"> 16</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00017"></a><span class="lineno"> 17</span> <span class="comment"> * <hr></span></div>
<div class="line"><a name="l00018"></a><span class="lineno"> 18</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00019"></a><span class="lineno"> 19</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00020"></a><span class="lineno"> 20</span> <span class="comment">/*****************************************************************************/</span></div>
<div class="line"><a name="l00021"></a><span class="lineno"> 21</span> </div>
<div class="line"><a name="l00022"></a><span class="lineno"> 22</span> <span class="preprocessor">#ifndef _cvc3__include__search_sat_h_</span></div>
<div class="line"><a name="l00023"></a><span class="lineno"> 23</span> <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__search_sat_h_</span></div>
<div class="line"><a name="l00024"></a><span class="lineno"> 24</span> <span class="preprocessor"></span></div>
<div class="line"><a name="l00025"></a><span class="lineno"> 25</span> <span class="preprocessor">#include <vector></span></div>
<div class="line"><a name="l00026"></a><span class="lineno"> 26</span> <span class="preprocessor">#include <set></span></div>
<div class="line"><a name="l00027"></a><span class="lineno"> 27</span> <span class="preprocessor">#include "<a class="code" href="search_8h.html" title="Abstract API to the proof search engine.">search.h</a>"</span></div>
<div class="line"><a name="l00028"></a><span class="lineno"> 28</span> <span class="preprocessor">#include "<a class="code" href="smartcdo_8h.html" title="Smart context-dependent object wrapper.">smartcdo.h</a>"</span></div>
<div class="line"><a name="l00029"></a><span class="lineno"> 29</span> <span class="preprocessor">#include "<a class="code" href="cdlist_8h.html">cdlist.h</a>"</span></div>
<div class="line"><a name="l00030"></a><span class="lineno"> 30</span> <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></div>
<div class="line"><a name="l00031"></a><span class="lineno"> 31</span> <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></div>
<div class="line"><a name="l00032"></a><span class="lineno"> 32</span> <span class="preprocessor">#include "<a class="code" href="dpllt_8h.html" title="Generic DPLL(T) module.">dpllt.h</a>"</span></div>
<div class="line"><a name="l00033"></a><span class="lineno"> 33</span> <span class="preprocessor">#include "<a class="code" href="theory__core_8h.html">theory_core.h</a>"</span></div>
<div class="line"><a name="l00034"></a><span class="lineno"> 34</span> <span class="preprocessor">#include "<a class="code" href="formula__value_8h.html" title="enumerated type for value of formulas">formula_value.h</a>"</span></div>
<div class="line"><a name="l00035"></a><span class="lineno"> 35</span> </div>
<div class="line"><a name="l00036"></a><span class="lineno"> 36</span> <span class="keyword">namespace </span>CVC3 {</div>
<div class="line"><a name="l00037"></a><span class="lineno"> 37</span> <span class="comment"></span></div>
<div class="line"><a name="l00038"></a><span class="lineno"> 38</span> <span class="comment">//! Search engine that connects to a generic SAT reasoning module</span></div>
<div class="line"><a name="l00039"></a><span class="lineno"> 39</span> <span class="comment"></span><span class="comment">/*! \ingroup SE */</span></div>
<div class="line"><a name="l00040"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html"> 40</a></span> <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> {</div>
<div class="line"><a name="l00041"></a><span class="lineno"> 41</span> <span class="comment"></span></div>
<div class="line"><a name="l00042"></a><span class="lineno"> 42</span> <span class="comment"> //! Name of search engine</span></div>
<div class="line"><a name="l00043"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#ab7dd09d7a8ea0c87e2e1ec42a837160b"> 43</a></span> <span class="comment"></span> std::string <a class="code" href="classCVC3_1_1SearchSat.html#ab7dd09d7a8ea0c87e2e1ec42a837160b" title="Name of search engine.">d_name</a>;</div>
<div class="line"><a name="l00044"></a><span class="lineno"> 44</span> <span class="comment"></span></div>
<div class="line"><a name="l00045"></a><span class="lineno"> 45</span> <span class="comment"> //! Bottom scope for current query</span></div>
<div class="line"><a name="l00046"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a8153b8d7b772217bafddf3d92be4759b"> 46</a></span> <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>;</div>
<div class="line"><a name="l00047"></a><span class="lineno"> 47</span> <span class="comment"></span></div>
<div class="line"><a name="l00048"></a><span class="lineno"> 48</span> <span class="comment"> //! Last expr checked for validity</span></div>
<div class="line"><a name="l00049"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#ac318c6520fbea766517991127affaafc"> 49</a></span> <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>;</div>
<div class="line"><a name="l00050"></a><span class="lineno"> 50</span> <span class="comment"></span></div>
<div class="line"><a name="l00051"></a><span class="lineno"> 51</span> <span class="comment"> /*! @brief Theorem from the last successful checkValid call. It is</span></div>
<div class="line"><a name="l00052"></a><span class="lineno"> 52</span> <span class="comment"> used by getProof and getAssumptions. */</span></div>
<div class="line"><a name="l00053"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#ab41637f4522c5e3f318993392adf84bb"> 53</a></span>  <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>;</div>
<div class="line"><a name="l00054"></a><span class="lineno"> 54</span> <span class="comment"></span></div>
<div class="line"><a name="l00055"></a><span class="lineno"> 55</span> <span class="comment"> //! List of all user assumptions</span></div>
<div class="line"><a name="l00056"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a3b9b2371a24908e62ec71b6f141afea8"> 56</a></span> <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>;</div>
<div class="line"><a name="l00057"></a><span class="lineno"> 57</span> <span class="comment"></span></div>
<div class="line"><a name="l00058"></a><span class="lineno"> 58</span> <span class="comment"> //! List of all internal assumptions</span></div>
<div class="line"><a name="l00059"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#ad3b9879d655cf3fce1a70de7b1d6fedc"> 59</a></span> <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>;</div>
<div class="line"><a name="l00060"></a><span class="lineno"> 60</span> <span class="comment"></span></div>
<div class="line"><a name="l00061"></a><span class="lineno"> 61</span> <span class="comment"> //! Index to where unprocessed assumptions start</span></div>
<div class="line"><a name="l00062"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a23b0c38d89ce24f463f2c2fc929df879"> 62</a></span> <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>;</div>
<div class="line"><a name="l00063"></a><span class="lineno"> 63</span> </div>
<div class="line"><a name="l00064"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#aab55d9ceeb2a938841230c920762ba77"> 64</a></span>  <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>;</div>
<div class="line"><a name="l00065"></a><span class="lineno"> 65</span> <span class="comment"></span></div>
<div class="line"><a name="l00066"></a><span class="lineno"> 66</span> <span class="comment"> //! Pointer to DPLLT implementation</span></div>
<div class="line"><a name="l00067"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a884c103ef1313d56a3a42d4e3e8468cb"> 67</a></span> <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>;</div>
<div class="line"><a name="l00068"></a><span class="lineno"> 68</span> <span class="comment"></span></div>
<div class="line"><a name="l00069"></a><span class="lineno"> 69</span> <span class="comment"> //! Implementation of TheoryAPI for DPLLT</span></div>
<div class="line"><a name="l00070"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a8abc1b647affa60cc367e0eeaa52cdf4"> 70</a></span> <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>;</div>
<div class="line"><a name="l00071"></a><span class="lineno"> 71</span> <span class="comment"></span></div>
<div class="line"><a name="l00072"></a><span class="lineno"> 72</span> <span class="comment"> //! Implementation of Decider for DPLLT</span></div>
<div class="line"><a name="l00073"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#aa4be1d02557a46fbbdc32deefc4f3a32"> 73</a></span> <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>;</div>
<div class="line"><a name="l00074"></a><span class="lineno"> 74</span> <span class="comment"></span></div>
<div class="line"><a name="l00075"></a><span class="lineno"> 75</span> <span class="comment"> //! Store of theorems for expressions sent to DPLLT</span></div>
<div class="line"><a name="l00076"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a3e6b8d2d1d9513329fbbb80464053b39"> 76</a></span> <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>;</div>
<div class="line"><a name="l00077"></a><span class="lineno"> 77</span> <span class="comment"></span></div>
<div class="line"><a name="l00078"></a><span class="lineno"> 78</span> <span class="comment"> //! Manages CNF formula and its relationship to original Exprs and Theorems</span></div>
<div class="line"><a name="l00079"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a996335737d383fd882b6f1085f72b964"> 79</a></span> <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>;</div>
<div class="line"><a name="l00080"></a><span class="lineno"> 80</span> <span class="comment"></span></div>
<div class="line"><a name="l00081"></a><span class="lineno"> 81</span> <span class="comment"> //! Callback for CNF_Manager</span></div>
<div class="line"><a name="l00082"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a158485ff14b490fc2c91936a4e72bf5b"> 82</a></span> <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>;</div>
<div class="line"><a name="l00083"></a><span class="lineno"> 83</span> <span class="comment"></span></div>
<div class="line"><a name="l00084"></a><span class="lineno"> 84</span> <span class="comment"> //! Cached values of variables</span></div>
<div class="line"><a name="l00085"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a455c295a13215ddc99b8df18f4598af4"> 85</a></span> <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>;</div>
<div class="line"><a name="l00086"></a><span class="lineno"> 86</span> <span class="comment"></span></div>
<div class="line"><a name="l00087"></a><span class="lineno"> 87</span> <span class="comment"> //! Whether we are currently in a call to dpllt->checkSat</span></div>
<div class="line"><a name="l00088"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a00573a594dd2b83cbb6f2997516862d3"> 88</a></span> <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>;</div>
<div class="line"><a name="l00089"></a><span class="lineno"> 89</span> <span class="comment"></span></div>
<div class="line"><a name="l00090"></a><span class="lineno"> 90</span> <span class="comment"> //! CNF Formula used for theory lemmas</span></div>
<div class="line"><a name="l00091"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#aed781537ef3315ffa019cdd7f02f0f8e"> 91</a></span> <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>;</div>
<div class="line"><a name="l00092"></a><span class="lineno"> 92</span> <span class="comment"></span></div>
<div class="line"><a name="l00093"></a><span class="lineno"> 93</span> <span class="comment"> //! Lemmas waiting to be translated since last call to getNewClauses()</span></div>
<div class="line"><a name="l00094"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a3997be227d7cd36e1f29f71a683f1428"> 94</a></span> <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>;</div>
<div class="line"><a name="l00095"></a><span class="lineno"> 95</span> <span class="comment"></span></div>
<div class="line"><a name="l00096"></a><span class="lineno"> 96</span> <span class="comment"> //! Scope parameter for lemmas waiting to be translated since last call to getNewClauses()</span></div>
<div class="line"><a name="l00097"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a83bb96cd69f2673e370e536a7946c5c3"> 97</a></span> <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>;</div>
<div class="line"><a name="l00098"></a><span class="lineno"> 98</span> <span class="comment"></span></div>
<div class="line"><a name="l00099"></a><span class="lineno"> 99</span> <span class="comment"> //! Backtracking size of d_pendingLemmas</span></div>
<div class="line"><a name="l00100"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#ab309591a57e34a9166c3baa056e2857f"> 100</a></span> <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>;</div>
<div class="line"><a name="l00101"></a><span class="lineno"> 101</span> <span class="comment"></span></div>
<div class="line"><a name="l00102"></a><span class="lineno"> 102</span> <span class="comment"> //! Backtracking next item in d_pendingLemmas</span></div>
<div class="line"><a name="l00103"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a8de03d523c9b0304eb95e72ec923274b"> 103</a></span> <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>;</div>
<div class="line"><a name="l00104"></a><span class="lineno"> 104</span> <span class="comment"></span></div>
<div class="line"><a name="l00105"></a><span class="lineno"> 105</span> <span class="comment"> //! Current position in d_lemmas</span></div>
<div class="line"><a name="l00106"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a819ee9729fd633651eb2cf27f7175d8a"> 106</a></span> <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>;</div>
<div class="line"><a name="l00107"></a><span class="lineno"> 107</span> <span class="comment"></span></div>
<div class="line"><a name="l00108"></a><span class="lineno"> 108</span> <span class="comment"> //! List for backtracking var values</span></div>
<div class="line"><a name="l00109"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a78ea4f3b48395a88f42bb4db58c44541"> 109</a></span> <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>;</div>
<div class="line"><a name="l00110"></a><span class="lineno"> 110</span> <span class="comment"></span></div>
<div class="line"><a name="l00111"></a><span class="lineno"> 111</span> <span class="comment"> //! Backtracking size of d_varsUndoList</span></div>
<div class="line"><a name="l00112"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a6c7fadcd8cd61189c6c3c38a28035993"> 112</a></span> <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>;</div>
<div class="line"><a name="l00113"></a><span class="lineno"> 113</span> </div>
<div class="line"><a name="l00114"></a><span class="lineno"> 114</span> <span class="keyword">public</span>:<span class="comment"></span></div>
<div class="line"><a name="l00115"></a><span class="lineno"> 115</span> <span class="comment"> //! Pair of Lit and priority of this Lit</span></div>
<div class="line"><a name="l00116"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html"> 116</a></span> <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> {</div>
<div class="line"><a name="l00117"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#adb293dd66bfb682cc70e8261c9920ec3"> 117</a></span>  <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>;</div>
<div class="line"><a name="l00118"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a58ee953d415954051680b4bbfd620e38"> 118</a></span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a58ee953d415954051680b4bbfd620e38">d_priority</a>;</div>
<div class="line"><a name="l00119"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a5e6570cbdb63cf05dc4849a10f614440"> 119</a></span>  <a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a5e6570cbdb63cf05dc4849a10f614440">LitPriorityPair</a>() {}</div>
<div class="line"><a name="l00120"></a><span class="lineno"> 120</span>  <span class="keyword">public</span>:</div>
<div class="line"><a name="l00121"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a693e54e7ed50745cf2f5954ae1143ea0"> 121</a></span>  <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)</div>
<div class="line"><a name="l00122"></a><span class="lineno"> 122</span>  : <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) {}</div>
<div class="line"><a name="l00123"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#a6b3a395df128bdf30ba375a1b55d76da"> 123</a></span>  <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>; }</div>
<div class="line"><a name="l00124"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#ad71d50229df3338a2ad460ddf4120b31"> 124</a></span>  <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>; }</div>
<div class="line"><a name="l00125"></a><span class="lineno"> 125</span>  <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,</div>
<div class="line"><a name="l00126"></a><span class="lineno"> 126</span>  <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);</div>
<div class="line"><a name="l00127"></a><span class="lineno"> 127</span>  };</div>
<div class="line"><a name="l00128"></a><span class="lineno"> 128</span> </div>
<div class="line"><a name="l00129"></a><span class="lineno"> 129</span> <span class="keyword">private</span>:<span class="comment"></span></div>
<div class="line"><a name="l00130"></a><span class="lineno"> 130</span> <span class="comment"> //! Used to determine order to find splitters</span></div>
<div class="line"><a name="l00131"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#ab4dbd42cf98469a2abb679024a402b77"> 131</a></span> <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></div>
<div class="line"><a name="l00132"></a><span class="lineno"> 132</span> <span class="comment"> //! Current position in prioritySet</span></div>
<div class="line"><a name="l00133"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#ad7b3c57fadbc655bddd204b9ea122a62"> 133</a></span> <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></div>
<div class="line"><a name="l00134"></a><span class="lineno"> 134</span> <span class="comment"> //! Backtracking size of priority set entries</span></div>
<div class="line"><a name="l00135"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a3495b7cac1dc81f07f54dc8d0b17b17a"> 135</a></span> <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></div>
<div class="line"><a name="l00136"></a><span class="lineno"> 136</span> <span class="comment"> //! Entries in priority set in insertion order (so set can be backtracked)</span></div>
<div class="line"><a name="l00137"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#ab57f9f48af74c9a6493986b8cb0c720d"> 137</a></span> <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></div>
<div class="line"><a name="l00138"></a><span class="lineno"> 138</span> <span class="comment"> //! Backtracking size of priority set entries at bottom scope</span></div>
<div class="line"><a name="l00139"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a99063dd2470eae948fa85d460a9b3868"> 139</a></span> <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></div>
<div class="line"><a name="l00140"></a><span class="lineno"> 140</span> <span class="comment"> //! Current size of bottom entries</span></div>
<div class="line"><a name="l00141"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#ab8e5996fd3e75c5b3c45f611d3639535"> 141</a></span> <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></div>
<div class="line"><a name="l00142"></a><span class="lineno"> 142</span> <span class="comment"> //! Entries in priority set in insertion order (so set can be backtracked)</span></div>
<div class="line"><a name="l00143"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a6d963065a2df65795626cf6d70f8fe99"> 143</a></span> <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>;</div>
<div class="line"><a name="l00144"></a><span class="lineno"> 144</span> <span class="comment"></span></div>
<div class="line"><a name="l00145"></a><span class="lineno"> 145</span> <span class="comment"> //! Last Var registered with core theory</span></div>
<div class="line"><a name="l00146"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a217f464659b186330934d046aa7cc764"> 146</a></span> <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>;</div>
<div class="line"><a name="l00147"></a><span class="lineno"> 147</span> <span class="comment"></span></div>
<div class="line"><a name="l00148"></a><span class="lineno"> 148</span> <span class="comment"> //! Whether it's OK to call DPLLT solver from the current scope</span></div>
<div class="line"><a name="l00149"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#af0953025654043f6f76040df7abf2658"> 149</a></span> <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>;</div>
<div class="line"><a name="l00150"></a><span class="lineno"> 150</span> </div>
<div class="line"><a name="l00151"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#ae97f61c9a0ae9ed8186929e15892ad73"> 151</a></span>  <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned></a> <a class="code" href="classCVC3_1_1SearchSat.html#ae97f61c9a0ae9ed8186929e15892ad73">d_nextImpliedLiteral</a>;</div>
<div class="line"><a name="l00152"></a><span class="lineno"> 152</span> <span class="comment"></span></div>
<div class="line"><a name="l00153"></a><span class="lineno"> 153</span> <span class="comment"> //! Helper class for resetting DPLLT engine</span></div>
<div class="line"><a name="l00154"></a><span class="lineno"> 154</span> <span class="comment"></span><span class="comment"> /*! We need to be notified when the scope goes below the scope from</span></div>
<div class="line"><a name="l00155"></a><span class="lineno"> 155</span> <span class="comment"> * which the last invalid call to checkValid originated. This helper class</span></div>
<div class="line"><a name="l00156"></a><span class="lineno"> 156</span> <span class="comment"> * ensures that this happens.</span></div>
<div class="line"><a name="l00157"></a><span class="lineno"> 157</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00158"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#aa9f952c8606458f1e777d9a05b11550d"> 158</a></span>  <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html">Restorer</a>;</div>
<div class="line"><a name="l00159"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html"> 159</a></span>  <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> {</div>
<div class="line"><a name="l00160"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html#a4c5124e80744f2d60b408328c648d85a"> 160</a></span>  <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>;</div>
<div class="line"><a name="l00161"></a><span class="lineno"> 161</span>  <span class="keyword">public</span>:</div>
<div class="line"><a name="l00162"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html#a60db1d8baa0ef8723379d512481d51d9"> 162</a></span>  <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)</div>
<div class="line"><a name="l00163"></a><span class="lineno"> 163</span>  : <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) {}</div>
<div class="line"><a name="l00164"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html#a482cb3047c1bba972a8ca6d7e474b9e9"> 164</a></span>  <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>(); }</div>
<div class="line"><a name="l00165"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat_1_1Restorer.html#a3ef0a65d1c37d83f9b3733c8d20c7c3d"> 165</a></span>  <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>(); }</div>
<div class="line"><a name="l00166"></a><span class="lineno"> 166</span>  };<span class="comment"></span></div>
<div class="line"><a name="l00167"></a><span class="lineno"> 167</span> <span class="comment"> //! Instance of Restorer class</span></div>
<div class="line"><a name="l00168"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a5b7313c3933e04b894089b1c2e09c57e"> 168</a></span> <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>;</div>
<div class="line"><a name="l00169"></a><span class="lineno"> 169</span> </div>
<div class="line"><a name="l00170"></a><span class="lineno"> 170</span> <span class="keyword">private</span>:</div>
<div class="line"><a name="l00171"></a><span class="lineno"> 171</span> <span class="comment"></span></div>
<div class="line"><a name="l00172"></a><span class="lineno"> 172</span> <span class="comment"> //! Get rid of bottom scope entries in prioritySet</span></div>
<div class="line"><a name="l00173"></a><span class="lineno"> 173</span> <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></div>
<div class="line"><a name="l00174"></a><span class="lineno"> 174</span> <span class="comment"> //! Get rid of entries in prioritySet and pendingLemmas added since last push</span></div>
<div class="line"><a name="l00175"></a><span class="lineno"> 175</span> <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></div>
<div class="line"><a name="l00176"></a><span class="lineno"> 176</span> <span class="comment"> //! Helper for addLemma and check</span></div>
<div class="line"><a name="l00177"></a><span class="lineno"> 177</span> <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>);</div>
<div class="line"><a name="l00178"></a><span class="lineno"> 178</span> </div>
<div class="line"><a name="l00179"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a71c71132ecb225ad44dd66fc2c3505f3"> 179</a></span>  <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchSatCoreSatAPI.html">SearchSatCoreSatAPI</a>;</div>
<div class="line"><a name="l00180"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#acfd18b3733ce33513e1e5ddaad615624"> 180</a></span>  <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchSatCNFCallback.html">SearchSatCNFCallback</a>;<span class="comment"></span></div>
<div class="line"><a name="l00181"></a><span class="lineno"> 181</span> <span class="comment"> //! Core theory callback which adds a new lemma from the core theory</span></div>
<div class="line"><a name="l00182"></a><span class="lineno"> 182</span> <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></div>
<div class="line"><a name="l00183"></a><span class="lineno"> 183</span> <span class="comment"> //! Core theory callback which asks for the bottom scope for current query</span></div>
<div class="line"><a name="l00184"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a7dd555ba6043bd8019091ac6289233d6"> 184</a></span> <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></div>
<div class="line"><a name="l00185"></a><span class="lineno"> 185</span> <span class="comment"> //! Core theory callback which suggests a splitter</span></div>
<div class="line"><a name="l00186"></a><span class="lineno"> 186</span> <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);</div>
<div class="line"><a name="l00187"></a><span class="lineno"> 187</span> </div>
<div class="line"><a name="l00188"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a8cb09d5d17839a0377e369713fcbbedf"> 188</a></span>  <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchSatTheoryAPI.html">SearchSatTheoryAPI</a>;<span class="comment"></span></div>
<div class="line"><a name="l00189"></a><span class="lineno"> 189</span> <span class="comment"> //! DPLLT callback to inform theory that a literal has been assigned</span></div>
<div class="line"><a name="l00190"></a><span class="lineno"> 190</span> <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></div>
<div class="line"><a name="l00191"></a><span class="lineno"> 191</span> <span class="comment"> //! DPLLT callback to ask if theory has detected inconsistency.</span></div>
<div class="line"><a name="l00192"></a><span class="lineno"> 192</span> <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></div>
<div class="line"><a name="l00193"></a><span class="lineno"> 193</span> <span class="comment"> //! DPLLT callback to get theory propagations.</span></div>
<div class="line"><a name="l00194"></a><span class="lineno"> 194</span> <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></div>
<div class="line"><a name="l00195"></a><span class="lineno"> 195</span> <span class="comment"> //! DPLLT callback to explain a theory propagation.</span></div>
<div class="line"><a name="l00196"></a><span class="lineno"> 196</span> <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></div>
<div class="line"><a name="l00197"></a><span class="lineno"> 197</span> <span class="comment"> //! DPLLT callback to get more general theory clauses.</span></div>
<div class="line"><a name="l00198"></a><span class="lineno"> 198</span> <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);</div>
<div class="line"><a name="l00199"></a><span class="lineno"> 199</span> </div>
<div class="line"><a name="l00200"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a447de240c99ed9d998d211b07609bc5d"> 200</a></span>  <span class="keyword">friend</span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1SearchSatDecider.html">SearchSatDecider</a>;<span class="comment"></span></div>
<div class="line"><a name="l00201"></a><span class="lineno"> 201</span> <span class="comment"> //! DPLLT callback to decide which literal to split on next</span></div>
<div class="line"><a name="l00202"></a><span class="lineno"> 202</span> <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>();</div>
<div class="line"><a name="l00203"></a><span class="lineno"> 203</span> <span class="comment"></span></div>
<div class="line"><a name="l00204"></a><span class="lineno"> 204</span> <span class="comment"> //! Recursively traverse DAG looking for a splitter</span></div>
<div class="line"><a name="l00205"></a><span class="lineno"> 205</span> <span class="comment"></span><span class="comment"> /*! Returns true if a splitter is found, false otherwise. The splitter is</span></div>
<div class="line"><a name="l00206"></a><span class="lineno"> 206</span> <span class="comment"> * returned in lit (lit should be set to true). Nodes whose current value is</span></div>
<div class="line"><a name="l00207"></a><span class="lineno"> 207</span> <span class="comment"> * fully justified are marked by calling setFlag to avoid searching them in</span></div>
<div class="line"><a name="l00208"></a><span class="lineno"> 208</span> <span class="comment"> * the future.</span></div>
<div class="line"><a name="l00209"></a><span class="lineno"> 209</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00210"></a><span class="lineno"> 210</span>  <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,</div>
<div class="line"><a name="l00211"></a><span class="lineno"> 211</span>  <a class="code" href="classSAT_1_1Lit.html">SAT::Lit</a>* litDecision);</div>
<div class="line"><a name="l00212"></a><span class="lineno"> 212</span> <span class="comment"></span></div>
<div class="line"><a name="l00213"></a><span class="lineno"> 213</span> <span class="comment"> //! Get the value of a CNF Literal</span></div>
<div class="line"><a name="l00214"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#ad0e5b15a0bee268c25db7ee980320e67"> 214</a></span> <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) {</div>
<div class="line"><a name="l00215"></a><span class="lineno"> 215</span>  <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(!c.<a class="code" href="classSAT_1_1Lit.html#ad5f6236c582c95356d720a7401623f36">isNull</a>() &&</div>
<div class="line"><a name="l00216"></a><span class="lineno"> 216</span>  (!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()),</div>
<div class="line"><a name="l00217"></a><span class="lineno"> 217</span>  <span class="stringliteral">"Lit out of bounds in getValue"</span>);</div>
<div class="line"><a name="l00218"></a><span class="lineno"> 218</span>  <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>()] :</div>
<div class="line"><a name="l00219"></a><span class="lineno"> 219</span>  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>()]) :</div>
<div class="line"><a name="l00220"></a><span class="lineno"> 220</span>  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="classSAT_1_1Var.html#ac9cf10f19f5f4d86ad539777fd8ca5aea008d21718d47e187cbc98a0fcd8fbc03">SAT::Var::FALSE_VAL</a>;</div>
<div class="line"><a name="l00221"></a><span class="lineno"> 221</span>  }</div>
<div class="line"><a name="l00222"></a><span class="lineno"> 222</span> </div>
<div class="line"><a name="l00223"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a333a205198c7df1975fe460bce80ae6a"> 223</a></span>  <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) {</div>
<div class="line"><a name="l00224"></a><span class="lineno"> 224</span>  <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>);</div>
<div class="line"><a name="l00225"></a><span class="lineno"> 225</span>  <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1SearchSat.html#a455c295a13215ddc99b8df18f4598af4" title="Cached values of variables.">d_vars</a>[v];</div>
<div class="line"><a name="l00226"></a><span class="lineno"> 226</span>  }</div>
<div class="line"><a name="l00227"></a><span class="lineno"> 227</span> <span class="comment"></span></div>
<div class="line"><a name="l00228"></a><span class="lineno"> 228</span> <span class="comment"> //! Set the value of a variable</span></div>
<div class="line"><a name="l00229"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a94c52626fff5a5c7563285f3571ddcc5"> 229</a></span> <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) {</div>
<div class="line"><a name="l00230"></a><span class="lineno"> 230</span>  <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>);</div>
<div class="line"><a name="l00231"></a><span class="lineno"> 231</span>  <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>);</div>
<div class="line"><a name="l00232"></a><span class="lineno"> 232</span>  <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>);</div>
<div class="line"><a name="l00233"></a><span class="lineno"> 233</span>  <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>);</div>
<div class="line"><a name="l00234"></a><span class="lineno"> 234</span>  <a class="code" href="classCVC3_1_1SearchSat.html#a455c295a13215ddc99b8df18f4598af4" title="Cached values of variables.">d_vars</a>[v] = val;</div>
<div class="line"><a name="l00235"></a><span class="lineno"> 235</span>  <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>);</div>
<div class="line"><a name="l00236"></a><span class="lineno"> 236</span>  <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));</div>
<div class="line"><a name="l00237"></a><span class="lineno"> 237</span>  <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;</div>
<div class="line"><a name="l00238"></a><span class="lineno"> 238</span>  }</div>
<div class="line"><a name="l00239"></a><span class="lineno"> 239</span> <span class="comment"></span></div>
<div class="line"><a name="l00240"></a><span class="lineno"> 240</span> <span class="comment"> //! Check whether this variable's value is justified</span></div>
<div class="line"><a name="l00241"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a74be94781b15e4c9c7787161264066c9"> 241</a></span> <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)</div>
<div class="line"><a name="l00242"></a><span class="lineno"> 242</span>  { <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>(); }</div>
<div class="line"><a name="l00243"></a><span class="lineno"> 243</span> <span class="comment"></span></div>
<div class="line"><a name="l00244"></a><span class="lineno"> 244</span> <span class="comment"> //! Mark this variable as justified</span></div>
<div class="line"><a name="l00245"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a628753b6aaaabd0e67a7405d543f8ed0"> 245</a></span> <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)</div>
<div class="line"><a name="l00246"></a><span class="lineno"> 246</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#ga98a725d64a530023a36be8045d87863a">setJustified</a>(); }</div>
<div class="line"><a name="l00247"></a><span class="lineno"> 247</span> <span class="comment"></span></div>
<div class="line"><a name="l00248"></a><span class="lineno"> 248</span> <span class="comment"> //! Main checking procedure shared by checkValid and restart</span></div>
<div class="line"><a name="l00249"></a><span class="lineno"> 249</span> <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>);</div>
<div class="line"><a name="l00250"></a><span class="lineno"> 250</span> <span class="comment"></span></div>
<div class="line"><a name="l00251"></a><span class="lineno"> 251</span> <span class="comment"> //! Helper for newUserAssumptionInt</span></div>
<div class="line"><a name="l00252"></a><span class="lineno"> 252</span> <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,</div>
<div class="line"><a name="l00253"></a><span class="lineno"> 253</span>  <span class="keywordtype">bool</span> atBottomScope);<span class="comment"></span></div>
<div class="line"><a name="l00254"></a><span class="lineno"> 254</span> <span class="comment"> //! Helper for newUserAssumption</span></div>
<div class="line"><a name="l00255"></a><span class="lineno"> 255</span> <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,</div>
<div class="line"><a name="l00256"></a><span class="lineno"> 256</span>  <span class="keywordtype">bool</span> atBottomScope);</div>
<div class="line"><a name="l00257"></a><span class="lineno"> 257</span> </div>
<div class="line"><a name="l00258"></a><span class="lineno"> 258</span> <span class="keyword">public</span>:</div>
<div class="line"><a name="l00259"></a><span class="lineno"> 259</span> <span class="comment"></span></div>
<div class="line"><a name="l00260"></a><span class="lineno"> 260</span> <span class="comment"> //! Constructor</span></div>
<div class="line"><a name="l00261"></a><span class="lineno"> 261</span> <span class="comment"> //! name is the name of the dpllt engine to use, as returned by getName()</span></div>
<div class="line"><a name="l00262"></a><span class="lineno"> 262</span> <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);</div>
<div class="line"><a name="l00263"></a><span class="lineno"> 263</span> <span class="comment"></span></div>
<div class="line"><a name="l00264"></a><span class="lineno"> 264</span> <span class="comment"> //! Destructor</span></div>
<div class="line"><a name="l00265"></a><span class="lineno"> 265</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1SearchSat.html#ad2e00c54dd9d8d8f1e674065f255a28b" title="Destructor.">~SearchSat</a>();</div>
<div class="line"><a name="l00266"></a><span class="lineno"> 266</span> </div>
<div class="line"><a name="l00267"></a><span class="lineno"> 267</span>  <span class="comment">// Implementation of virtual SearchEngine methods</span></div>
<div class="line"><a name="l00268"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a40df6c2ecc6cf95be36169849da3fd3a"> 268</a></span>  <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>; }</div>
<div class="line"><a name="l00269"></a><span class="lineno"> 269</span>  <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);</div>
<div class="line"><a name="l00270"></a><span class="lineno"> 270</span>  <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>();</div>
<div class="line"><a name="l00271"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a9f129c2415d3eef0d73ad6d98ff13d44"> 271</a></span>  <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>(); }</div>
<div class="line"><a name="l00272"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a5c3eeec4b2c970f9d503b2892c9eb770"> 272</a></span>  <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>(); }</div>
<div class="line"><a name="l00273"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a2921a84d2f2f33413ccda78789f40147"> 273</a></span>  <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)</div>
<div class="line"><a name="l00274"></a><span class="lineno"> 274</span>  { <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); }</div>
<div class="line"><a name="l00275"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#ae7bf52f7780c6f2e085cf23c507fc3e1"> 275</a></span>  <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)</div>
<div class="line"><a name="l00276"></a><span class="lineno"> 276</span>  { <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>); }</div>
<div class="line"><a name="l00277"></a><span class="lineno"> 277</span>  <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>();</div>
<div class="line"><a name="l00278"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#a0828289ad2b19cc7fac453b41287ca50"> 278</a></span>  <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>; }</div>
<div class="line"><a name="l00279"></a><span class="lineno"> 279</span>  <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);</div>
<div class="line"><a name="l00280"></a><span class="lineno"> 280</span>  <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);</div>
<div class="line"><a name="l00281"></a><span class="lineno"> 281</span>  <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);</div>
<div class="line"><a name="l00282"></a><span class="lineno"> 282</span>  <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);</div>
<div class="line"><a name="l00283"></a><span class="lineno"> 283</span>  <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);</div>
<div class="line"><a name="l00284"></a><span class="lineno"> 284</span>  <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,</div>
<div class="line"><a name="l00285"></a><span class="lineno"> 285</span>  <span class="keywordtype">bool</span> inOrder = <span class="keyword">true</span>);</div>
<div class="line"><a name="l00286"></a><span class="lineno"> 286</span>  <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>();</div>
<div class="line"><a name="l00287"></a><span class="lineno"> 287</span> </div>
<div class="line"><a name="l00288"></a><span class="lineno"> 288</span>  <span class="comment">//:ALEX:</span></div>
<div class="line"><a name="l00289"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchSat.html#ad3267f576f114e049609a8c3c4f01118"> 289</a></span>  <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) {</div>
<div class="line"><a name="l00290"></a><span class="lineno"> 290</span>  <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);</div>
<div class="line"><a name="l00291"></a><span class="lineno"> 291</span> </div>
<div class="line"><a name="l00292"></a><span class="lineno"> 292</span>  <span class="keywordflow">if</span> (l.<a class="code" href="classSAT_1_1Lit.html#ad5f6236c582c95356d720a7401623f36">isNull</a>()) {</div>
<div class="line"><a name="l00293"></a><span class="lineno"> 293</span>  <span class="comment">//:DEBUG:</span></div>
<div class="line"><a name="l00294"></a><span class="lineno"> 294</span>  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>;</div>
<div class="line"><a name="l00295"></a><span class="lineno"> 295</span>  <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>);</div>
<div class="line"><a name="l00296"></a><span class="lineno"> 296</span>  <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfadb6455bbcb14daca672dfcc52df342d7">UNKNOWN_VAL</a>;</div>
<div class="line"><a name="l00297"></a><span class="lineno"> 297</span>  } <span class="keywordflow">else</span> {</div>
<div class="line"><a name="l00298"></a><span class="lineno"> 298</span>  <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)) {</div>
<div class="line"><a name="l00299"></a><span class="lineno"> 299</span>  <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>;</div>
<div class="line"><a name="l00300"></a><span class="lineno"> 300</span>  <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>;</div>
<div class="line"><a name="l00301"></a><span class="lineno"> 301</span>  <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>;</div>
<div class="line"><a name="l00302"></a><span class="lineno"> 302</span>  <span class="keywordflow">default</span>:</div>
<div class="line"><a name="l00303"></a><span class="lineno"> 303</span>  <a class="code" href="debug_8h.html#a40dac3bdb2166ffc852ee8b1489d2b56">DebugAssert</a>(<span class="keyword">false</span>, <span class="stringliteral">"unreachable"</span>);</div>
<div class="line"><a name="l00304"></a><span class="lineno"> 304</span>  <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bfadb6455bbcb14daca672dfcc52df342d7">UNKNOWN_VAL</a>;</div>
<div class="line"><a name="l00305"></a><span class="lineno"> 305</span>  }</div>
<div class="line"><a name="l00306"></a><span class="lineno"> 306</span>  }</div>
<div class="line"><a name="l00307"></a><span class="lineno"> 307</span>  }</div>
<div class="line"><a name="l00308"></a><span class="lineno"> 308</span> </div>
<div class="line"><a name="l00309"></a><span class="lineno"> 309</span> };</div>
<div class="line"><a name="l00310"></a><span class="lineno"> 310</span> </div>
<div class="line"><a name="l00311"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#a9d5504b16aa74dbc6e57c5e928b4ed84"> 311</a></span> <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,</div>
<div class="line"><a name="l00312"></a><span class="lineno"> 312</span>  <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)</div>
<div class="line"><a name="l00313"></a><span class="lineno"> 313</span> {</div>
<div class="line"><a name="l00314"></a><span class="lineno"> 314</span>  <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>;</div>
<div class="line"><a name="l00315"></a><span class="lineno"> 315</span>  <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>;</div>
<div class="line"><a name="l00316"></a><span class="lineno"> 316</span>  <span class="keywordflow">return</span> <a class="code" href="namespaceCVC3.html#a1463331d2ef3e7d42ae05802d02271d7">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#a1463331d2ef3e7d42ae05802d02271d7">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>()) ||</div>
<div class="line"><a name="l00317"></a><span class="lineno"> 317</span>  (<a class="code" href="namespaceCVC3.html#a1463331d2ef3e7d42ae05802d02271d7">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#a1463331d2ef3e7d42ae05802d02271d7">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)));</div>
<div class="line"><a name="l00318"></a><span class="lineno"> 318</span> }</div>
<div class="line"><a name="l00319"></a><span class="lineno"> 319</span> </div>
<div class="line"><a name="l00320"></a><span class="lineno"> 320</span> }</div>
<div class="line"><a name="l00321"></a><span class="lineno"> 321</span> </div>
<div class="line"><a name="l00322"></a><span class="lineno"> 322</span> <span class="preprocessor">#endif</span></div>
</div><!-- fragment --></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:14 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
