<!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 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="#groups">Modules</a> |
<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">Search Engine</div> </div>
<div class="ingroups"><a class="el" href="group__VC.html">Validity Checker</a></div></div><!--header-->
<div class="contents">
<div class="dynheader">
Collaboration diagram for Search Engine:</div>
<div class="dyncontent">
<center><table><tr><td><img src="group__SE.gif" border="0" alt="" usemap="#group____SE"/>
<map name="group____SE" id="group____SE">
<area shape="rect" id="node1" href="group__DE.html" title="Decision Engine, used by Search Engine." alt="" coords="345,107,463,133"/><area shape="rect" id="node2" href="group__SE__Simple.html" title="Simple Search Engine" alt="" coords="329,56,479,83"/><area shape="rect" id="node3" href="group__SE__Fast.html" title="Fast Search Engine" alt="" coords="335,5,473,32"/><area shape="rect" id="node4" href="group__SE__Rules.html" title="Proof Rules for the\l Search Engines" alt="" coords="338,158,470,199"/><area shape="rect" id="node6" href="group__VC.html" title="The modules that make up the validity checker." alt="" coords="6,81,125,108"/></map>
</td></tr></table></center>
</div>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="groups"></a>
Modules</h2></td></tr>
<tr class="memitem:group__SE__Fast"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE__Fast.html">Fast Search Engine</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:group__SE__Simple"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE__Simple.html">Simple Search Engine</a></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:group__DE"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__DE.html">Decision Engine</a></td></tr>
<tr class="memdesc:group__DE"><td class="mdescLeft"> </td><td class="mdescRight">Decision Engine, used by Search Engine. <br/></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:group__SE__Rules"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE__Rules.html">Proof Rules for the Search Engines</a></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="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_1SearchEngine.html">CVC3::SearchEngine</a></td></tr>
<tr class="memdesc:"><td class="mdescLeft"> </td><td class="mdescRight">API to to a generic proof search engine. <a href="classCVC3_1_1SearchEngine.html#details">More...</a><br/></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </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_1SearchImplBase.html">CVC3::SearchImplBase</a></td></tr>
<tr class="memdesc:"><td class="mdescLeft"> </td><td class="mdescRight">API to to a generic proof search engine (a.k.a. <a class="el" href="namespaceSAT.html">SAT</a> solver) <a href="classCVC3_1_1SearchImplBase.html#details">More...</a><br/></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </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_1SearchImplBase_1_1Splitter.html">CVC3::SearchImplBase::Splitter</a></td></tr>
<tr class="memdesc:"><td class="mdescLeft"> </td><td class="mdescRight">Representation of a DP-suggested splitter. <a href="classCVC3_1_1SearchImplBase_1_1Splitter.html#details">More...</a><br/></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </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_1SearchSat.html">CVC3::SearchSat</a></td></tr>
<tr class="memdesc:"><td class="mdescLeft"> </td><td class="mdescRight">Search engine that connects to a generic <a class="el" href="namespaceSAT.html">SAT</a> reasoning module. <a href="classCVC3_1_1SearchSat.html#details">More...</a><br/></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </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_1SearchSat_1_1LitPriorityPair.html">CVC3::SearchSat::LitPriorityPair</a></td></tr>
<tr class="memdesc:"><td class="mdescLeft"> </td><td class="mdescRight">Pair of Lit and priority of this Lit. <a href="classCVC3_1_1SearchSat_1_1LitPriorityPair.html#details">More...</a><br/></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </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_1SearchSat_1_1Restorer.html">CVC3::SearchSat::Restorer</a></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:ga11dd236b3ba4ca5faad7563dfe6f3d72"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1SearchEngineRules.html">SearchEngineRules</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga11dd236b3ba4ca5faad7563dfe6f3d72">CVC3::SearchEngine::createRules</a> ()</td></tr>
<tr class="memdesc:ga11dd236b3ba4ca5faad7563dfe6f3d72"><td class="mdescLeft"> </td><td class="mdescRight">Create the trusted component. <a href="#ga11dd236b3ba4ca5faad7563dfe6f3d72"></a><br/></td></tr>
<tr class="separator:ga11dd236b3ba4ca5faad7563dfe6f3d72"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga5ee040962725cff9a07cd33cbb6d6232"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1SearchEngineRules.html">SearchEngineRules</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga5ee040962725cff9a07cd33cbb6d6232">CVC3::SearchEngine::createRules</a> (<a class="el" href="classCVC3_1_1SearchEngine.html">SearchEngine</a> *s_eng)</td></tr>
<tr class="separator:ga5ee040962725cff9a07cd33cbb6d6232"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga2763859e03e0a91877d91e20a3d26a7a"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga2763859e03e0a91877d91e20a3d26a7a">CVC3::SearchEngine::SearchEngine</a> (<a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> *core)</td></tr>
<tr class="memdesc:ga2763859e03e0a91877d91e20a3d26a7a"><td class="mdescLeft"> </td><td class="mdescRight">Constructor. <a href="#ga2763859e03e0a91877d91e20a3d26a7a"></a><br/></td></tr>
<tr class="separator:ga2763859e03e0a91877d91e20a3d26a7a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga863ab87efd742b9a8f20b87774ab570f"><td class="memItemLeft" align="right" valign="top">virtual </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga863ab87efd742b9a8f20b87774ab570f">CVC3::SearchEngine::~SearchEngine</a> ()</td></tr>
<tr class="memdesc:ga863ab87efd742b9a8f20b87774ab570f"><td class="mdescLeft"> </td><td class="mdescRight">Destructor. <a href="#ga863ab87efd742b9a8f20b87774ab570f"></a><br/></td></tr>
<tr class="separator:ga863ab87efd742b9a8f20b87774ab570f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga942b3cc50f5ea9da1b3117ee23eff9c2"><td class="memItemLeft" align="right" valign="top">virtual const std::string & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga942b3cc50f5ea9da1b3117ee23eff9c2">CVC3::SearchEngine::getName</a> ()=0</td></tr>
<tr class="memdesc:ga942b3cc50f5ea9da1b3117ee23eff9c2"><td class="mdescLeft"> </td><td class="mdescRight">Name of this search engine. <a href="#ga942b3cc50f5ea9da1b3117ee23eff9c2"></a><br/></td></tr>
<tr class="separator:ga942b3cc50f5ea9da1b3117ee23eff9c2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga09d347bd55d59dc8f1d2f711df0d1c4c"><td class="memItemLeft" align="right" valign="top">CommonProofRules * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga09d347bd55d59dc8f1d2f711df0d1c4c">CVC3::SearchEngine::getCommonRules</a> ()</td></tr>
<tr class="memdesc:ga09d347bd55d59dc8f1d2f711df0d1c4c"><td class="mdescLeft"> </td><td class="mdescRight">Accessor for common rules. <a href="#ga09d347bd55d59dc8f1d2f711df0d1c4c"></a><br/></td></tr>
<tr class="separator:ga09d347bd55d59dc8f1d2f711df0d1c4c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga895a3150e972fb79a7a3ab26100dd31e"><td class="memItemLeft" align="right" valign="top">TheoryCore * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga895a3150e972fb79a7a3ab26100dd31e">CVC3::SearchEngine::theoryCore</a> ()</td></tr>
<tr class="memdesc:ga895a3150e972fb79a7a3ab26100dd31e"><td class="mdescLeft"> </td><td class="mdescRight">Accessor for <a class="el" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">TheoryCore</a>. <a href="#ga895a3150e972fb79a7a3ab26100dd31e"></a><br/></td></tr>
<tr class="separator:ga895a3150e972fb79a7a3ab26100dd31e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga0f7c2870341319738e7d8c6662e6d7cc"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga0f7c2870341319738e7d8c6662e6d7cc">CVC3::SearchEngine::registerAtom</a> (const Expr &e)=0</td></tr>
<tr class="memdesc:ga0f7c2870341319738e7d8c6662e6d7cc"><td class="mdescLeft"> </td><td class="mdescRight">Register an atomic formula of interest. <a href="#ga0f7c2870341319738e7d8c6662e6d7cc"></a><br/></td></tr>
<tr class="separator:ga0f7c2870341319738e7d8c6662e6d7cc"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga29a287b5dd638015f974a8a046e19d8a"><td class="memItemLeft" align="right" valign="top">virtual Theorem </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga29a287b5dd638015f974a8a046e19d8a">CVC3::SearchEngine::getImpliedLiteral</a> ()=0</td></tr>
<tr class="memdesc:ga29a287b5dd638015f974a8a046e19d8a"><td class="mdescLeft"> </td><td class="mdescRight">Return next literal implied by last assertion. Null <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> if none. <a href="#ga29a287b5dd638015f974a8a046e19d8a"></a><br/></td></tr>
<tr class="separator:ga29a287b5dd638015f974a8a046e19d8a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gadea197447ea40330f3b0739aa944c800"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gadea197447ea40330f3b0739aa944c800">CVC3::SearchEngine::push</a> ()=0</td></tr>
<tr class="memdesc:gadea197447ea40330f3b0739aa944c800"><td class="mdescLeft"> </td><td class="mdescRight">Push a checkpoint. <a href="#gadea197447ea40330f3b0739aa944c800"></a><br/></td></tr>
<tr class="separator:gadea197447ea40330f3b0739aa944c800"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga2c7fa9d3a42a543ff23891110ad673e5"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga2c7fa9d3a42a543ff23891110ad673e5">CVC3::SearchEngine::pop</a> ()=0</td></tr>
<tr class="memdesc:ga2c7fa9d3a42a543ff23891110ad673e5"><td class="mdescLeft"> </td><td class="mdescRight">Restore last checkpoint. <a href="#ga2c7fa9d3a42a543ff23891110ad673e5"></a><br/></td></tr>
<tr class="separator:ga2c7fa9d3a42a543ff23891110ad673e5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga34a9133f5342719526863d24cd1a0fcc"><td class="memItemLeft" align="right" valign="top">virtual QueryResult </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga34a9133f5342719526863d24cd1a0fcc">CVC3::SearchEngine::checkValid</a> (const Expr &e, Theorem &result)=0</td></tr>
<tr class="memdesc:ga34a9133f5342719526863d24cd1a0fcc"><td class="mdescLeft"> </td><td class="mdescRight">Checks the validity of a formula in the current context. <a href="#ga34a9133f5342719526863d24cd1a0fcc"></a><br/></td></tr>
<tr class="separator:ga34a9133f5342719526863d24cd1a0fcc"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga715936653b5bef3e3d9fd2a8a873bafd"><td class="memItemLeft" align="right" valign="top">virtual QueryResult </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga715936653b5bef3e3d9fd2a8a873bafd">CVC3::SearchEngine::restart</a> (const Expr &e, Theorem &result)=0</td></tr>
<tr class="memdesc:ga715936653b5bef3e3d9fd2a8a873bafd"><td class="mdescLeft"> </td><td class="mdescRight">Reruns last check with e as an additional assumption. <a href="#ga715936653b5bef3e3d9fd2a8a873bafd"></a><br/></td></tr>
<tr class="separator:ga715936653b5bef3e3d9fd2a8a873bafd"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gad552593fb43fd5751f12942f3a29a90e"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gad552593fb43fd5751f12942f3a29a90e">CVC3::SearchEngine::returnFromCheck</a> ()=0</td></tr>
<tr class="memdesc:gad552593fb43fd5751f12942f3a29a90e"><td class="mdescLeft"> </td><td class="mdescRight">Returns to context immediately before last call to checkValid. <a href="#gad552593fb43fd5751f12942f3a29a90e"></a><br/></td></tr>
<tr class="separator:gad552593fb43fd5751f12942f3a29a90e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga9757a6fd272ea550d0e910d20bd7d00b"><td class="memItemLeft" align="right" valign="top">virtual Theorem </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga9757a6fd272ea550d0e910d20bd7d00b">CVC3::SearchEngine::lastThm</a> ()=0</td></tr>
<tr class="memdesc:ga9757a6fd272ea550d0e910d20bd7d00b"><td class="mdescLeft"> </td><td class="mdescRight">Returns the result of the most recent valid theorem. <a href="#ga9757a6fd272ea550d0e910d20bd7d00b"></a><br/></td></tr>
<tr class="separator:ga9757a6fd272ea550d0e910d20bd7d00b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga5782663fc8ae00ec2965506c8ba65a86"><td class="memItemLeft" align="right" valign="top">virtual Theorem </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga5782663fc8ae00ec2965506c8ba65a86">CVC3::SearchEngine::newUserAssumption</a> (const Expr &e)=0</td></tr>
<tr class="memdesc:ga5782663fc8ae00ec2965506c8ba65a86"><td class="mdescLeft"> </td><td class="mdescRight">Generate and add an assumption to the set of assumptions in the current context. <a href="#ga5782663fc8ae00ec2965506c8ba65a86"></a><br/></td></tr>
<tr class="separator:ga5782663fc8ae00ec2965506c8ba65a86"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga43f52699cddc6e0feffffaf22424fe47"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga43f52699cddc6e0feffffaf22424fe47">CVC3::SearchEngine::getUserAssumptions</a> (std::vector< Expr > &assumptions)=0</td></tr>
<tr class="memdesc:ga43f52699cddc6e0feffffaf22424fe47"><td class="mdescLeft"> </td><td class="mdescRight">Get all user assumptions made in this and all previous contexts. <a href="#ga43f52699cddc6e0feffffaf22424fe47"></a><br/></td></tr>
<tr class="separator:ga43f52699cddc6e0feffffaf22424fe47"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga320e15a994a712bc7c20854853501b27"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga320e15a994a712bc7c20854853501b27">CVC3::SearchEngine::getInternalAssumptions</a> (std::vector< Expr > &assumptions)=0</td></tr>
<tr class="memdesc:ga320e15a994a712bc7c20854853501b27"><td class="mdescLeft"> </td><td class="mdescRight">Get assumptions made internally in this and all previous contexts. <a href="#ga320e15a994a712bc7c20854853501b27"></a><br/></td></tr>
<tr class="separator:ga320e15a994a712bc7c20854853501b27"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga3167148206cca25a3434cb8bb15c69fe"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga3167148206cca25a3434cb8bb15c69fe">CVC3::SearchEngine::getAssumptions</a> (std::vector< Expr > &assumptions)=0</td></tr>
<tr class="memdesc:ga3167148206cca25a3434cb8bb15c69fe"><td class="mdescLeft"> </td><td class="mdescRight">Get all assumptions made in this and all previous contexts. <a href="#ga3167148206cca25a3434cb8bb15c69fe"></a><br/></td></tr>
<tr class="separator:ga3167148206cca25a3434cb8bb15c69fe"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga20730f5acacc4b18d29031632d88904c"><td class="memItemLeft" align="right" valign="top">virtual bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga20730f5acacc4b18d29031632d88904c">CVC3::SearchEngine::isAssumption</a> (const Expr &e)=0</td></tr>
<tr class="memdesc:ga20730f5acacc4b18d29031632d88904c"><td class="mdescLeft"> </td><td class="mdescRight">Check if the formula has already been assumed previously. <a href="#ga20730f5acacc4b18d29031632d88904c"></a><br/></td></tr>
<tr class="separator:ga20730f5acacc4b18d29031632d88904c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga739867521b23967ee6739ec32a8070e2"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga739867521b23967ee6739ec32a8070e2">CVC3::SearchEngine::getCounterExample</a> (std::vector< Expr > &assertions, bool inOrder=true)=0</td></tr>
<tr class="memdesc:ga739867521b23967ee6739ec32a8070e2"><td class="mdescLeft"> </td><td class="mdescRight">Will return the set of assertions which make the queried formula false. <a href="#ga739867521b23967ee6739ec32a8070e2"></a><br/></td></tr>
<tr class="separator:ga739867521b23967ee6739ec32a8070e2"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaa0ce3839d5f7b64168d62ff5eb59cf1f"><td class="memItemLeft" align="right" valign="top">virtual Proof </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gaa0ce3839d5f7b64168d62ff5eb59cf1f">CVC3::SearchEngine::getProof</a> ()=0</td></tr>
<tr class="memdesc:gaa0ce3839d5f7b64168d62ff5eb59cf1f"><td class="mdescLeft"> </td><td class="mdescRight">Returns the proof term for the last proven query. <a href="#gaa0ce3839d5f7b64168d62ff5eb59cf1f"></a><br/></td></tr>
<tr class="separator:gaa0ce3839d5f7b64168d62ff5eb59cf1f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gae2a1cd46200160ac5855d7cd5f65517c"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gae2a1cd46200160ac5855d7cd5f65517c">CVC3::SearchEngine::getConcreteModel</a> (<a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &m)</td></tr>
<tr class="memdesc:gae2a1cd46200160ac5855d7cd5f65517c"><td class="mdescLeft"> </td><td class="mdescRight">Build a concrete Model (assign values to variables), should only be called after a query which returns INVALID. <a href="#gae2a1cd46200160ac5855d7cd5f65517c"></a><br/></td></tr>
<tr class="separator:gae2a1cd46200160ac5855d7cd5f65517c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga44f1c2fefc202249cd2cda55d7712bdf"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga44f1c2fefc202249cd2cda55d7712bdf">CVC3::SearchEngine::tryModelGeneration</a> (<a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)</td></tr>
<tr class="memdesc:ga44f1c2fefc202249cd2cda55d7712bdf"><td class="mdescLeft"> </td><td class="mdescRight">Try to build a concrete Model (assign values to variables), should only be called after a query which returns UNKNOWN. Returns a theorem if inconsistent. <a href="#ga44f1c2fefc202249cd2cda55d7712bdf"></a><br/></td></tr>
<tr class="separator:ga44f1c2fefc202249cd2cda55d7712bdf"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga38ced857c272afeecbe0429e1dcca28e"><td class="memItemLeft" align="right" valign="top">virtual FormulaValue </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga38ced857c272afeecbe0429e1dcca28e">CVC3::SearchEngine::getValue</a> (const <a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a> &e)=0</td></tr>
<tr class="separator:ga38ced857c272afeecbe0429e1dcca28e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaf0dbbb1806723760ab8744e96a8c6657"><td class="memItemLeft" align="right" valign="top">Literal </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gaf0dbbb1806723760ab8744e96a8c6657">CVC3::SearchImplBase::newLiteral</a> (const Expr &e)</td></tr>
<tr class="memdesc:gaf0dbbb1806723760ab8744e96a8c6657"><td class="mdescLeft"> </td><td class="mdescRight">Construct a <a class="el" href="classCVC3_1_1Literal.html">Literal</a> out of an <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> or return an existing one. <a href="#gaf0dbbb1806723760ab8744e96a8c6657"></a><br/></td></tr>
<tr class="separator:gaf0dbbb1806723760ab8744e96a8c6657"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaaa621df0c7e2a2043139e6451eab7072"><td class="memItemLeft" align="right" valign="top">Theorem </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gaaa621df0c7e2a2043139e6451eab7072">CVC3::SearchImplBase::simplify</a> (const Theorem &e)</td></tr>
<tr class="memdesc:gaaa621df0c7e2a2043139e6451eab7072"><td class="mdescLeft"> </td><td class="mdescRight">Our version of simplifier: take Theorem(e), apply simplifier to get <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>(e==e'), return <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>(e') <a href="#gaaa621df0c7e2a2043139e6451eab7072"></a><br/></td></tr>
<tr class="separator:gaaa621df0c7e2a2043139e6451eab7072"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaed2d918b4d0eb14d99bf63882fe2df1a"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gaed2d918b4d0eb14d99bf63882fe2df1a">CVC3::SearchImplBase::addLiteralFact</a> (const Theorem &thm)=0</td></tr>
<tr class="memdesc:gaed2d918b4d0eb14d99bf63882fe2df1a"><td class="mdescLeft"> </td><td class="mdescRight">Notify the search engine about a new literal fact. <a href="#gaed2d918b4d0eb14d99bf63882fe2df1a"></a><br/></td></tr>
<tr class="separator:gaed2d918b4d0eb14d99bf63882fe2df1a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gae95c78de94900637db19e3b7dee5d7c3"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gae95c78de94900637db19e3b7dee5d7c3">CVC3::SearchImplBase::addNonLiteralFact</a> (const Theorem &thm)=0</td></tr>
<tr class="memdesc:gae95c78de94900637db19e3b7dee5d7c3"><td class="mdescLeft"> </td><td class="mdescRight">Notify the search engine about a new non-literal fact. <a href="#gae95c78de94900637db19e3b7dee5d7c3"></a><br/></td></tr>
<tr class="separator:gae95c78de94900637db19e3b7dee5d7c3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gadebc5b605b4a358789b697e44065a97e"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gadebc5b605b4a358789b697e44065a97e">CVC3::SearchImplBase::addCNFFact</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm, bool fromCore=false)</td></tr>
<tr class="memdesc:gadebc5b605b4a358789b697e44065a97e"><td class="mdescLeft"> </td><td class="mdescRight">Add a new fact to the search engine bypassing CNF converter. <a href="#gadebc5b605b4a358789b697e44065a97e"></a><br/></td></tr>
<tr class="separator:gadebc5b605b4a358789b697e44065a97e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga12db60dd52e1223d009f6b51b654f70e"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga12db60dd52e1223d009f6b51b654f70e">CVC3::SearchImplBase::getBottomScope</a> ()</td></tr>
<tr class="separator:ga12db60dd52e1223d009f6b51b654f70e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga9babda9b0bcd226dd4d0a736cd433893"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga9babda9b0bcd226dd4d0a736cd433893">CVC3::SearchImplBase::isClause</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:ga9babda9b0bcd226dd4d0a736cd433893"><td class="mdescLeft"> </td><td class="mdescRight">Check if e is a clause (a literal, or a disjunction of literals) <a href="#ga9babda9b0bcd226dd4d0a736cd433893"></a><br/></td></tr>
<tr class="separator:ga9babda9b0bcd226dd4d0a736cd433893"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga9db77121699fbbdbff209014b8ab26c3"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga9db77121699fbbdbff209014b8ab26c3">CVC3::SearchImplBase::isPropClause</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:ga9db77121699fbbdbff209014b8ab26c3"><td class="mdescLeft"> </td><td class="mdescRight">Check if e is a propositional clause. <a href="#ga9db77121699fbbdbff209014b8ab26c3"></a><br/></td></tr>
<tr class="separator:ga9db77121699fbbdbff209014b8ab26c3"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga92018736294ba073bc5db887467944ad"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga92018736294ba073bc5db887467944ad">CVC3::SearchImplBase::isCNFVar</a> (const Expr &e)</td></tr>
<tr class="memdesc:ga92018736294ba073bc5db887467944ad"><td class="mdescLeft"> </td><td class="mdescRight">Check whether e is a fresh variable introduced by the CNF converter. <a href="#ga92018736294ba073bc5db887467944ad"></a><br/></td></tr>
<tr class="separator:ga92018736294ba073bc5db887467944ad"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaed4079f44a18e496b87366ce65b20d99"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gaed4079f44a18e496b87366ce65b20d99">CVC3::SearchImplBase::isGoodSplitter</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:gaed4079f44a18e496b87366ce65b20d99"><td class="mdescLeft"> </td><td class="mdescRight">Check if a splitter is required for completeness. <a href="#gaed4079f44a18e496b87366ce65b20d99"></a><br/></td></tr>
<tr class="separator:gaed4079f44a18e496b87366ce65b20d99"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga4bcd481c70362c589aa7e712a8cc746d"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga4bcd481c70362c589aa7e712a8cc746d">CVC3::SearchImplBase::enqueueCNF</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &theta)</td></tr>
<tr class="memdesc:ga4bcd481c70362c589aa7e712a8cc746d"><td class="mdescLeft"> </td><td class="mdescRight">Translate theta to CNF and enqueue the new clauses. <a href="#ga4bcd481c70362c589aa7e712a8cc746d"></a><br/></td></tr>
<tr class="separator:ga4bcd481c70362c589aa7e712a8cc746d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga62e31e3c4dbadb6cc5fddc3b0b73e047"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga62e31e3c4dbadb6cc5fddc3b0b73e047">CVC3::SearchImplBase::enqueueCNFrec</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &theta)</td></tr>
<tr class="memdesc:ga62e31e3c4dbadb6cc5fddc3b0b73e047"><td class="mdescLeft"> </td><td class="mdescRight">Recursive version of <a class="el" href="group__SE.html#ga4bcd481c70362c589aa7e712a8cc746d" title="Translate theta to CNF and enqueue the new clauses.">enqueueCNF()</a> <a href="#ga62e31e3c4dbadb6cc5fddc3b0b73e047"></a><br/></td></tr>
<tr class="separator:ga62e31e3c4dbadb6cc5fddc3b0b73e047"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaa7bf3c385bae481d4ea35179e818a09a"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gaa7bf3c385bae481d4ea35179e818a09a">CVC3::SearchImplBase::applyCNFRules</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e)</td></tr>
<tr class="memdesc:gaa7bf3c385bae481d4ea35179e818a09a"><td class="mdescLeft"> </td><td class="mdescRight">FIXME: write a comment. <a href="#gaa7bf3c385bae481d4ea35179e818a09a"></a><br/></td></tr>
<tr class="separator:gaa7bf3c385bae481d4ea35179e818a09a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaa78fb38536d0a2e34ad140f3ec865f2b"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gaa78fb38536d0a2e34ad140f3ec865f2b">CVC3::SearchImplBase::addToCNFCache</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)</td></tr>
<tr class="memdesc:gaa78fb38536d0a2e34ad140f3ec865f2b"><td class="mdescLeft"> </td><td class="mdescRight">Cache a theorem phi <=> v by phi, where v is a literal. <a href="#gaa78fb38536d0a2e34ad140f3ec865f2b"></a><br/></td></tr>
<tr class="separator:gaa78fb38536d0a2e34ad140f3ec865f2b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga298ad740ab490d5b3337445573b8c4d7"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga298ad740ab490d5b3337445573b8c4d7">CVC3::SearchImplBase::findInCNFCache</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:ga298ad740ab490d5b3337445573b8c4d7"><td class="mdescLeft"> </td><td class="mdescRight">Find a theorem phi <=> v by phi, where v is a literal. <a href="#ga298ad740ab490d5b3337445573b8c4d7"></a><br/></td></tr>
<tr class="separator:ga298ad740ab490d5b3337445573b8c4d7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga687e32d21d7fe7e4b26873ae86a47ae5"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga687e32d21d7fe7e4b26873ae86a47ae5">CVC3::SearchImplBase::replaceITE</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:ga687e32d21d7fe7e4b26873ae86a47ae5"><td class="mdescLeft"> </td><td class="mdescRight">Replaces ITE subexpressions in e with variables. <a href="#ga687e32d21d7fe7e4b26873ae86a47ae5"></a><br/></td></tr>
<tr class="separator:ga687e32d21d7fe7e4b26873ae86a47ae5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gab267d9f29c30c8e26b5c7bcc4d15306a"><td class="memItemLeft" align="right" valign="top">int </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gab267d9f29c30c8e26b5c7bcc4d15306a">CVC3::SearchImplBase::scopeLevel</a> ()</td></tr>
<tr class="memdesc:gab267d9f29c30c8e26b5c7bcc4d15306a"><td class="mdescLeft"> </td><td class="mdescRight">Return the current scope level (for convenience) <a href="#gab267d9f29c30c8e26b5c7bcc4d15306a"></a><br/></td></tr>
<tr class="separator:gab267d9f29c30c8e26b5c7bcc4d15306a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaa6e44780a3c5e714f4fd5d8ee41bb1fb"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gaa6e44780a3c5e714f4fd5d8ee41bb1fb">CVC3::SearchImplBase::SearchImplBase</a> (<a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> *core)</td></tr>
<tr class="memdesc:gaa6e44780a3c5e714f4fd5d8ee41bb1fb"><td class="mdescLeft"> </td><td class="mdescRight">Constructor. <a href="#gaa6e44780a3c5e714f4fd5d8ee41bb1fb"></a><br/></td></tr>
<tr class="separator:gaa6e44780a3c5e714f4fd5d8ee41bb1fb"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga139d4116c2b14d5357f2696dc8f29cac"><td class="memItemLeft" align="right" valign="top">virtual </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga139d4116c2b14d5357f2696dc8f29cac">CVC3::SearchImplBase::~SearchImplBase</a> ()</td></tr>
<tr class="memdesc:ga139d4116c2b14d5357f2696dc8f29cac"><td class="mdescLeft"> </td><td class="mdescRight">Destructor. <a href="#ga139d4116c2b14d5357f2696dc8f29cac"></a><br/></td></tr>
<tr class="separator:ga139d4116c2b14d5357f2696dc8f29cac"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gac4e5351fec1964bf7571d67e90a1538d"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gac4e5351fec1964bf7571d67e90a1538d">CVC3::SearchImplBase::registerAtom</a> (const Expr &e)</td></tr>
<tr class="memdesc:gac4e5351fec1964bf7571d67e90a1538d"><td class="mdescLeft"> </td><td class="mdescRight">Register an atomic formula of interest. <a href="#gac4e5351fec1964bf7571d67e90a1538d"></a><br/></td></tr>
<tr class="separator:gac4e5351fec1964bf7571d67e90a1538d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga65ca9e33c2ac0807f0ef680415457c45"><td class="memItemLeft" align="right" valign="top">virtual Theorem </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga65ca9e33c2ac0807f0ef680415457c45">CVC3::SearchImplBase::getImpliedLiteral</a> ()</td></tr>
<tr class="memdesc:ga65ca9e33c2ac0807f0ef680415457c45"><td class="mdescLeft"> </td><td class="mdescRight">Return next literal implied by last assertion. Null <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> if none. <a href="#ga65ca9e33c2ac0807f0ef680415457c45"></a><br/></td></tr>
<tr class="separator:ga65ca9e33c2ac0807f0ef680415457c45"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gae987ab9ab6129f83efb0b5649cc2003c"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gae987ab9ab6129f83efb0b5649cc2003c">CVC3::SearchImplBase::push</a> ()</td></tr>
<tr class="memdesc:gae987ab9ab6129f83efb0b5649cc2003c"><td class="mdescLeft"> </td><td class="mdescRight">Push a checkpoint. <a href="#gae987ab9ab6129f83efb0b5649cc2003c"></a><br/></td></tr>
<tr class="separator:gae987ab9ab6129f83efb0b5649cc2003c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga84ceb5e9dcc4e57c1f48f77f4b2f8db5"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga84ceb5e9dcc4e57c1f48f77f4b2f8db5">CVC3::SearchImplBase::pop</a> ()</td></tr>
<tr class="memdesc:ga84ceb5e9dcc4e57c1f48f77f4b2f8db5"><td class="mdescLeft"> </td><td class="mdescRight">Restore last checkpoint. <a href="#ga84ceb5e9dcc4e57c1f48f77f4b2f8db5"></a><br/></td></tr>
<tr class="separator:ga84ceb5e9dcc4e57c1f48f77f4b2f8db5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga1e6282534845cfe93f245d9983d58761"><td class="memItemLeft" align="right" valign="top">virtual QueryResult </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga1e6282534845cfe93f245d9983d58761">CVC3::SearchImplBase::checkValidInternal</a> (const Expr &e)=0</td></tr>
<tr class="memdesc:ga1e6282534845cfe93f245d9983d58761"><td class="mdescLeft"> </td><td class="mdescRight">Checks the validity of a formula in the current context. <a href="#ga1e6282534845cfe93f245d9983d58761"></a><br/></td></tr>
<tr class="separator:ga1e6282534845cfe93f245d9983d58761"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga83d82b8cf43e9dc8240e762b180f6343"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga83d82b8cf43e9dc8240e762b180f6343">CVC3::SearchImplBase::checkValid</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &result)</td></tr>
<tr class="memdesc:ga83d82b8cf43e9dc8240e762b180f6343"><td class="mdescLeft"> </td><td class="mdescRight">Similar to <a class="el" href="group__SE.html#ga1e6282534845cfe93f245d9983d58761" title="Checks the validity of a formula in the current context.">checkValidInternal()</a>, only returns Theorem(e) or Null. <a href="#ga83d82b8cf43e9dc8240e762b180f6343"></a><br/></td></tr>
<tr class="separator:ga83d82b8cf43e9dc8240e762b180f6343"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaf89e6b914a2099b366258953fccb6277"><td class="memItemLeft" align="right" valign="top">virtual QueryResult </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gaf89e6b914a2099b366258953fccb6277">CVC3::SearchImplBase::restartInternal</a> (const Expr &e)=0</td></tr>
<tr class="memdesc:gaf89e6b914a2099b366258953fccb6277"><td class="mdescLeft"> </td><td class="mdescRight">Reruns last check with e as an additional assumption. <a href="#gaf89e6b914a2099b366258953fccb6277"></a><br/></td></tr>
<tr class="separator:gaf89e6b914a2099b366258953fccb6277"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gad4a8edbe5a6520fc9f564ec1c65d4729"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gad4a8edbe5a6520fc9f564ec1c65d4729">CVC3::SearchImplBase::restart</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &result)</td></tr>
<tr class="memdesc:gad4a8edbe5a6520fc9f564ec1c65d4729"><td class="mdescLeft"> </td><td class="mdescRight">Reruns last check with e as an additional assumption. <a href="#gad4a8edbe5a6520fc9f564ec1c65d4729"></a><br/></td></tr>
<tr class="separator:gad4a8edbe5a6520fc9f564ec1c65d4729"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga7d62893d0d19ed50cc1f616a92d536c0"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga7d62893d0d19ed50cc1f616a92d536c0">CVC3::SearchImplBase::returnFromCheck</a> ()</td></tr>
<tr class="memdesc:ga7d62893d0d19ed50cc1f616a92d536c0"><td class="mdescLeft"> </td><td class="mdescRight">Returns to context immediately before last call to checkValid. <a href="#ga7d62893d0d19ed50cc1f616a92d536c0"></a><br/></td></tr>
<tr class="separator:ga7d62893d0d19ed50cc1f616a92d536c0"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga95428fe99c7a85e5e90ba6b2dce0e024"><td class="memItemLeft" align="right" valign="top">virtual Theorem </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga95428fe99c7a85e5e90ba6b2dce0e024">CVC3::SearchImplBase::lastThm</a> ()</td></tr>
<tr class="memdesc:ga95428fe99c7a85e5e90ba6b2dce0e024"><td class="mdescLeft"> </td><td class="mdescRight">Returns the result of the most recent valid theorem. <a href="#ga95428fe99c7a85e5e90ba6b2dce0e024"></a><br/></td></tr>
<tr class="separator:ga95428fe99c7a85e5e90ba6b2dce0e024"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaf46a82b16f76c9e97cfe252d4398eac7"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gaf46a82b16f76c9e97cfe252d4398eac7">CVC3::SearchImplBase::newUserAssumption</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:gaf46a82b16f76c9e97cfe252d4398eac7"><td class="mdescLeft"> </td><td class="mdescRight">Generate and add a new assertion to the set of assertions in the current context. This should only be used by class <a class="el" href="classCVC3_1_1VCL.html">VCL</a> in assertFormula(). <a href="#gaf46a82b16f76c9e97cfe252d4398eac7"></a><br/></td></tr>
<tr class="separator:gaf46a82b16f76c9e97cfe252d4398eac7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga635768498a239f0193de5f1445676f65"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga635768498a239f0193de5f1445676f65">CVC3::SearchImplBase::newIntAssumption</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:ga635768498a239f0193de5f1445676f65"><td class="mdescLeft"> </td><td class="mdescRight">Add a new internal asserion. <a href="#ga635768498a239f0193de5f1445676f65"></a><br/></td></tr>
<tr class="separator:ga635768498a239f0193de5f1445676f65"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gab6852f32844435f73f86665c40d2fda8"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gab6852f32844435f73f86665c40d2fda8">CVC3::SearchImplBase::newIntAssumption</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)</td></tr>
<tr class="memdesc:gab6852f32844435f73f86665c40d2fda8"><td class="mdescLeft"> </td><td class="mdescRight">Helper for above function. <a href="#gab6852f32844435f73f86665c40d2fda8"></a><br/></td></tr>
<tr class="separator:gab6852f32844435f73f86665c40d2fda8"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gab730f3f048637996f532f77af932fe55"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gab730f3f048637996f532f77af932fe55">CVC3::SearchImplBase::getUserAssumptions</a> (std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &assumptions)</td></tr>
<tr class="memdesc:gab730f3f048637996f532f77af932fe55"><td class="mdescLeft"> </td><td class="mdescRight">Get all assumptions made in this and all previous contexts. <a href="#gab730f3f048637996f532f77af932fe55"></a><br/></td></tr>
<tr class="separator:gab730f3f048637996f532f77af932fe55"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gae65e0921e9ef2b475242b1a284a413ad"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gae65e0921e9ef2b475242b1a284a413ad">CVC3::SearchImplBase::getInternalAssumptions</a> (std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &assumptions)</td></tr>
<tr class="memdesc:gae65e0921e9ef2b475242b1a284a413ad"><td class="mdescLeft"> </td><td class="mdescRight">Get assumptions made internally in this and all previous contexts. <a href="#gae65e0921e9ef2b475242b1a284a413ad"></a><br/></td></tr>
<tr class="separator:gae65e0921e9ef2b475242b1a284a413ad"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gadadf46fa5200744c9f30ca548080d35d"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gadadf46fa5200744c9f30ca548080d35d">CVC3::SearchImplBase::getAssumptions</a> (std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &assumptions)</td></tr>
<tr class="memdesc:gadadf46fa5200744c9f30ca548080d35d"><td class="mdescLeft"> </td><td class="mdescRight">Get all assumptions made in this and all previous contexts. <a href="#gadadf46fa5200744c9f30ca548080d35d"></a><br/></td></tr>
<tr class="separator:gadadf46fa5200744c9f30ca548080d35d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga38ec2c19ebab8525ebc3c6249bf97442"><td class="memItemLeft" align="right" valign="top">virtual bool </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga38ec2c19ebab8525ebc3c6249bf97442">CVC3::SearchImplBase::isAssumption</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:ga38ec2c19ebab8525ebc3c6249bf97442"><td class="mdescLeft"> </td><td class="mdescRight">Check if the formula has been assumed. <a href="#ga38ec2c19ebab8525ebc3c6249bf97442"></a><br/></td></tr>
<tr class="separator:ga38ec2c19ebab8525ebc3c6249bf97442"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gac6e807418fb26dee354f7f934eb432ba"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gac6e807418fb26dee354f7f934eb432ba">CVC3::SearchImplBase::addFact</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)</td></tr>
<tr class="memdesc:gac6e807418fb26dee354f7f934eb432ba"><td class="mdescLeft"> </td><td class="mdescRight">Add a new fact to the search engine from the core. <a href="#gac6e807418fb26dee354f7f934eb432ba"></a><br/></td></tr>
<tr class="separator:gac6e807418fb26dee354f7f934eb432ba"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga6c1448b58fb299bc084aa9c522faf36d"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga6c1448b58fb299bc084aa9c522faf36d">CVC3::SearchImplBase::addSplitter</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int priority)</td></tr>
<tr class="memdesc:ga6c1448b58fb299bc084aa9c522faf36d"><td class="mdescLeft"> </td><td class="mdescRight">Suggest a splitter to the <a class="el" href="classCVC3_1_1SearchEngine.html" title="API to to a generic proof search engine.">SearchEngine</a>. <a href="#ga6c1448b58fb299bc084aa9c522faf36d"></a><br/></td></tr>
<tr class="separator:ga6c1448b58fb299bc084aa9c522faf36d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gacf93ae1a488573c6d34dee7721007351"><td class="memItemLeft" align="right" valign="top">virtual void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gacf93ae1a488573c6d34dee7721007351">CVC3::SearchImplBase::getCounterExample</a> (std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &assertions, bool inOrder=true)</td></tr>
<tr class="memdesc:gacf93ae1a488573c6d34dee7721007351"><td class="mdescLeft"> </td><td class="mdescRight">Will return the set of assertions which make the queried formula false. <a href="#gacf93ae1a488573c6d34dee7721007351"></a><br/></td></tr>
<tr class="separator:gacf93ae1a488573c6d34dee7721007351"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaf90e8ae5cd67dc6c43787a9d3ebdca53"><td class="memItemLeft" align="right" valign="top">virtual <a class="el" href="classCVC3_1_1Proof.html">Proof</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gaf90e8ae5cd67dc6c43787a9d3ebdca53">CVC3::SearchImplBase::getProof</a> ()</td></tr>
<tr class="memdesc:gaf90e8ae5cd67dc6c43787a9d3ebdca53"><td class="mdescLeft"> </td><td class="mdescRight">Returns the proof term for the last proven query. <a href="#gaf90e8ae5cd67dc6c43787a9d3ebdca53"></a><br/></td></tr>
<tr class="separator:gaf90e8ae5cd67dc6c43787a9d3ebdca53"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga24dc510f27c40d8044f461308bcdb62d"><td class="memItemLeft" align="right" valign="top">virtual const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga24dc510f27c40d8044f461308bcdb62d">CVC3::SearchImplBase::getAssumptionsUsed</a> ()</td></tr>
<tr class="memdesc:ga24dc510f27c40d8044f461308bcdb62d"><td class="mdescLeft"> </td><td class="mdescRight">Returns the set of assumptions used in the proof. It should be a subset of <a class="el" href="group__SE.html#gadadf46fa5200744c9f30ca548080d35d" title="Get all assumptions made in this and all previous contexts.">getAssumptions()</a>. <a href="#ga24dc510f27c40d8044f461308bcdb62d"></a><br/></td></tr>
<tr class="separator:ga24dc510f27c40d8044f461308bcdb62d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga0d509e38a03048dcbdb9e28f3f5da724"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga0d509e38a03048dcbdb9e28f3f5da724">CVC3::SearchImplBase::processResult</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &res, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:ga0d509e38a03048dcbdb9e28f3f5da724"><td class="mdescLeft"> </td><td class="mdescRight">Process result of checkValid. <a href="#ga0d509e38a03048dcbdb9e28f3f5da724"></a><br/></td></tr>
<tr class="separator:ga0d509e38a03048dcbdb9e28f3f5da724"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gadf867c70d67d05d72a11895a2cc13971"><td class="memItemLeft" align="right" valign="top">virtual FormulaValue </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gadf867c70d67d05d72a11895a2cc13971">CVC3::SearchImplBase::getValue</a> (const <a class="el" href="classCVC3_1_1Expr.html">CVC3::Expr</a> &e)</td></tr>
<tr class="separator:gadf867c70d67d05d72a11895a2cc13971"><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:ga3772c6af7eac91b9ed7fc278edf5ef90"><td class="memItemLeft" align="right" valign="top">TheoryCore * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga3772c6af7eac91b9ed7fc278edf5ef90">CVC3::SearchEngine::d_core</a></td></tr>
<tr class="memdesc:ga3772c6af7eac91b9ed7fc278edf5ef90"><td class="mdescLeft"> </td><td class="mdescRight">Access to theory reasoning. <a href="#ga3772c6af7eac91b9ed7fc278edf5ef90"></a><br/></td></tr>
<tr class="separator:ga3772c6af7eac91b9ed7fc278edf5ef90"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga63f2a3cfcfa86820bea2f45cb890cc1c"><td class="memItemLeft" align="right" valign="top">CommonProofRules * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga63f2a3cfcfa86820bea2f45cb890cc1c">CVC3::SearchEngine::d_commonRules</a></td></tr>
<tr class="memdesc:ga63f2a3cfcfa86820bea2f45cb890cc1c"><td class="mdescLeft"> </td><td class="mdescRight">Common proof rules. <a href="#ga63f2a3cfcfa86820bea2f45cb890cc1c"></a><br/></td></tr>
<tr class="separator:ga63f2a3cfcfa86820bea2f45cb890cc1c"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga879b68112123e2b4ae7175d85a03bfec"><td class="memItemLeft" align="right" valign="top">SearchEngineRules * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga879b68112123e2b4ae7175d85a03bfec">CVC3::SearchEngine::d_rules</a></td></tr>
<tr class="memdesc:ga879b68112123e2b4ae7175d85a03bfec"><td class="mdescLeft"> </td><td class="mdescRight"><a class="el" href="classCVC3_1_1Proof.html">Proof</a> rules for the search engine. <a href="#ga879b68112123e2b4ae7175d85a03bfec"></a><br/></td></tr>
<tr class="separator:ga879b68112123e2b4ae7175d85a03bfec"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga626a0fe24f363d007d729e16d13349e5"><td class="memItemLeft" align="right" valign="top">VariableManager * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga626a0fe24f363d007d729e16d13349e5">CVC3::SearchImplBase::d_vm</a></td></tr>
<tr class="memdesc:ga626a0fe24f363d007d729e16d13349e5"><td class="mdescLeft"> </td><td class="mdescRight"><a class="el" href="classCVC3_1_1Variable.html">Variable</a> manager for classes <a class="el" href="classCVC3_1_1Variable.html">Variable</a> and <a class="el" href="classCVC3_1_1Literal.html">Literal</a>. <a href="#ga626a0fe24f363d007d729e16d13349e5"></a><br/></td></tr>
<tr class="separator:ga626a0fe24f363d007d729e16d13349e5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga640e08e2b051e08f2abdd4111b9a2e71"><td class="memItemLeft" align="right" valign="top">CDO< int > </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga640e08e2b051e08f2abdd4111b9a2e71">CVC3::SearchImplBase::d_bottomScope</a></td></tr>
<tr class="memdesc:ga640e08e2b051e08f2abdd4111b9a2e71"><td class="mdescLeft"> </td><td class="mdescRight">The bottom-most scope for the current call to checkSAT (where conflict clauses are still valid). <a href="#ga640e08e2b051e08f2abdd4111b9a2e71"></a><br/></td></tr>
<tr class="separator:ga640e08e2b051e08f2abdd4111b9a2e71"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga02f72989536076eab8c55e452a6662d9"><td class="memItemLeft" align="right" valign="top">TheoryCore::CoreSatAPI * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga02f72989536076eab8c55e452a6662d9">CVC3::SearchImplBase::d_coreSatAPI_implBase</a></td></tr>
<tr class="separator:ga02f72989536076eab8c55e452a6662d9"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga8ea9b2ab9f50d3ddf595595b1f3d7974"><td class="memItemLeft" align="right" valign="top">CDList< Splitter > </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga8ea9b2ab9f50d3ddf595595b1f3d7974">CVC3::SearchImplBase::d_dpSplitters</a></td></tr>
<tr class="memdesc:ga8ea9b2ab9f50d3ddf595595b1f3d7974"><td class="mdescLeft"> </td><td class="mdescRight">Backtracking ordered set of DP-suggested splitters. <a href="#ga8ea9b2ab9f50d3ddf595595b1f3d7974"></a><br/></td></tr>
<tr class="separator:ga8ea9b2ab9f50d3ddf595595b1f3d7974"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga88ba664573602ecfca1d6eadc14a30af"><td class="memItemLeft" align="right" valign="top">Theorem </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga88ba664573602ecfca1d6eadc14a30af">CVC3::SearchImplBase::d_lastValid</a></td></tr>
<tr class="memdesc:ga88ba664573602ecfca1d6eadc14a30af"><td class="mdescLeft"> </td><td class="mdescRight"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> from the last successful checkValid call. It is used by getProof and getAssumptions. <a href="#ga88ba664573602ecfca1d6eadc14a30af"></a><br/></td></tr>
<tr class="separator:ga88ba664573602ecfca1d6eadc14a30af"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaf6841e86841006b6917d46664de64d21"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classExprHashMap.html">ExprHashMap</a>< bool > </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gaf6841e86841006b6917d46664de64d21">CVC3::SearchImplBase::d_lastCounterExample</a></td></tr>
<tr class="memdesc:gaf6841e86841006b6917d46664de64d21"><td class="mdescLeft"> </td><td class="mdescRight"><a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> from the last unsuccessful checkValid call. These are used by getCounterExample. <a href="#gaf6841e86841006b6917d46664de64d21"></a><br/></td></tr>
<tr class="separator:gaf6841e86841006b6917d46664de64d21"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga83dfe2d2d85bacf5e4aa10c0320a140b"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCDMap.html">CDMap</a>< Expr, Theorem > </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga83dfe2d2d85bacf5e4aa10c0320a140b">CVC3::SearchImplBase::d_assumptions</a></td></tr>
<tr class="memdesc:ga83dfe2d2d85bacf5e4aa10c0320a140b"><td class="mdescLeft"> </td><td class="mdescRight">Maintain the list of current assumptions (user asserts and splitters) for <a class="el" href="group__SE.html#gadadf46fa5200744c9f30ca548080d35d" title="Get all assumptions made in this and all previous contexts.">getAssumptions()</a>. <a href="#ga83dfe2d2d85bacf5e4aa10c0320a140b"></a><br/></td></tr>
<tr class="separator:ga83dfe2d2d85bacf5e4aa10c0320a140b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gab60a7d204ed01875c98629e874575cd6"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCDMap.html">CDMap</a>< Expr, Theorem > </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gab60a7d204ed01875c98629e874575cd6">CVC3::SearchImplBase::d_cnfCache</a></td></tr>
<tr class="memdesc:gab60a7d204ed01875c98629e874575cd6"><td class="mdescLeft"> </td><td class="mdescRight">Backtracking cache for the CNF generator. <a href="#gab60a7d204ed01875c98629e874575cd6"></a><br/></td></tr>
<tr class="separator:gab60a7d204ed01875c98629e874575cd6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga1c64a37d94b4cadedce29f3e4b98a3af"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCDMap.html">CDMap</a>< Expr, bool > </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga1c64a37d94b4cadedce29f3e4b98a3af">CVC3::SearchImplBase::d_cnfVars</a></td></tr>
<tr class="memdesc:ga1c64a37d94b4cadedce29f3e4b98a3af"><td class="mdescLeft"> </td><td class="mdescRight">Backtracking set of new variables generated by CNF translator. <a href="#ga1c64a37d94b4cadedce29f3e4b98a3af"></a><br/></td></tr>
<tr class="separator:ga1c64a37d94b4cadedce29f3e4b98a3af"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gae3b8b3cfd965e7d5138320d26808767a"><td class="memItemLeft" align="right" valign="top">const bool * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gae3b8b3cfd965e7d5138320d26808767a">CVC3::SearchImplBase::d_cnfOption</a></td></tr>
<tr class="memdesc:gae3b8b3cfd965e7d5138320d26808767a"><td class="mdescLeft"> </td><td class="mdescRight">Command line flag whether to convert to CNF. <a href="#gae3b8b3cfd965e7d5138320d26808767a"></a><br/></td></tr>
<tr class="separator:gae3b8b3cfd965e7d5138320d26808767a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gaa28d7e60bbe1df69ffb304f939b984b7"><td class="memItemLeft" align="right" valign="top">const bool * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gaa28d7e60bbe1df69ffb304f939b984b7">CVC3::SearchImplBase::d_ifLiftOption</a></td></tr>
<tr class="memdesc:gaa28d7e60bbe1df69ffb304f939b984b7"><td class="mdescLeft"> </td><td class="mdescRight">Flag: whether to convert term ITEs into CNF. <a href="#gaa28d7e60bbe1df69ffb304f939b984b7"></a><br/></td></tr>
<tr class="separator:gaa28d7e60bbe1df69ffb304f939b984b7"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:gafc2c782e4f24b55c8af7cb0189d281d8"><td class="memItemLeft" align="right" valign="top">const bool * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#gafc2c782e4f24b55c8af7cb0189d281d8">CVC3::SearchImplBase::d_ignoreCnfVarsOption</a></td></tr>
<tr class="memdesc:gafc2c782e4f24b55c8af7cb0189d281d8"><td class="mdescLeft"> </td><td class="mdescRight">Flag: ignore auxiliary CNF variables when searching for a splitter. <a href="#gafc2c782e4f24b55c8af7cb0189d281d8"></a><br/></td></tr>
<tr class="separator:gafc2c782e4f24b55c8af7cb0189d281d8"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga2287fd23d4250cc74db446983b2c3274"><td class="memItemLeft" align="right" valign="top">const bool * </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga2287fd23d4250cc74db446983b2c3274">CVC3::SearchImplBase::d_origFormulaOption</a></td></tr>
<tr class="memdesc:ga2287fd23d4250cc74db446983b2c3274"><td class="mdescLeft"> </td><td class="mdescRight">Flag: Preserve the original formula with +cnf (for splitter heuristics) <a href="#ga2287fd23d4250cc74db446983b2c3274"></a><br/></td></tr>
<tr class="separator:ga2287fd23d4250cc74db446983b2c3274"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="member-group"></a>
CNF Caches</h2></td></tr>
<tr><td class="ititle" colspan="2"><p><a class="anchor" id="amgrpf1de9eaffdc2dfafb049d21a3671dba7"></a>These caches are for subexpressions of the translated formula phi, to avoid expanding phi into a tree. We cannot use d_cnfCache for that, since it is effectively non-backtracking, and we do not know if a subexpression of phi was translated at the current level, or at some other (inactive) branch of the decision tree. </p>
</td></tr>
<tr class="memitem:ga9dc16eb11f046d9a615aff3018957c6d"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCDMap.html">CDMap</a>< Expr, bool > </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga9dc16eb11f046d9a615aff3018957c6d">CVC3::SearchImplBase::d_enqueueCNFCache</a></td></tr>
<tr class="memdesc:ga9dc16eb11f046d9a615aff3018957c6d"><td class="mdescLeft"> </td><td class="mdescRight">Cache for <a class="el" href="group__SE.html#ga4bcd481c70362c589aa7e712a8cc746d" title="Translate theta to CNF and enqueue the new clauses.">enqueueCNF()</a> <a href="#ga9dc16eb11f046d9a615aff3018957c6d"></a><br/></td></tr>
<tr class="separator:ga9dc16eb11f046d9a615aff3018957c6d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga401319b3ede7162504e979aaf2119deb"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCDMap.html">CDMap</a>< Expr, bool > </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga401319b3ede7162504e979aaf2119deb">CVC3::SearchImplBase::d_applyCNFRulesCache</a></td></tr>
<tr class="memdesc:ga401319b3ede7162504e979aaf2119deb"><td class="mdescLeft"> </td><td class="mdescRight">Cache for <a class="el" href="group__SE.html#gaa7bf3c385bae481d4ea35179e818a09a" title="FIXME: write a comment.">applyCNFRules()</a> <a href="#ga401319b3ede7162504e979aaf2119deb"></a><br/></td></tr>
<tr class="separator:ga401319b3ede7162504e979aaf2119deb"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ga0c829909b9e3ab2b59ba40e681905c4b"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCDMap.html">CDMap</a>< Expr, Theorem > </td><td class="memItemRight" valign="bottom"><a class="el" href="group__SE.html#ga0c829909b9e3ab2b59ba40e681905c4b">CVC3::SearchImplBase::d_replaceITECache</a></td></tr>
<tr class="memdesc:ga0c829909b9e3ab2b59ba40e681905c4b"><td class="mdescLeft"> </td><td class="mdescRight">Cache for <a class="el" href="group__SE.html#ga687e32d21d7fe7e4b26873ae86a47ae5" title="Replaces ITE subexpressions in e with variables.">replaceITE()</a> <a href="#ga0c829909b9e3ab2b59ba40e681905c4b"></a><br/></td></tr>
<tr class="separator:ga0c829909b9e3ab2b59ba40e681905c4b"><td class="memSeparator" colspan="2"> </td></tr>
</table>
<a name="details" id="details"></a><h2 class="groupheader">Detailed Description</h2>
<p>The search engine includes Boolean reasoning and coordinates with theory reasoning. It consists of a generic abstract API (class <a class="el" href="classCVC3_1_1SearchEngine.html" title="API to to a generic proof search engine.">SearchEngine</a>) and subclasses implementing concrete instances of search engines. </p>
<h2 class="groupheader">Function Documentation</h2>
<a class="anchor" id="ga11dd236b3ba4ca5faad7563dfe6f3d72"></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="classCVC3_1_1SearchEngineRules.html">SearchEngineRules</a> * SearchEngine::createRules </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Create the trusted component. </p>
<p>This function is defined in <a class="el" href="search__theorem__producer_8cpp.html" title="Implementation of the proof rules for the simple search engine.">search_theorem_producer.cpp</a> </p>
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00046">46</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>Referenced by <a class="el" href="search_8cpp_source.html#l00035">CVC3::SearchEngine::SearchEngine()</a>.</p>
</div>
</div>
<a class="anchor" id="ga5ee040962725cff9a07cd33cbb6d6232"></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="classCVC3_1_1SearchEngineRules.html">SearchEngineRules</a> * SearchEngine::createRules </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1SearchEngine.html">SearchEngine</a> * </td>
<td class="paramname"><em>s_eng</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="search__theorem__producer_8cpp_source.html#l00056">56</a> of file <a class="el" href="search__theorem__producer_8cpp_source.html">search_theorem_producer.cpp</a>.</p>
<p>References <a class="el" href="search__theorem__producer_8cpp_source.html#l00053">search_engine</a>.</p>
</div>
</div>
<a class="anchor" id="ga2763859e03e0a91877d91e20a3d26a7a"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">SearchEngine::SearchEngine </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_8cpp_source.html#l00035">35</a> of file <a class="el" href="search_8cpp_source.html">search.cpp</a>.</p>
<p>References <a class="el" href="search__theorem__producer_8cpp_source.html#l00046">CVC3::SearchEngine::createRules()</a>, <a class="el" href="search_8h_source.html#l00064">CVC3::SearchEngine::d_rules</a>, <a class="el" href="theorem__manager_8h_source.html#l00077">CVC3::TheoremManager::getFlags()</a>, and <a class="el" href="theory__core_8h_source.html#l00349">CVC3::TheoryCore::getTM()</a>.</p>
</div>
</div>
<a class="anchor" id="ga863ab87efd742b9a8f20b87774ab570f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">SearchEngine::~SearchEngine </td>
<td>(</td>
<td class="paramname"></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>Destructor. </p>
<p>Definition at line <a class="el" href="search_8cpp_source.html#l00052">52</a> of file <a class="el" href="search_8cpp_source.html">search.cpp</a>.</p>
<p>References <a class="el" href="search_8h_source.html#l00064">CVC3::SearchEngine::d_rules</a>.</p>
</div>
</div>
<a class="anchor" id="ga942b3cc50f5ea9da1b3117ee23eff9c2"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual const std::string& CVC3::SearchEngine::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">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Name of this search engine. </p>
<p>Implemented in <a class="el" href="group__SE__Fast.html#ga3f564001c310c9e4ff519da68f8ea670">CVC3::SearchEngineFast</a>, <a class="el" href="classCVC3_1_1SearchSat.html#a40df6c2ecc6cf95be36169849da3fd3a">CVC3::SearchSat</a>, and <a class="el" href="group__SE__Simple.html#ga3785ec3f6b938d4a60efac0948587d57">CVC3::SearchSimple</a>.</p>
</div>
</div>
<a class="anchor" id="ga09d347bd55d59dc8f1d2f711df0d1c4c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CommonProofRules* CVC3::SearchEngine::getCommonRules </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> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Accessor for common rules. </p>
<p>Definition at line <a class="el" href="search_8h_source.html#l00084">84</a> of file <a class="el" href="search_8h_source.html">search.h</a>.</p>
<p>References <a class="el" href="search_8h_source.html#l00061">CVC3::SearchEngine::d_commonRules</a>.</p>
</div>
</div>
<a class="anchor" id="ga895a3150e972fb79a7a3ab26100dd31e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">TheoryCore* CVC3::SearchEngine::theoryCore </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> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Accessor for <a class="el" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">TheoryCore</a>. </p>
<p>Definition at line <a class="el" href="search_8h_source.html#l00087">87</a> of file <a class="el" href="search_8h_source.html">search.h</a>.</p>
<p>References <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00170">CVC3::SearchImplBase::newIntAssumption()</a>.</p>
</div>
</div>
<a class="anchor" id="ga0f7c2870341319738e7d8c6662e6d7cc"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void CVC3::SearchEngine::registerAtom </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">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Register an atomic formula of interest. </p>
<p>Registered atoms are tracked by the decision procedures. If one of them is deduced to be true or false, it is added to a list of implied literals. Implied literals can be retrieved with the getImpliedLiteral function </p>
<p>Implemented in <a class="el" href="classCVC3_1_1SearchSat.html#a2ca4a66d1bf7d0227e646edd3c9b9964">CVC3::SearchSat</a>, and <a class="el" href="group__SE.html#gac4e5351fec1964bf7571d67e90a1538d">CVC3::SearchImplBase</a>.</p>
</div>
</div>
<a class="anchor" id="ga29a287b5dd638015f974a8a046e19d8a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual Theorem CVC3::SearchEngine::getImpliedLiteral </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Return next literal implied by last assertion. Null <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> if none. </p>
<p>Returned literals are either registered atomic formulas or their negation </p>
<p>Implemented in <a class="el" href="classCVC3_1_1SearchSat.html#a737cf8f3791197c405017db18163ce6b">CVC3::SearchSat</a>, and <a class="el" href="group__SE.html#ga65ca9e33c2ac0807f0ef680415457c45">CVC3::SearchImplBase</a>.</p>
</div>
</div>
<a class="anchor" id="gadea197447ea40330f3b0739aa944c800"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void CVC3::SearchEngine::push </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Push a checkpoint. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1SearchSat.html#a9f129c2415d3eef0d73ad6d98ff13d44">CVC3::SearchSat</a>, and <a class="el" href="group__SE.html#gae987ab9ab6129f83efb0b5649cc2003c">CVC3::SearchImplBase</a>.</p>
<p>Referenced by <a class="el" href="search_8cpp_source.html#l00091">CVC3::SearchEngine::getConcreteModel()</a>, and <a class="el" href="search_8cpp_source.html#l00057">CVC3::SearchEngine::tryModelGeneration()</a>.</p>
</div>
</div>
<a class="anchor" id="ga2c7fa9d3a42a543ff23891110ad673e5"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void CVC3::SearchEngine::pop </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Restore last checkpoint. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1SearchSat.html#a5c3eeec4b2c970f9d503b2892c9eb770">CVC3::SearchSat</a>, and <a class="el" href="group__SE.html#ga84ceb5e9dcc4e57c1f48f77f4b2f8db5">CVC3::SearchImplBase</a>.</p>
<p>Referenced by <a class="el" href="search_8cpp_source.html#l00091">CVC3::SearchEngine::getConcreteModel()</a>, and <a class="el" href="search_8cpp_source.html#l00057">CVC3::SearchEngine::tryModelGeneration()</a>.</p>
</div>
</div>
<a class="anchor" id="ga34a9133f5342719526863d24cd1a0fcc"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual QueryResult CVC3::SearchEngine::checkValid </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>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>result</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Checks the validity of a formula in the current context. </p>
<p>If the query is valid, it returns VALID, the result parameter contains the corresponding theorem, and the scope and context are the same as when called. If it returns INVALID, the context will be one which falsifies the query. If it returns UNKNOWN, the context will falsify the query, but the context may be inconsistent. Finally, if it returns ABORT, the context will be one which satisfies as much as possible. </p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">e</td><td>the formula to check. </td></tr>
<tr><td class="paramname">result</td><td>the resulting theorem, if the formula is valid. </td></tr>
</table>
</dd>
</dl>
<p>Implemented in <a class="el" href="classCVC3_1_1SearchSat.html#a2921a84d2f2f33413ccda78789f40147">CVC3::SearchSat</a>, and <a class="el" href="group__SE.html#ga83d82b8cf43e9dc8240e762b180f6343">CVC3::SearchImplBase</a>.</p>
<p>Referenced by <a class="el" href="search_8cpp_source.html#l00091">CVC3::SearchEngine::getConcreteModel()</a>, and <a class="el" href="search_8cpp_source.html#l00057">CVC3::SearchEngine::tryModelGeneration()</a>.</p>
</div>
</div>
<a class="anchor" id="ga715936653b5bef3e3d9fd2a8a873bafd"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual QueryResult CVC3::SearchEngine::restart </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>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>result</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Reruns last check with e as an additional assumption. </p>
<p>This method should only be called after a query which is invalid. </p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">e</td><td>the additional assumption </td></tr>
<tr><td class="paramname">result</td><td>the resulting theorem, if the query is valid. </td></tr>
</table>
</dd>
</dl>
<p>Implemented in <a class="el" href="classCVC3_1_1SearchSat.html#ae7bf52f7780c6f2e085cf23c507fc3e1">CVC3::SearchSat</a>, and <a class="el" href="group__SE.html#gad4a8edbe5a6520fc9f564ec1c65d4729">CVC3::SearchImplBase</a>.</p>
</div>
</div>
<a class="anchor" id="gad552593fb43fd5751f12942f3a29a90e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void CVC3::SearchEngine::returnFromCheck </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Returns to context immediately before last call to checkValid. </p>
<p>This method should only be called after a query which returns something other than VALID. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1SearchSat.html#a43a09dbf7232bfdb6f10aee4df1add94">CVC3::SearchSat</a>, and <a class="el" href="group__SE.html#ga7d62893d0d19ed50cc1f616a92d536c0">CVC3::SearchImplBase</a>.</p>
</div>
</div>
<a class="anchor" id="ga9757a6fd272ea550d0e910d20bd7d00b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual Theorem CVC3::SearchEngine::lastThm </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Returns the result of the most recent valid theorem. </p>
<p>Returns Null <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> if last call was not valid </p>
<p>Implemented in <a class="el" href="classCVC3_1_1SearchSat.html#a0828289ad2b19cc7fac453b41287ca50">CVC3::SearchSat</a>, and <a class="el" href="group__SE.html#ga95428fe99c7a85e5e90ba6b2dce0e024">CVC3::SearchImplBase</a>.</p>
<p>Referenced by <a class="el" href="search_8cpp_source.html#l00091">CVC3::SearchEngine::getConcreteModel()</a>, and <a class="el" href="search_8cpp_source.html#l00057">CVC3::SearchEngine::tryModelGeneration()</a>.</p>
</div>
</div>
<a class="anchor" id="ga5782663fc8ae00ec2965506c8ba65a86"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual Theorem CVC3::SearchEngine::newUserAssumption </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">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Generate and add an assumption to the set of assumptions in the current context. </p>
<p>By default, the assumption is added at the current scope. The default can be overridden by specifying the scope parameter. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1SearchSat.html#a859331cc6fc93adfdd09cb848cd6de0b">CVC3::SearchSat</a>, and <a class="el" href="group__SE.html#gaf46a82b16f76c9e97cfe252d4398eac7">CVC3::SearchImplBase</a>.</p>
</div>
</div>
<a class="anchor" id="ga43f52699cddc6e0feffffaf22424fe47"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void CVC3::SearchEngine::getUserAssumptions </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>assumptions</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Get all user assumptions made in this and all previous contexts. </p>
<p>User assumptions are created either by calls to newUserAssumption or a call to checkValid. In the latter case, the negated query is added as an assumption. </p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">assumptions</td><td>should be empty on entry. </td></tr>
</table>
</dd>
</dl>
<p>Implemented in <a class="el" href="classCVC3_1_1SearchSat.html#a7344ad67225c0d6e30f8c2215bc7e0b0">CVC3::SearchSat</a>, and <a class="el" href="group__SE.html#gab730f3f048637996f532f77af932fe55">CVC3::SearchImplBase</a>.</p>
<p>Referenced by <a class="el" href="search__theorem__producer_8cpp_source.html#l01419">CVC3::SearchEngineTheoremProducer::satProof()</a>.</p>
</div>
</div>
<a class="anchor" id="ga320e15a994a712bc7c20854853501b27"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void CVC3::SearchEngine::getInternalAssumptions </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>assumptions</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Get assumptions made internally in this and all previous contexts. </p>
<p>Internal assumptions are literals assumed by the sat solver. </p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">assumptions</td><td>should be empty on entry. </td></tr>
</table>
</dd>
</dl>
<p>Implemented in <a class="el" href="classCVC3_1_1SearchSat.html#acee513ead4033fd5bfc16cbab7951dc7">CVC3::SearchSat</a>, and <a class="el" href="group__SE.html#gae65e0921e9ef2b475242b1a284a413ad">CVC3::SearchImplBase</a>.</p>
</div>
</div>
<a class="anchor" id="ga3167148206cca25a3434cb8bb15c69fe"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void CVC3::SearchEngine::getAssumptions </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>assumptions</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Get all assumptions made in this and all previous contexts. </p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">assumptions</td><td>should be an empty vector which will be filled \ with the assumptions </td></tr>
</table>
</dd>
</dl>
<p>Implemented in <a class="el" href="classCVC3_1_1SearchSat.html#a63ffdace5647b9d783e4a4a0dd90fb0b">CVC3::SearchSat</a>, and <a class="el" href="group__SE.html#gadadf46fa5200744c9f30ca548080d35d">CVC3::SearchImplBase</a>.</p>
<p>Referenced by <a class="el" href="search_8cpp_source.html#l00091">CVC3::SearchEngine::getConcreteModel()</a>.</p>
</div>
</div>
<a class="anchor" id="ga20730f5acacc4b18d29031632d88904c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual bool CVC3::SearchEngine::isAssumption </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">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Check if the formula has already been assumed previously. </p>
<p>Implemented in <a class="el" href="group__SE__Fast.html#ga4b55b5f49d921ca4b63f874d8404c4d5">CVC3::SearchEngineFast</a>, <a class="el" href="classCVC3_1_1SearchSat.html#a4ec713d6bbbd5d4bd6a9fcacc42a044e">CVC3::SearchSat</a>, and <a class="el" href="group__SE.html#ga38ec2c19ebab8525ebc3c6249bf97442">CVC3::SearchImplBase</a>.</p>
</div>
</div>
<a class="anchor" id="ga739867521b23967ee6739ec32a8070e2"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void CVC3::SearchEngine::getCounterExample </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>assertions</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>inOrder</em> = <code>true</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Will return the set of assertions which make the queried formula false. </p>
<p>This method should only be called after an query which returns INVALID. It will try to return the simplest possible set of assertions which are sufficient to make the queried expression false. </p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">assertions</td><td>should be empty on entry. </td></tr>
<tr><td class="paramname">inOrder</td><td>if true, returns the assertions in the order they were asserted. This is slightly more expensive than inOrder = false. </td></tr>
</table>
</dd>
</dl>
<p>Implemented in <a class="el" href="classCVC3_1_1SearchSat.html#af2296bfb7f363cb9b83ca2fa6042d496">CVC3::SearchSat</a>, and <a class="el" href="group__SE.html#gacf93ae1a488573c6d34dee7721007351">CVC3::SearchImplBase</a>.</p>
</div>
</div>
<a class="anchor" id="gaa0ce3839d5f7b64168d62ff5eb59cf1f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual Proof CVC3::SearchEngine::getProof </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Returns the proof term for the last proven query. </p>
<p>It should be called only after a query which returns VALID. In any other case, it returns Null. </p>
<p>Implemented in <a class="el" href="classCVC3_1_1SearchSat.html#aa8b7c9812f7f61fc567c502ef3240d85">CVC3::SearchSat</a>, and <a class="el" href="group__SE.html#gaf90e8ae5cd67dc6c43787a9d3ebdca53">CVC3::SearchImplBase</a>.</p>
</div>
</div>
<a class="anchor" id="gae2a1cd46200160ac5855d7cd5f65517c"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchEngine::getConcreteModel </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>m</em></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Build a concrete Model (assign values to variables), should only be called after a query which returns INVALID. </p>
<p>Definition at line <a class="el" href="search_8cpp_source.html#l00091">91</a> of file <a class="el" href="search_8cpp_source.html">search.cpp</a>.</p>
<p>References <a class="el" href="theory__core_8cpp_source.html#l03862">CVC3::TheoryCore::buildModel()</a>, <a class="el" href="group__SE.html#ga34a9133f5342719526863d24cd1a0fcc">CVC3::SearchEngine::checkValid()</a>, <a class="el" href="theory__core_8cpp_source.html#l03763">CVC3::TheoryCore::collectBasicVars()</a>, <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="theory_8h_source.html#l00579">CVC3::Theory::falseExpr()</a>, <a class="el" href="group__SE.html#ga3167148206cca25a3434cb8bb15c69fe">CVC3::SearchEngine::getAssumptions()</a>, <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, <a class="el" href="theorem_8cpp_source.html#l00274">CVC3::Theorem::getLeafAssumptions()</a>, <a class="el" href="theory__core_8h_source.html#l00425">CVC3::TheoryCore::inconsistentThm()</a>, <a class="el" href="group__SE.html#ga9757a6fd272ea550d0e910d20bd7d00b">CVC3::SearchEngine::lastThm()</a>, <a class="el" href="group__SE.html#ga2c7fa9d3a42a543ff23891110ad673e5">CVC3::SearchEngine::pop()</a>, <a class="el" href="group__SE.html#gadea197447ea40330f3b0739aa944c800">CVC3::SearchEngine::push()</a>, <a class="el" href="kinds_8h_source.html#l00044">RAW_LIST</a>, <a class="el" href="theory__core_8cpp_source.html#l03429">CVC3::TheoryCore::refineCounterExample()</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="queryresult_8h_source.html#l00035">CVC3::VALID</a>.</p>
</div>
</div>
<a class="anchor" id="ga44f1c2fefc202249cd2cda55d7712bdf"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool SearchEngine::tryModelGeneration </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>
</div><div class="memdoc">
<p>Try to build a concrete Model (assign values to variables), should only be called after a query which returns UNKNOWN. Returns a theorem if inconsistent. </p>
<p>Definition at line <a class="el" href="search_8cpp_source.html#l00057">57</a> of file <a class="el" href="search_8cpp_source.html">search.cpp</a>.</p>
<p>References <a class="el" href="theory__core_8cpp_source.html#l03862">CVC3::TheoryCore::buildModel()</a>, <a class="el" href="group__SE.html#ga34a9133f5342719526863d24cd1a0fcc">CVC3::SearchEngine::checkValid()</a>, <a class="el" href="theory__core_8cpp_source.html#l03763">CVC3::TheoryCore::collectBasicVars()</a>, <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="theory_8h_source.html#l00579">CVC3::Theory::falseExpr()</a>, <a class="el" href="group__SE.html#ga9757a6fd272ea550d0e910d20bd7d00b">CVC3::SearchEngine::lastThm()</a>, <a class="el" href="group__SE.html#ga2c7fa9d3a42a543ff23891110ad673e5">CVC3::SearchEngine::pop()</a>, <a class="el" href="group__SE.html#gadea197447ea40330f3b0739aa944c800">CVC3::SearchEngine::push()</a>, <a class="el" href="theory__core_8cpp_source.html#l03429">CVC3::TheoryCore::refineCounterExample()</a>, and <a class="el" href="queryresult_8h_source.html#l00035">CVC3::VALID</a>.</p>
</div>
</div>
<a class="anchor" id="ga38ced857c272afeecbe0429e1dcca28e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual FormulaValue CVC3::SearchEngine::getValue </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">CVC3::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">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implemented in <a class="el" href="classCVC3_1_1SearchSat.html#ad3267f576f114e049609a8c3c4f01118">CVC3::SearchSat</a>, and <a class="el" href="group__SE.html#gadf867c70d67d05d72a11895a2cc13971">CVC3::SearchImplBase</a>.</p>
</div>
</div>
<a class="anchor" id="gaf0dbbb1806723760ab8744e96a8c6657"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Literal CVC3::SearchImplBase::newLiteral </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">inline</span><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Construct a <a class="el" href="classCVC3_1_1Literal.html">Literal</a> out of an <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> or return an existing one. </p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00120">120</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>References <a class="el" href="search__impl__base_8h_source.html#l00044">CVC3::SearchImplBase::d_vm</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01530">CVC3::SearchEngineFast::addLiteralFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l01445">CVC3::SearchEngineFast::addNonLiteralFact()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00241">CVC3::SearchImplBase::addSplitter()</a>, <a class="el" href="search__fast_8cpp_source.html#l01601">CVC3::SearchEngineFast::addSplitter()</a>, <a class="el" href="search__fast_8cpp_source.html#l01573">CVC3::SearchEngineFast::newIntAssumption()</a>, <a class="el" href="circuit_8cpp_source.html#l00047">CVC3::Circuit::propagate()</a>, <a class="el" href="search__fast_8cpp_source.html#l00549">CVC3::SearchEngineFast::recordFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l00254">CVC3::SearchEngineFast::split()</a>, <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00915">CVC3::SearchEngineFast::unitPropagation()</a>.</p>
</div>
</div>
<a class="anchor" id="gaaa621df0c7e2a2043139e6451eab7072"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Theorem CVC3::SearchImplBase::simplify </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</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">inline</span><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Our version of simplifier: take Theorem(e), apply simplifier to get <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>(e==e'), return <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>(e') </p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00124">124</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>References <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theory_8h_source.html#l00714">CVC3::Theory::iffMP()</a>, and <a class="el" href="theory__core_8cpp_source.html#l00184">CVC3::TheoryCore::simplify()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>.</p>
</div>
</div>
<a class="anchor" id="gaed2d918b4d0eb14d99bf63882fe2df1a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void CVC3::SearchImplBase::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">protected</span><span class="mlabel">pure 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>Implemented in <a class="el" href="group__SE__Fast.html#gaef3113afb8dc9ea1b06217ab77f5d713">CVC3::SearchEngineFast</a>, and <a class="el" href="group__SE__Simple.html#gab6bfda32dfb4b7d9176ace21c7ca404e">CVC3::SearchSimple</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00218">CVC3::SearchImplBase::addCNFFact()</a>, and <a class="el" href="decision__engine_8cpp_source.html#l00128">CVC3::DecisionEngine::pushDecision()</a>.</p>
</div>
</div>
<a class="anchor" id="gae95c78de94900637db19e3b7dee5d7c3"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void CVC3::SearchImplBase::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">protected</span><span class="mlabel">pure 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>Implemented in <a class="el" href="group__SE__Fast.html#ga03501a968c3c7122a999b1f57d6640a0">CVC3::SearchEngineFast</a>, and <a class="el" href="group__SE__Simple.html#gadf91beae0add624c57c6481ab23147f8">CVC3::SearchSimple</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00218">CVC3::SearchImplBase::addCNFFact()</a>.</p>
</div>
</div>
<a class="anchor" id="gadebc5b605b4a358789b697e44065a97e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void SearchImplBase::addCNFFact </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>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>fromCore</em> = <code>false</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Add a new fact to the search engine bypassing CNF converter. </p>
<p>Calls either <a class="el" href="group__SE.html#gaed2d918b4d0eb14d99bf63882fe2df1a" title="Notify the search engine about a new literal fact.">addLiteralFact()</a> or <a class="el" href="group__SE.html#gae95c78de94900637db19e3b7dee5d7c3" title="Notify the search engine about a new non-literal fact.">addNonLiteralFact()</a> appropriately, and converts to CNF when d_cnfOption is set. If fromCore==true, this fact already comes from the core, and doesn't need to be reported back to the core. </p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00218">218</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="group__SE.html#gaed2d918b4d0eb14d99bf63882fe2df1a">CVC3::SearchImplBase::addLiteralFact()</a>, <a class="el" href="group__SE.html#gae95c78de94900637db19e3b7dee5d7c3">CVC3::SearchImplBase::addNonLiteralFact()</a>, <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="classCVC3_1_1TheoryCore.html#a0ceab59114fc3864bac9a347c61ec444">CVC3::TheoryCore::enqueueFact()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00482">CVC3::Theorem::isAbsLiteral()</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>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00231">CVC3::SearchImplBase::addFact()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00360">CVC3::SearchImplBase::enqueueCNF()</a>, and <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>.</p>
</div>
</div>
<a class="anchor" id="ga12db60dd52e1223d009f6b51b654f70e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::SearchImplBase::getBottomScope </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> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00153">153</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>References <a class="el" href="search__impl__base_8h_source.html#l00049">CVC3::SearchImplBase::d_bottomScope</a>.</p>
</div>
</div>
<a class="anchor" id="ga9babda9b0bcd226dd4d0a736cd433893"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool SearchImplBase::isClause </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>
</div><div class="memdoc">
<p>Check if e is a clause (a literal, or a disjunction of literals) </p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00687">687</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr_8h_source.html#l00406">CVC3::Expr::isAbsLiteral()</a>, and <a class="el" href="expr_8h_source.html#l00422">CVC3::Expr::isOr()</a>.</p>
</div>
</div>
<a class="anchor" id="ga9db77121699fbbdbff209014b8ab26c3"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool SearchImplBase::isPropClause </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>
</div><div class="memdoc">
<p>Check if e is a propositional clause. </p>
<dl class="section see"><dt>See Also</dt><dd>isPropAtom() </dd></dl>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00699">699</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr_8h_source.html#l00422">CVC3::Expr::isOr()</a>, and <a class="el" href="expr_8h_source.html#l00413">CVC3::Expr::isPropLiteral()</a>.</p>
</div>
</div>
<a class="anchor" id="ga92018736294ba073bc5db887467944ad"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::SearchImplBase::isCNFVar </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">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Check whether e is a fresh variable introduced by the CNF converter. </p>
<p>Search engines do not need to split on those variables in order to be complete </p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00165">165</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>References <a class="el" href="cdmap_8h_source.html#l00172">CVC3::CDMap< Key, Data, HashFcn >::count()</a>, and <a class="el" href="search__impl__base_8h_source.html#l00090">CVC3::SearchImplBase::d_cnfVars</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00711">CVC3::SearchImplBase::isGoodSplitter()</a>.</p>
</div>
</div>
<a class="anchor" id="gaed4079f44a18e496b87366ce65b20d99"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool SearchImplBase::isGoodSplitter </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>
</div><div class="memdoc">
<p>Check if a splitter is required for completeness. </p>
<p>Currently, it checks that 'e' is not an auxiliary CNF variable </p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00711">711</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="search__impl__base_8h_source.html#l00096">CVC3::SearchImplBase::d_ignoreCnfVarsOption</a>, <a class="el" href="search__impl__base_8h_source.html#l00165">CVC3::SearchImplBase::isCNFVar()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l00438">CVC3::SearchEngineFast::findSplitter()</a>, and <a class="el" href="decision__engine_8cpp_source.html#l00055">CVC3::DecisionEngine::findSplitterRec()</a>.</p>
</div>
</div>
<a class="anchor" id="ga4bcd481c70362c589aa7e712a8cc746d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void SearchImplBase::enqueueCNF </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>theta</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>Translate theta to CNF and enqueue the new clauses. </p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00360">360</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="search__impl__base_8cpp_source.html#l00218">CVC3::SearchImplBase::addCNFFact()</a>, <a class="el" href="search__impl__base_8h_source.html#l00098">CVC3::SearchImplBase::d_origFormulaOption</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</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>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00231">CVC3::SearchImplBase::addFact()</a>.</p>
</div>
</div>
<a class="anchor" id="ga62e31e3c4dbadb6cc5fddc3b0b73e047"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void SearchImplBase::enqueueCNFrec </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>theta</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 version of <a class="el" href="group__SE.html#ga4bcd481c70362c589aa7e712a8cc746d" title="Translate theta to CNF and enqueue the new clauses.">enqueueCNF()</a> </p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00371">371</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="search__impl__base_8cpp_source.html#l00218">CVC3::SearchImplBase::addCNFFact()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00723">CVC3::SearchImplBase::addToCNFCache()</a>, <a class="el" href="kinds_8h_source.html#l00067">AND</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a3f3592ac74d0aa0caa3b9224ea7e61f4">CVC3::CommonProofRules::andElim()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</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#l00090">CVC3::SearchImplBase::d_cnfVars</a>, <a class="el" href="search_8h_source.html#l00061">CVC3::SearchEngine::d_commonRules</a>, <a class="el" href="search__impl__base_8h_source.html#l00112">CVC3::SearchImplBase::d_enqueueCNFCache</a>, <a class="el" href="search__impl__base_8h_source.html#l00094">CVC3::SearchImplBase::d_ifLiftOption</a>, <a class="el" href="search_8h_source.html#l00064">CVC3::SearchEngine::d_rules</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00750">CVC3::SearchImplBase::findInCNFCache()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00486">CVC3::Theorem::getScope()</a>, <a class="el" href="kinds_8h_source.html#l00070">IFF</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#aebbcd4a194e4fdca0bcd16143fb03a75">CVC3::CommonProofRules::iffMP()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="theorem_8cpp_source.html#l00482">CVC3::Theorem::isAbsLiteral()</a>, <a class="el" href="expr_8h_source.html#l00406">CVC3::Expr::isAbsLiteral()</a>, <a class="el" href="expr_8h_source.html#l00421">CVC3::Expr::isAnd()</a>, <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>, <a class="el" href="expr_8h_source.html#l00413">CVC3::Expr::isPropLiteral()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, <a class="el" href="kinds_8h_source.html#l00081">ITE</a>, <a class="el" href="group__SE__Rules.html#ga9b9c0fe62505477b6ec9774c1b5b2494">CVC3::SearchEngineRules::iteToClauses()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#ace6786234994faf89bc1b0ac8575278a">CVC3::CommonProofRules::notNotElim()</a>, <a class="el" href="kinds_8h_source.html#l00068">OR</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00804">CVC3::SearchImplBase::replaceITE()</a>, <a class="el" href="search__impl__base_8h_source.html#l00192">CVC3::SearchImplBase::scopeLevel()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a776c827bb6e3b889234429c49ae9ad6f">CVC3::CommonProofRules::substitutivityRule()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a0a87e88508f49b73037e0024afa841bf">CVC3::CommonProofRules::symmetryRule()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::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>, <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a">CVC3::CommonProofRules::transitivityRule()</a>, and <a class="el" href="classCVC3_1_1CommonProofRules.html#a10fa187373ec24079c10874d8e804ecb">CVC3::CommonProofRules::varIntroSkolem()</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00360">CVC3::SearchImplBase::enqueueCNF()</a>.</p>
</div>
</div>
<a class="anchor" id="gaa7bf3c385bae481d4ea35179e818a09a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void SearchImplBase::applyCNFRules </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">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>FIXME: write a comment. </p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">thm</td><td>is the input of the form phi <=> v </td></tr>
</table>
</dd>
</dl>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00563">563</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="search__impl__base_8cpp_source.html#l00218">CVC3::SearchImplBase::addCNFFact()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00723">CVC3::SearchImplBase::addToCNFCache()</a>, <a class="el" href="kinds_8h_source.html#l00067">AND</a>, <a class="el" href="group__SE__Rules.html#gab183ff7d1013729d0d3e2dbe28686e3c">CVC3::SearchEngineRules::andCNFRule()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a3f3592ac74d0aa0caa3b9224ea7e61f4">CVC3::CommonProofRules::andElim()</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="search__impl__base_8h_source.html#l00114">CVC3::SearchImplBase::d_applyCNFRulesCache</a>, <a class="el" href="search_8h_source.html#l00061">CVC3::SearchEngine::d_commonRules</a>, <a class="el" href="search_8h_source.html#l00064">CVC3::SearchEngine::d_rules</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cdmap_8h_source.html#l00258">CVC3::CDMap< Key, Data, HashFcn >::end()</a>, <a class="el" href="cdmap_8h_source.html#l00303">CVC3::CDMap< Key, Data, HashFcn >::find()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00750">CVC3::SearchImplBase::findInCNFCache()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="kinds_8h_source.html#l00070">IFF</a>, <a class="el" href="group__SE__Rules.html#ga4ab7606744594db9050cb83fe6b73668">CVC3::SearchEngineRules::iffCNFRule()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#af38f25446a561384c3de66392c4d3544">CVC3::CommonProofRules::iffContrapositive()</a>, <a class="el" href="group__SE__Rules.html#ga356cd5a36ede50921fbaa3bc7e222d4f">CVC3::SearchEngineRules::iffToClauses()</a>, <a class="el" href="group__SE__Rules.html#ga25f7b95c8ebce2be117d03a1c93d715f">CVC3::SearchEngineRules::impCNFRule()</a>, <a class="el" href="kinds_8h_source.html#l00071">IMPLIES</a>, <a class="el" href="expr_8h_source.html#l00406">CVC3::Expr::isAbsLiteral()</a>, <a class="el" href="expr_8h_source.html#l00421">CVC3::Expr::isAnd()</a>, <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>, <a class="el" href="expr_8h_source.html#l00413">CVC3::Expr::isPropLiteral()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, <a class="el" href="kinds_8h_source.html#l00081">ITE</a>, <a class="el" href="group__SE__Rules.html#gae9263cbcedf5def99b3c49ee6978497a">CVC3::SearchEngineRules::iteCNFRule()</a>, <a class="el" href="kinds_8h_source.html#l00068">OR</a>, <a class="el" href="group__SE__Rules.html#ga7086aa693d2a3421bc349eca8e9938ba">CVC3::SearchEngineRules::orCNFRule()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00804">CVC3::SearchImplBase::replaceITE()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a776c827bb6e3b889234429c49ae9ad6f">CVC3::CommonProofRules::substitutivityRule()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a0a87e88508f49b73037e0024afa841bf">CVC3::CommonProofRules::symmetryRule()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::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>, <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a">CVC3::CommonProofRules::transitivityRule()</a>, and <a class="el" href="classCVC3_1_1CommonProofRules.html#a10fa187373ec24079c10874d8e804ecb">CVC3::CommonProofRules::varIntroSkolem()</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, and <a class="el" href="search__impl__base_8cpp_source.html#l00804">CVC3::SearchImplBase::replaceITE()</a>.</p>
</div>
</div>
<a class="anchor" id="gaa78fb38536d0a2e34ad140f3ec865f2b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void SearchImplBase::addToCNFCache </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">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Cache a theorem phi <=> v by phi, where v is a literal. </p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00723">723</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="cdmap_8h_source.html#l00172">CVC3::CDMap< Key, Data, HashFcn >::count()</a>, <a class="el" href="statistics_8h_source.html#l00163">CVC3::Statistics::counter()</a>, <a class="el" href="search__impl__base_8h_source.html#l00049">CVC3::SearchImplBase::d_bottomScope</a>, <a class="el" href="search__impl__base_8h_source.html#l00087">CVC3::SearchImplBase::d_cnfCache</a>, <a class="el" href="search__impl__base_8h_source.html#l00090">CVC3::SearchImplBase::d_cnfVars</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="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="theory__core_8h_source.html#l00351">CVC3::TheoryCore::getStatistics()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#af38f25446a561384c3de66392c4d3544">CVC3::CommonProofRules::iffContrapositive()</a>, <a class="el" href="cdmap_8h_source.html#l00190">CVC3::CDMap< Key, Data, HashFcn >::insert()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, and <a class="el" href="search__impl__base_8cpp_source.html#l00804">CVC3::SearchImplBase::replaceITE()</a>.</p>
</div>
</div>
<a class="anchor" id="ga298ad740ab490d5b3337445573b8c4d7"></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="classCVC3_1_1Theorem.html">Theorem</a> SearchImplBase::findInCNFCache </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">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Find a theorem phi <=> v by phi, where v is a literal. </p>
<dl class="section return"><dt>Returns</dt><dd>Null <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> if not found. </dd></dl>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00750">750</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="statistics_8h_source.html#l00163">CVC3::Statistics::counter()</a>, <a class="el" href="search__impl__base_8h_source.html#l00087">CVC3::SearchImplBase::d_cnfCache</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="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="cdmap_8h_source.html#l00258">CVC3::CDMap< Key, Data, HashFcn >::end()</a>, <a class="el" href="cdmap_8h_source.html#l00303">CVC3::CDMap< Key, Data, HashFcn >::find()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="theory__core_8h_source.html#l00351">CVC3::TheoryCore::getStatistics()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#af38f25446a561384c3de66392c4d3544">CVC3::CommonProofRules::iffContrapositive()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a8a04ff29591a019d4d4cf073c0987316">CVC3::CommonProofRules::rewriteNotNot()</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>, <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>, and <a class="el" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a">CVC3::CommonProofRules::transitivityRule()</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, and <a class="el" href="search__impl__base_8cpp_source.html#l00804">CVC3::SearchImplBase::replaceITE()</a>.</p>
</div>
</div>
<a class="anchor" id="ga687e32d21d7fe7e4b26873ae86a47ae5"></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="classCVC3_1_1Theorem.html">Theorem</a> SearchImplBase::replaceITE </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">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Replaces ITE subexpressions in e with variables. </p>
<p>Strategy:</p>
<p>For a given atomic formula phi(ite(c, t1, t2)) which depends on a term ITE, generate an equisatisfiable formula:</p>
<p>phi(x) & ite(c, t1=x, t2=x),</p>
<p>where x is a new variable.</p>
<p>The phi(x) part will be generated by the caller, and our job is to assert the 'ite(c, t1=x, t2=x)', and return a rewrite theorem phi(ite(c, t1, t2)) <=> phi(x). </p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00804">804</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="search__impl__base_8cpp_source.html#l00723">CVC3::SearchImplBase::addToCNFCache()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</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__impl__base_8h_source.html#l00116">CVC3::SearchImplBase::d_replaceITECache</a>, <a class="el" href="cdmap_8h_source.html#l00258">CVC3::CDMap< Key, Data, HashFcn >::end()</a>, <a class="el" href="cdmap_8h_source.html#l00303">CVC3::CDMap< Key, Data, HashFcn >::find()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00750">CVC3::SearchImplBase::findInCNFCache()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#aebbcd4a194e4fdca0bcd16143fb03a75">CVC3::CommonProofRules::iffMP()</a>, <a class="el" href="expr_8h_source.html#l00406">CVC3::Expr::isAbsLiteral()</a>, <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>, <a class="el" href="expr_8h_source.html#l00413">CVC3::Expr::isPropLiteral()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a61c1fe56b4ed9744006883a7784ddb71">CVC3::CommonProofRules::reflexivityRule()</a>, <a class="el" href="theory__core_8cpp_source.html#l04029">CVC3::TheoryCore::rewriteLiteral()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a">CVC3::CommonProofRules::transitivityRule()</a>, and <a class="el" href="classCVC3_1_1CommonProofRules.html#a10fa187373ec24079c10874d8e804ecb">CVC3::CommonProofRules::varIntroSkolem()</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>, and <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>.</p>
</div>
</div>
<a class="anchor" id="gab267d9f29c30c8e26b5c7bcc4d15306a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">int CVC3::SearchImplBase::scopeLevel </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">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Return the current scope level (for convenience) </p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00192">192</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>References <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="theory__core_8h_source.html#l00348">CVC3::TheoryCore::getCM()</a>, and <a class="el" href="context_8h_source.html#l00404">CVC3::ContextManager::scopeLevel()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01530">CVC3::SearchEngineFast::addLiteralFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l01445">CVC3::SearchEngineFast::addNonLiteralFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, <a class="el" href="search__simple_8cpp_source.html#l00165">CVC3::SearchSimple::checkValidInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>, <a class="el" href="search__fast_8cpp_source.html#l01573">CVC3::SearchEngineFast::newIntAssumption()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="gaa6e44780a3c5e714f4fd5d8ee41bb1fb"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">SearchImplBase::SearchImplBase </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__impl__base_8cpp_source.html#l00107">107</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <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#l00051">CVC3::SearchImplBase::d_coreSatAPI_implBase</a>, <a class="el" href="search_8h_source.html#l00064">CVC3::SearchEngine::d_rules</a>, <a class="el" href="search__impl__base_8h_source.html#l00044">CVC3::SearchImplBase::d_vm</a>, <a class="el" href="theory__core_8h_source.html#l00348">CVC3::TheoryCore::getCM()</a>, <a class="el" href="theory__core_8h_source.html#l00350">CVC3::TheoryCore::getFlags()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, and <a class="el" href="theory__core_8h_source.html#l00340">CVC3::TheoryCore::registerCoreSatAPI()</a>.</p>
</div>
</div>
<a class="anchor" id="ga139d4116c2b14d5357f2696dc8f29cac"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">SearchImplBase::~SearchImplBase </td>
<td>(</td>
<td class="paramname"></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>Destructor. </p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00132">132</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="search__impl__base_8h_source.html#l00051">CVC3::SearchImplBase::d_coreSatAPI_implBase</a>, and <a class="el" href="search__impl__base_8h_source.html#l00044">CVC3::SearchImplBase::d_vm</a>.</p>
</div>
</div>
<a class="anchor" id="gac4e5351fec1964bf7571d67e90a1538d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void CVC3::SearchImplBase::registerAtom </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">inline</span><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Register an atomic formula of interest. </p>
<p>Registered atoms are tracked by the decision procedures. If one of them is deduced to be true or false, it is added to a list of implied literals. Implied literals can be retrieved with the getImpliedLiteral function </p>
<p>Implements <a class="el" href="group__SE.html#ga0f7c2870341319738e7d8c6662e6d7cc">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00200">200</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>References <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="theory_8cpp_source.html#l00091">CVC3::Theory::registerAtom()</a>, and <a class="el" href="theory_8cpp_source.html#l00252">CVC3::Theory::theoryOf()</a>.</p>
</div>
</div>
<a class="anchor" id="ga65ca9e33c2ac0807f0ef680415457c45"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual Theorem CVC3::SearchImplBase::getImpliedLiteral </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>Return next literal implied by last assertion. Null <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> if none. </p>
<p>Returned literals are either registered atomic formulas or their negation </p>
<p>Implements <a class="el" href="group__SE.html#ga29a287b5dd638015f974a8a046e19d8a">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00202">202</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>References <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, and <a class="el" href="theory__core_8cpp_source.html#l03571">CVC3::TheoryCore::getImpliedLiteral()</a>.</p>
</div>
</div>
<a class="anchor" id="gae987ab9ab6129f83efb0b5649cc2003c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void CVC3::SearchImplBase::push </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>Push a checkpoint. </p>
<p>Implements <a class="el" href="group__SE.html#gadea197447ea40330f3b0739aa944c800">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00203">203</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>References <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="theory__core_8h_source.html#l00348">CVC3::TheoryCore::getCM()</a>, and <a class="el" href="context_8h_source.html#l00401">CVC3::ContextManager::push()</a>.</p>
</div>
</div>
<a class="anchor" id="ga84ceb5e9dcc4e57c1f48f77f4b2f8db5"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual void CVC3::SearchImplBase::pop </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>Restore last checkpoint. </p>
<p>Implements <a class="el" href="group__SE.html#ga2c7fa9d3a42a543ff23891110ad673e5">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00204">204</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>References <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="theory__core_8h_source.html#l00348">CVC3::TheoryCore::getCM()</a>, and <a class="el" href="context_8h_source.html#l00402">CVC3::ContextManager::pop()</a>.</p>
</div>
</div>
<a class="anchor" id="ga1e6282534845cfe93f245d9983d58761"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual QueryResult CVC3::SearchImplBase::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">pure 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>Implemented in <a class="el" href="group__SE__Fast.html#ga1db688bc99f93a978079b3d2efd1bd9f">CVC3::SearchEngineFast</a>, and <a class="el" href="group__SE__Simple.html#ga7a84d46236fb724f3057702c1fb9e073">CVC3::SearchSimple</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00344">CVC3::SearchImplBase::checkValid()</a>.</p>
</div>
</div>
<a class="anchor" id="ga83d82b8cf43e9dc8240e762b180f6343"></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> SearchImplBase::checkValid </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>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>result</em> </td>
</tr>
<tr>
<td></td>
<td>)</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>Similar to <a class="el" href="group__SE.html#ga1e6282534845cfe93f245d9983d58761" title="Checks the validity of a formula in the current context.">checkValidInternal()</a>, only returns Theorem(e) or Null. </p>
<p>Implements <a class="el" href="group__SE.html#ga34a9133f5342719526863d24cd1a0fcc">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00344">344</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="group__SE.html#ga1e6282534845cfe93f245d9983d58761">CVC3::SearchImplBase::checkValidInternal()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a6f8068606f30fe7b2c405ddf5ce1a53b">CVC3::CommonProofRules::clearSkolemAxioms()</a>, <a class="el" href="search_8h_source.html#l00061">CVC3::SearchEngine::d_commonRules</a>, and <a class="el" href="search__impl__base_8h_source.html#l00078">CVC3::SearchImplBase::d_lastValid</a>.</p>
</div>
</div>
<a class="anchor" id="gaf89e6b914a2099b366258953fccb6277"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual QueryResult CVC3::SearchImplBase::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">pure virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Reruns last check with e as an additional assumption. </p>
<p>Implemented in <a class="el" href="group__SE__Fast.html#ga99dd1f1c52ecae319bd0b5a3b689a31d">CVC3::SearchEngineFast</a>, and <a class="el" href="group__SE__Simple.html#ga29f819e266d4821ae874f69da080247c">CVC3::SearchSimple</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00352">CVC3::SearchImplBase::restart()</a>.</p>
</div>
</div>
<a class="anchor" id="gad4a8edbe5a6520fc9f564ec1c65d4729"></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> SearchImplBase::restart </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>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>result</em> </td>
</tr>
<tr>
<td></td>
<td>)</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#ga715936653b5bef3e3d9fd2a8a873bafd">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00352">352</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="search__impl__base_8h_source.html#l00078">CVC3::SearchImplBase::d_lastValid</a>, and <a class="el" href="group__SE.html#gaf89e6b914a2099b366258953fccb6277">CVC3::SearchImplBase::restartInternal()</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8h_source.html#l00222">CVC3::SearchImplBase::returnFromCheck()</a>.</p>
</div>
</div>
<a class="anchor" id="ga7d62893d0d19ed50cc1f616a92d536c0"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::SearchImplBase::returnFromCheck </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>Returns to context immediately before last call to checkValid. </p>
<p>This method should only be called after a query which returns something other than VALID. </p>
<p>Implements <a class="el" href="group__SE.html#gad552593fb43fd5751f12942f3a29a90e">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00222">222</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>References <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="theory_8h_source.html#l00579">CVC3::Theory::falseExpr()</a>, and <a class="el" href="search__impl__base_8cpp_source.html#l00352">CVC3::SearchImplBase::restart()</a>.</p>
</div>
</div>
<a class="anchor" id="ga95428fe99c7a85e5e90ba6b2dce0e024"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual Theorem CVC3::SearchImplBase::lastThm </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>Returns the result of the most recent valid theorem. </p>
<p>Returns Null <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> if last call was not valid </p>
<p>Implements <a class="el" href="group__SE.html#ga9757a6fd272ea550d0e910d20bd7d00b">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00224">224</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>References <a class="el" href="search__impl__base_8h_source.html#l00078">CVC3::SearchImplBase::d_lastValid</a>.</p>
</div>
</div>
<a class="anchor" id="gaf46a82b16f76c9e97cfe252d4398eac7"></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="classCVC3_1_1Theorem.html">Theorem</a> SearchImplBase::newUserAssumption </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>Generate and add a new assertion to the set of assertions in the current context. This should only be used by class <a class="el" href="classCVC3_1_1VCL.html">VCL</a> in assertFormula(). </p>
<p>Implements <a class="el" href="group__SE.html#ga5782663fc8ae00ec2965506c8ba65a86">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00141">141</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="theory__core_8cpp_source.html#l03468">CVC3::TheoryCore::addFact()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#ab4527c48e9f88d94d7ca076757a6f3ba">CVC3::CommonProofRules::assumpRule()</a>, <a class="el" href="cdmap_8h_source.html#l00257">CVC3::CDMap< Key, Data, HashFcn >::begin()</a>, <a class="el" href="search__impl__base_8h_source.html#l00084">CVC3::SearchImplBase::d_assumptions</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="cdmap_8h_source.html#l00258">CVC3::CDMap< Key, Data, HashFcn >::end()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="cdmap_8h_source.html#l00303">CVC3::CDMap< Key, Data, HashFcn >::find()</a>, <a class="el" href="theory__core_8h_source.html#l00352">CVC3::TheoryCore::getExprTrans()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00079">CVC3::ExprTransform::preprocess()</a>, <a class="el" href="expr_8h_source.html#l01498">CVC3::Expr::setUserAssumption()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
<p>Referenced by <a class="el" href="search__simple_8cpp_source.html#l00165">CVC3::SearchSimple::checkValidInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, <a class="el" href="search__simple_8cpp_source.html#l00207">CVC3::SearchSimple::restartInternal()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01750">CVC3::SearchEngineFast::restartInternal()</a>.</p>
</div>
</div>
<a class="anchor" id="ga635768498a239f0193de5f1445676f65"></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="classCVC3_1_1Theorem.html">Theorem</a> SearchImplBase::newIntAssumption </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>Add a new internal asserion. </p>
<p>Reimplemented in <a class="el" href="group__SE__Fast.html#gaf54422149559aa048f32723a3dc6fcce">CVC3::SearchEngineFast</a>.</p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00170">170</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="classCVC3_1_1CommonProofRules.html#ab4527c48e9f88d94d7ca076757a6f3ba">CVC3::CommonProofRules::assumpRule()</a>, <a class="el" href="search_8h_source.html#l00061">CVC3::SearchEngine::d_commonRules</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="theorem_8cpp_source.html#l00504">CVC3::Theorem::setQuantLevel()</a>, and <a class="el" href="search_8h_source.html#l00087">CVC3::SearchEngine::theoryCore()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01573">CVC3::SearchEngineFast::newIntAssumption()</a>, and <a class="el" href="decision__engine_8cpp_source.html#l00128">CVC3::DecisionEngine::pushDecision()</a>.</p>
</div>
</div>
<a class="anchor" id="gab6852f32844435f73f86665c40d2fda8"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchImplBase::newIntAssumption </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>
</div><div class="memdoc">
<p>Helper for above function. </p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00179">179</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <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="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#l01508">CVC3::Expr::setIntAssumption()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>.</p>
</div>
</div>
<a class="anchor" id="gab730f3f048637996f532f77af932fe55"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void SearchImplBase::getUserAssumptions </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>assumptions</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>Get all assumptions made in this and all previous contexts. </p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">assumptions</td><td>should be an empty vector which will be filled \ with the assumptions </td></tr>
</table>
</dd>
</dl>
<p>Implements <a class="el" href="group__SE.html#ga43f52699cddc6e0feffffaf22424fe47">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00189">189</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="search__impl__base_8h_source.html#l00084">CVC3::SearchImplBase::d_assumptions</a>, <a class="el" href="cdmap_8h_source.html#l00300">CVC3::CDMap< Key, Data, HashFcn >::orderedBegin()</a>, and <a class="el" href="cdmap_8h_source.html#l00301">CVC3::CDMap< Key, Data, HashFcn >::orderedEnd()</a>.</p>
</div>
</div>
<a class="anchor" id="gae65e0921e9ef2b475242b1a284a413ad"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void SearchImplBase::getInternalAssumptions </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>assumptions</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>Get assumptions made internally in this and all previous contexts. </p>
<p>Internal assumptions are literals assumed by the sat solver. </p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">assumptions</td><td>should be empty on entry. </td></tr>
</table>
</dd>
</dl>
<p>Implements <a class="el" href="group__SE.html#ga320e15a994a712bc7c20854853501b27">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00197">197</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="search__impl__base_8h_source.html#l00084">CVC3::SearchImplBase::d_assumptions</a>, <a class="el" href="cdmap_8h_source.html#l00300">CVC3::CDMap< Key, Data, HashFcn >::orderedBegin()</a>, and <a class="el" href="cdmap_8h_source.html#l00301">CVC3::CDMap< Key, Data, HashFcn >::orderedEnd()</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00247">CVC3::SearchImplBase::getCounterExample()</a>.</p>
</div>
</div>
<a class="anchor" id="gadadf46fa5200744c9f30ca548080d35d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void SearchImplBase::getAssumptions </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>assumptions</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>Get all assumptions made in this and all previous contexts. </p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">assumptions</td><td>should be an empty vector which will be filled \ with the assumptions </td></tr>
</table>
</dd>
</dl>
<p>Implements <a class="el" href="group__SE.html#ga3167148206cca25a3434cb8bb15c69fe">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00205">205</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="search__impl__base_8h_source.html#l00084">CVC3::SearchImplBase::d_assumptions</a>, <a class="el" href="cdmap_8h_source.html#l00300">CVC3::CDMap< Key, Data, HashFcn >::orderedBegin()</a>, and <a class="el" href="cdmap_8h_source.html#l00301">CVC3::CDMap< Key, Data, HashFcn >::orderedEnd()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01424">CVC3::SearchEngineFast::getCounterExample()</a>.</p>
</div>
</div>
<a class="anchor" id="ga38ec2c19ebab8525ebc3c6249bf97442"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool SearchImplBase::isAssumption </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>Check if the formula has been assumed. </p>
<p>Implements <a class="el" href="group__SE.html#ga20730f5acacc4b18d29031632d88904c">CVC3::SearchEngine</a>.</p>
<p>Reimplemented in <a class="el" href="group__SE__Fast.html#ga4b55b5f49d921ca4b63f874d8404c4d5">CVC3::SearchEngineFast</a>.</p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00213">213</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="cdmap_8h_source.html#l00172">CVC3::CDMap< Key, Data, HashFcn >::count()</a>, and <a class="el" href="search__impl__base_8h_source.html#l00084">CVC3::SearchImplBase::d_assumptions</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01594">CVC3::SearchEngineFast::isAssumption()</a>.</p>
</div>
</div>
<a class="anchor" id="gac6e807418fb26dee354f7f934eb432ba"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchImplBase::addFact </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>
</div><div class="memdoc">
<p>Add a new fact to the search engine from the core. </p>
<p>It should be called by <a class="el" href="classCVC3_1_1TheoryCore.html#a3a897e60d6dd1dfd382870054e5ad777" title="The assumptions for e must be in H or phi. "Core" added to avoid conflict with theory interface funct...">TheoryCore::assertFactCore()</a>. </p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00231">231</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="search__impl__base_8cpp_source.html#l00218">CVC3::SearchImplBase::addCNFFact()</a>, <a class="el" href="search__impl__base_8h_source.html#l00092">CVC3::SearchImplBase::d_cnfOption</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00360">CVC3::SearchImplBase::enqueueCNF()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</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="ga6c1448b58fb299bc084aa9c522faf36d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void SearchImplBase::addSplitter </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>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>priority</em> </td>
</tr>
<tr>
<td></td>
<td>)</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>Suggest a splitter to the <a class="el" href="classCVC3_1_1SearchEngine.html" title="API to to a generic proof search engine.">SearchEngine</a>. </p>
<p>The higher is the priority, the sooner the <a class="el" href="namespaceSAT.html">SAT</a> solver will split on it. It can be positive or negative (default is 0).</p>
<p>The set of suggested splitters is backtracking; that is, a splitter is "forgotten" once the scope is backtracked.</p>
<p>This method can be used either to change the priority of existing splitters, or to introduce new splitters that DPs consider relevant, even though they do not appear in existing formulas. </p>
<p>Reimplemented in <a class="el" href="group__SE__Fast.html#ga40b361c2f9374c541282feca1e237dba">CVC3::SearchEngineFast</a>.</p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00241">241</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="search__impl__base_8h_source.html#l00074">CVC3::SearchImplBase::d_dpSplitters</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l00406">CVC3::Expr::isAbsLiteral()</a>, <a class="el" href="search__impl__base_8h_source.html#l00120">CVC3::SearchImplBase::newLiteral()</a>, <a class="el" href="cdlist_8h_source.html#l00066">CVC3::CDList< T >::push_back()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="gacf93ae1a488573c6d34dee7721007351"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void SearchImplBase::getCounterExample </td>
<td>(</td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>assertions</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>inOrder</em> = <code>true</code> </td>
</tr>
<tr>
<td></td>
<td>)</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>Will return the set of assertions which make the queried formula false. </p>
<p>This method should only be called after an query which returns INVALID. It will try to return the simplest possible set of assertions which are sufficient to make the queried expression false. </p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">assertions</td><td>should be empty on entry. </td></tr>
<tr><td class="paramname">inOrder</td><td>if true, returns the assertions in the order they were asserted. This is slightly more expensive than inOrder = false. </td></tr>
</table>
</dd>
</dl>
<p>Implements <a class="el" href="group__SE.html#ga739867521b23967ee6739ec32a8070e2">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00247">247</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="search__impl__base_8h_source.html#l00078">CVC3::SearchImplBase::d_lastValid</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00197">CVC3::SearchImplBase::getInternalAssumptions()</a>, <a class="el" href="theory__core_8h_source.html#l00349">CVC3::TheoryCore::getTM()</a>, <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>, and <a class="el" href="theorem__manager_8h_source.html#l00094">CVC3::TheoremManager::withAssumptions()</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01424">CVC3::SearchEngineFast::getCounterExample()</a>.</p>
</div>
</div>
<a class="anchor" id="gaf90e8ae5cd67dc6c43787a9d3ebdca53"></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="classCVC3_1_1Proof.html">Proof</a> SearchImplBase::getProof </td>
<td>(</td>
<td class="paramname"></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>Returns the proof term for the last proven query. </p>
<p>It should be called only after a checkValid which returns true. In any other case, it returns Null. </p>
<p>Implements <a class="el" href="group__SE.html#gaa0ce3839d5f7b64168d62ff5eb59cf1f">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00282">282</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="search__impl__base_8h_source.html#l00078">CVC3::SearchImplBase::d_lastValid</a>, <a class="el" href="theorem_8cpp_source.html#l00402">CVC3::Theorem::getProof()</a>, <a class="el" href="theory__core_8h_source.html#l00349">CVC3::TheoryCore::getTM()</a>, <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>, and <a class="el" href="theorem__manager_8h_source.html#l00091">CVC3::TheoremManager::withProof()</a>.</p>
</div>
</div>
<a class="anchor" id="ga24dc510f27c40d8044f461308bcdb62d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & SearchImplBase::getAssumptionsUsed </td>
<td>(</td>
<td class="paramname"></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>Returns the set of assumptions used in the proof. It should be a subset of <a class="el" href="group__SE.html#gadadf46fa5200744c9f30ca548080d35d" title="Get all assumptions made in this and all previous contexts.">getAssumptions()</a>. </p>
<p>It should be called only after a checkValid which returns true. In any other case, it returns Null. </p>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00297">297</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <a class="el" href="search_8h_source.html#l00058">CVC3::SearchEngine::d_core</a>, <a class="el" href="search__impl__base_8h_source.html#l00078">CVC3::SearchImplBase::d_lastValid</a>, <a class="el" href="assumptions_8h_source.html#l00083">CVC3::Assumptions::emptyAssump()</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theory__core_8h_source.html#l00349">CVC3::TheoryCore::getTM()</a>, <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>, and <a class="el" href="theorem__manager_8h_source.html#l00094">CVC3::TheoremManager::withAssumptions()</a>.</p>
</div>
</div>
<a class="anchor" id="ga0d509e38a03048dcbdb9e28f3f5da724"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void SearchImplBase::processResult </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>res</em>, </td>
</tr>
<tr>
<td class="paramkey"></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>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Process result of checkValid. </p>
<p>Given a proof of FALSE ('res') from an assumption 'e', derive the proof of the inverse of e.</p>
<dl class="params"><dt>Parameters</dt><dd>
<table class="params">
<tr><td class="paramname">res</td><td>is a proof of FALSE </td></tr>
<tr><td class="paramname">e</td><td>is the assumption used in the above proof </td></tr>
</table>
</dd>
</dl>
<p>Definition at line <a class="el" href="search__impl__base_8cpp_source.html#l00317">317</a> of file <a class="el" href="search__impl__base_8cpp_source.html">search_impl_base.cpp</a>.</p>
<p>References <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__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_8h_source.html#l00064">CVC3::SearchEngine::d_rules</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="group__SE__Rules.html#ga3ddf95924d2ff2efb59e84dc78a19821">CVC3::SearchEngineRules::eliminateSkolemAxioms()</a>, <a class="el" href="expr__map_8h_source.html#l00313">CVC3::ExprHashMap< Data >::erase()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#ac773341edabcc5091ca25af74fcb7653">CVC3::CommonProofRules::getSkolemAxioms()</a>, <a class="el" href="expr_8h_source.html#l00355">CVC3::Expr::isFalse()</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>, <a class="el" href="group__SE__Rules.html#ga846c2bdc33f6ff2080e76637ea618626">CVC3::SearchEngineRules::negIntro()</a>, <a class="el" href="group__SE__Rules.html#ga64c9fb7058e52c324ce76f15fcea37e2">CVC3::SearchEngineRules::proofByContradiction()</a>, and <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>.</p>
<p>Referenced by <a class="el" href="search__simple_8cpp_source.html#l00126">CVC3::SearchSimple::checkValidMain()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>.</p>
</div>
</div>
<a class="anchor" id="gadf867c70d67d05d72a11895a2cc13971"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">virtual FormulaValue CVC3::SearchImplBase::getValue </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">CVC3::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">inline</span><span class="mlabel">virtual</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Implements <a class="el" href="group__SE.html#ga38ced857c272afeecbe0429e1dcca28e">CVC3::SearchEngine</a>.</p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00286">286</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, and <a class="el" href="formula__value_8h_source.html#l00034">CVC3::UNKNOWN_VAL</a>.</p>
</div>
</div>
<h2 class="groupheader">Variable Documentation</h2>
<a class="anchor" id="ga3772c6af7eac91b9ed7fc278edf5ef90"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">TheoryCore* CVC3::SearchEngine::d_core</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Access to theory reasoning. </p>
<p>Definition at line <a class="el" href="search_8h_source.html#l00058">58</a> of file <a class="el" href="search_8h_source.html">search.h</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00218">CVC3::SearchImplBase::addCNFFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l01445">CVC3::SearchEngineFast::addNonLiteralFact()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00723">CVC3::SearchImplBase::addToCNFCache()</a>, <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, <a class="el" href="search__fast_8cpp_source.html#l00186">CVC3::SearchEngineFast::checkSAT()</a>, <a class="el" href="search__simple_8cpp_source.html#l00165">CVC3::SearchSimple::checkValidInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, <a class="el" href="search__simple_8cpp_source.html#l00126">CVC3::SearchSimple::checkValidMain()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, <a class="el" href="search__fast_8cpp_source.html#l01050">CVC3::SearchEngineFast::commitFacts()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00750">CVC3::SearchImplBase::findInCNFCache()</a>, <a class="el" href="search__fast_8cpp_source.html#l00438">CVC3::SearchEngineFast::findSplitter()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00297">CVC3::SearchImplBase::getAssumptionsUsed()</a>, <a class="el" href="search_8cpp_source.html#l00091">CVC3::SearchEngine::getConcreteModel()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00247">CVC3::SearchImplBase::getCounterExample()</a>, <a class="el" href="search__impl__base_8h_source.html#l00202">CVC3::SearchImplBase::getImpliedLiteral()</a>, <a class="el" href="search__sat_8cpp_source.html#l01010">CVC3::SearchSat::getImpliedLiteral()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00282">CVC3::SearchImplBase::getProof()</a>, <a class="el" href="search__sat_8cpp_source.html#l01178">CVC3::SearchSat::getProof()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00141">CVC3::SearchImplBase::newUserAssumption()</a>, <a class="el" href="search__sat_8cpp_source.html#l01064">CVC3::SearchSat::newUserAssumptionInt()</a>, <a class="el" href="search__sat_8cpp_source.html#l01042">CVC3::SearchSat::newUserAssumptionIntHelper()</a>, <a class="el" href="search__impl__base_8h_source.html#l00204">CVC3::SearchImplBase::pop()</a>, <a class="el" href="circuit_8cpp_source.html#l00047">CVC3::Circuit::propagate()</a>, <a class="el" href="search__impl__base_8h_source.html#l00203">CVC3::SearchImplBase::push()</a>, <a class="el" href="search__impl__base_8h_source.html#l00200">CVC3::SearchImplBase::registerAtom()</a>, <a class="el" href="search__sat_8cpp_source.html#l01002">CVC3::SearchSat::registerAtom()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00804">CVC3::SearchImplBase::replaceITE()</a>, <a class="el" href="search__simple_8cpp_source.html#l00207">CVC3::SearchSimple::restartInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01750">CVC3::SearchEngineFast::restartInternal()</a>, <a class="el" href="search__impl__base_8h_source.html#l00222">CVC3::SearchImplBase::returnFromCheck()</a>, <a class="el" href="search__impl__base_8h_source.html#l00192">CVC3::SearchImplBase::scopeLevel()</a>, <a class="el" href="search__fast_8cpp_source.html#l01043">CVC3::SearchEngineFast::setInconsistent()</a>, <a class="el" href="search__impl__base_8h_source.html#l00124">CVC3::SearchImplBase::simplify()</a>, <a class="el" href="search__fast_8cpp_source.html#l00254">CVC3::SearchEngineFast::split()</a>, <a class="el" href="search_8h_source.html#l00087">CVC3::SearchEngine::theoryCore()</a>, and <a class="el" href="search_8cpp_source.html#l00057">CVC3::SearchEngine::tryModelGeneration()</a>.</p>
</div>
</div>
<a class="anchor" id="ga63f2a3cfcfa86820bea2f45cb890cc1c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CommonProofRules* CVC3::SearchEngine::d_commonRules</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Common proof rules. </p>
<p>Definition at line <a class="el" href="search_8h_source.html#l00061">61</a> of file <a class="el" href="search_8h_source.html">search.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01530">CVC3::SearchEngineFast::addLiteralFact()</a>, <a class="el" href="search__simple_8cpp_source.html#l00237">CVC3::SearchSimple::addNonLiteralFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l01445">CVC3::SearchEngineFast::addNonLiteralFact()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00723">CVC3::SearchImplBase::addToCNFCache()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>, <a class="el" href="search__fast_8cpp_source.html#l00637">CVC3::SearchEngineFast::bcp()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00344">CVC3::SearchImplBase::checkValid()</a>, <a class="el" href="search__simple_8cpp_source.html#l00126">CVC3::SearchSimple::checkValidMain()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00750">CVC3::SearchImplBase::findInCNFCache()</a>, <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>, <a class="el" href="search_8h_source.html#l00084">CVC3::SearchEngine::getCommonRules()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00170">CVC3::SearchImplBase::newIntAssumption()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00141">CVC3::SearchImplBase::newUserAssumption()</a>, <a class="el" href="search__sat_8cpp_source.html#l01064">CVC3::SearchSat::newUserAssumptionInt()</a>, <a class="el" href="search__sat_8cpp_source.html#l01042">CVC3::SearchSat::newUserAssumptionIntHelper()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00317">CVC3::SearchImplBase::processResult()</a>, <a class="el" href="search__fast_8cpp_source.html#l00549">CVC3::SearchEngineFast::recordFact()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00804">CVC3::SearchImplBase::replaceITE()</a>, <a class="el" href="search__simple_8cpp_source.html#l00101">CVC3::SearchSimple::SearchSimple()</a>, and <a class="el" href="search__fast_8cpp_source.html#l00254">CVC3::SearchEngineFast::split()</a>.</p>
</div>
</div>
<a class="anchor" id="ga879b68112123e2b4ae7175d85a03bfec"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">SearchEngineRules* CVC3::SearchEngine::d_rules</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p><a class="el" href="classCVC3_1_1Proof.html">Proof</a> rules for the search engine. </p>
<p>Definition at line <a class="el" href="search_8h_source.html#l00064">64</a> of file <a class="el" href="search_8h_source.html">search.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01445">CVC3::SearchEngineFast::addNonLiteralFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00317">CVC3::SearchImplBase::processResult()</a>, <a class="el" href="circuit_8cpp_source.html#l00047">CVC3::Circuit::propagate()</a>, <a class="el" href="search__fast_8cpp_source.html#l00816">CVC3::SearchEngineFast::propagate()</a>, <a class="el" href="search_8cpp_source.html#l00035">CVC3::SearchEngine::SearchEngine()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00107">CVC3::SearchImplBase::SearchImplBase()</a>, <a class="el" href="search__fast_8cpp_source.html#l00915">CVC3::SearchEngineFast::unitPropagation()</a>, and <a class="el" href="search_8cpp_source.html#l00052">CVC3::SearchEngine::~SearchEngine()</a>.</p>
</div>
</div>
<a class="anchor" id="ga626a0fe24f363d007d729e16d13349e5"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">VariableManager* CVC3::SearchImplBase::d_vm</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p><a class="el" href="classCVC3_1_1Variable.html">Variable</a> manager for classes <a class="el" href="classCVC3_1_1Variable.html">Variable</a> and <a class="el" href="classCVC3_1_1Literal.html">Literal</a>. </p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00044">44</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01445">CVC3::SearchEngineFast::addNonLiteralFact()</a>, <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, <a class="el" href="circuit_8cpp_source.html#l00028">CVC3::Circuit::Circuit()</a>, <a class="el" href="search__impl__base_8h_source.html#l00120">CVC3::SearchImplBase::newLiteral()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00107">CVC3::SearchImplBase::SearchImplBase()</a>, and <a class="el" href="search__impl__base_8cpp_source.html#l00132">CVC3::SearchImplBase::~SearchImplBase()</a>.</p>
</div>
</div>
<a class="anchor" id="ga640e08e2b051e08f2abdd4111b9a2e71"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CDO<int> CVC3::SearchImplBase::d_bottomScope</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>The bottom-most scope for the current call to checkSAT (where conflict clauses are still valid). </p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00049">49</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00723">CVC3::SearchImplBase::addToCNFCache()</a>, <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, <a class="el" href="search__simple_8cpp_source.html#l00165">CVC3::SearchSimple::checkValidInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, <a class="el" href="search__fast_8cpp_source.html#l00939">CVC3::SearchEngineFast::fixConflict()</a>, <a class="el" href="search__impl__base_8h_source.html#l00153">CVC3::SearchImplBase::getBottomScope()</a>, <a class="el" href="search__simple_8cpp_source.html#l00207">CVC3::SearchSimple::restartInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01750">CVC3::SearchEngineFast::restartInternal()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="ga02f72989536076eab8c55e452a6662d9"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">TheoryCore::CoreSatAPI* CVC3::SearchImplBase::d_coreSatAPI_implBase</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00051">51</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00107">CVC3::SearchImplBase::SearchImplBase()</a>, and <a class="el" href="search__impl__base_8cpp_source.html#l00132">CVC3::SearchImplBase::~SearchImplBase()</a>.</p>
</div>
</div>
<a class="anchor" id="ga8ea9b2ab9f50d3ddf595595b1f3d7974"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CDList<Splitter> CVC3::SearchImplBase::d_dpSplitters</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Backtracking ordered set of DP-suggested splitters. </p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00074">74</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00241">CVC3::SearchImplBase::addSplitter()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01601">CVC3::SearchEngineFast::addSplitter()</a>.</p>
</div>
</div>
<a class="anchor" id="ga88ba664573602ecfca1d6eadc14a30af"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">Theorem CVC3::SearchImplBase::d_lastValid</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> from the last successful checkValid call. It is used by getProof and getAssumptions. </p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00078">78</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00344">CVC3::SearchImplBase::checkValid()</a>, <a class="el" href="search__simple_8cpp_source.html#l00126">CVC3::SearchSimple::checkValidMain()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00297">CVC3::SearchImplBase::getAssumptionsUsed()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00247">CVC3::SearchImplBase::getCounterExample()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00282">CVC3::SearchImplBase::getProof()</a>, <a class="el" href="search__impl__base_8h_source.html#l00224">CVC3::SearchImplBase::lastThm()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00317">CVC3::SearchImplBase::processResult()</a>, and <a class="el" href="search__impl__base_8cpp_source.html#l00352">CVC3::SearchImplBase::restart()</a>.</p>
</div>
</div>
<a class="anchor" id="gaf6841e86841006b6917d46664de64d21"></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="classExprHashMap.html">ExprHashMap</a><bool> CVC3::SearchImplBase::d_lastCounterExample</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p><a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> from the last unsuccessful checkValid call. These are used by getCounterExample. </p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00081">81</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>Referenced by <a class="el" href="search__simple_8cpp_source.html#l00126">CVC3::SearchSimple::checkValidMain()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, and <a class="el" href="search__impl__base_8cpp_source.html#l00317">CVC3::SearchImplBase::processResult()</a>.</p>
</div>
</div>
<a class="anchor" id="ga83dfe2d2d85bacf5e4aa10c0320a140b"></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="classCDMap.html">CDMap</a><Expr,Theorem> CVC3::SearchImplBase::d_assumptions</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Maintain the list of current assumptions (user asserts and splitters) for <a class="el" href="group__SE.html#gadadf46fa5200744c9f30ca548080d35d" title="Get all assumptions made in this and all previous contexts.">getAssumptions()</a>. </p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00084">84</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.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__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01624">CVC3::SearchEngineFast::checkValidMain()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00205">CVC3::SearchImplBase::getAssumptions()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00197">CVC3::SearchImplBase::getInternalAssumptions()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00189">CVC3::SearchImplBase::getUserAssumptions()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00213">CVC3::SearchImplBase::isAssumption()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00179">CVC3::SearchImplBase::newIntAssumption()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00141">CVC3::SearchImplBase::newUserAssumption()</a>, <a class="el" href="search__simple_8cpp_source.html#l00207">CVC3::SearchSimple::restartInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01750">CVC3::SearchEngineFast::restartInternal()</a>, and <a class="el" href="search__impl__base_8cpp_source.html#l00107">CVC3::SearchImplBase::SearchImplBase()</a>.</p>
</div>
</div>
<a class="anchor" id="gab60a7d204ed01875c98629e874575cd6"></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="classCDMap.html">CDMap</a><Expr, Theorem> CVC3::SearchImplBase::d_cnfCache</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Backtracking cache for the CNF generator. </p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00087">87</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00723">CVC3::SearchImplBase::addToCNFCache()</a>, and <a class="el" href="search__impl__base_8cpp_source.html#l00750">CVC3::SearchImplBase::findInCNFCache()</a>.</p>
</div>
</div>
<a class="anchor" id="ga1c64a37d94b4cadedce29f3e4b98a3af"></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="classCDMap.html">CDMap</a><Expr, bool> CVC3::SearchImplBase::d_cnfVars</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Backtracking set of new variables generated by CNF translator. </p>
<p>Specific search engines do not have to split on these variables </p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00090">90</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00723">CVC3::SearchImplBase::addToCNFCache()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>, and <a class="el" href="search__impl__base_8h_source.html#l00165">CVC3::SearchImplBase::isCNFVar()</a>.</p>
</div>
</div>
<a class="anchor" id="gae3b8b3cfd965e7d5138320d26808767a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const bool* CVC3::SearchImplBase::d_cnfOption</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Command line flag whether to convert to CNF. </p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00092">92</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00231">CVC3::SearchImplBase::addFact()</a>.</p>
</div>
</div>
<a class="anchor" id="gaa28d7e60bbe1df69ffb304f939b984b7"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const bool* CVC3::SearchImplBase::d_ifLiftOption</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Flag: whether to convert term ITEs into CNF. </p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00094">94</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>.</p>
</div>
</div>
<a class="anchor" id="gafc2c782e4f24b55c8af7cb0189d281d8"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const bool* CVC3::SearchImplBase::d_ignoreCnfVarsOption</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Flag: ignore auxiliary CNF variables when searching for a splitter. </p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00096">96</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00711">CVC3::SearchImplBase::isGoodSplitter()</a>.</p>
</div>
</div>
<a class="anchor" id="ga2287fd23d4250cc74db446983b2c3274"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const bool* CVC3::SearchImplBase::d_origFormulaOption</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Flag: Preserve the original formula with +cnf (for splitter heuristics) </p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00098">98</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00360">CVC3::SearchImplBase::enqueueCNF()</a>.</p>
</div>
</div>
<a class="anchor" id="ga9dc16eb11f046d9a615aff3018957c6d"></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="classCDMap.html">CDMap</a><Expr,bool> CVC3::SearchImplBase::d_enqueueCNFCache</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Cache for <a class="el" href="group__SE.html#ga4bcd481c70362c589aa7e712a8cc746d" title="Translate theta to CNF and enqueue the new clauses.">enqueueCNF()</a> </p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00112">112</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00371">CVC3::SearchImplBase::enqueueCNFrec()</a>.</p>
</div>
</div>
<a class="anchor" id="ga401319b3ede7162504e979aaf2119deb"></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="classCDMap.html">CDMap</a><Expr,bool> CVC3::SearchImplBase::d_applyCNFRulesCache</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Cache for <a class="el" href="group__SE.html#gaa7bf3c385bae481d4ea35179e818a09a" title="FIXME: write a comment.">applyCNFRules()</a> </p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00114">114</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00563">CVC3::SearchImplBase::applyCNFRules()</a>.</p>
</div>
</div>
<a class="anchor" id="ga0c829909b9e3ab2b59ba40e681905c4b"></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="classCDMap.html">CDMap</a><Expr,Theorem> CVC3::SearchImplBase::d_replaceITECache</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">protected</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Cache for <a class="el" href="group__SE.html#ga687e32d21d7fe7e4b26873ae86a47ae5" title="Replaces ITE subexpressions in e with variables.">replaceITE()</a> </p>
<p>Definition at line <a class="el" href="search__impl__base_8h_source.html#l00116">116</a> of file <a class="el" href="search__impl__base_8h_source.html">search_impl_base.h</a>.</p>
<p>Referenced by <a class="el" href="search__impl__base_8cpp_source.html#l00804">CVC3::SearchImplBase::replaceITE()</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>
