<!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: Simple Search Engine</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><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
</div><!-- top -->
<div class="header">
<div class="summary">
<a href="#nested-classes">Classes</a> |
<a href="#func-members">Functions</a> |
<a href="#var-members">Variables</a> </div>
<div class="headertitle">
<div class="title">Simple Search Engine</div> </div>
<div class="ingroups"><a class="el" href="group__SE.html">Search Engine</a></div></div><!--header-->
<div class="contents">
<div class="dynheader">
Collaboration diagram for Simple Search Engine:</div>
<div class="dyncontent">
<center><table><tr><td><img src="group__SE__Simple.gif" border="0" alt="" usemap="#group____SE____Simple"/>
<map name="group____SE____Simple" id="group____SE____Simple">
<area shape="rect" id="node2" href="group__SE.html" title="Search Engine" alt="" coords="5,5,112,32"/></map>
</td></tr></table></center>
</div>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="nested-classes"></a>
Classes</h2></td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">class  </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1SearchSimple.html">CVC3::SearchSimple</a></td></tr>
<tr class="memdesc:"><td class="mdescLeft"> </td><td class="mdescRight">Implementation of the simple search engine. <a href="classCVC3_1_1SearchSimple.html#details">More...</a><br/></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="func-members"></a>
Functions</h2></td></tr>
<tr class="memitem:ga419ec575e6d5efc40222b50ee9448bae"><td class="memItemLeft" align="right" valign="top"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE__Simple.html#ga419ec575e6d5efc40222b50ee9448bae">CVC3::SearchSimple::checkValidRec</a> (<a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)</td></tr>
<tr class="memdesc:ga419ec575e6d5efc40222b50ee9448bae"><td class="mdescLeft"> </td><td class="mdescRight">Recursive DPLL algorithm used by checkValid. <a href="#ga419ec575e6d5efc40222b50ee9448bae"></a><br/></td></tr>
<tr class="separator:ga419ec575e6d5efc40222b50ee9448bae"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga8f4845fe98fd0da613062d118335192a"><td class="memItemLeft" align="right" valign="top"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE__Simple.html#ga8f4845fe98fd0da613062d118335192a">CVC3::SearchSimple::checkValidMain</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e2)</td></tr>
<tr class="memdesc:ga8f4845fe98fd0da613062d118335192a"><td class="mdescLeft"> </td><td class="mdescRight">Private helper function for checkValid and restart. <a href="#ga8f4845fe98fd0da613062d118335192a"></a><br/></td></tr>
<tr class="separator:ga8f4845fe98fd0da613062d118335192a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gad315bc80781ed5344d2803a28587b504"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE__Simple.html#gad315bc80781ed5344d2803a28587b504">CVC3::SearchSimple::SearchSimple</a> (<a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> *core)</td></tr>
<tr class="memdesc:gad315bc80781ed5344d2803a28587b504"><td class="mdescLeft"> </td><td class="mdescRight">Constructor. <a href="#gad315bc80781ed5344d2803a28587b504"></a><br/></td></tr>
<tr class="separator:gad315bc80781ed5344d2803a28587b504"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaf145d5394c5d9a598ea05e40628e6807"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE__Simple.html#gaf145d5394c5d9a598ea05e40628e6807">CVC3::SearchSimple::~SearchSimple</a> ()</td></tr>
<tr class="memdesc:gaf145d5394c5d9a598ea05e40628e6807"><td class="mdescLeft"> </td><td class="mdescRight">Destructor. <a href="#gaf145d5394c5d9a598ea05e40628e6807"></a><br/></td></tr>
<tr class="separator:gaf145d5394c5d9a598ea05e40628e6807"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga3785ec3f6b938d4a60efac0948587d57"><td class="memItemLeft" align="right" valign="top">const std::string & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE__Simple.html#ga3785ec3f6b938d4a60efac0948587d57">CVC3::SearchSimple::getName</a> ()</td></tr>
<tr class="memdesc:ga3785ec3f6b938d4a60efac0948587d57"><td class="mdescLeft"> </td><td class="mdescRight">Name of this search engine. <a href="#ga3785ec3f6b938d4a60efac0948587d57"></a><br/></td></tr>
<tr class="separator:ga3785ec3f6b938d4a60efac0948587d57"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga7a84d46236fb724f3057702c1fb9e073"><td class="memItemLeft" align="right" valign="top"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE__Simple.html#ga7a84d46236fb724f3057702c1fb9e073">CVC3::SearchSimple::checkValidInternal</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:ga7a84d46236fb724f3057702c1fb9e073"><td class="mdescLeft"> </td><td class="mdescRight">Checks the validity of a formula in the current context. <a href="#ga7a84d46236fb724f3057702c1fb9e073"></a><br/></td></tr>
<tr class="separator:ga7a84d46236fb724f3057702c1fb9e073"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga29f819e266d4821ae874f69da080247c"><td class="memItemLeft" align="right" valign="top"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE__Simple.html#ga29f819e266d4821ae874f69da080247c">CVC3::SearchSimple::restartInternal</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:ga29f819e266d4821ae874f69da080247c"><td class="mdescLeft"> </td><td class="mdescRight">Reruns last check with e as an additional assumption. <a href="#ga29f819e266d4821ae874f69da080247c"></a><br/></td></tr>
<tr class="separator:ga29f819e266d4821ae874f69da080247c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gab6bfda32dfb4b7d9176ace21c7ca404e"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE__Simple.html#gab6bfda32dfb4b7d9176ace21c7ca404e">CVC3::SearchSimple::addLiteralFact</a> (const Theorem &thm)</td></tr>
<tr class="memdesc:gab6bfda32dfb4b7d9176ace21c7ca404e"><td class="mdescLeft"> </td><td class="mdescRight">Notify the search engine about a new literal fact. <a href="#gab6bfda32dfb4b7d9176ace21c7ca404e"></a><br/></td></tr>
<tr class="separator:gab6bfda32dfb4b7d9176ace21c7ca404e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gadf91beae0add624c57c6481ab23147f8"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE__Simple.html#gadf91beae0add624c57c6481ab23147f8">CVC3::SearchSimple::addNonLiteralFact</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)</td></tr>
<tr class="memdesc:gadf91beae0add624c57c6481ab23147f8"><td class="mdescLeft"> </td><td class="mdescRight">Notify the search engine about a new non-literal fact. <a href="#gadf91beae0add624c57c6481ab23147f8"></a><br/></td></tr>
<tr class="separator:gadf91beae0add624c57c6481ab23147f8"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="var-members"></a>
Variables</h2></td></tr>
<tr class="memitem:ga387b080605ddbd0b7a124ff3fe44d645"><td class="memItemLeft" align="right" valign="top">std::string </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE__Simple.html#ga387b080605ddbd0b7a124ff3fe44d645">CVC3::SearchSimple::d_name</a></td></tr>
<tr class="memdesc:ga387b080605ddbd0b7a124ff3fe44d645"><td class="mdescLeft"> </td><td class="mdescRight">Name. <a href="#ga387b080605ddbd0b7a124ff3fe44d645"></a><br/></td></tr>
<tr class="separator:ga387b080605ddbd0b7a124ff3fe44d645"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga2768cc5c1cd7cc3ddad85c58a12be346"><td class="memItemLeft" align="right" valign="top">DecisionEngine * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE__Simple.html#ga2768cc5c1cd7cc3ddad85c58a12be346">CVC3::SearchSimple::d_decisionEngine</a></td></tr>
<tr class="memdesc:ga2768cc5c1cd7cc3ddad85c58a12be346"><td class="mdescLeft"> </td><td class="mdescRight">Decision Engine. <a href="#ga2768cc5c1cd7cc3ddad85c58a12be346"></a><br/></td></tr>
<tr class="separator:ga2768cc5c1cd7cc3ddad85c58a12be346"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gac6fb434835121c59d9ddfb6292ba1748"><td class="memItemLeft" align="right" valign="top">CDO< Theorem > </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE__Simple.html#gac6fb434835121c59d9ddfb6292ba1748">CVC3::SearchSimple::d_goal</a></td></tr>
<tr class="memdesc:gac6fb434835121c59d9ddfb6292ba1748"><td class="mdescLeft"> </td><td class="mdescRight">Formula being checked. <a href="#gac6fb434835121c59d9ddfb6292ba1748"></a><br/></td></tr>
<tr class="separator:gac6fb434835121c59d9ddfb6292ba1748"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga5993bff58130ad6cf24be03068caafc0"><td class="memItemLeft" align="right" valign="top">CDO< Theorem > </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE__Simple.html#ga5993bff58130ad6cf24be03068caafc0">CVC3::SearchSimple::d_nonLiterals</a></td></tr>
<tr class="memdesc:ga5993bff58130ad6cf24be03068caafc0"><td class="mdescLeft"> </td><td class="mdescRight">Non-literals generated by DP's. <a href="#ga5993bff58130ad6cf24be03068caafc0"></a><br/></td></tr>
<tr class="separator:ga5993bff58130ad6cf24be03068caafc0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gacb55ccfffc8ddac8c90c3f77e24867ec"><td class="memItemLeft" align="right" valign="top">CDO< Theorem > </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE__Simple.html#gacb55ccfffc8ddac8c90c3f77e24867ec">CVC3::SearchSimple::d_simplifiedThm</a></td></tr>
<tr class="memdesc:gacb55ccfffc8ddac8c90c3f77e24867ec"><td class="mdescLeft"> </td><td class="mdescRight"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> which records simplification of the last query. <a href="#gacb55ccfffc8ddac8c90c3f77e24867ec"></a><br/></td></tr>
<tr class="separator:gacb55ccfffc8ddac8c90c3f77e24867ec"><td class="memSeparator" colspan="2"> </td></tr>
</table>
<a name="details" id="details"></a><h2 class="groupheader">Detailed Description</h2>
<p>This module includes all the components of a very simplistic search engine. It is used mainly for debugging purposes. </p>
<h2 class="groupheader">Function Documentation</h2>
<a class="anchor" id="ga419ec575e6d5efc40222b50ee9448bae"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> SearchSimple::checkValidRec </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Recursive DPLL algorithm used by checkValid. </p>
<p>Definition at line <a class="el" href="search__simple_8cpp_source.html#l00037">37</a> of file <a class="el" href="search__simple_8cpp_source.html">search_simple.cpp</a>.</p>
<p>References <a class="el" href="queryresult_8h_source.html#l00037">CVC3::ABORT</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="expr_8h_source.html#l01232">CVC3::Expr::hasFind()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="expr_8h_source.html#l01223">CVC3::Expr::isNull()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>, <a class="el" href="xchaff__solver_8h_source.html#l00055">SATISFIABLE</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>, and <a class="el" href="xchaff__solver_8h_source.html#l00054">UNSATISFIABLE</a>.</p>
<p>Referenced by <a class="el" href="search__simple_8cpp_source.html#l00126">CVC3::SearchSimple::checkValidMain()</a>.</p>
</div>
</div>
<a class="anchor" id="ga8f4845fe98fd0da613062d118335192a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> SearchSimple::checkValidMain </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e2</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Private helper function for checkValid and restart. </p>
<p>Definition at line <a class="el" href="search__simple_8cpp_source.html#l00126">126</a> of file <a class="el" href="search__simple_8cpp_source.html">search_simple.cpp</a>.</p>
<p>References <a class="el" href="search__simple_8cpp_source.html#l00037">CVC3::SearchSimple::checkValidRec()</a>, <a class="el" href="expr__map_8h_source.html#l00310">CVC3::ExprHashMap< Data >::clear()</a>, <a class="el" href="search_8h_source.html#l00061">CVC3::SearchEngine::d_commonRules</a>, <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="search__simple_8h_source.html#l00053">CVC3::SearchSimple::d_goal</a>, <a class="el" href="search__impl__base_8h_source.html#l00081">CVC3::SearchImplBase::d_lastCounterExample</a>, <a class="el" href="search__impl__base_8h_source.html#l00078">CVC3::SearchImplBase::d_lastValid</a>, <a class="el" href="search__simple_8h_source.html#l00057">CVC3::SearchSimple::d_simplifiedThm</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cdo_8h_source.html#l00064">CVC3::CDO< T >::get()</a>, <a class="el" href="theory__core_8h_source.html#l00348">CVC3::TheoryCore::getCM()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00274">CVC3::Theorem::getLeafAssumptions()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#af38f25446a561384c3de66392c4d3544">CVC3::CommonProofRules::iffContrapositive()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#aebbcd4a194e4fdca0bcd16143fb03a75">CVC3::CommonProofRules::iffMP()</a>, <a class="el" href="theory__core_8h_source.html#l00435">CVC3::TheoryCore::incomplete()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>, <a class="el" href="context_8h_source.html#l00402">CVC3::ContextManager::pop()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00317">CVC3::SearchImplBase::processResult()</a>, <a class="el" href="queryresult_8h_source.html#l00033">CVC3::SATISFIABLE</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a0a87e88508f49b73037e0024afa841bf">CVC3::CommonProofRules::symmetryRule()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>, <a class="el" href="queryresult_8h_source.html#l00038">CVC3::UNKNOWN</a>, and <a class="el" href="queryresult_8h_source.html#l00036">CVC3::UNSATISFIABLE</a>.</p>
<p>Referenced by <a class="el" href="search__simple_8cpp_source.html#l00165">CVC3::SearchSimple::checkValidInternal()</a>, and <a class="el" href="search__simple_8cpp_source.html#l00207">CVC3::SearchSimple::restartInternal()</a>.</p>
</div>
</div>
<a class="anchor" id="gad315bc80781ed5344d2803a28587b504"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">SearchSimple::SearchSimple </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> * </td>
<td class="paramname"><em>core</em></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Constructor. </p>
<p>Definition at line <a class="el" href="search__simple_8cpp_source.html#l00101">101</a> of file <a class="el" href="search__simple_8cpp_source.html">search_simple.cpp</a>.</p>
<p>References <a class="el" href="search_8h_source.html#l00061">CVC3::SearchEngine::d_commonRules</a>, <a class="el" href="search__simple_8h_source.html#l00050">CVC3::SearchSimple::d_decisionEngine</a>, <a class="el" href="search__simple_8h_source.html#l00053">CVC3::SearchSimple::d_goal</a>, <a class="el" href="search__simple_8h_source.html#l00055">CVC3::SearchSimple::d_nonLiterals</a>, <a class="el" href="cdo_8h_source.html#l00063">CVC3::CDO< T >::set()</a>, and <a class="el" href="classCVC3_1_1CommonProofRules.html#a6e93694c76f7b567487bc8cae674ae5d">CVC3::CommonProofRules::trueTheorem()</a>.</p>
</div>
</div>
<a class="anchor" id="gaf145d5394c5d9a598ea05e40628e6807"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">SearchSimple::~SearchSimple </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Destructor. </p>
<p>Definition at line <a class="el" href="search__simple_8cpp_source.html#l00120">120</a> of file <a class="el" href="search__simple_8cpp_source.html">search_simple.cpp</a>.</p>
<p>References <a class="el" href="search__simple_8h_source.html#l00050">CVC3::SearchSimple::d_decisionEngine</a>.</p>
</div>
</div>
<a class="anchor" id="ga3785ec3f6b938d4a60efac0948587d57"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const std::string& CVC3::SearchSimple::getName </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Name of this search engine. </p>
<p>Implements <a class="el" href="group__SE.html#ga942b3cc50f5ea9da1b3117ee23eff9c2">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__simple_8h_source.html#l00071">71</a> of file <a class="el" href="search__simple_8h_source.html">search_simple.h</a>.</p>
<p>References <a class="el" href="search__simple_8h_source.html#l00047">CVC3::SearchSimple::d_name</a>.</p>
</div>
</div>
<a class="anchor" id="ga7a84d46236fb724f3057702c1fb9e073"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> SearchSimple::checkValidInternal </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Checks the validity of a formula in the current context. </p>
<p>The method that actually calls the <a class="el" href="namespaceSAT.html">SAT</a> solver (implemented in a subclass). It should maintain d_assumptions (add all asserted splitters to it), and set d_lastValid and d_lastCounterExample appropriately before exiting. </p>
<p>Implements <a class="el" href="group__SE.html#ga1e6282534845cfe93f245d9983d58761">CVC3::SearchImplBase</a>.</p>
<p>Definition at line <a class="el" href="search__simple_8cpp_source.html#l00165">165</a> of file <a class="el" href="search__simple_8cpp_source.html">search_simple.cpp</a>.</p>
<p>References <a class="el" href="theory__core_8cpp_source.html#l03468">CVC3::TheoryCore::addFact()</a>, <a class="el" href="search__simple_8cpp_source.html#l00126">CVC3::SearchSimple::checkValidMain()</a>, <a class="el" href="cdmap_8h_source.html#l00172">CVC3::CDMap< Key, Data, HashFcn >::count()</a>, <a class="el" href="search__impl__base_8h_source.html#l00084">CVC3::SearchImplBase::d_assumptions</a>, <a class="el" href="search__impl__base_8h_source.html#l00049">CVC3::SearchImplBase::d_bottomScope</a>, <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="search__simple_8h_source.html#l00053">CVC3::SearchSimple::d_goal</a>, <a class="el" href="search__simple_8h_source.html#l00055">CVC3::SearchSimple::d_nonLiterals</a>, <a class="el" href="search__simple_8h_source.html#l00057">CVC3::SearchSimple::d_simplifiedThm</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cdo_8h_source.html#l00064">CVC3::CDO< T >::get()</a>, <a class="el" href="theory__core_8h_source.html#l00348">CVC3::TheoryCore::getCM()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theory__core_8h_source.html#l00352">CVC3::TheoryCore::getExprTrans()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr_8h_source.html#l00356">CVC3::Expr::isTrue()</a>, <a class="el" href="expr_8h_source.html#l00937">CVC3::Expr::negate()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00141">CVC3::SearchImplBase::newUserAssumption()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00079">CVC3::ExprTransform::preprocess()</a>, <a class="el" href="context_8h_source.html#l00401">CVC3::ContextManager::push()</a>, <a class="el" href="search__impl__base_8h_source.html#l00192">CVC3::SearchImplBase::scopeLevel()</a>, <a class="el" href="cdo_8h_source.html#l00063">CVC3::CDO< T >::set()</a>, <a class="el" href="type_8h_source.html#l00080">CVC3::Type::toString()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, and <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>.</p>
</div>
</div>
<a class="anchor" id="ga29f819e266d4821ae874f69da080247c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> SearchSimple::restartInternal </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Reruns last check with e as an additional assumption. </p>
<p>Implements <a class="el" href="group__SE.html#gaf89e6b914a2099b366258953fccb6277">CVC3::SearchImplBase</a>.</p>
<p>Definition at line <a class="el" href="search__simple_8cpp_source.html#l00207">207</a> of file <a class="el" href="search__simple_8cpp_source.html">search_simple.cpp</a>.</p>
<p>References <a class="el" href="theory__core_8cpp_source.html#l03468">CVC3::TheoryCore::addFact()</a>, <a class="el" href="search__simple_8cpp_source.html#l00126">CVC3::SearchSimple::checkValidMain()</a>, <a class="el" href="cdmap_8h_source.html#l00172">CVC3::CDMap< Key, Data, HashFcn >::count()</a>, <a class="el" href="search__impl__base_8h_source.html#l00084">CVC3::SearchImplBase::d_assumptions</a>, <a class="el" href="search__impl__base_8h_source.html#l00049">CVC3::SearchImplBase::d_bottomScope</a>, <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="search__simple_8h_source.html#l00057">CVC3::SearchSimple::d_simplifiedThm</a>, <a class="el" href="cdo_8h_source.html#l00064">CVC3::CDO< T >::get()</a>, <a class="el" href="theory__core_8h_source.html#l00348">CVC3::TheoryCore::getCM()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr_8h_source.html#l00937">CVC3::Expr::negate()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00141">CVC3::SearchImplBase::newUserAssumption()</a>, <a class="el" href="context_8h_source.html#l00403">CVC3::ContextManager::popto()</a>, <a class="el" href="type_8h_source.html#l00080">CVC3::Type::toString()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, and <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>.</p>
</div>
</div>
<a class="anchor" id="gab6bfda32dfb4b7d9176ace21c7ca404e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::SearchSimple::addLiteralFact </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Notify the search engine about a new literal fact. </p>
<p>It should be called by SearchEngine::addFact() only. Must be implemented by the subclasses of <a class="el" href="classCVC3_1_1SearchEngine.html" title="API to to a generic proof search engine.">SearchEngine</a>.</p>
<p>IMPORTANT: do not call <a class="el" href="group__SE.html#gac6e807418fb26dee354f7f934eb432ba" title="Add a new fact to the search engine from the core.">addFact()</a> from this function; use enqueueFact() or setInconsistent() instead. </p>
<p>Implements <a class="el" href="group__SE.html#gaed2d918b4d0eb14d99bf63882fe2df1a">CVC3::SearchImplBase</a>.</p>
<p>Definition at line <a class="el" href="search__simple_8h_source.html#l00074">74</a> of file <a class="el" href="search__simple_8h_source.html">search_simple.h</a>.</p>
</div>
</div>
<a class="anchor" id="gadf91beae0add624c57c6481ab23147f8"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void SearchSimple::addNonLiteralFact </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Notify the search engine about a new non-literal fact. </p>
<p>It should be called by SearchEngine::addFact() only. Must be implemented by the subclasses of <a class="el" href="classCVC3_1_1SearchEngine.html" title="API to to a generic proof search engine.">SearchEngine</a>.</p>
<p>IMPORTANT: do not call <a class="el" href="group__SE.html#gac6e807418fb26dee354f7f934eb432ba" title="Add a new fact to the search engine from the core.">addFact()</a> from this function; use enqueueFact() or setInconsistent() instead. </p>
<p>Implements <a class="el" href="group__SE.html#gae95c78de94900637db19e3b7dee5d7c3">CVC3::SearchImplBase</a>.</p>
<p>Definition at line <a class="el" href="search__simple_8cpp_source.html#l00237">237</a> of file <a class="el" href="search__simple_8cpp_source.html">search_simple.cpp</a>.</p>
<p>References <a class="el" href="classCVC3_1_1CommonProofRules.html#a4aa193bfeb969c96b63db39a70470015">CVC3::CommonProofRules::andIntro()</a>, <a class="el" href="search_8h_source.html#l00061">CVC3::SearchEngine::d_commonRules</a>, <a class="el" href="search__simple_8h_source.html#l00055">CVC3::SearchSimple::d_nonLiterals</a>, <a class="el" href="cdo_8h_source.html#l00064">CVC3::CDO< T >::get()</a>, and <a class="el" href="cdo_8h_source.html#l00063">CVC3::CDO< T >::set()</a>.</p>
</div>
</div>
<h2 class="groupheader">Variable Documentation</h2>
<a class="anchor" id="ga387b080605ddbd0b7a124ff3fe44d645"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::string CVC3::SearchSimple::d_name</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Name. </p>
<p>Definition at line <a class="el" href="search__simple_8h_source.html#l00047">47</a> of file <a class="el" href="search__simple_8h_source.html">search_simple.h</a>.</p>
<p>Referenced by <a class="el" href="search__simple_8h_source.html#l00071">CVC3::SearchSimple::getName()</a>.</p>
</div>
</div>
<a class="anchor" id="ga2768cc5c1cd7cc3ddad85c58a12be346"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">DecisionEngine* CVC3::SearchSimple::d_decisionEngine</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Decision Engine. </p>
<p>Definition at line <a class="el" href="search__simple_8h_source.html#l00050">50</a> of file <a class="el" href="search__simple_8h_source.html">search_simple.h</a>.</p>
<p>Referenced by <a class="el" href="search__simple_8cpp_source.html#l00101">CVC3::SearchSimple::SearchSimple()</a>, and <a class="el" href="search__simple_8cpp_source.html#l00120">CVC3::SearchSimple::~SearchSimple()</a>.</p>
</div>
</div>
<a class="anchor" id="gac6fb434835121c59d9ddfb6292ba1748"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CDO<Theorem> CVC3::SearchSimple::d_goal</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Formula being checked. </p>
<p>Definition at line <a class="el" href="search__simple_8h_source.html#l00053">53</a> of file <a class="el" href="search__simple_8h_source.html">search_simple.h</a>.</p>
<p>Referenced by <a class="el" href="search__simple_8cpp_source.html#l00165">CVC3::SearchSimple::checkValidInternal()</a>, <a class="el" href="search__simple_8cpp_source.html#l00126">CVC3::SearchSimple::checkValidMain()</a>, and <a class="el" href="search__simple_8cpp_source.html#l00101">CVC3::SearchSimple::SearchSimple()</a>.</p>
</div>
</div>
<a class="anchor" id="ga5993bff58130ad6cf24be03068caafc0"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CDO<Theorem> CVC3::SearchSimple::d_nonLiterals</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Non-literals generated by DP's. </p>
<p>Definition at line <a class="el" href="search__simple_8h_source.html#l00055">55</a> of file <a class="el" href="search__simple_8h_source.html">search_simple.h</a>.</p>
<p>Referenced by <a class="el" href="search__simple_8cpp_source.html#l00237">CVC3::SearchSimple::addNonLiteralFact()</a>, <a class="el" href="search__simple_8cpp_source.html#l00165">CVC3::SearchSimple::checkValidInternal()</a>, and <a class="el" href="search__simple_8cpp_source.html#l00101">CVC3::SearchSimple::SearchSimple()</a>.</p>
</div>
</div>
<a class="anchor" id="gacb55ccfffc8ddac8c90c3f77e24867ec"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CDO<Theorem> CVC3::SearchSimple::d_simplifiedThm</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> which records simplification of the last query. </p>
<p>Definition at line <a class="el" href="search__simple_8h_source.html#l00057">57</a> of file <a class="el" href="search__simple_8h_source.html">search_simple.h</a>.</p>
<p>Referenced by <a class="el" href="search__simple_8cpp_source.html#l00165">CVC3::SearchSimple::checkValidInternal()</a>, <a class="el" href="search__simple_8cpp_source.html#l00126">CVC3::SearchSimple::checkValidMain()</a>, and <a class="el" href="search__simple_8cpp_source.html#l00207">CVC3::SearchSimple::restartInternal()</a>.</p>
</div>
</div>
</div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:16 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>
