<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: Simple Search Engine</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
</div>
<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>
<div class="contents">
<h2><a name="nested-classes"></a>
Classes</h2>
<ul>
<li>class <a class="el" href="classCVC3_1_1SearchSimple.html">CVC3::SearchSimple</a>
<dl class="el"><dd class="mdescRight">Implementation of the simple search engine. <a href="classCVC3_1_1SearchSimple.html#details">More...</a><br/></dl></ul>
<h2><a name="func-members"></a>
Functions</h2>
<ul>
<li><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <a class="el" href="group__SE__Simple.html#ga419ec575e6d5efc40222b50ee9448bae">CVC3::SearchSimple::checkValidRec</a> (<a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<dl class="el"><dd class="mdescRight">Recursive DPLL algorithm used by checkValid. <a href="#ga419ec575e6d5efc40222b50ee9448bae"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <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)
<dl class="el"><dd class="mdescRight">Private helper function for checkValid and restart. <a href="#ga8f4845fe98fd0da613062d118335192a"></a><br/></dl><li><a class="el" href="group__SE__Simple.html#gad315bc80781ed5344d2803a28587b504">CVC3::SearchSimple::SearchSimple</a> (<a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> *core)
<dl class="el"><dd class="mdescRight">Constructor. <a href="#gad315bc80781ed5344d2803a28587b504"></a><br/></dl><li><a class="el" href="group__SE__Simple.html#gaf145d5394c5d9a598ea05e40628e6807">CVC3::SearchSimple::~SearchSimple</a> ()
<dl class="el"><dd class="mdescRight">Destructor. <a href="#gaf145d5394c5d9a598ea05e40628e6807"></a><br/></dl><li>const std::string & <a class="el" href="group__SE__Simple.html#ga3785ec3f6b938d4a60efac0948587d57">CVC3::SearchSimple::getName</a> ()
<dl class="el"><dd class="mdescRight">Name of this search engine. <a href="#ga3785ec3f6b938d4a60efac0948587d57"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <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)
<dl class="el"><dd class="mdescRight">Checks the validity of a formula in the current context. <a href="#ga7a84d46236fb724f3057702c1fb9e073"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> <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)
<dl class="el"><dd class="mdescRight">Reruns last check with e as an additional assumption. <a href="#ga29f819e266d4821ae874f69da080247c"></a><br/></dl><li>void <a class="el" href="group__SE__Simple.html#gab6bfda32dfb4b7d9176ace21c7ca404e">CVC3::SearchSimple::addLiteralFact</a> (const Theorem &thm)
<dl class="el"><dd class="mdescRight">Notify the search engine about a new literal fact. <a href="#gab6bfda32dfb4b7d9176ace21c7ca404e"></a><br/></dl><li>void <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)
<dl class="el"><dd class="mdescRight">Notify the search engine about a new non-literal fact. <a href="#gadf91beae0add624c57c6481ab23147f8"></a><br/></dl></ul>
<h2><a name="var-members"></a>
Variables</h2>
<ul>
<li>std::string <a class="el" href="group__SE__Simple.html#ga387b080605ddbd0b7a124ff3fe44d645">CVC3::SearchSimple::d_name</a>
<dl class="el"><dd class="mdescRight">Name. <a href="#ga387b080605ddbd0b7a124ff3fe44d645"></a><br/></dl><li>DecisionEngine * <a class="el" href="group__SE__Simple.html#ga2768cc5c1cd7cc3ddad85c58a12be346">CVC3::SearchSimple::d_decisionEngine</a>
<dl class="el"><dd class="mdescRight">Decision Engine. <a href="#ga2768cc5c1cd7cc3ddad85c58a12be346"></a><br/></dl><li>CDO< Theorem > <a class="el" href="group__SE__Simple.html#gac6fb434835121c59d9ddfb6292ba1748">CVC3::SearchSimple::d_goal</a>
<dl class="el"><dd class="mdescRight">Formula being checked. <a href="#gac6fb434835121c59d9ddfb6292ba1748"></a><br/></dl><li>CDO< Theorem > <a class="el" href="group__SE__Simple.html#ga5993bff58130ad6cf24be03068caafc0">CVC3::SearchSimple::d_nonLiterals</a>
<dl class="el"><dd class="mdescRight">Non-literals generated by DP's. <a href="#ga5993bff58130ad6cf24be03068caafc0"></a><br/></dl><li>CDO< Theorem > <a class="el" href="group__SE__Simple.html#gacb55ccfffc8ddac8c90c3f77e24867ec">CVC3::SearchSimple::d_simplifiedThm</a>
<dl class="el"><dd class="mdescRight"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> which records simplification of the last query. <a href="#gacb55ccfffc8ddac8c90c3f77e24867ec"></a><br/></dl></ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<p>This module includes all the components of a very simplistic search engine. It is used mainly for debugging purposes. </p>
<hr/><h2>Function Documentation</h2>
<a class="anchor" id="ga419ec575e6d5efc40222b50ee9448bae"></a><!-- doxytag: member="CVC3::SearchSimple::checkValidRec" ref="ga419ec575e6d5efc40222b50ee9448bae" args="(Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<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><code> [private]</code></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><!-- doxytag: member="CVC3::SearchSimple::checkValidMain" ref="ga8f4845fe98fd0da613062d118335192a" args="(const Expr &e2)" -->
<div class="memitem">
<div class="memproto">
<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><code> [private]</code></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><!-- doxytag: member="CVC3::SearchSimple::SearchSimple" ref="gad315bc80781ed5344d2803a28587b504" args="(TheoryCore *core)" -->
<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><!-- doxytag: member="CVC3::SearchSimple::~SearchSimple" ref="gaf145d5394c5d9a598ea05e40628e6807" args="()" -->
<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><!-- doxytag: member="CVC3::SearchSimple::getName" ref="ga3785ec3f6b938d4a60efac0948587d57" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const std::string& CVC3::SearchSimple::getName </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline, virtual]</code></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><!-- doxytag: member="CVC3::SearchSimple::checkValidInternal" ref="ga7a84d46236fb724f3057702c1fb9e073" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<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><code> [virtual]</code></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><!-- doxytag: member="CVC3::SearchSimple::restartInternal" ref="ga29f819e266d4821ae874f69da080247c" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<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><code> [virtual]</code></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><!-- doxytag: member="CVC3::SearchSimple::addLiteralFact" ref="gab6bfda32dfb4b7d9176ace21c7ca404e" args="(const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<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><code> [inline, virtual]</code></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><!-- doxytag: member="CVC3::SearchSimple::addNonLiteralFact" ref="gadf91beae0add624c57c6481ab23147f8" args="(const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<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><code> [virtual]</code></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>
<hr/><h2>Variable Documentation</h2>
<a class="anchor" id="ga387b080605ddbd0b7a124ff3fe44d645"></a><!-- doxytag: member="CVC3::SearchSimple::d_name" ref="ga387b080605ddbd0b7a124ff3fe44d645" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string <a class="el" href="group__SE__Simple.html#ga387b080605ddbd0b7a124ff3fe44d645">CVC3::SearchSimple::d_name</a><code> [private]</code></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><!-- doxytag: member="CVC3::SearchSimple::d_decisionEngine" ref="ga2768cc5c1cd7cc3ddad85c58a12be346" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">DecisionEngine* <a class="el" href="group__SE__Simple.html#ga2768cc5c1cd7cc3ddad85c58a12be346">CVC3::SearchSimple::d_decisionEngine</a><code> [private]</code></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><!-- doxytag: member="CVC3::SearchSimple::d_goal" ref="gac6fb434835121c59d9ddfb6292ba1748" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CDO<Theorem> <a class="el" href="group__SE__Simple.html#gac6fb434835121c59d9ddfb6292ba1748">CVC3::SearchSimple::d_goal</a><code> [private]</code></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><!-- doxytag: member="CVC3::SearchSimple::d_nonLiterals" ref="ga5993bff58130ad6cf24be03068caafc0" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CDO<Theorem> <a class="el" href="group__SE__Simple.html#ga5993bff58130ad6cf24be03068caafc0">CVC3::SearchSimple::d_nonLiterals</a><code> [private]</code></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><!-- doxytag: member="CVC3::SearchSimple::d_simplifiedThm" ref="gacb55ccfffc8ddac8c90c3f77e24867ec" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CDO<Theorem> <a class="el" href="group__SE__Simple.html#gacb55ccfffc8ddac8c90c3f77e24867ec">CVC3::SearchSimple::d_simplifiedThm</a><code> [private]</code></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>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
