<!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.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.h</div> </div>
</div><!--header-->
<div class="contents">
<a href="search_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.h</span></div>
<div class="line"><a name="l00004"></a><span class="lineno"> 4</span> <span class="comment"> * \brief Abstract API to the proof search 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, Vijay Ganesh (Clausal Normal Form Converter)</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: Fri Jan 17 13:35:03 2003</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_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_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 "<a class="code" href="queryresult_8h.html" title="enumerated type for result of queries">queryresult.h</a>"</span></div>
<div class="line"><a name="l00027"></a><span class="lineno"> 27</span> <span class="preprocessor">#include "<a class="code" href="cdo_8h.html">cdo.h</a>"</span></div>
<div class="line"><a name="l00028"></a><span class="lineno"> 28</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="l00029"></a><span class="lineno"> 29</span> </div>
<div class="line"><a name="l00030"></a><span class="lineno"> 30</span> <span class="keyword">namespace </span>CVC3 {</div>
<div class="line"><a name="l00031"></a><span class="lineno"> 31</span> </div>
<div class="line"><a name="l00032"></a><span class="lineno"> 32</span> <span class="keyword">class </span>SearchEngineRules;</div>
<div class="line"><a name="l00033"></a><span class="lineno"> 33</span> <span class="keyword">class </span>Theorem;</div>
<div class="line"><a name="l00034"></a><span class="lineno"> 34</span> <span class="keyword">class </span>Expr;</div>
<div class="line"><a name="l00035"></a><span class="lineno"> 35</span> <span class="keyword">class </span>Proof;</div>
<div class="line"><a name="l00036"></a><span class="lineno"> 36</span> <span class="keyword">class </span>TheoryCore;</div>
<div class="line"><a name="l00037"></a><span class="lineno"> 37</span> <span class="keyword">class </span>CommonProofRules;</div>
<div class="line"><a name="l00038"></a><span class="lineno"> 38</span> </div>
<div class="line"><a name="l00039"></a><span class="lineno"> 39</span> <span class="keyword">template</span><<span class="keyword">class</span> Data> <span class="keyword">class </span>ExprMap;</div>
<div class="line"><a name="l00040"></a><span class="lineno"> 40</span> <span class="comment"></span></div>
<div class="line"><a name="l00041"></a><span class="lineno"> 41</span> <span class="comment"> /*! \defgroup SE Search Engine</span></div>
<div class="line"><a name="l00042"></a><span class="lineno"> 42</span> <span class="comment"> * \ingroup VC</span></div>
<div class="line"><a name="l00043"></a><span class="lineno"> 43</span> <span class="comment"> * The search engine includes Boolean reasoning and coordinates with theory</span></div>
<div class="line"><a name="l00044"></a><span class="lineno"> 44</span> <span class="comment"> * reasoning. It consists of a generic abstract API (class SearchEngine) and</span></div>
<div class="line"><a name="l00045"></a><span class="lineno"> 45</span> <span class="comment"> * subclasses implementing concrete instances of search engines.</span></div>
<div class="line"><a name="l00046"></a><span class="lineno"> 46</span> <span class="comment"> */</span></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"> //! API to to a generic proof search engine</span></div>
<div class="line"><a name="l00049"></a><span class="lineno"> 49</span> <span class="comment"></span><span class="comment"> /*! \ingroup SE */</span></div>
<div class="line"><a name="l00050"></a><span class="lineno"><a class="code" href="classCVC3_1_1SearchEngine.html"> 50</a></span> <span class="keyword">class </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="l00051"></a><span class="lineno"> 51</span> </div>
<div class="line"><a name="l00052"></a><span class="lineno"> 52</span> <span class="keyword">protected</span>:<span class="comment"></span></div>
<div class="line"><a name="l00053"></a><span class="lineno"> 53</span> <span class="comment"> /*! \addtogroup SE</span></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"> */</span></div>
<div class="line"><a name="l00056"></a><span class="lineno"> 56</span> <span class="comment"></span></div>
<div class="line"><a name="l00057"></a><span class="lineno"> 57</span> <span class="comment"> //! Access to theory reasoning</span></div>
<div class="line"><a name="l00058"></a><span class="lineno"><a class="code" href="group__SE.html#ga3772c6af7eac91b9ed7fc278edf5ef90"> 58</a></span> <span class="comment"></span> <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>* <a class="code" href="group__SE.html#ga3772c6af7eac91b9ed7fc278edf5ef90" title="Access to theory reasoning.">d_core</a>;</div>
<div class="line"><a name="l00059"></a><span class="lineno"> 59</span> <span class="comment"></span></div>
<div class="line"><a name="l00060"></a><span class="lineno"> 60</span> <span class="comment"> //! Common proof rules</span></div>
<div class="line"><a name="l00061"></a><span class="lineno"><a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c"> 61</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1CommonProofRules.html">CommonProofRules</a>* <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>;</div>
<div class="line"><a name="l00062"></a><span class="lineno"> 62</span> <span class="comment"></span></div>
<div class="line"><a name="l00063"></a><span class="lineno"> 63</span> <span class="comment"> //! Proof rules for the search engine</span></div>
<div class="line"><a name="l00064"></a><span class="lineno"><a class="code" href="group__SE.html#ga879b68112123e2b4ae7175d85a03bfec"> 64</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1SearchEngineRules.html" title="API to the proof rules for the Search Engines.">SearchEngineRules</a>* <a class="code" href="group__SE.html#ga879b68112123e2b4ae7175d85a03bfec" title="Proof rules for the search engine.">d_rules</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"> //! Create the trusted component</span></div>
<div class="line"><a name="l00067"></a><span class="lineno"> 67</span> <span class="comment"></span><span class="comment"> /*! This function is defined in search_theorem_producer.cpp */</span></div>
<div class="line"><a name="l00068"></a><span class="lineno"> 68</span>  <a class="code" href="classCVC3_1_1SearchEngineRules.html" title="API to the proof rules for the Search Engines.">SearchEngineRules</a>* <a class="code" href="group__SE.html#ga11dd236b3ba4ca5faad7563dfe6f3d72" title="Create the trusted component.">createRules</a>();</div>
<div class="line"><a name="l00069"></a><span class="lineno"> 69</span>  <span class="comment">// hack for printing original assumptions in LFSC proofs by liana</span></div>
<div class="line"><a name="l00070"></a><span class="lineno"> 70</span>  <a class="code" href="classCVC3_1_1SearchEngineRules.html" title="API to the proof rules for the Search Engines.">SearchEngineRules</a>* <a class="code" href="group__SE.html#ga11dd236b3ba4ca5faad7563dfe6f3d72" title="Create the trusted component.">createRules</a>(<a class="code" href="classCVC3_1_1SearchEngine.html" title="API to to a generic proof search engine.">SearchEngine</a>* s_eng);</div>
<div class="line"><a name="l00071"></a><span class="lineno"> 71</span> </div>
<div class="line"><a name="l00072"></a><span class="lineno"> 72</span>  <span class="keyword">public</span>:</div>
<div class="line"><a name="l00073"></a><span class="lineno"> 73</span> <span class="comment"></span></div>
<div class="line"><a name="l00074"></a><span class="lineno"> 74</span> <span class="comment"> //! Constructor</span></div>
<div class="line"><a name="l00075"></a><span class="lineno"> 75</span> <span class="comment"></span> <a class="code" href="group__SE.html#ga2763859e03e0a91877d91e20a3d26a7a" title="Constructor.">SearchEngine</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);</div>
<div class="line"><a name="l00076"></a><span class="lineno"> 76</span> <span class="comment"></span></div>
<div class="line"><a name="l00077"></a><span class="lineno"> 77</span> <span class="comment"> //! Destructor</span></div>
<div class="line"><a name="l00078"></a><span class="lineno"> 78</span> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="group__SE.html#ga863ab87efd742b9a8f20b87774ab570f" title="Destructor.">~SearchEngine</a>();</div>
<div class="line"><a name="l00079"></a><span class="lineno"> 79</span> <span class="comment"></span></div>
<div class="line"><a name="l00080"></a><span class="lineno"> 80</span> <span class="comment"> //! Name of this search engine</span></div>
<div class="line"><a name="l00081"></a><span class="lineno"> 81</span> <span class="comment"></span> <span class="keyword">virtual</span> <span class="keyword">const</span> std::string& <a class="code" href="group__SE.html#ga942b3cc50f5ea9da1b3117ee23eff9c2" title="Name of this search engine.">getName</a>() = 0;</div>
<div class="line"><a name="l00082"></a><span class="lineno"> 82</span> <span class="comment"></span></div>
<div class="line"><a name="l00083"></a><span class="lineno"> 83</span> <span class="comment"> //! Accessor for common rules</span></div>
<div class="line"><a name="l00084"></a><span class="lineno"><a class="code" href="group__SE.html#ga09d347bd55d59dc8f1d2f711df0d1c4c"> 84</a></span> <span class="comment"></span> <a class="code" href="classCVC3_1_1CommonProofRules.html">CommonProofRules</a>* <a class="code" href="group__SE.html#ga09d347bd55d59dc8f1d2f711df0d1c4c" title="Accessor for common rules.">getCommonRules</a>() { <span class="keywordflow">return</span> <a class="code" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c" title="Common proof rules.">d_commonRules</a>; }</div>
<div class="line"><a name="l00085"></a><span class="lineno"> 85</span> <span class="comment"></span></div>
<div class="line"><a name="l00086"></a><span class="lineno"> 86</span> <span class="comment"> //! Accessor for TheoryCore</span></div>
<div class="line"><a name="l00087"></a><span class="lineno"><a class="code" href="group__SE.html#ga895a3150e972fb79a7a3ab26100dd31e"> 87</a></span> <span class="comment"></span> <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>* <a class="code" href="group__SE.html#ga895a3150e972fb79a7a3ab26100dd31e" title="Accessor for TheoryCore.">theoryCore</a>() { <span class="keywordflow">return</span> <a class="code" href="group__SE.html#ga3772c6af7eac91b9ed7fc278edf5ef90" title="Access to theory reasoning.">d_core</a>; }</div>
<div class="line"><a name="l00088"></a><span class="lineno"> 88</span> <span class="comment"></span></div>
<div class="line"><a name="l00089"></a><span class="lineno"> 89</span> <span class="comment"> //! Register an atomic formula of interest.</span></div>
<div class="line"><a name="l00090"></a><span class="lineno"> 90</span> <span class="comment"></span><span class="comment"> /*! Registered atoms are tracked by the decision procedures. If one of them</span></div>
<div class="line"><a name="l00091"></a><span class="lineno"> 91</span> <span class="comment"> is deduced to be true or false, it is added to a list of implied literals.</span></div>
<div class="line"><a name="l00092"></a><span class="lineno"> 92</span> <span class="comment"> Implied literals can be retrieved with the getImpliedLiteral function */</span></div>
<div class="line"><a name="l00093"></a><span class="lineno"> 93</span>  <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#ga0f7c2870341319738e7d8c6662e6d7cc" 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) = 0;</div>
<div class="line"><a name="l00094"></a><span class="lineno"> 94</span> <span class="comment"></span></div>
<div class="line"><a name="l00095"></a><span class="lineno"> 95</span> <span class="comment"> //! Return next literal implied by last assertion. Null Expr if none.</span></div>
<div class="line"><a name="l00096"></a><span class="lineno"> 96</span> <span class="comment"></span><span class="comment"> /*! Returned literals are either registered atomic formulas or their negation</span></div>
<div class="line"><a name="l00097"></a><span class="lineno"> 97</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00098"></a><span class="lineno"> 98</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="group__SE.html#ga29a287b5dd638015f974a8a046e19d8a" title="Return next literal implied by last assertion. Null Expr if none.">getImpliedLiteral</a>() = 0;</div>
<div class="line"><a name="l00099"></a><span class="lineno"> 99</span> <span class="comment"></span></div>
<div class="line"><a name="l00100"></a><span class="lineno"> 100</span> <span class="comment"> //! Push a checkpoint</span></div>
<div class="line"><a name="l00101"></a><span class="lineno"> 101</span> <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#gadea197447ea40330f3b0739aa944c800" title="Push a checkpoint.">push</a>() = 0;</div>
<div class="line"><a name="l00102"></a><span class="lineno"> 102</span> <span class="comment"></span></div>
<div class="line"><a name="l00103"></a><span class="lineno"> 103</span> <span class="comment"> //! Restore last checkpoint</span></div>
<div class="line"><a name="l00104"></a><span class="lineno"> 104</span> <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#ga2c7fa9d3a42a543ff23891110ad673e5" title="Restore last checkpoint.">pop</a>() = 0;</div>
<div class="line"><a name="l00105"></a><span class="lineno"> 105</span> <span class="comment"></span></div>
<div class="line"><a name="l00106"></a><span class="lineno"> 106</span> <span class="comment"> //! Checks the validity of a formula in the current context</span></div>
<div class="line"><a name="l00107"></a><span class="lineno"> 107</span> <span class="comment"></span><span class="comment"> /*! If the query is valid, it returns VALID, the result parameter contains</span></div>
<div class="line"><a name="l00108"></a><span class="lineno"> 108</span> <span class="comment"> * the corresponding theorem, and the scope and context are the same</span></div>
<div class="line"><a name="l00109"></a><span class="lineno"> 109</span> <span class="comment"> * as when called. If it returns INVALID, the context will be one which</span></div>
<div class="line"><a name="l00110"></a><span class="lineno"> 110</span> <span class="comment"> * falsifies the query. If it returns UNKNOWN, the context will falsify the</span></div>
<div class="line"><a name="l00111"></a><span class="lineno"> 111</span> <span class="comment"> * query, but the context may be inconsistent. Finally, if it returns</span></div>
<div class="line"><a name="l00112"></a><span class="lineno"> 112</span> <span class="comment"> * ABORT, the context will be one which satisfies as much as</span></div>
<div class="line"><a name="l00113"></a><span class="lineno"> 113</span> <span class="comment"> * possible.</span></div>
<div class="line"><a name="l00114"></a><span class="lineno"> 114</span> <span class="comment"> * \param e the formula to check.</span></div>
<div class="line"><a name="l00115"></a><span class="lineno"> 115</span> <span class="comment"> * \param result the resulting theorem, if the formula is valid.</span></div>
<div class="line"><a name="l00116"></a><span class="lineno"> 116</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00117"></a><span class="lineno"> 117</span>  <span class="keyword">virtual</span> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="group__SE.html#ga34a9133f5342719526863d24cd1a0fcc" 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) = 0;</div>
<div class="line"><a name="l00118"></a><span class="lineno"> 118</span> <span class="comment"></span></div>
<div class="line"><a name="l00119"></a><span class="lineno"> 119</span> <span class="comment"> //! Reruns last check with e as an additional assumption</span></div>
<div class="line"><a name="l00120"></a><span class="lineno"> 120</span> <span class="comment"></span><span class="comment"> /*! This method should only be called after a query which is invalid.</span></div>
<div class="line"><a name="l00121"></a><span class="lineno"> 121</span> <span class="comment"> * \param e the additional assumption</span></div>
<div class="line"><a name="l00122"></a><span class="lineno"> 122</span> <span class="comment"> * \param result the resulting theorem, if the query is valid.</span></div>
<div class="line"><a name="l00123"></a><span class="lineno"> 123</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00124"></a><span class="lineno"> 124</span>  <span class="keyword">virtual</span> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="code" href="group__SE.html#ga715936653b5bef3e3d9fd2a8a873bafd" 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) = 0;</div>
<div class="line"><a name="l00125"></a><span class="lineno"> 125</span> <span class="comment"></span></div>
<div class="line"><a name="l00126"></a><span class="lineno"> 126</span> <span class="comment"> //! Returns to context immediately before last call to checkValid</span></div>
<div class="line"><a name="l00127"></a><span class="lineno"> 127</span> <span class="comment"></span><span class="comment"> /*! This method should only be called after a query which returns something</span></div>
<div class="line"><a name="l00128"></a><span class="lineno"> 128</span> <span class="comment"> * other than VALID.</span></div>
<div class="line"><a name="l00129"></a><span class="lineno"> 129</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00130"></a><span class="lineno"> 130</span>  <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#gad552593fb43fd5751f12942f3a29a90e" title="Returns to context immediately before last call to checkValid.">returnFromCheck</a>() = 0;</div>
<div class="line"><a name="l00131"></a><span class="lineno"> 131</span> <span class="comment"></span></div>
<div class="line"><a name="l00132"></a><span class="lineno"> 132</span> <span class="comment"> //! Returns the result of the most recent valid theorem</span></div>
<div class="line"><a name="l00133"></a><span class="lineno"> 133</span> <span class="comment"></span><span class="comment"> /*! Returns Null Theorem if last call was not valid */</span></div>
<div class="line"><a name="l00134"></a><span class="lineno"> 134</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="group__SE.html#ga9757a6fd272ea550d0e910d20bd7d00b" title="Returns the result of the most recent valid theorem.">lastThm</a>() = 0;</div>
<div class="line"><a name="l00135"></a><span class="lineno"> 135</span> <span class="comment"></span></div>
<div class="line"><a name="l00136"></a><span class="lineno"> 136</span> <span class="comment"> /*! @brief Generate and add an assumption to the set of</span></div>
<div class="line"><a name="l00137"></a><span class="lineno"> 137</span> <span class="comment"> * assumptions in the current context. */</span><span class="comment"></span></div>
<div class="line"><a name="l00138"></a><span class="lineno"> 138</span> <span class="comment"> /*! By default, the assumption is added at the current scope. The default</span></div>
<div class="line"><a name="l00139"></a><span class="lineno"> 139</span> <span class="comment"> * can be overridden by specifying the scope parameter. */</span></div>
<div class="line"><a name="l00140"></a><span class="lineno"> 140</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="group__SE.html#ga5782663fc8ae00ec2965506c8ba65a86" 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) = 0;</div>
<div class="line"><a name="l00141"></a><span class="lineno"> 141</span> <span class="comment"></span></div>
<div class="line"><a name="l00142"></a><span class="lineno"> 142</span> <span class="comment"> //! Get all user assumptions made in this and all previous contexts.</span></div>
<div class="line"><a name="l00143"></a><span class="lineno"> 143</span> <span class="comment"></span><span class="comment"> /*! User assumptions are created either by calls to newUserAssumption or</span></div>
<div class="line"><a name="l00144"></a><span class="lineno"> 144</span> <span class="comment"> * a call to checkValid. In the latter case, the negated query is added</span></div>
<div class="line"><a name="l00145"></a><span class="lineno"> 145</span> <span class="comment"> * as an assumption.</span></div>
<div class="line"><a name="l00146"></a><span class="lineno"> 146</span> <span class="comment"> * \param assumptions should be empty on entry.</span></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="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#ga43f52699cddc6e0feffffaf22424fe47" title="Get all user assumptions made in this and all previous contexts.">getUserAssumptions</a>(std::vector<Expr>& assumptions) = 0;</div>
<div class="line"><a name="l00149"></a><span class="lineno"> 149</span> <span class="comment"></span></div>
<div class="line"><a name="l00150"></a><span class="lineno"> 150</span> <span class="comment"> //! Get assumptions made internally in this and all previous contexts.</span></div>
<div class="line"><a name="l00151"></a><span class="lineno"> 151</span> <span class="comment"></span><span class="comment"> /*! Internal assumptions are literals assumed by the sat solver.</span></div>
<div class="line"><a name="l00152"></a><span class="lineno"> 152</span> <span class="comment"> * \param assumptions should be empty on entry.</span></div>
<div class="line"><a name="l00153"></a><span class="lineno"> 153</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00154"></a><span class="lineno"> 154</span>  <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#ga320e15a994a712bc7c20854853501b27" title="Get assumptions made internally in this and all previous contexts.">getInternalAssumptions</a>(std::vector<Expr>& assumptions) = 0;</div>
<div class="line"><a name="l00155"></a><span class="lineno"> 155</span> <span class="comment"></span></div>
<div class="line"><a name="l00156"></a><span class="lineno"> 156</span> <span class="comment"> //! Get all assumptions made in this and all previous contexts.</span></div>
<div class="line"><a name="l00157"></a><span class="lineno"> 157</span> <span class="comment"></span><span class="comment"> /*! \param assumptions should be an empty vector which will be filled \</span></div>
<div class="line"><a name="l00158"></a><span class="lineno"> 158</span> <span class="comment"> with the assumptions */</span></div>
<div class="line"><a name="l00159"></a><span class="lineno"> 159</span>  <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#ga3167148206cca25a3434cb8bb15c69fe" title="Get all assumptions made in this and all previous contexts.">getAssumptions</a>(std::vector<Expr>& assumptions) = 0;</div>
<div class="line"><a name="l00160"></a><span class="lineno"> 160</span> <span class="comment"></span></div>
<div class="line"><a name="l00161"></a><span class="lineno"> 161</span> <span class="comment"> //! Check if the formula has already been assumed previously</span></div>
<div class="line"><a name="l00162"></a><span class="lineno"> 162</span> <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">bool</span> <a class="code" href="group__SE.html#ga20730f5acacc4b18d29031632d88904c" 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) = 0;</div>
<div class="line"><a name="l00163"></a><span class="lineno"> 163</span> <span class="comment"></span></div>
<div class="line"><a name="l00164"></a><span class="lineno"> 164</span> <span class="comment"> //! Will return the set of assertions which make the queried formula false.</span></div>
<div class="line"><a name="l00165"></a><span class="lineno"> 165</span> <span class="comment"></span><span class="comment"> /*! This method should only be called after an query which returns INVALID.</span></div>
<div class="line"><a name="l00166"></a><span class="lineno"> 166</span> <span class="comment"> * It will try to return the simplest possible set of assertions which are</span></div>
<div class="line"><a name="l00167"></a><span class="lineno"> 167</span> <span class="comment"> * sufficient to make the queried expression false.</span></div>
<div class="line"><a name="l00168"></a><span class="lineno"> 168</span> <span class="comment"> * \param assertions should be empty on entry.</span></div>
<div class="line"><a name="l00169"></a><span class="lineno"> 169</span> <span class="comment"> * \param inOrder if true, returns the assertions in the order they were</span></div>
<div class="line"><a name="l00170"></a><span class="lineno"> 170</span> <span class="comment"> * asserted. This is slightly more expensive than inOrder = false.</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="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="group__SE.html#ga739867521b23967ee6739ec32a8070e2" 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="l00173"></a><span class="lineno"> 173</span>  <span class="keywordtype">bool</span> inOrder = <span class="keyword">true</span>) = 0;</div>
<div class="line"><a name="l00174"></a><span class="lineno"> 174</span> <span class="comment"></span></div>
<div class="line"><a name="l00175"></a><span class="lineno"> 175</span> <span class="comment"> //! Returns the proof term for the last proven query</span></div>
<div class="line"><a name="l00176"></a><span class="lineno"> 176</span> <span class="comment"></span><span class="comment"> /*! It should be called only after a query which returns VALID.</span></div>
<div class="line"><a name="l00177"></a><span class="lineno"> 177</span> <span class="comment"> * In any other case, it returns Null. */</span></div>
<div class="line"><a name="l00178"></a><span class="lineno"> 178</span>  <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Proof.html">Proof</a> <a class="code" href="group__SE.html#gaa0ce3839d5f7b64168d62ff5eb59cf1f" title="Returns the proof term for the last proven query.">getProof</a>() = 0;</div>
<div class="line"><a name="l00179"></a><span class="lineno"> 179</span> <span class="comment"></span></div>
<div class="line"><a name="l00180"></a><span class="lineno"> 180</span> <span class="comment"> /*! @brief Build a concrete Model (assign values to variables),</span></div>
<div class="line"><a name="l00181"></a><span class="lineno"> 181</span> <span class="comment"> * should only be called after a query which returns INVALID. */</span></div>
<div class="line"><a name="l00182"></a><span class="lineno"> 182</span>  <span class="keywordtype">void</span> <a class="code" href="group__SE.html#gae2a1cd46200160ac5855d7cd5f65517c" title="Build a concrete Model (assign values to variables), should only be called after a query which return...">getConcreteModel</a>(<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a>& m);</div>
<div class="line"><a name="l00183"></a><span class="lineno"> 183</span> <span class="comment"></span></div>
<div class="line"><a name="l00184"></a><span class="lineno"> 184</span> <span class="comment"> /*! @brief Try to build a concrete Model (assign values to variables),</span></div>
<div class="line"><a name="l00185"></a><span class="lineno"> 185</span> <span class="comment"> * should only be called after a query which returns UNKNOWN.</span></div>
<div class="line"><a name="l00186"></a><span class="lineno"> 186</span> <span class="comment"> * Returns a theorem if inconsistent */</span></div>
<div class="line"><a name="l00187"></a><span class="lineno"> 187</span>  <span class="keywordtype">bool</span> <a class="code" href="group__SE.html#ga44f1c2fefc202249cd2cda55d7712bdf" title="Try to build a concrete Model (assign values to variables), should only be called after a query which...">tryModelGeneration</a>(<a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm);</div>
<div class="line"><a name="l00188"></a><span class="lineno"> 188</span> </div>
<div class="line"><a name="l00189"></a><span class="lineno"> 189</span>  <span class="comment">//:ALEX: returns the current truth value of a formula</span></div>
<div class="line"><a name="l00190"></a><span class="lineno"> 190</span>  <span class="comment">// returns CVC3::UNKNOWN_VAL if e is not associated</span></div>
<div class="line"><a name="l00191"></a><span class="lineno"> 191</span>  <span class="comment">// with a boolean variable in the SAT module,</span></div>
<div class="line"><a name="l00192"></a><span class="lineno"> 192</span>  <span class="comment">// i.e. if its value can not determined without search.</span></div>
<div class="line"><a name="l00193"></a><span class="lineno"> 193</span>  <span class="keyword">virtual</span> <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bf">FormulaValue</a> <a class="code" href="group__SE.html#ga38ced857c272afeecbe0429e1dcca28e">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) = 0;</div>
<div class="line"><a name="l00194"></a><span class="lineno"> 194</span> </div>
<div class="line"><a name="l00195"></a><span class="lineno"> 195</span>  <span class="comment">/* @} */</span> <span class="comment">// end of group SE</span></div>
<div class="line"><a name="l00196"></a><span class="lineno"> 196</span> </div>
<div class="line"><a name="l00197"></a><span class="lineno"> 197</span> };</div>
<div class="line"><a name="l00198"></a><span class="lineno"> 198</span> </div>
<div class="line"><a name="l00199"></a><span class="lineno"> 199</span> </div>
<div class="line"><a name="l00200"></a><span class="lineno"> 200</span> }</div>
<div class="line"><a name="l00201"></a><span class="lineno"> 201</span> </div>
<div class="line"><a name="l00202"></a><span class="lineno"> 202</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>
